first oracle seems ok

1 files changed, 12 insertions, 11 deletions

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 3c9b7644..9a61f55e 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -5,6 +5,7 @@ open Registers
 open DebugPrint
 open PrintRTL
 open PrintBTL
+open Camlcoq
 
 (* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
         This should be accessible everywhere. *)
@@ -84,8 +85,6 @@ let translate_inst inst is_final =
     | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr))
     | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s))
     | Icond (cond, lr, ifso, ifnot, info) ->
-        (* TODO gourdinl remove this *)
-        assert (info = None);
         Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info)
     | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
     | Ireturn oreg -> BF (Breturn oreg)
@@ -140,28 +139,30 @@ let translate_function code entry join_points =
   build_btl_tree entry;
   !btl_code
 
-(*let print_dm dm =*)
-  (*List.iter (fun (n,ib) ->*)
-    (*debug "%d:" (P.to_int n);*)
-    (*print_iblock stderr false ib.entry)*)
-  (*(PTree.elements dm)*)
-
-
+let print_dm dm =
+  List.iter (fun (n,n') ->
+    debug "%d -> %d" (P.to_int n) (P.to_int n');
+    (*print_btl_inst stderr ib.entry;*)
+    debug "\n"
+    )
+  (PTree.elements dm)
 
 let rtl2btl (f : RTL.coq_function) =
-  debug_flag := true;
+  (*debug_flag := true;*)
   let code = f.fn_code in
   let entry = f.fn_entrypoint in
   let join_points = get_join_points code entry in
   let btl = translate_function code entry join_points in
   let dm = PTree.map (fun n i -> n) btl in
+  debug "Entry %d\n" (P.to_int entry);
   debug "RTL Code: ";
   print_code code;
   debug "BTL Code: ";
   print_btl_code stderr btl true;
+  debug "BTL Dupmap:\n";
+  print_dm dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  (*print_dm dm;*)
   debug_flag := false;
   ((btl, entry), dm)