Moving common tools, adding liveness input/output information to BTL generation oracle

12 files changed, 73 insertions, 54 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index e8e60a4f..8ca6c6ab 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -23,7 +23,7 @@ open RTL
 open Maps
 open Camlcoq
 open DebugPrint
-open AuxTools
+open RTLcommonaux
 
 let stats_oc = ref None
 
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index df609505..82e4629f 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -17,7 +17,7 @@ open Kildall;;
 open HashedSet;;
 open Inject;;
 open DebugPrint;;
-open AuxTools;;
+open RTLcommonaux;;
 
 type reg = P.t;;
 
diff --git a/backend/AuxTools.ml b/backend/RTLcommonaux.ml
index 1e334524..2334dfee 100644
--- a/backend/AuxTools.ml
+++ b/backend/RTLcommonaux.ml
@@ -1,6 +1,9 @@
 open RTL
 open Maps
 open Camlcoq
+open Registers
+open Kildall
+open Lattice
 
 let p2i r = P.to_int r
 
@@ -50,3 +53,37 @@ let get_join_points code entry =
     | [pc] -> traverse pc
     | pc :: l -> traverse pc; traverse_succs l
   in traverse entry; !reached_twice
+
+let transfer f pc after = let open Liveness in
+  match PTree.get pc f.fn_code with
+  | Some i ->
+    (match i with
+    | Inop _ -> after
+    | Iop (_, args, res, _) ->
+        reg_list_live args (Regset.remove res after)
+    | Iload (_, _, _, args, dst, _) ->
+        reg_list_live args (Regset.remove dst after)
+    | Istore (_, _, args, src, _) ->
+        reg_list_live args (Regset.add src after)
+    | Icall (_, ros, args, res, _) ->
+        reg_list_live args (reg_sum_live ros (Regset.remove res after))
+    | Itailcall (_, ros, args) ->
+        reg_list_live args (reg_sum_live ros Regset.empty)
+    | Ibuiltin (_, args, res, _) ->
+        reg_list_live (AST.params_of_builtin_args args)
+          (reg_list_dead (AST.params_of_builtin_res res) after)
+    | Icond (_, args, _, _, _) ->
+        reg_list_live args after
+    | Ijumptable (arg, _) ->
+        Regset.add arg after
+    | Ireturn optarg ->
+        reg_option_live optarg Regset.empty)
+  | None -> Regset.empty
+
+module RegsetLat = LFSet(Regset)
+
+module DS = Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward)
+
+let analyze f =
+  let liveouts = get_some @@ DS.fixpoint f.fn_code successors_instr (transfer f) in
+  PTree.map (fun n _ -> let lo = PMap.get n liveouts in transfer f n lo) f.fn_code
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 021ea5c0..d94b31d8 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -1,7 +1,7 @@
 open Maps
 open Camlcoq
 open Registers
-open AuxTools
+open RTLcommonaux
 
 let debug_flag = ref false
 
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 735f5cf5..8a17217a 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -23,7 +23,7 @@ open Camlcoq
 open Option
 open AST
 open DebugPrint
-open AuxTools
+open RTLcommonaux
 
 (** Mini CSE (a dynamic numbering is applied during expansion. 
     The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)
diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml
index 863afdf0..e8758f61 100644
--- a/scheduling/BTLaux.ml
+++ b/scheduling/BTLaux.ml
@@ -1,3 +1,9 @@
+open Registers
+
 type inst_info = { mutable inumb : int; mutable pcond : bool option }
 
-type block_info = { mutable bnumb : int; mutable visited: bool }
+type block_info = {
+  mutable bnumb : int;
+  mutable visited : bool;
+  mutable output_regs : Regset.t;
+}
diff --git a/scheduling/BTLrenumber.ml b/scheduling/BTLrenumber.ml
index dd6baa89..f9cacd6a 100644
--- a/scheduling/BTLrenumber.ml
+++ b/scheduling/BTLrenumber.ml
@@ -1,7 +1,7 @@
 (* XXX uncomment
 open !BTL
 open DebugPrint
-open AuxTools
+open RTLcommonaux
 open Maps*)
 
 (** A quick note on the BTL renumber algorithm
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index 36d3e6a4..521f6ef2 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -2,7 +2,7 @@ open Maps
 open BTL
 open RTL
 open Camlcoq
-open AuxTools
+open RTLcommonaux
 open DebugPrint
 open BTLaux
 
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index 0ed3981d..502565c2 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -101,6 +101,8 @@ let print_btl_code pp btl is_rec =
     fprintf pp "\n";
     List.iter
       (fun (n, ibf) ->
+        fprintf pp "[BTL Liveness]\n";
+        print_regset ibf.input_regs;
         fprintf pp "[BTL block %d]\n" (P.to_int n);
         print_iblock pp is_rec "  " ibf.entry;
         fprintf pp "\n")
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index c9bb94d3..976ddc16 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -4,10 +4,8 @@ open Registers
 open Maps
 open Camlcoq
 open Datatypes
-open Kildall
-open Lattice
 open DebugPrint
-open AuxTools
+open RTLcommonaux
 
 let rec list_to_regset = function
   | [] -> Regset.empty
@@ -77,40 +75,6 @@ let get_path_map code entry join_points =
     !path_map
   end
 
-let transfer f pc after = let open Liveness in
-  match PTree.get pc f.fn_code with
-  | Some i ->
-    (match i with
-    | Inop _ -> after
-    | Iop (_, args, res, _) ->
-        reg_list_live args (Regset.remove res after)
-    | Iload (_, _, _, args, dst, _) ->
-        reg_list_live args (Regset.remove dst after)
-    | Istore (_, _, args, src, _) ->
-        reg_list_live args (Regset.add src after)
-    | Icall (_, ros, args, res, _) ->
-        reg_list_live args (reg_sum_live ros (Regset.remove res after))
-    | Itailcall (_, ros, args) ->
-        reg_list_live args (reg_sum_live ros Regset.empty)
-    | Ibuiltin (_, args, res, _) ->
-        reg_list_live (AST.params_of_builtin_args args)
-          (reg_list_dead (AST.params_of_builtin_res res) after)
-    | Icond (_, args, _, _, _) ->
-        reg_list_live args after
-    | Ijumptable (arg, _) ->
-        Regset.add arg after
-    | Ireturn optarg ->
-        reg_option_live optarg Regset.empty)
-  | None -> Regset.empty
-
-module RegsetLat = LFSet(Regset)
-
-module DS = Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward)
-
-let analyze f =
-  let liveouts = get_some @@ DS.fixpoint f.fn_code successors_instr (transfer f) in
-  PTree.map (fun n _ -> let lo = PMap.get n liveouts in transfer f n lo) f.fn_code
-
 (** OLD CODE - If needed to have our own kildall
 
 let transfer after = let open Liveness in function
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index 70a0c507..3db25d82 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -7,7 +7,7 @@ open RTL
 open Maps
 open Registers
 open ExpansionOracle
-open AuxTools
+open RTLcommonaux
 
 let config = Machine.config
 
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)