From 9f252d9055ad16f9433caaf41f6490e45424e88a Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 19 May 2021 15:53:02 +0200
Subject: Adding a BTL record to help oracles

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

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index e14e0ab3..859bbf07 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -7,34 +7,36 @@ open PrintBTL
 open Camlcoq
 open AuxTools
 
+let mk_ni n = n
+
 let encaps_final inst osucc =
   match inst with
   | BF _ | Bcond _ -> inst
   | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
 
-let translate_inst inst is_final =
+let translate_inst ni inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
     | Inop s ->
         osucc := Some s;
-        Bnop
+        Bnop ni
     | Iop (op, lr, rd, s) ->
         osucc := Some s;
-        Bop (op, lr, rd)
+        Bop (op, lr, rd, ni)
     | Iload (trap, chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bload (trap, chk, addr, lr, rd)
+        Bload (trap, chk, addr, lr, rd, ni)
     | Istore (chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bstore (chk, addr, lr, rd)
-    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s))
-    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr))
-    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s))
+        Bstore (chk, addr, lr, rd, ni)
+    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s, ni))
+    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr, ni))
+    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s, ni))
     | Icond (cond, lr, ifso, ifnot, info) ->
-        Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info)
-    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
-    | Ireturn oreg -> BF (Breturn oreg)
+        Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info, ni)
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl, ni))
+    | Ireturn oreg -> BF (Breturn (oreg, ni))
   in
   if is_final then encaps_final btli !osucc else btli
 
@@ -50,6 +52,7 @@ let translate_function code entry join_points =
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
         let psucc = predicted_successor inst in
+        let ni = mk_ni n in
         let succ =
           match psucc with
           | Some ps ->
@@ -67,12 +70,12 @@ let translate_function code entry join_points =
                 (* TODO gourdinl remove this *)
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
-                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info)
-            | _ -> Bseq (translate_inst inst false, build_btl_block s))
+                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info, ni)
+            | _ -> Bseq (translate_inst ni inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
             next_nodes := !next_nodes @ successors_inst inst;
-            translate_inst inst true
+            translate_inst ni inst true
       in
       let ib = build_btl_block e in
       let succs = !next_nodes in
@@ -84,12 +87,12 @@ let translate_function code entry join_points =
   !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)
+  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;
-- 
cgit