From bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 17 May 2021 23:19:16 +0200
Subject: preparing compiler passes and ml oracles

---
 scheduling/RTLtoBTLaux.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 scheduling/RTLtoBTLaux.ml

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
new file mode 100644
index 00000000..8ace6e2a
--- /dev/null
+++ b/scheduling/RTLtoBTLaux.ml
@@ -0,0 +1,17 @@
+open RTLpathLivegenaux
+open Maps
+open RTL
+open BinNums
+open DebugPrint
+
+let rtl2btl (f: RTL.coq_function) =
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let join_points = get_join_points code entry in
+  Printf.eprintf "test";
+  debug_flag := true;
+  debug "Join points: ";
+  print_true_nodes join_points;
+  debug "\n";
+  debug_flag := false;
+  ((PTree.empty, Coq_xH), PTree.empty)
-- 
cgit 


From 4553ef98a44da4b34263935b5529b206a89d6dd0 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 18 May 2021 12:42:30 +0200
Subject: First draft of the RTL2BTL oracle

---
 scheduling/RTLtoBTLaux.ml | 109 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 105 insertions(+), 4 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 8ace6e2a..20aa01aa 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -1,17 +1,118 @@
-open RTLpathLivegenaux
 open Maps
 open RTL
-open BinNums
+open BTL
+open Registers
 open DebugPrint
 
+(* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
+        This should be accessible everywhere. *)
+let get_some = function
+| None -> failwith "Got None instead of Some _"
+| Some thing -> thing
+
+let successors_inst = function
+| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n]
+| Icond (_,_,n1,n2,_) -> [n1; n2]
+| Ijumptable (_,l) -> l
+| Itailcall _ | Ireturn _ -> []
+
+let predicted_successor = function
+| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n
+| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None
+| Icond (_,_,n1,n2,p) -> (
+    match p with
+    | Some true -> Some n1
+    | Some false -> Some n2
+    | None -> None )
+| Ijumptable _ | Itailcall _ | Ireturn _ -> None
+
+(* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
+let non_predicted_successors i = function
+  | None -> successors_inst i
+  | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
+
+(* adapted from Linearizeaux.get_join_points *)
+let get_join_points code entry =
+  let reached = ref (PTree.map (fun n i -> false) code) in
+  let reached_twice = ref (PTree.map (fun n i -> false) code) in
+  let rec traverse pc =
+    if get_some @@ PTree.get pc !reached then begin
+      if not (get_some @@ PTree.get pc !reached_twice) then
+        reached_twice := PTree.set pc true !reached_twice
+    end else begin
+      reached := PTree.set pc true !reached;
+      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
+    end
+  and traverse_succs = function
+    | [] -> ()
+    | [pc] -> traverse pc
+    | pc :: l -> traverse pc; traverse_succs l
+  in traverse entry; !reached_twice
+
+let translate_inst = function
+    | Inop (_) -> Bnop
+    | Iop (op,lr,rd,_) -> Bop (op,lr,rd)
+    | Iload (trap,chk,addr,lr,rd,_) -> Bload (trap,chk,addr,lr,rd)
+    | Istore (chk,addr,lr,rd,_) -> 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))
+    | Icond (cond,lr,ifso,ifnot,info) -> (
+        (* TODO gourdinl remove this *)
+        assert (info = None);
+        Bcond (cond,lr,BF (Bgoto(ifso)),BF (Bgoto(ifnot)),info))
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg,tbl))
+    | Ireturn (oreg) -> BF (Breturn (oreg))
+
+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
+  (* SEPARATE IN A BETTER WAY!! *)
+  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 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 = ifso || s = ifnot);
+              next_nodes := !next_nodes @ non_predicted_successors inst psucc;
+              if s = ifso then
+                Bcond (cond,lr,build_btl_block s,BF (Bgoto (ifnot)),info)
+              else
+                Bcond (cond,lr,BF (Bgoto (ifso)),build_btl_block s,info))
+          | _ -> Bseq (translate_inst inst, build_btl_block s))
+        | None -> (
+            next_nodes := !next_nodes @ successors_inst inst;
+            translate_inst inst)
+      in
+      let ib = build_btl_block e in
+      let succs = !next_nodes in
+      let ibf = { entry = ib; input_regs = Regset.empty } 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) =
   let code = f.fn_code in
   let entry = f.fn_entrypoint in
   let join_points = get_join_points code entry in
