From bc6129876ffc6f0323752908f5de12bb5c5a7c74 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 20 May 2021 17:28:55 +0200
Subject: working oracles (no renumber for now)

---
 scheduling/RTLtoBTLaux.ml | 40 ++++++++++++++++++++--------------------
 1 file changed, 20 insertions(+), 20 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index d4fd2643..43556150 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -4,15 +4,16 @@ open BTL
 open Registers
 open DebugPrint
 open PrintBTL
-open Camlcoq
 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 }
+let mk_binfo _bnumb = { bnumb = _bnumb; visited = false }
 
 let encaps_final inst osucc =
   match inst with
@@ -40,16 +41,20 @@ let translate_inst iinfo inst is_final =
     | 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)
+        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)
+    | 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
-  (* TODO gourdinl SEPARATE IN A BETTER WAY!! *)
   let rec build_btl_tree e =
     if get_some @@ PTree.get e !reached then ()
     else (
@@ -63,21 +68,24 @@ let translate_function code entry join_points =
           match psucc with
           | Some ps ->
               if get_some @@ PTree.get ps join_points then (
-                debug "IS JOIN PT\n";
                 None)
               else Some ps
           | None -> None
         in
         match succ with
         | Some s -> (
-            debug "BLOCK CONTINUE\n";
             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)
+                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";
@@ -94,25 +102,16 @@ let translate_function code entry join_points =
   build_btl_tree entry;
   !btl_code
 
-let print_dm dm =
-  List.iter
-    (fun (n, n') ->
-      debug "%d -> %d" (P.to_int n) (P.to_int n');
-      (*print_btl_inst stderr ib.entry;*)
-      debug "\n")
-    (PTree.elements dm)
-
 let rtl2btl (f : RTL.coq_function) =
-  debug_flag := true;
+  (*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" (P.to_int entry);
+  debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
-  print_code code;
-  debug_flag := false;
+  (*print_code code;*)
   debug "BTL Code: ";
   print_btl_code stderr btl true;
   debug "Dupmap:\n";
@@ -120,4 +119,5 @@ let rtl2btl (f : RTL.coq_function) =
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
+  (*debug_flag := false;*)
   ((btl, entry), dm)
-- 
cgit