Merge branch 'mppa-RTLpathSE-oracle-outputregs' into mppa-RTLpathSE-oracle

3 files changed, 40 insertions, 10 deletions

diff --git a/kvx/lib/RTLpath.v b/kvx/lib/RTLpath.v
index 64f3917e..82991a4d 100644
--- a/kvx/lib/RTLpath.v
+++ b/kvx/lib/RTLpath.v
@@ -82,8 +82,11 @@ Definition early_exit (i: instruction): option node := (* FIXME: for jumptable,
 *)
 
 Record path_info := { 
-   psize: nat; (* number minus 1 of instructions in the path *)
-   input_regs: Regset.t 
+    psize: nat; (* number minus 1 of instructions in the path *)
+    input_regs: Regset.t;
+    (** Registers that are used (as input_regs) by the "fallthrough successors" of the path *)
+    (** This field is not used by the verificator, but is helpful for the superblock scheduler *)
+    output_regs: Regset.t 
 }.
 
 Definition path_map: Type := PTree.t path_info.
diff --git a/kvx/lib/RTLpathLivegenaux.ml b/kvx/lib/RTLpathLivegenaux.ml
index 09684f22..dd971db8 100644
--- a/kvx/lib/RTLpathLivegenaux.ml
+++ b/kvx/lib/RTLpathLivegenaux.ml
@@ -83,7 +83,7 @@ let get_join_points code entry =
     | pc :: l -> traverse pc; traverse_succs l
   in traverse entry; !reached_twice
 
-(* Does not set the input_regs field *)
+(* Does not set the input_regs and liveouts field *)
 let get_path_map code entry join_points =
   let visited = ref (PTree.map (fun n i -> false) code) in
   let path_map = ref PTree.empty in
@@ -104,7 +104,9 @@ let get_path_map code entry join_points =
                 path_successors := !path_successors @ non_predicted_successors inst;
                 dig_path_rec n'
               end
-          | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize); input_regs = Regset.empty }, !path_successors @ successors_inst inst)
+          | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);
+                            input_regs = Regset.empty; output_regs = Regset.empty },
+                        !path_successors @ successors_inst inst)
         end
       else None
     in match dig_path_rec e with
@@ -235,14 +237,32 @@ let analyze f =
   end
 *)
 
+let rec traverse code n size =
+  let inst = get_some @@ PTree.get n code in
+  if (size == 0) then inst
+  else 
+    let n' = get_some @@ predicted_successor inst in
+    traverse code n' (size-1)
+
+let get_outputs liveness code n pi =
+  let last_instruction = traverse code n (Camlcoq.Nat.to_int pi.psize) in
+  let path_last_successors = successors_inst last_instruction in
+  let list_input_regs = List.map (
+      fun n -> get_some @@ PTree.get n liveness
+    ) path_last_successors in
+  List.fold_left Regset.union Regset.empty list_input_regs
+
 let set_pathmap_liveness f pm =
   let liveness = analyze f in
   let new_pm = ref PTree.empty in
+  let code = f.fn_code in
   begin
     dprintf "Liveness: "; print_ptree_regset liveness; dprintf "\n";
     List.iter (fun (n, pi) ->
-      let rs = get_some @@ PTree.get n liveness in
-      new_pm := PTree.set n {psize=pi.psize; input_regs=rs} !new_pm
+      let inputs = get_some @@ PTree.get n liveness in
+      let outputs = get_outputs liveness code n pi in
+      new_pm := PTree.set n
+        {psize=pi.psize; input_regs=inputs; output_regs=outputs} !new_pm
     ) (PTree.elements pm);
     !new_pm
   end
@@ -259,6 +279,8 @@ let print_path_info pi = begin
   dprintf "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
   dprintf "input_regs=";
   print_regset pi.input_regs;
+  dprintf "; output_regs=";
+  print_regset pi.output_regs;
   dprintf ")"
 end
 
diff --git a/kvx/lib/RTLpathScheduleraux.ml b/kvx/lib/RTLpathScheduleraux.ml
index ad6f28b4..f332507c 100644
--- a/kvx/lib/RTLpathScheduleraux.ml
+++ b/kvx/lib/RTLpathScheduleraux.ml
@@ -10,6 +10,8 @@ type superblock = {
   (* each predicted Pcb has its attached liveins *)
   (* This is indexed by the pc value *)
   liveins: Regset.t PTree.t;
+  (* Union of the input_regs of the last successors *)
+  output_regs: Regset.t
 }
 
 let print_instructions insts code =
@@ -23,9 +25,11 @@ let print_instructions insts code =
 let print_superblock sb code =
   let insts = sb.instructions in
   let li = sb.liveins in
+  let outs = sb.output_regs in
   begin
     dprintf "{ instructions = "; print_instructions (Array.to_list insts) code; dprintf "\n";
-    dprintf "  liveins = "; print_ptree_regset li; dprintf "}"
+    dprintf "  liveins = "; print_ptree_regset li; dprintf "\n";
+    dprintf "  output_regs = "; print_regset outs; dprintf "}"
   end
 
 let print_superblocks lsb code =
@@ -81,9 +85,10 @@ let get_superblocks code entry pm =
     in if (get_some @@ PTree.get pc !visited) then []
     else begin
       visited := PTree.set pc true !visited;
-      let n = (get_some @@ PTree.get pc pm).psize in
-      let (insts, nexts) = follow pc (Camlcoq.Nat.to_int n) in
-      let superblock = { instructions = Array.of_list insts; liveins = !liveins } in
+      let pi = get_some @@ PTree.get pc pm in
+      let (insts, nexts) = follow pc (Camlcoq.Nat.to_int pi.psize) in
+      let superblock = { instructions = Array.of_list insts; liveins = !liveins;
+        output_regs = pi.output_regs } in
       superblock :: (List.concat @@ List.map get_superblocks_rec nexts)
     end
   in let lsb = get_superblocks_rec entry in begin