This commit gives a first try to compute pre_output_regs from the livenesss oracle

1 files changed, 19 insertions, 10 deletions

diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index 3d14a393..db3fc9d4 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -217,41 +217,50 @@ let analyze f =
 
 let rec traverse code n size =
   let inst = get_some @@ PTree.get n code in
-  if (size == 0) then inst
+  if (size == 0) then (inst, n)
   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 get_outputs liveness f n pi =
+  let (last_instruction, pc_last) = traverse f.fn_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 outputs = List.fold_left Regset.union Regset.empty list_input_regs in
+
+  match last_instruction with
+  | Icall (_, _, _, _, _) | Itailcall (_, _, _)
+  | Ibuiltin (_, _, _, _) | Ijumptable (_, _)
+  | Ireturn _ -> ((transfer f pc_last outputs), outputs)
+  | _ -> (outputs, outputs)
 
 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
     debug "Liveness: "; print_ptree_regset liveness; debug "\n";
     List.iter (fun (n, pi) ->
       let inputs = get_some @@ PTree.get n liveness in
-      let outputs = get_outputs liveness code n pi in
+      let (por, outputs) = get_outputs liveness f n pi in
       new_pm := PTree.set n
-                  {psize=pi.psize; input_regs=inputs; pre_output_regs=outputs; output_regs=outputs} !new_pm (* FIXME: STUB *)
+                  {psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm (* FIXME: STUB *)
     ) (PTree.elements pm);
     !new_pm
   end
 
 let print_path_info pi = begin
+  (*debug_flag := true;*)
   debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
-  debug "input_regs=";
+  debug "\ninput_regs=";
   print_regset pi.input_regs;
-  debug "; output_regs=";
+  debug "\n; pre_output_regs=";
+  print_regset pi.pre_output_regs;
+  debug "\n; output_regs=";
   print_regset pi.output_regs;
-  debug ")"
+  debug ")\n"
+  (*debug_flag := false*)
 end
 
 let print_path_map path_map = begin