[disabled checker] BTL Scheduling and Renumbering OK!

1 files changed, 18 insertions, 28 deletions

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index e932d766..056fe213 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -4,23 +4,16 @@ open BTL
 open PrintBTL
 open RTLcommonaux
 open DebugPrint
-open BTLaux
+open BTLtypes
+open BTLcommonaux
 open BTLScheduleraux
 
-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; visited = false }
-
 let encaps_final inst osucc =
   match inst with
   | BF _ | Bcond _ -> inst
-  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo))
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ()))
 
-let translate_inst (iinfo: BTL.inst_info) inst is_final =
+let translate_inst (iinfo : BTL.inst_info) inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
@@ -44,8 +37,8 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final =
         Bcond
           ( cond,
             lr,
-            BF (Bgoto ifso, def_iinfo),
-            BF (Bgoto ifnot, def_iinfo),
+            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)
@@ -67,9 +60,7 @@ let translate_function code entry join_points liveness =
         let succ =
           match psucc with
           | Some ps ->
-              if get_some @@ PTree.get ps join_points then (
-                None)
-              else Some ps
+              if get_some @@ PTree.get ps join_points then None else Some ps
           | None -> None
         in
         match succ with
@@ -80,13 +71,10 @@ let translate_function code entry join_points liveness =
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
                 iinfo.pcond <- info;
-                Bseq (
-                Bcond
-                  ( cond,
-                    lr,
-                    BF (Bgoto ifso, def_iinfo),
-                    Bnop None,
-                    iinfo ), build_btl_block s)
+                Bseq
+                  ( Bcond
+                      (cond, lr, BF (Bgoto ifso, def_iinfo ()), Bnop None, iinfo),
+                    build_btl_block s )
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
@@ -113,17 +101,19 @@ let rtl2btl (f : RTL.coq_function) =
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   (* TODO gourdinl move elsewhere *)
-  btl_scheduler btl entry;
+  let btl' = btl_scheduler btl in
   debug "Entry %d\n" (p2i entry);
+  (*debug_flag := true;*)
   debug "RTL Code: ";
   print_code code;
-  (*debug_flag := true;*)
-  debug "BTL Code: ";
-  print_btl_code stderr btl true;
+  debug "BTL Code:\n";
+  print_btl_code stderr btl;
+  debug "Scheduled BTL Code:\n";
+  print_btl_code stderr btl';
   (*debug_flag := false;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  ((btl, entry), dm)
+  ((btl', entry), dm)