diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-18 19:01:48 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-18 19:01:48 +0200 |
commit | a352cc3f9b9355e8b823750b9c4e5e1d37606dc4 (patch) | |
tree | 94304a3b52c66f9350f997760de6ce1d085f45de /backend | |
parent | 669612fc3165cd9898decb7ae5c70f9fb4ef327b (diff) | |
download | compcert-kvx-a352cc3f9b9355e8b823750b9c4e5e1d37606dc4.tar.gz compcert-kvx-a352cc3f9b9355e8b823750b9c4e5e1d37606dc4.zip |
dominated sets
Diffstat (limited to 'backend')
-rw-r--r-- | backend/LICMaux.ml | 34 |
1 files changed, 30 insertions, 4 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 52e5077f..66c1530e 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -57,14 +57,40 @@ let dominated_parts (f : coq_function) : PSet.t PTree.t = let (headers, dominated) = dominated_parts1 f in match dominated with - | None -> failwith "dominated_parts" + | None -> failwith "dominated_parts 1" | Some dominated -> - PTree.fold (fun before pc flag -> + let singletons = + PTree.fold (fun before pc flag -> if flag - then PTree.set pc PSet.empty before - else before) headers PTree.empty;; + then PTree.set pc (PSet.add pc PSet.empty) before + else before) headers PTree.empty in + PTree.fold (fun before pc ii -> + match PMap.get pc dominated with + | Dominator.Dominated x -> + let px = P.of_int x in + (match PTree.get px before with + | None -> failwith "dominated_parts 2" + | Some old -> + PTree.set px (PSet.add pc old) before) + | _ -> before) f.fn_code singletons;; + +let pp_pset oc s = + output_string oc "{ "; + let first = ref true in + List.iter (fun x -> + (if !first + then first := false + else output_string oc ", "); + Printf.printf "%d" x) + (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s))); + output_string oc " }";; let print_dominated_parts oc f = + List.iter (fun (header, nodes) -> + Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) + (PTree.elements (dominated_parts f));; + +let print_dominated_parts1 oc f = match snd (dominated_parts1 f) with | None -> output_string oc "error\n" | Some parts -> |