Turning loads into non-trapping when necessary

3 files changed, 43 insertions, 2 deletions

diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 97ca9223..73b71ea0 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -61,6 +61,7 @@ type t = {
   supports_unaligned_accesses: bool;
   struct_passing_style: struct_passing_style;
   struct_return_style : struct_return_style;
+  has_non_trapping_loads : bool;
 }
 
 let ilp32ll64 = {
@@ -96,6 +97,7 @@ let ilp32ll64 = {
   supports_unaligned_accesses = false;
   struct_passing_style = SP_ref_callee;
   struct_return_style = SR_ref;
+  has_non_trapping_loads = false;
 }
 
 let i32lpll64 = {
@@ -131,6 +133,7 @@ let i32lpll64 = {
   supports_unaligned_accesses = false;
   struct_passing_style = SP_ref_callee;
   struct_return_style = SR_ref;
+  has_non_trapping_loads = false;
 }
 
 let il32pll64 = {
@@ -166,6 +169,7 @@ let il32pll64 = {
   supports_unaligned_accesses = false;
   struct_passing_style = SP_ref_callee;
   struct_return_style = SR_ref;
+  has_non_trapping_loads = false;
 }
 
 (* Canned configurations for some ABIs *)
@@ -270,7 +274,9 @@ let kvx =
     bitfields_msb_first = false; (* TO CHECK *)
     supports_unaligned_accesses = true;
     struct_passing_style = SP_value32_ref_callee;
-    struct_return_style = SR_int1to4 }
+    struct_return_style = SR_int1to4;
+    has_non_trapping_loads = true;
+}
 
 let aarch64 =
   { i32lpll64 with name = "aarch64";
@@ -323,6 +329,7 @@ let undef = {
   supports_unaligned_accesses = false;
   struct_passing_style = SP_ref_callee;
   struct_return_style = SR_ref;
+  has_non_trapping_loads = false;
 }
 
 (* The current configuration.  Must be initialized before use. *)
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index 0e1e22d1..54436758 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -60,6 +60,7 @@ type t = {
   supports_unaligned_accesses: bool;
   struct_passing_style: struct_passing_style;
   struct_return_style: struct_return_style;
+  has_non_trapping_loads: bool;
 }
 
 (* The current configuration *)
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index 66910bdf..80fc766d 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -4,6 +4,9 @@ open Maps
 open RTLpathLivegenaux
 open Registers
 open Camlcoq
+open Machine
+
+let has_non_trapping_loads = !(Machine.config).has_non_trapping_loads
 
 type superblock = {
   instructions: P.t array; (* pointers to code instructions *)
@@ -219,11 +222,24 @@ let sinst_to_rinst = function
       )
   | Send i -> i
 
+let is_a_cb = function Icond _ -> true | _ -> false
+let is_a_load = function Iload _ -> true | _ -> false
+
 let apply_schedule code sb new_order =
   let tc = ref code in
   let old_order = sb.instructions in
-  begin
+  let count_cbs order =
+    let current_cbs = ref HashedSet.PSet.empty in
+    let cbs_above = ref PTree.empty in
+    Array.iter (fun n ->
+      let inst = get_some @@ PTree.get n code in
+      if is_a_cb inst then current_cbs := HashedSet.PSet.add n !current_cbs
+      else if is_a_load inst then cbs_above := PTree.set n !current_cbs !cbs_above
+    ) order;
+    !cbs_above
+  in begin
     check_order code old_order new_order;
+    (* First pass - modify the successors, nothing else *)
     Array.iteri (fun i n' ->
       let inst' = get_some @@ PTree.get n' code in
       let iend = Array.length old_order - 1 in
@@ -246,6 +262,23 @@ let apply_schedule code sb new_order =
           @@ rinst_to_sinst inst'
       in tc := PTree.set (Array.get old_order i) new_inst !tc
     ) new_order;
+    (* Second pass - turn the loads into non-trapping when needed, if the architecture supports it *)
+    if has_non_trapping_loads then begin
+      (* 1) We remember which CBs are "above" a given load *)
+      let cbs_above = count_cbs old_order in
+      (* 2) We do the same for new_order *)
+      let cbs_above' = count_cbs new_order in
+      (* 3) We examine each load, turn it into non-trapping if cbs_above is not included in cbs_above' *)
+      Array.iter (fun n ->
+        let inst = get_some @@ PTree.get n !tc in
+        match inst with
+        | Iload (t,a,b,c,d,s) -> 
+            let pset = get_some @@ PTree.get n cbs_above in
+            let pset' = get_some @@ PTree.get n cbs_above' in
+            if not @@ HashedSet.PSet.is_subset pset pset' then tc := PTree.set n (Iload (AST.NOTRAP,a,b,c,d,s)) !tc
+        | _ -> ()
+      ) old_order
+    end;
     !tc
   end