fix issue #247 by using a BTL's ghostfield

6 files changed, 35 insertions, 12 deletions

diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml
index 0e682c4c..38bc685c 100644
--- a/scheduling/BTLScheduleraux.ml
+++ b/scheduling/BTLScheduleraux.ml
@@ -19,7 +19,7 @@ let flatten_blk_basics ibf =
         last := Some ib;
         []
     | Bseq ((Bcond (_, _, _, _, iinfo) as ib1), ib2) -> (
-        match iinfo.pcond with
+        match iinfo.opt_info with
         | Some _ -> [ ib1 ] @ traverse_blk ib2
         | None ->
             last := Some ib;
@@ -78,7 +78,8 @@ let apply_schedule bseq olast positions =
            let set_old = Hashtbl.find cbs_above_old n' in
            let set_new = Hashtbl.find cbs_above_new n' in
            if SI.subset set_old set_new then
-             bseq_new.(n') <- Bload (AST.TRAP, a, b, c, d, e)
+             if get_some @@ e.opt_info then
+               bseq_new.(n') <- Bload (AST.TRAP, a, b, c, d, e)
            else assert !config.has_non_trapping_loads
        | _ -> ())
      bseq);
@@ -277,7 +278,13 @@ let turn_all_loads_nontrap n ibf btl =
     let rec traverse_rec ib =
       match ib with
       | Bseq (ib1, ib2) -> Bseq (traverse_rec ib1, traverse_rec ib2)
-      | Bload (t, a, b, c, d, e) -> Bload (AST.NOTRAP, a, b, c, d, e)
+      | Bload (t, a, b, c, d, e) ->
+        let _opt_info =
+          match t with
+          | AST.TRAP -> Some true
+          | AST.NOTRAP -> Some false in
+        e.opt_info <- _opt_info;
+        Bload (AST.NOTRAP, a, b, c, d, e)
       | _ -> ib
     in
     let ib' = traverse_rec ibf.entry in
@@ -304,7 +311,7 @@ let compute_liveins n ibf btl =
             iinfo.liveins <- Regset.union iinfo.liveins lives)
           tbl
     | Bcond (_, _, BF (Bgoto succ, _), Bnop None, iinfo) -> (
-        match iinfo.pcond with
+        match iinfo.opt_info with
         | Some predb ->
             assert (predb = false);
             let lives = (get_some @@ PTree.get succ btl).input_regs in
diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml
index 577e4828..11a7ee7f 100644
--- a/scheduling/BTLcommonaux.ml
+++ b/scheduling/BTLcommonaux.ml
@@ -6,9 +6,9 @@ open RTLcommonaux
 
 let undef_node = -1
 
-let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond; visited = false; liveins = Regset.empty }
+let mk_iinfo _inumb _opt_info = { inumb = _inumb; opt_info = _opt_info; visited = false; liveins = Regset.empty }
 
-let def_iinfo () = { inumb = undef_node; pcond = None; visited = false; liveins = Regset.empty }
+let def_iinfo () = { inumb = undef_node; opt_info = None; visited = false; liveins = Regset.empty }
 
 let mk_binfo _bnumb _s_output_regs _typing =
   {
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index ddec991d..47262b3e 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -22,7 +22,7 @@ let translate_function btl entry =
       match ib with
       | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) ->
           Some
-            ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond),
+            ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.opt_info),
               get_inumb iinfo )
       | Bcond (_, _, _, _, _) ->
           failwith "translate_function: unsupported Bcond"
diff --git a/scheduling/BTLtypes.ml b/scheduling/BTLtypes.ml
index 12ca30e8..64001adf 100644
--- a/scheduling/BTLtypes.ml
+++ b/scheduling/BTLtypes.ml
@@ -2,10 +2,19 @@ open Registers
 
 type inst_info = {
   mutable inumb : int;
-  mutable pcond : bool option;
+  mutable opt_info : bool option;
   mutable visited : bool;
-  mutable liveins: Regset.t;
+  mutable liveins : Regset.t;
 }
+(** This struct is a ghost field attached to each BTL instruction
+ * inumb: int field used for remembering the original numbering of CFG
+ * opt_info: option bool used for various tests:
+ *  - On Bcond, stores the prediction information
+ *  - On Bload, stores the trapping information (if Some false, the load was
+ *  initially non-trapping, and the opposite if some true)
+ * visited: boolean used to mark nodes
+ * liveins: set of lives registers
+ *)
 
 type block_info = {
   mutable bnumb : int;
@@ -13,3 +22,10 @@ type block_info = {
   s_output_regs : Regset.t;
   typing : RTLtyping.regenv;
 }
+(** Struct attached to each BTL iblock_info type
+ * bnumb: int representing the block id in the BTL CFG
+ * visited:  boolean used to mark blocks
+ * s_output_regs: set of output registers
+ * typing: field transferring RTL typing information in BTL (used in regpres
+ * scheduling)
+ *)
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index 89254301..64e83651 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -66,7 +66,7 @@ let rec print_iblock pp is_rec pref ib =
       fprintf pp "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb
         (PrintOp.print_condition reg)
         (cond, args)
-        (match iinfo.pcond with
+        (match iinfo.opt_info with
         | None -> "none"
         | Some true -> "branch"
         | Some false -> "fallthrough");
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 3c06f4cb..0ed6ec61 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -33,7 +33,7 @@ let translate_inst (iinfo : BTL.inst_info) inst is_final =
     | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo)
     | Icond (cond, lr, ifso, ifnot, info) ->
         osucc := Some ifnot;
-        iinfo.pcond <- info;
+        iinfo.opt_info <- info;
         Bcond
           ( cond,
             lr,
@@ -70,7 +70,7 @@ let translate_function code entry join_points liveness (typing : RTLtyping.regen
             | Icond (cond, lr, ifso, ifnot, info) ->
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
-                iinfo.pcond <- info;
+                iinfo.opt_info <- info;
                 Bseq
                   ( Bcond
                       (cond, lr, BF (Bgoto ifso, def_iinfo ()), Bnop None, iinfo),