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