From 2efb64e96105c90f68f22a0a0bc386d1ac039354 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 22:00:49 +0200 Subject: compute inner loops --- backend/LICMaux.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'backend/LICMaux.ml') diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 269d9353..ecc11a00 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -52,7 +52,6 @@ let dominated_parts1 (f : coq_function) : Dominator.top in (headers, dominated);; -(* unfinished *) let dominated_parts (f : coq_function) : PSet.t PTree.t = let (headers, dominated) = dominated_parts1 f in match dominated with @@ -103,6 +102,11 @@ let filter_dominated_part (predecessors : P.t list PTree.t) then f x) l );; +let inner_loops (f : coq_function) : PSet.t PTree.t = + let parts = dominated_parts f + and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in + PTree.map (filter_dominated_part predecessors) parts;; + let pp_pset oc s = output_string oc "{ "; let first = ref true in @@ -119,6 +123,11 @@ let print_dominated_parts oc f = Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) (PTree.elements (dominated_parts f));; +let print_inner_loops oc f = + List.iter (fun (header, nodes) -> + Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) + (PTree.elements (inner_loops f));; + let print_dominated_parts1 oc f = match snd (dominated_parts1 f) with | None -> output_string oc "error\n" @@ -142,7 +151,7 @@ let print_loop_headers f = let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): (Inject.inj_instr list) PTree.t = - let _ = print_dominated_parts stdout f in + let _ = print_inner_loops stdout f in PTree.empty;; (* let max_reg = P.to_int coq_max_reg in -- cgit