-  Printf.eprintf "test";
+  let btl = translate_function code entry join_points in
   debug_flag := true;
+  debug"Code: ";
+  print_code code;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
   debug_flag := false;
-  ((PTree.empty, Coq_xH), PTree.empty)
+  ((btl, entry), PTree.empty)
-- 
cgit 


From c27d87ffe33242840964dd9bd67090409eea79a5 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 18 May 2021 16:55:56 +0200
Subject: oracle simplification, BTL printer, and error msg spec

---
 scheduling/RTLtoBTLaux.ml | 161 ++++++++++++++++++++++++++++++----------------
 1 file changed, 105 insertions(+), 56 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 20aa01aa..3c9b7644 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -3,28 +3,35 @@ open RTL
 open BTL
 open Registers
 open DebugPrint
+open PrintRTL
+open PrintBTL
 
 (* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
         This should be accessible everywhere. *)
 let get_some = function
-| None -> failwith "Got None instead of Some _"
-| Some thing -> thing
+  | None -> failwith "Got None instead of Some _"
+  | Some thing -> thing
 
 let successors_inst = function
-| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n]
-| Icond (_,_,n1,n2,_) -> [n1; n2]
-| Ijumptable (_,l) -> l
-| Itailcall _ | Ireturn _ -> []
+  | Inop n
+  | Iop (_, _, _, n)
+  | Iload (_, _, _, _, _, n)
+  | Istore (_, _, _, _, n)
+  | Icall (_, _, _, _, n)
+  | Ibuiltin (_, _, _, n) ->
+      [ n ]
+  | Icond (_, _, n1, n2, _) -> [ n1; n2 ]
+  | Ijumptable (_, l) -> l
+  | Itailcall _ | Ireturn _ -> []
 
 let predicted_successor = function
-| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n
-| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None
-| Icond (_,_,n1,n2,p) -> (
-    match p with
-    | Some true -> Some n1
-    | Some false -> Some n2
-    | None -> None )
-| Ijumptable _ | Itailcall _ | Ireturn _ -> None
+  | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
+    ->
+      Some n
+  | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
+  | Icond (_, _, n1, n2, p) -> (
+      match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
+  | Ijumptable _ | Itailcall _ | Ireturn _ -> None
 
 (* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
 let non_predicted_successors i = function
@@ -36,83 +43,125 @@ let get_join_points code entry =
   let reached = ref (PTree.map (fun n i -> false) code) in
   let reached_twice = ref (PTree.map (fun n i -> false) code) in
   let rec traverse pc =
-    if get_some @@ PTree.get pc !reached then begin
+    if get_some @@ PTree.get pc !reached then (
       if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice
-    end else begin
+        reached_twice := PTree.set pc true !reached_twice)
+    else (
       reached := PTree.set pc true !reached;
-      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
-    end
+      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code))
   and traverse_succs = function
     | [] -> ()
-    | [pc] -> traverse pc
-    | pc :: l -> traverse pc; traverse_succs l
-  in traverse entry; !reached_twice
+    | [ pc ] -> traverse pc
+    | pc :: l ->
+        traverse pc;
+        traverse_succs l
+  in
+  traverse entry;
+  !reached_twice
+
+let encaps_final inst osucc =
+  match inst with
+  | BF _ | Bcond _ -> inst
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
 
-let translate_inst = function
-    | Inop (_) -> Bnop
-    | Iop (op,lr,rd,_) -> Bop (op,lr,rd)
-    | Iload (trap,chk,addr,lr,rd,_) -> Bload (trap,chk,addr,lr,rd)
-    | Istore (chk,addr,lr,rd,_) -> 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))
-    | Icond (cond,lr,ifso,ifnot,info) -> (
+let translate_inst inst is_final =
+  let osucc = ref None in
+  let btli =
+    match inst with
+    | Inop s ->
+        osucc := Some s;
+        Bnop
+    | Iop (op, lr, rd, s) ->
+        osucc := Some s;
+        Bop (op, lr, rd)
+    | Iload (trap, chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bload (trap, chk, addr, lr, rd)
+    | 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))
+    | Icond (cond, lr, ifso, ifnot, info) ->
         (* TODO gourdinl remove this *)
         assert (info = None);
