diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-15 13:08:57 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-15 13:08:57 +0100 |
commit | aa51677a82301a6c5d65717c6d9799bc8f8a0fea (patch) | |
tree | 48b0094c27b7ac2ffd5efa733ec7edfe47d5503e /scheduling | |
parent | 89c714ce7ef5d86517fa5da17e488b0f111814c3 (diff) | |
download | compcert-kvx-aa51677a82301a6c5d65717c6d9799bc8f8a0fea.tar.gz compcert-kvx-aa51677a82301a6c5d65717c6d9799bc8f8a0fea.zip |
This commit gives a first try to compute pre_output_regs from the livenesss oracle
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 29 |
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 |