Adding a BTL record to help oracles

1 files changed, 101 insertions, 3 deletions

diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index 3d8d44d0..dd7ba4c7 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -1,5 +1,103 @@
 open Maps
-open BinNums
+open BTL
+open RTL
+open Camlcoq
+open AuxTools
+open DebugPrint
+open PrintBTL
 
-let btl2rtl f =
-  ((PTree.empty, Coq_xH), PTree.empty)
+let is_atom = function
+  | 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 translate_function code entry =
+  let reached = ref (PTree.map (fun n i -> false) code) in
+  let rtl_code = ref PTree.empty in
+  let rec build_rtl_tree e =
+    if get_some @@ PTree.get e !reached then ()
+    else (
+      reached := PTree.set e true !reached;
+      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) ->
+              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);
+              next_nodes := s1 :: !next_nodes;
+              translate_btl_block ib2 None;
+              Some (Icond (cond, lr, s1, get_nn ib2, info), ni)
+          (* TODO gourdinl remove dynamic check *)
+          | Bcond (_, _, _, _, _, _) ->
+              failwith "translate_function: invalid Bcond"
+          | Bseq (ib1, ib2) ->
+              (* TODO gourdinl remove dynamic check *)
+              assert (is_atom ib1);
+              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)) ->
+              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)) ->
+              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) ->
+              next_nodes := s :: !next_nodes;
+              None
+        in
+        match rtli with
+        | Some (inst, ni) -> rtl_code := PTree.set ni inst !rtl_code
+        | None -> ()
+      in
+      translate_btl_block ib None;
+      let succs = !next_nodes in
+      List.iter build_rtl_tree succs)
+  in
+  build_rtl_tree entry;
+  !rtl_code
+
+let btl2rtl (f : BTL.coq_function) =
+  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 "RTL Code: ";
+  print_code rtl;
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
+  debug "\n";
+  debug_flag := false;
+  ((rtl, entry), dm)