-        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)
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
+    | Ireturn oreg -> BF (Breturn oreg)
+  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
   (* SEPARATE IN A BETTER WAY!! *)
   let rec build_btl_tree e =
-    if (get_some @@ PTree.get e !reached) then ()
+    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
+        debug "Inst is : ";
+        print_instruction stderr (0, inst);
+        debug "\n";
         let psucc = predicted_successor inst 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
+          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 -> (
-          match inst with
-          | Icond (cond,lr,ifso,ifnot,info) -> (
-              (* TODO gourdinl remove this *)
-              assert (s = ifso || s = ifnot);
-              next_nodes := !next_nodes @ non_predicted_successors inst psucc;
-              if s = ifso then
-                Bcond (cond,lr,build_btl_block s,BF (Bgoto (ifnot)),info)
-              else
-                Bcond (cond,lr,BF (Bgoto (ifso)),build_btl_block s,info))
-          | _ -> Bseq (translate_inst inst, build_btl_block s))
-        | None -> (
+            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;
+                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info)
+            | _ -> Bseq (translate_inst inst false, build_btl_block s))
+        | None ->
+            debug "BLOCK END.\n";
             next_nodes := !next_nodes @ successors_inst inst;
-            translate_inst inst)
+            translate_inst inst true
       in
       let ib = build_btl_block e in
       let succs = !next_nodes in
       let ibf = { entry = ib; input_regs = Regset.empty } in
       btl_code := PTree.set e ibf !btl_code;
       List.iter build_btl_tree succs)
-  in build_btl_tree entry; !btl_code
+  in
+  build_btl_tree entry;
+  !btl_code
+
+(*let print_dm dm =*)
+  (*List.iter (fun (n,ib) ->*)
+    (*debug "%d:" (P.to_int n);*)
+    (*print_iblock stderr false ib.entry)*)
+  (*(PTree.elements dm)*)
+
 
-let rtl2btl (f: RTL.coq_function) =
+
+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
-  debug_flag := true;
-  debug"Code: ";
+  let dm = PTree.map (fun n i -> n) btl in
+  debug "RTL Code: ";
   print_code code;
+  debug "BTL Code: ";
+  print_btl_code stderr btl true;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
+  (*print_dm dm;*)
   debug_flag := false;
-  ((btl, entry), PTree.empty)
+  ((btl, entry), dm)
-- 
cgit 


From af2208a2c7126d4d101fb07c40920e12c9ebbab3 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 18 May 2021 19:15:39 +0200
Subject: first oracle seems ok

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

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 3c9b7644..9a61f55e 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -5,6 +5,7 @@ open Registers
 open DebugPrint
 open PrintRTL
 open PrintBTL
+open Camlcoq
 
 (* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
         This should be accessible everywhere. *)
@@ -84,8 +85,6 @@ let translate_inst inst is_final =
     | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr))
     | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s))
     | Icond (cond, lr, ifso, ifnot, info) ->
-        (* TODO gourdinl remove this *)
-        assert (info = None);
         Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info)
     | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
     | Ireturn oreg -> BF (Breturn oreg)
@@ -140,28 +139,30 @@ let translate_function code entry join_points =
   build_btl_tree entry;
   !btl_code
 
-(*let print_dm dm =*)
-  (*List.iter (fun (n,ib) ->*)
-    (*debug "%d:" (P.to_int n);*)
-    (*print_iblock stderr false ib.entry)*)
-  (*(PTree.elements dm)*)
-
-
+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 "RTL Code: ";
   print_code code;
   debug "BTL Code: ";
   print_btl_code stderr btl true;
+  debug "BTL Dupmap:\n";
+  print_dm dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  (*print_dm dm;*)
   debug_flag := false;
   ((btl, entry), dm)
-- 
cgit 


From ab520acd80f7d39aa14fdda6932accbb2a787ebf Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 19 May 2021 12:47:22 +0200
Subject: Grouping common RTL functions, printer improvement

---
 scheduling/RTLtoBTLaux.ml | 68 +++++------------------------------------------
 1 file changed, 6 insertions(+), 62 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 9a61f55e..e14e0ab3 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -3,62 +3,9 @@ open RTL
 open BTL
 open Registers
 open DebugPrint
-open PrintRTL
 open PrintBTL
 open Camlcoq
-
-(* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
-        This should be accessible everywhere. *)
-let get_some = function
-  | None -> failwith "Got None instead of Some _"
-  | Some thing -> thing
-
-let successors_inst = function
-  | Inop n
-  | Iop (_, _, _, n)
-  | Iload (_, _, _, _, _, n)
-  | Istore (_, _, _, _, n)
-  | Icall (_, _, _, _, n)
-  | Ibuiltin (_, _, _, n) ->
-      [ n ]
-  | Icond (_, _, n1, n2, _) -> [ n1; n2 ]
-  | Ijumptable (_, l) -> l
-  | Itailcall _ | Ireturn _ -> []
-
-let predicted_successor = function
-  | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
-    ->
-      Some n
-  | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
-  | Icond (_, _, n1, n2, p) -> (
-      match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
-  | Ijumptable _ | Itailcall _ | Ireturn _ -> None
-
-(* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
-let non_predicted_successors i = function
-  | None -> successors_inst i
-  | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
-
-(* adapted from Linearizeaux.get_join_points *)
-let get_join_points code entry =
-  let reached = ref (PTree.map (fun n i -> false) code) in
-  let reached_twice = ref (PTree.map (fun n i -> false) code) in
-  let rec traverse pc =
-    if get_some @@ PTree.get pc !reached then (
-      if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice)
-    else (
-      reached := PTree.set pc true !reached;
-      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code))
-  and traverse_succs = function
-    | [] -> ()
-    | [ pc ] -> traverse pc
-    | pc :: l ->
-        traverse pc;
-        traverse_succs l
-  in
-  traverse entry;
-  !reached_twice
+open AuxTools
 
 let encaps_final inst osucc =
   match inst with
@@ -94,7 +41,7 @@ let translate_inst inst is_final =
 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
-  (* SEPARATE IN A BETTER WAY!! *)
+  (* TODO gourdinl SEPARATE IN A BETTER WAY!! *)
   let rec build_btl_tree e =
     if get_some @@ PTree.get e !reached then ()
     else (
@@ -102,9 +49,6 @@ let translate_function code entry join_points =
       let next_nodes = ref [] in
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
-        debug "Inst is : ";
-        print_instruction stderr (0, inst);
-        debug "\n";
         let psucc = predicted_successor inst in
         let succ =
           match psucc with
@@ -148,7 +92,7 @@ let print_dm dm =
   (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
@@ -157,12 +101,12 @@ let rtl2btl (f : RTL.coq_function) =
   debug "Entry %d\n" (P.to_int entry);
   debug "RTL Code: ";
   print_code code;
+  debug_flag := false;
   debug "BTL Code: ";
   print_btl_code stderr btl true;
-  debug "BTL Dupmap:\n";
-  print_dm dm;
+  debug "Dupmap:\n";
+  print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  debug_flag := false;
   ((btl, entry), dm)
-- 
cgit 


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 


From 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 20 May 2021 11:58:40 +0200
Subject: Changing to an opaq record in BTL info, this is a broken commit

---
 scheduling/RTLtoBTLaux.ml | 44 ++++++++++++++++++++++++++------------------
 1 file changed, 26 insertions(+), 18 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 859bbf07..d4fd2643 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -6,37 +6,43 @@ open DebugPrint
 open PrintBTL
 open Camlcoq
 open AuxTools
+open BTLaux
 
-let mk_ni n = n
+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 encaps_final inst osucc =
   match inst with
   | BF _ | Bcond _ -> inst
-  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo))
 
-let translate_inst ni inst is_final =
+let translate_inst iinfo inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
     | Inop s ->
         osucc := Some s;
-        Bnop ni
+        Bnop iinfo
     | Iop (op, lr, rd, s) ->
         osucc := Some s;
-        Bop (op, lr, rd, ni)
+        Bop (op, lr, rd, iinfo)
     | Iload (trap, chk, addr, lr, rd, s) ->
         osucc := Some s;
-        Bload (trap, chk, addr, lr, rd, ni)
+        Bload (trap, chk, addr, lr, rd, iinfo)
     | Istore (chk, addr, lr, rd, s) ->
         osucc := Some 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))
+        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) ->
-        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))
+        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
 
@@ -52,7 +58,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 iinfo = mk_iinfo (p2i n) None in
         let succ =
           match psucc with
           | Some ps ->
@@ -70,16 +76,18 @@ 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, ni)
-            | _ -> Bseq (translate_inst ni inst false, build_btl_block s))
+                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 ni inst true
+            translate_inst iinfo inst true
       in
       let ib = build_btl_block e in
       let succs = !next_nodes in
-      let ibf = { entry = ib; input_regs = Regset.empty } 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
-- 
cgit 


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 


From 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 21 May 2021 21:18:59 +0200
Subject: Now supporting Bnop insertion in conditions

---
 scheduling/RTLtoBTLaux.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 43556150..4be2b180 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -2,9 +2,9 @@ open Maps
 open RTL
 open BTL
 open Registers
-open DebugPrint
 open PrintBTL
 open AuxTools
+open DebugPrint
 open BTLaux
 
 let undef_node = -1
@@ -20,13 +20,13 @@ let encaps_final inst osucc =
   | BF _ | Bcond _ -> inst
   | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo))
 
-let translate_inst iinfo inst is_final =
+let translate_inst (iinfo: BTL.inst_info) inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
     | Inop s ->
         osucc := Some s;
-        Bnop iinfo
+        Bnop (Some iinfo)
     | Iop (op, lr, rd, s) ->
         osucc := Some s;
         Bop (op, lr, rd, iinfo)
@@ -80,12 +80,13 @@ let translate_function code entry join_points =
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
                 iinfo.pcond <- info;
+                Bseq (
                 Bcond
                   ( cond,
                     lr,
                     BF (Bgoto ifso, def_iinfo),
-                    build_btl_block s,
-                    iinfo )
+                    Bnop None,
+                    iinfo ), build_btl_block s)
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
-- 
cgit 


From 0efe7783c50d72858352fda93d30e0f52792d658 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 24 May 2021 10:07:52 +0200
Subject: Moving common tools, adding liveness input/output information to BTL
 generation oracle

---
 scheduling/RTLtoBTLaux.ml | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 4be2b180..07e7a9d9 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -3,7 +3,7 @@ open RTL
 open BTL
 open Registers
 open PrintBTL
-open AuxTools
+open RTLcommonaux
 open DebugPrint
 open BTLaux
 
@@ -13,7 +13,7 @@ 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 mk_binfo _bnumb _output_regs = { bnumb = _bnumb; visited = false; output_regs = _output_regs }
 
 let encaps_final inst osucc =
   match inst with
@@ -52,7 +52,7 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final =
   in
   if is_final then encaps_final btli !osucc else btli
 
-let translate_function code entry join_points =
+let translate_function code entry join_points liveness =
   let reached = ref (PTree.map (fun n i -> false) code) in
   let btl_code = ref PTree.empty in
   let rec build_btl_tree e =
@@ -60,6 +60,7 @@ let translate_function code entry join_points =
     else (
       reached := PTree.set e true !reached;
       let next_nodes = ref [] in
+      let last = ref None in
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
         let psucc = predicted_successor inst in
@@ -90,13 +91,21 @@ let translate_function code entry join_points =
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
+            last := Some inst;
             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
+
+      let inputs = get_some @@ PTree.get e liveness in
+      let blk_last_successors = successors_inst (get_some @@ !last) in
+      let list_input_regs = List.map (
+          fun n -> get_some @@ PTree.get n liveness
+        ) blk_last_successors in
+      let outputs = List.fold_left Regset.union Regset.empty list_input_regs in
+      let bi = mk_binfo (p2i e) outputs in
+      let ibf = { entry = ib; input_regs = inputs; binfo = bi } in
       btl_code := PTree.set e ibf !btl_code;
       List.iter build_btl_tree succs)
   in
@@ -104,21 +113,22 @@ let translate_function code entry join_points =
   !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 liveness = analyze f in
+  let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
-  (*print_code code;*)
+  print_code code;
+  (*debug_flag := true;*)
   debug "BTL Code: ";
   print_btl_code stderr btl true;
