Commit aa51677a authored by Léo Gourdin's avatar Léo Gourdin
Browse files

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

parent 89c714ce
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment