From 1a78c940f46273b7146d2111b1e2da309434f021 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 27 May 2021 16:55:18 +0200
Subject: [disabled checker] BTL Scheduling and Renumbering OK!

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

(limited to 'scheduling/BTLtoRTLaux.ml')

diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index 42c20942..6d8c3d87 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -4,33 +4,19 @@ open RTL
 open Camlcoq
 open RTLcommonaux
 open DebugPrint
-open BTLaux
+open BTLcommonaux
+open BTLtypes
+open BTLRenumber
 
 let get_inumb iinfo = P.of_int iinfo.inumb
 
-let rec get_ib_num = function
-  | BF (Bgoto s, _) -> s
-  | Bnop Some iinfo
-  | Bop (_, _, _, iinfo)
-  | Bload (_, _, _, _, _, iinfo)
-  | Bstore (_, _, _, _, iinfo)
-  | Bcond (_, _, _, _, iinfo)
-  | BF (_, iinfo) ->
-      get_inumb iinfo
-  | Bseq (ib1, _) -> get_ib_num ib1
-  | Bnop None -> failwith "get_ib_num: Bnop None found"
+let get_ib_num ib = P.of_int (get_inumb_or_next ib)
 
-let translate_function code entry =
+let translate_function btl entry =
   let rtl_code = ref PTree.empty in
-  let code =
-    PTree.map
-      (fun n ibf ->
-        ibf.binfo.visited <- false;
-        ibf)
-      code
-  in
+  let btl = reset_visited_ibf btl in
   let rec build_rtl_tree e =
-    let ibf = get_some @@ PTree.get e code in
+    let ibf = get_some @@ PTree.get e btl in
     if ibf.binfo.visited then ()
     else (
       ibf.binfo.visited <- true;
@@ -38,6 +24,7 @@ let translate_function code entry =
       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;
@@ -48,15 +35,18 @@ let translate_function code entry =
               Some
                 ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond),
                   get_inumb iinfo )
-          (* TODO gourdinl remove dynamic check *)
           | Bcond (_, _, _, _, _) ->
-              failwith "translate_function: invalid 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: invalid Bnop"
+          | 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) ->
@@ -76,7 +66,7 @@ let translate_function code entry =
               next_nodes := s :: !next_nodes;
               Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
           | BF (Bjumptable (arg, tbl), iinfo) ->
-              next_nodes := !next_nodes @ tbl;
+              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) ->
@@ -96,13 +86,14 @@ let translate_function code entry =
 
 let btl2rtl (f : BTL.coq_function) =
   (*debug_flag := true;*)
-  let code = f.fn_code in
+  let btl = 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
+  let ordered_btl, new_entry = renumber btl entry in
+  let rtl = translate_function ordered_btl new_entry in
+  let dm = PTree.map (fun n i -> n) btl in
   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";
-- 
cgit