+  (*debug_flag := false;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  (*debug_flag := false;*)
   ((btl, entry), dm)
-- 
cgit 


From a6006df63f0d03cc223d13834e81a71651513fbe Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 24 May 2021 17:39:44 +0200
Subject: a draft frontend for prepass

---
 scheduling/RTLtoBTLaux.ml | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 07e7a9d9..e932d766 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -1,11 +1,11 @@
 open Maps
 open RTL
 open BTL
-open Registers
 open PrintBTL
 open RTLcommonaux
 open DebugPrint
 open BTLaux
+open BTLScheduleraux
 
 let undef_node = -1
 
@@ -13,7 +13,7 @@ let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond }
 
 let def_iinfo = { inumb = undef_node; pcond = None }
 
-let mk_binfo _bnumb _output_regs = { bnumb = _bnumb; visited = false; output_regs = _output_regs }
+let mk_binfo _bnumb = { bnumb = _bnumb; visited = false }
 
 let encaps_final inst osucc =
   match inst with
@@ -33,9 +33,9 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final =
     | Iload (trap, chk, addr, lr, rd, s) ->
         osucc := Some s;
         Bload (trap, chk, addr, lr, rd, iinfo)
-    | Istore (chk, addr, lr, rd, s) ->
+    | Istore (chk, addr, lr, src, s) ->
         osucc := Some s;
-        Bstore (chk, addr, lr, rd, iinfo)
+        Bstore (chk, addr, lr, src, 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)
@@ -60,7 +60,6 @@ let translate_function code entry join_points liveness =
     else (
       reached := PTree.set e true !reached;
       let next_nodes = ref [] in
-      let last = ref None in
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
         let psucc = predicted_successor inst in
@@ -91,7 +90,6 @@ let translate_function code entry join_points liveness =
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
-            last := Some inst;
             next_nodes := !next_nodes @ successors_inst inst;
             translate_inst iinfo inst true
       in
@@ -99,12 +97,7 @@ let translate_function code entry join_points liveness =
       let succs = !next_nodes in
 
       let inputs = get_some @@ PTree.get e liveness in
-      let blk_last_successors = successors_inst (get_some @@ !last) in
-      let list_input_regs = List.map (
-          fun n -> get_some @@ PTree.get n liveness
-        ) blk_last_successors in
-      let outputs = List.fold_left Regset.union Regset.empty list_input_regs in
-      let bi = mk_binfo (p2i e) outputs in
+      let bi = mk_binfo (p2i e) in
       let ibf = { entry = ib; input_regs = inputs; binfo = bi } in
       btl_code := PTree.set e ibf !btl_code;
       List.iter build_btl_tree succs)
@@ -119,6 +112,8 @@ let rtl2btl (f : RTL.coq_function) =
   let liveness = analyze f in
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
+  (* TODO gourdinl move elsewhere *)
+  btl_scheduler btl entry;
   debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
   print_code code;
-- 
cgit 


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/RTLtoBTLaux.ml | 46 ++++++++++++++++++----------------------------
 1 file changed, 18 insertions(+), 28 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index e932d766..056fe213 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -4,23 +4,16 @@ open BTL
 open PrintBTL
 open RTLcommonaux
 open DebugPrint
-open BTLaux
+open BTLtypes
+open BTLcommonaux
 open BTLScheduleraux
 
-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))
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ()))
 
-let translate_inst (iinfo: BTL.inst_info) inst is_final =
+let translate_inst (iinfo : BTL.inst_info) inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
@@ -44,8 +37,8 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final =
         Bcond
           ( cond,
             lr,
-            BF (Bgoto ifso, def_iinfo),
-            BF (Bgoto ifnot, def_iinfo),
+            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)
@@ -67,9 +60,7 @@ let translate_function code entry join_points liveness =
         let succ =
           match psucc with
           | Some ps ->
-              if get_some @@ PTree.get ps join_points then (
-                None)
-              else Some ps
+              if get_some @@ PTree.get ps join_points then None else Some ps
           | None -> None
         in
         match succ with
@@ -80,13 +71,10 @@ let translate_function code entry join_points liveness =
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
                 iinfo.pcond <- info;
