From 05b24fdb11414100b9b04867e6e2d3a1a9054162 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 28 May 2021 11:44:11 +0200
Subject: Improvements in scheduling and renumbering BTL code

---
 scheduling/BTLtoRTLaux.ml | 117 ++++++++++++++++++++--------------------------
 1 file changed, 51 insertions(+), 66 deletions(-)

(limited to 'scheduling/BTLtoRTLaux.ml')

diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index 6d8c3d87..8e728bd2 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -4,6 +4,7 @@ open RTL
 open Camlcoq
 open RTLcommonaux
 open DebugPrint
+open PrintBTL
 open BTLcommonaux
 open BTLtypes
 open BTLRenumber
@@ -14,74 +15,58 @@ 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 btl = reset_visited_ibf btl in
-  let rec build_rtl_tree e =
-    let ibf = get_some @@ PTree.get e btl in
-    if ibf.binfo.visited then ()
-    else (
+  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
-      let next_nodes = ref [] in
-      let rec translate_btl_block ib k =
-        let rtli =
-          (* TODO gourdinl remove assertions *)
-          match ib with
-          | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) ->
-              next_nodes := s1 :: s2 :: !next_nodes;
-              Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo)
-          | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) ->
-              assert (iinfo.pcond = Some false);
-              next_nodes := s1 :: !next_nodes;
-              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) ->
-              next_nodes := s :: !next_nodes;
-              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), get_inumb iinfo)
-          | BF (Bjumptable (arg, tbl), iinfo) ->
-              next_nodes := tbl @ !next_nodes;
-              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, inumb) -> rtl_code := PTree.set inumb 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;
+      translate_btl_block ib None)
+    (PTree.elements btl);
   !rtl_code
 
 let btl2rtl (f : BTL.coq_function) =
-- 
cgit