1 files changed, 88 insertions, 0 deletions
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
new file mode 100644
index 00000000..ddec991d
--- /dev/null
+++ b/scheduling/BTLtoRTLaux.ml
@@ -0,0 +1,88 @@
+open Maps
+open BTL
+open RTL
+open Camlcoq
+open RTLcommonaux
+open DebugPrint
+open PrintBTL
+open BTLcommonaux
+open BTLtypes
+open BTLRenumber
+
+let get_inumb iinfo = P.of_int iinfo.inumb
+
+let get_ib_num ib = P.of_int (get_inumb_or_next ib)
+
+let translate_function btl entry =
+  let rtl_code = ref PTree.empty in
+  let rec translate_btl_block ib k =
+    debug "Entering translate_btl_block...\n";
+    print_btl_inst stderr ib;
+    let rtli =
+      match ib with
+      | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) ->
+          Some
+            ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond),
+              get_inumb iinfo )
+      | Bcond (_, _, _, _, _) ->
+          failwith "translate_function: unsupported Bcond"
+      | Bseq (ib1, ib2) ->
+          translate_btl_block ib1 (Some ib2);
+          translate_btl_block ib2 None;
+          None
+      | Bnop (Some iinfo) ->
+          Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
+      | Bnop None ->
+          failwith
+            "translate_function: Bnop None can only be in the right child of \
+             Bcond"
+      | 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, src, iinfo) ->
+          Some
+            ( Istore (chk, addr, lr, src, get_ib_num (get_some k)),
+              get_inumb iinfo )
+      | BF (Bcall (sign, fn, lr, rd, s), iinfo) ->
+          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) ->
+          Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
+      | BF (Bjumptable (arg, tbl), iinfo) ->
+          Some (Ijumptable (arg, tbl), get_inumb iinfo)
+      | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
+      | BF (Bgoto s, iinfo) -> None
+    in
+    match rtli with
+    | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code
+    | None -> ()
+  in
+  List.iter
+    (fun (n, ibf) ->
+      ibf.binfo.visited <- true;
+      let ib = ibf.entry in
+      translate_btl_block ib None)
+    (PTree.elements btl);
+  !rtl_code
+
+let btl2rtl (f : BTL.coq_function) =
+  (*debug_flag := true;*)
+  let btl = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let obne, dm = renumber btl entry in
+  let ordered_btl, new_entry = obne in
+  let rtl = translate_function ordered_btl new_entry in
+  debug "Entry %d\n" (p2i new_entry);
+  debug "BTL Code:\n";
+  print_btl_code stderr ordered_btl;
+  debug "RTL Code: ";
+  print_code rtl;
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
+  debug "\n";
+  (*debug_flag := false;*)
+  ((rtl, new_entry), dm)