Changing to an opaq record in BTL info, this is a broken commit

1 files changed, 26 insertions, 18 deletions

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 859bbf07..d4fd2643 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -6,37 +6,43 @@ open DebugPrint
 open PrintBTL
 open Camlcoq
 open AuxTools
+open BTLaux
 
-let mk_ni n = n
+let undef_node = -1
+let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond }
+let def_iinfo = { inumb = undef_node; pcond = None }
+
+let mk_binfo _bnumb = { bnumb = _bnumb }
 
 let encaps_final inst osucc =
   match inst with
   | BF _ | Bcond _ -> inst
-  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo))
 
-let translate_inst ni inst is_final =
+let translate_inst iinfo inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
     | Inop s ->
         osucc := Some s;
-        Bnop ni
+        Bnop iinfo
     | Iop (op, lr, rd, s) ->
         osucc := Some s;
-        Bop (op, lr, rd, ni)
+        Bop (op, lr, rd, iinfo)
     | Iload (trap, chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bload (trap, chk, addr, lr, rd, ni)
+        Bload (trap, chk, addr, lr, rd, iinfo)
     | Istore (chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bstore (chk, addr, lr, rd, ni)
-    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s, ni))
-    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr, ni))
-    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s, ni))
+        Bstore (chk, addr, lr, rd, iinfo)
+    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo)
+    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo)
+    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo)
     | Icond (cond, lr, ifso, ifnot, info) ->
-        Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info, ni)
-    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl, ni))
-    | Ireturn oreg -> BF (Breturn (oreg, ni))
+        iinfo.pcond <- info;
+        Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), BF (Bgoto ifnot, def_iinfo), iinfo)
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo)
+    | Ireturn oreg -> BF (Breturn (oreg), iinfo)
   in
   if is_final then encaps_final btli !osucc else btli
 
@@ -52,7 +58,7 @@ let translate_function code entry join_points =
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
         let psucc = predicted_successor inst in
-        let ni = mk_ni n in
+        let iinfo = mk_iinfo (p2i n) None in
         let succ =
           match psucc with
           | Some ps ->
@@ -70,16 +76,18 @@ let translate_function code entry join_points =
                 (* TODO gourdinl remove this *)
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
-                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info, ni)
-            | _ -> Bseq (translate_inst ni inst false, build_btl_block s))
+                iinfo.pcond <- info;
+                Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), build_btl_block s, iinfo)
+            | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
             next_nodes := !next_nodes @ successors_inst inst;
-            translate_inst ni inst true
+            translate_inst iinfo inst true
       in
       let ib = build_btl_block e in
       let succs = !next_nodes in
-      let ibf = { entry = ib; input_regs = Regset.empty } in
+      let bi = mk_binfo (p2i e) in
+      let ibf = { entry = ib; input_regs = Regset.empty; binfo = bi } in
       btl_code := PTree.set e ibf !btl_code;
       List.iter build_btl_tree succs)
   in