diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-07-08 15:30:09 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-07-08 15:30:24 +0200 |
commit | b67c28dd4dc6df5a5d3827f3a5827e437f3fcce4 (patch) | |
tree | f0f326e6cfb61b8c06c06857cb1532fb131c0b14 /kvx | |
parent | 5b1071d9f46bbb6083b1e6dd6f7975aaa64d0a9a (diff) | |
download | compcert-kvx-b67c28dd4dc6df5a5d3827f3a5827e437f3fcce4.tar.gz compcert-kvx-b67c28dd4dc6df5a5d3827f3a5827e437f3fcce4.zip |
Output regs in RTLpath
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/lib/RTLpath.v | 7 | ||||
-rw-r--r-- | kvx/lib/RTLpathLivegenaux.ml | 30 |
2 files changed, 31 insertions, 6 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..6875f155 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 |