Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

1 files changed, 123 insertions, 0 deletions

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
new file mode 100644
index 00000000..43556150
--- /dev/null
+++ b/scheduling/RTLtoBTLaux.ml
@@ -0,0 +1,123 @@
+open Maps
+open RTL
+open BTL
+open Registers
+open DebugPrint
+open PrintBTL
+open AuxTools
+open BTLaux
+
+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))
+
+let translate_inst iinfo inst is_final =
+  let osucc = ref None in
+  let btli =
+    match inst with
+    | Inop s ->
+        osucc := Some s;
+        Bnop iinfo
+    | Iop (op, lr, rd, s) ->
+        osucc := Some s;
+        Bop (op, lr, rd, iinfo)
+    | Iload (trap, chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bload (trap, chk, addr, lr, rd, iinfo)
+    | Istore (chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bstore (chk, addr, lr, rd, iinfo)
+    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo)
+    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo)
+    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo)
+    | Icond (cond, lr, ifso, ifnot, info) ->
+        iinfo.pcond <- info;
+        Bcond
+          ( cond,
+            lr,
+            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)
+  in
+  if is_final then encaps_final btli !osucc else btli
+
+let translate_function code entry join_points =
+  let reached = ref (PTree.map (fun n i -> false) code) in
+  let btl_code = ref PTree.empty in
+  let rec build_btl_tree e =
+    if get_some @@ PTree.get e !reached then ()
+    else (
+      reached := PTree.set e true !reached;
+      let next_nodes = ref [] in
+      let rec build_btl_block n =
+        let inst = get_some @@ PTree.get n code in
+        let psucc = predicted_successor inst in
+        let iinfo = mk_iinfo (p2i n) None in
+        let succ =
+          match psucc with
+          | Some ps ->
+              if get_some @@ PTree.get ps join_points then (
+                None)
+              else Some ps
+          | None -> None
+        in
+        match succ with
+        | Some s -> (
+            match inst with
+            | Icond (cond, lr, ifso, ifnot, info) ->
+                (* TODO gourdinl remove this *)
+                assert (s = ifnot);
+                next_nodes := !next_nodes @ non_predicted_successors inst psucc;
+                iinfo.pcond <- info;
+                Bcond
+                  ( cond,
+                    lr,
+                    BF (Bgoto ifso, def_iinfo),
+                    build_btl_block s,
+                    iinfo )
+            | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
+        | None ->
+            debug "BLOCK END.\n";
+            next_nodes := !next_nodes @ successors_inst inst;
+            translate_inst iinfo inst true
+      in
+      let ib = build_btl_block e in
+      let succs = !next_nodes in
+      let bi = mk_binfo (p2i e) in
+      let ibf = { entry = ib; input_regs = Regset.empty; binfo = bi } in
+      btl_code := PTree.set e ibf !btl_code;
+      List.iter build_btl_tree succs)
+  in
+  build_btl_tree entry;
+  !btl_code
+
+let rtl2btl (f : RTL.coq_function) =
+  (*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" (p2i entry);
+  debug "RTL Code: ";
+  (*print_code code;*)
+  debug "BTL Code: ";
+  print_btl_code stderr btl true;
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
+  debug "Join points: ";
+  print_true_nodes join_points;
+  debug "\n";
+  (*debug_flag := false;*)
+  ((btl, entry), dm)