working oracles (no renumber for now)

1 files changed, 60 insertions, 48 deletions

diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index dd7ba4c7..b4833b2c 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -4,50 +4,56 @@ open RTL
 open Camlcoq
 open AuxTools
 open DebugPrint
-open PrintBTL
+open BTLaux
 
 let is_atom = function
-  | Bseq (_, _) | Bcond (_, _, _, _, _, _) -> false
+  | Bseq (_, _) | Bcond (_, _, _, _, _) -> false
   | _ -> true
 
-let rec get_nn = function
-  | Bnop ni
-  | Bop (_, _, _, ni)
-  | Bload (_, _, _, _, _, ni)
-  | Bstore (_, _, _, _, ni)
-  | Bcond (_, _, _, _, _, ni)
-  | BF (Breturn (_, ni))
-  | BF (Bcall (_, _, _, _, _, ni))
-  | BF (Btailcall (_, _, _, ni))
-  | BF (Bbuiltin (_, _, _, _, ni))
-  | BF (Bjumptable (_, _, ni)) ->
-      ni
-  | BF (Bgoto s) -> s
-  | Bseq (ib1, _) -> get_nn ib1
+let get_inumb iinfo = P.of_int iinfo.inumb
+
+let rec get_ib_num = function
+  | BF (Bgoto s, _) -> s
+  | Bnop iinfo
+  | Bop (_, _, _, iinfo)
+  | Bload (_, _, _, _, _, iinfo)
+  | Bstore (_, _, _, _, iinfo)
+  | Bcond (_, _, _, _, iinfo)
+  | BF (_, iinfo) ->
+      get_inumb iinfo
+  | Bseq (ib1, _) -> get_ib_num ib1
 
 let translate_function code entry =
-  let reached = ref (PTree.map (fun n i -> false) code) in
   let rtl_code = ref PTree.empty in
+  let code =
+    PTree.map
+      (fun n ibf ->
+        ibf.binfo.visited <- false;
+        ibf)
+      code
+  in
   let rec build_rtl_tree e =
-    if get_some @@ PTree.get e !reached then ()
+    let ibf = get_some @@ PTree.get e code in
+    if ibf.binfo.visited then ()
     else (
-      reached := PTree.set e true !reached;
+      ibf.binfo.visited <- true;
+      let ib = ibf.entry in
       let next_nodes = ref [] in
-      let ib = (get_some @@ PTree.get e code).entry in
       let rec translate_btl_block ib k =
-        print_btl_inst stderr ib;
         let rtli =
           match ib with
-          | Bcond (cond, lr, BF (Bgoto s1), BF (Bgoto s2), info, ni) ->
+          | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) ->
               next_nodes := s1 :: s2 :: !next_nodes;
-              Some (Icond (cond, lr, s1, s2, info), ni)
-          | Bcond (cond, lr, BF (Bgoto s1), ib2, info, ni) ->
-              assert (info = Some false);
+              Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo)
+          | Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) ->
+              assert (iinfo.pcond = Some false);
               next_nodes := s1 :: !next_nodes;
               translate_btl_block ib2 None;
-              Some (Icond (cond, lr, s1, get_nn ib2, info), ni)
+              Some
+                ( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond),
+                  get_inumb iinfo )
           (* TODO gourdinl remove dynamic check *)
-          | Bcond (_, _, _, _, _, _) ->
+          | Bcond (_, _, _, _, _) ->
               failwith "translate_function: invalid Bcond"
           | Bseq (ib1, ib2) ->
               (* TODO gourdinl remove dynamic check *)
@@ -55,29 +61,35 @@ let translate_function code entry =
               translate_btl_block ib1 (Some ib2);
               translate_btl_block ib2 None;
               None
-          | Bnop ni -> Some (Inop (get_nn (get_some k)), ni)
-          | Bop (op, lr, rd, ni) ->
-              Some (Iop (op, lr, rd, get_nn (get_some k)), ni)
-          | Bload (trap, chk, addr, lr, rd, ni) ->
-              Some (Iload (trap, chk, addr, lr, rd, get_nn (get_some k)), ni)
-          | Bstore (chk, addr, lr, rd, ni) ->
-              Some (Istore (chk, addr, lr, rd, get_nn (get_some k)), ni)
-          | BF (Bcall (sign, fn, lr, rd, s, ni)) ->
+          | Bnop iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
+          | Bop (op, lr, rd, iinfo) ->
+              Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo)
+          | Bload (trap, chk, addr, lr, rd, iinfo) ->
+              Some
+                ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)),
+                  get_inumb iinfo )
+          | Bstore (chk, addr, lr, rd, iinfo) ->
+              Some
+                ( Istore (chk, addr, lr, rd, get_ib_num (get_some k)),
+                  get_inumb iinfo )
+          | BF (Bcall (sign, fn, lr, rd, s), iinfo) ->
               next_nodes := s :: !next_nodes;
-              Some (Icall (sign, fn, lr, rd, s), ni)
-          | BF (Btailcall (sign, fn, lr, ni)) ->
-              Some (Itailcall (sign, fn, lr), ni)
-          | BF (Bbuiltin (ef, lr, rd, s, ni)) ->
+              Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo)
+          | BF (Btailcall (sign, fn, lr), iinfo) ->
+              Some (Itailcall (sign, fn, lr), get_inumb iinfo)
+          | BF (Bbuiltin (ef, lr, rd, s), iinfo) ->
               next_nodes := s :: !next_nodes;
-              Some (Ibuiltin (ef, lr, rd, s), ni)
-          | BF (Bjumptable (arg, tbl, ni)) -> Some (Ijumptable (arg, tbl), ni)
-          | BF (Breturn (oreg, ni)) -> Some (Ireturn oreg, ni)
-          | BF (Bgoto s) ->
+              Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
+          | BF (Bjumptable (arg, tbl), iinfo) ->
+              next_nodes := !next_nodes @ tbl;
+              Some (Ijumptable (arg, tbl), get_inumb iinfo)
+          | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
+          | BF (Bgoto s, iinfo) ->
               next_nodes := s :: !next_nodes;
               None
         in
         match rtli with
-        | Some (inst, ni) -> rtl_code := PTree.set ni inst !rtl_code
+        | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code
         | None -> ()
       in
       translate_btl_block ib None;
@@ -88,16 +100,16 @@ let translate_function code entry =
   !rtl_code
 
 let btl2rtl (f : BTL.coq_function) =
-  debug_flag := true;
+  (*debug_flag := true;*)
   let code = f.fn_code in
   let entry = f.fn_entrypoint in
   let rtl = translate_function code entry in
   let dm = PTree.map (fun n i -> n) code in
-  debug "Entry %d\n" (P.to_int entry);
+  debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
-  print_code rtl;
+  (*print_code rtl;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "\n";
-  debug_flag := false;
+  (*debug_flag := false;*)
   ((rtl, entry), dm)