diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-18 11:29:18 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-18 11:29:18 +0200 |
| commit | 871643ce4897ba645d922812a3fb546bdb2f48a4 (patch) | |
| tree | 96df9e5683469b51b9b0c8d8c7f465deae892fb7 /backend/LICMaux.ml | |
| parent | 967dbc3b939784ef3246bb5e931a62da26cf51a9 (diff) | |
| download | compcert-kvx-871643ce4897ba645d922812a3fb546bdb2f48a4.tar.gz compcert-kvx-871643ce4897ba645d922812a3fb546bdb2f48a4.zip | |
headers vs dominators
Diffstat (limited to 'backend/LICMaux.ml')
| -rw-r--r-- | backend/LICMaux.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 82cd74a2..e236b173 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -41,16 +41,18 @@ let apply_dominator (is_marked : node -> bool) (pc : node) then Dominator.Dominated (P.to_int pc) else before;; -let dominated_parts (f : coq_function) : Dominator.t PMap.t option = +let dominated_parts (f : coq_function) : + (bool PTree.t) * (Dominator.t PMap.t option) = let headers = Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint in - Dominator_Solver.fixpoint f.fn_code RTL.successors_instr + let dominated = Dominator_Solver.fixpoint f.fn_code RTL.successors_instr (apply_dominator (fun pc -> match PTree.get pc headers with | Some x -> x | None -> false)) f.fn_entrypoint - Dominator.top;; + Dominator.top in + (headers, dominated);; let print_dominated_parts oc f = - match dominated_parts f with + match snd (dominated_parts f) with | None -> output_string oc "error\n" | Some parts -> List.iter |