From e6612fdfd69037099037def2acba5df553c3b49a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 31 Oct 2020 09:58:28 +0100 Subject: refining CSE3 nodes --- backend/CSE3analysisaux.ml | 95 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 81 insertions(+), 14 deletions(-) (limited to 'backend/CSE3analysisaux.ml') diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 8c83dc2e..6e190d35 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -14,7 +14,8 @@ open CSE3analysis open Maps open HashedSet open Camlcoq - +open Coqlib + let flatten_eq eq = ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);; @@ -98,10 +99,72 @@ let pp_results f (invariants : RB.t PMap.t) hints chan = let max_pc = P.to_int (RTL.max_pc_function f) in for pc=max_pc downto 1 do - Printf.fprintf chan "%d: %a\n" pc + Printf.fprintf chan "%d: %a\n\n" pc (pp_relation_b hints) (PMap.get (P.of_int pc) invariants) done +module IntSet=Set.Make(struct type t=int let compare = ( - ) end);; + +let rec union_list prev = function + | [] -> prev + | h::t -> union_list (RB.lub prev h) t;; + +let rb_glb (x : RB.t) (y : RB.t) : RB.t = + match x, y with + | None, _ | _, None -> None + | (Some x'), (Some y') -> Some (RELATION.glb x' y');; + +let refine_invariants + (nodes : RTL.node list) + (entrypoint : RTL.node) + (successors : RTL.node -> RTL.node list) + (predecessors : RTL.node -> RTL.node list) + (tfr : RTL.node -> RB.t -> RB.t) (invariants0 : RB.t PMap.t) = + let todo = ref IntSet.empty + and invariants = ref invariants0 in + let add_todo (pc : RTL.node) = + todo := IntSet.add (P.to_int pc) !todo in + let update_node (pc : RTL.node) = + Printf.printf "updating node %d\n" (P.to_int pc); + if not (peq pc entrypoint) + then + let cur = PMap.get pc !invariants in + let nxt = union_list RB.bot + (List.map + (fun pred_pc-> + rb_glb cur + (tfr pred_pc (PMap.get pred_pc !invariants))) + (predecessors pc)) in + if not (RB.beq cur nxt) + then + begin + Printf.printf "refining CSE3 node %d\n" (P.to_int pc); + List.iter add_todo (successors pc) + end in + (List.iter add_todo nodes); + while not (IntSet.is_empty !todo) do + let nxt = IntSet.max_elt !todo in + todo := IntSet.remove nxt !todo; + update_node (P.of_int nxt) + done; + !invariants;; + +let get_default default x ptree = + match PTree.get x ptree with + | None -> default + | Some y -> y;; + +let refine_analysis ctx tenv + (f : RTL.coq_function) (invariants0 : RB.t PMap.t) = + let succ_map = RTL.successors_map f in + let succ_f x = get_default [] x succ_map in + let pred_map = Kildall.make_predecessors f.RTL.fn_code RTL.successors_instr in + let pred_f x = get_default [] x pred_map in + let tfr = apply_instr' ctx tenv f.RTL.fn_code in + refine_invariants + (List.map fst (PTree.elements f.RTL.fn_code)) + f.RTL.fn_entrypoint succ_f pred_f tfr invariants0;; + let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 and cur_catalog = ref PTree.empty @@ -113,6 +176,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let eq_find_oracle node eq = assert (not (is_trivial eq)); let o = Hashtbl.find_opt eq_table (flatten_eq eq) in + (if o = None then failwith "eq_find_oracle"); (if !Clflags.option_debug_compcert > 5 then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node) pp_eq eq (pp_option pp_P) o); @@ -161,21 +225,24 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = pp_eq eq (pp_option pp_P) o); o in - match - internal_analysis - { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); - eq_find_oracle = mutating_eq_find_oracle; - eq_rhs_oracle = rhs_find_oracle ; - eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); - eq_kill_mem = (fun () -> !cur_kill_mem); - eq_moves = (fun reg -> PMap.get reg !cur_moves) - } tenv f + let ctx = { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); + eq_find_oracle = mutating_eq_find_oracle; + eq_rhs_oracle = rhs_find_oracle ; + eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); + eq_kill_mem = (fun () -> !cur_kill_mem); + eq_moves = (fun reg -> PMap.get reg !cur_moves) + } in + match internal_analysis ctx tenv f with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3" | Some invariants -> - let hints = { hint_eq_catalog = !cur_catalog; + let invariants' = + if ! Clflags.option_fcse3_refine + then refine_analysis ctx tenv f invariants + else invariants + and hints = { hint_eq_catalog = !cur_catalog; hint_eq_find_oracle= eq_find_oracle; hint_eq_rhs_oracle = rhs_find_oracle } in (if !Clflags.option_debug_compcert > 1 - then pp_results f invariants hints stdout); - invariants, hints + then pp_results f invariants' hints stdout); + invariants', hints ;; -- cgit