-                Bseq (
-                Bcond
-                  ( cond,
-                    lr,
-                    BF (Bgoto ifso, def_iinfo),
-                    Bnop None,
-                    iinfo ), build_btl_block s)
+                Bseq
+                  ( Bcond
+                      (cond, lr, BF (Bgoto ifso, def_iinfo ()), Bnop None, iinfo),
+                    build_btl_block s )
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
@@ -113,17 +101,19 @@ let rtl2btl (f : RTL.coq_function) =
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   (* TODO gourdinl move elsewhere *)
-  btl_scheduler btl entry;
+  let btl' = btl_scheduler btl in
   debug "Entry %d\n" (p2i entry);
+  (*debug_flag := true;*)
   debug "RTL Code: ";
   print_code code;
-  (*debug_flag := true;*)
-  debug "BTL Code: ";
-  print_btl_code stderr btl true;
+  debug "BTL Code:\n";
+  print_btl_code stderr btl;
+  debug "Scheduled BTL Code:\n";
+  print_btl_code stderr btl';
   (*debug_flag := false;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  ((btl, entry), dm)
+  ((btl', entry), dm)
-- 
cgit 


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/RTLtoBTLaux.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 056fe213..d04326ea 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -10,7 +10,7 @@ open BTLScheduleraux
 
 let encaps_final inst osucc =
   match inst with
-  | BF _ | Bcond _ -> inst
+  | BF _ -> inst
   | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ()))
 
 let translate_inst (iinfo : BTL.inst_info) inst is_final =
@@ -33,12 +33,13 @@ let translate_inst (iinfo : BTL.inst_info) inst is_final =
     | 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) ->
+        osucc := Some ifnot;
         iinfo.pcond <- info;
         Bcond
           ( cond,
             lr,
             BF (Bgoto ifso, def_iinfo ()),
-            BF (Bgoto ifnot, def_iinfo ()),
+            Bnop None,
             iinfo )
     | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo)
     | Ireturn oreg -> BF (Breturn oreg, iinfo)
-- 
cgit 


From 271f87ba08f42340900378c0797511d4071fc1b8 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 31 May 2021 16:55:18 +0200
Subject: BTL Scheduler oracle and some drafts

---
 scheduling/RTLtoBTLaux.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index d04326ea..e709d846 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -6,7 +6,6 @@ open RTLcommonaux
 open DebugPrint
 open BTLtypes
 open BTLcommonaux
-open BTLScheduleraux
 
 let encaps_final inst osucc =
   match inst with
@@ -102,19 +101,16 @@ let rtl2btl (f : RTL.coq_function) =
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   (* TODO gourdinl move elsewhere *)
-  let btl' = btl_scheduler btl in
   debug "Entry %d\n" (p2i entry);
   (*debug_flag := true;*)
   debug "RTL Code: ";
   print_code code;
   debug "BTL Code:\n";
   print_btl_code stderr btl;
-  debug "Scheduled BTL Code:\n";
-  print_btl_code stderr btl';
   (*debug_flag := false;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  ((btl', entry), dm)
+  ((btl, entry), dm)
-- 
cgit 


From 78fbb0e6f4c2065460a0ddb7e2e3ec94da21169f Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 31 May 2021 23:51:31 +0200
Subject: Dupmap bugfix and some advance in Livegen

---
 scheduling/RTLtoBTLaux.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index e709d846..3de82d96 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -101,8 +101,8 @@ let rtl2btl (f : RTL.coq_function) =
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   (* TODO gourdinl move elsewhere *)
-  debug "Entry %d\n" (p2i entry);
   (*debug_flag := true;*)
+  debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
   print_code code;
   debug "BTL Code:\n";
-- 
cgit 


From 056658bd2986d9e12ac07a54d25c08eb8a62ff60 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@lilo.org>
Date: Wed, 28 Jul 2021 10:32:09 +0200
Subject: remove todos, clean

---
 scheduling/RTLtoBTLaux.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 3de82d96..d544e87f 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -67,7 +67,6 @@ let translate_function code entry join_points liveness =
         | 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;
@@ -100,7 +99,6 @@ let rtl2btl (f : RTL.coq_function) =
   let liveness = analyze f in
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
-  (* TODO gourdinl move elsewhere *)
   (*debug_flag := true;*)
   debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
-- 
cgit