diff options
Diffstat (limited to 'backend/CSE3analysisaux.ml')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 143 |
1 files changed, 104 insertions, 39 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index e038331c..efe6b600 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -16,8 +16,15 @@ 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);; +type flattened_equation_or_condition = + | Flat_equ of int * sym_op * int list + | Flat_cond of Op.condition * int list;; + +let flatten_eq = function + | Equ(lhs, sop, args) -> + Flat_equ((P.to_int lhs), sop, (List.map P.to_int args)) + | Cond(cond, args) -> + Flat_cond(cond, (List.map P.to_int args));; let imp_add_i_j s i j = s := PMap.set i (PSet.add j (PMap.get i !s)) !s;; @@ -45,6 +52,9 @@ let print_eq channel (lhs, sop, args) = Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk) (PrintOp.print_addressing print_reg) (addr, args);; +let print_cond channel (cond, args) = + Printf.printf "cond %a" (PrintOp.print_condition print_reg) (cond, args);; + let pp_intset oc s = Printf.fprintf oc "{ "; List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s); @@ -58,9 +68,14 @@ let pp_rhs oc (sop, args) = (PrintAST.name_of_chunk chunk) (PrintOp.print_addressing PrintRTL.reg) (addr, args);; -let pp_eq oc eq = - Printf.fprintf oc "x%d = %a" (P.to_int eq.eq_lhs) - pp_rhs (eq.eq_op, eq.eq_args);; +let pp_eq oc eq_cond = + match eq_cond with + | Equ(lhs, sop, args) -> + Printf.fprintf oc "x%d = %a" (P.to_int lhs) + pp_rhs (sop, args) + | Cond(cond, args) -> + Printf.fprintf oc "cond %a" + (PrintOp.print_condition PrintRTL.reg) (cond, args);; let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x) @@ -68,8 +83,9 @@ let pp_option pp oc = function | None -> output_string oc "none" | Some x -> pp oc x;; -let is_trivial eq = - (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);; +let is_trivial = function + | Equ(lhs, (SOp Op.Omove), [lhs']) -> lhs=lhs' + | _ -> false;; let rec pp_list separator pp_item chan = function | [] -> () @@ -86,7 +102,11 @@ let pp_equation hints chan x = match PTree.get x hints.hint_eq_catalog with | None -> output_string chan "???" | Some eq -> - print_eq chan (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);; + match eq with + | Equ(lhs, sop, args) -> + print_eq chan (P.to_int lhs, sop, List.map P.to_int args) + | Cond(cond, args) -> + print_cond chan (cond, List.map P.to_int args);; let pp_relation hints chan rel = pp_set "; " (pp_equation hints) chan rel;; @@ -114,19 +134,47 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t = | None, _ | _, None -> None | (Some x'), (Some y') -> Some (RELATION.glb x' y');; +let compute_invariants + (nodes : RTL.node list) + (entrypoint : RTL.node) + (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list) = + let todo = ref IntSet.empty + and invariants = ref (PMap.set entrypoint (Some RELATION.top) (PMap.init RB.bot)) in + let add_todo (pc : RTL.node) = + todo := IntSet.add (P.to_int pc) !todo in + let update_node (pc : RTL.node) = + (if !Clflags.option_debug_compcert > 9 + then Printf.printf "UP updating node %d\n" (P.to_int pc)); + let cur = PMap.get pc !invariants in + List.iter (fun (next_pc, next_contrib) -> + let previous = PMap.get next_pc !invariants in + let next = RB.lub previous next_contrib in + if not (RB.beq previous next) + then ( + invariants := PMap.set next_pc next !invariants; + add_todo next_pc)) (tfr pc cur) in + add_todo entrypoint; + 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 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) = + (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list) + (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) = (if !Clflags.option_debug_compcert > 9 - then Printf.printf "updating node %d\n" (P.to_int pc)); + then Printf.printf "DOWN updating node %d\n" (P.to_int pc)); if not (peq pc entrypoint) then let cur = PMap.get pc !invariants in @@ -134,7 +182,7 @@ let refine_invariants (List.map (fun pred_pc-> rb_glb cur - (tfr pred_pc (PMap.get pred_pc !invariants))) + (List.assoc pc (tfr pred_pc (PMap.get pred_pc !invariants)))) (predecessors pc)) in if not (RB.beq cur nxt) then @@ -156,6 +204,12 @@ let get_default default x ptree = | None -> default | Some y -> y;; +let initial_analysis ctx tenv (f : RTL.coq_function) = + let tfr = apply_instr' ctx tenv f.RTL.fn_code in + compute_invariants + (List.map fst (PTree.elements f.RTL.fn_code)) + f.RTL.fn_entrypoint tfr;; + let refine_analysis ctx tenv (f : RTL.coq_function) (invariants0 : RB.t PMap.t) = let succ_map = RTL.successors_map f in @@ -166,6 +220,13 @@ let refine_analysis ctx tenv refine_invariants (List.map fst (PTree.elements f.RTL.fn_code)) f.RTL.fn_entrypoint succ_f pred_f tfr invariants0;; + +let add_to_set_in_table table key item = + Hashtbl.add table key + (PSet.add item + (match Hashtbl.find_opt table key with + | None -> PSet.empty + | Some s -> s));; let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let cur_eq_id = ref 0 @@ -179,7 +240,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"); + (* FIXME (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); @@ -194,7 +255,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = (P.to_int node) pp_rhs (sop, args) pp_intset o); o in let mutating_eq_find_oracle node eq : P.t option = - let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in + let flat_eq = flatten_eq eq in let o = match Hashtbl.find_opt eq_table flat_eq with | Some x -> @@ -207,21 +268,27 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = begin Hashtbl.add eq_table flat_eq coq_id; (cur_catalog := PTree.set coq_id eq !cur_catalog); - Hashtbl.add rhs_table (flat_eq_op, flat_eq_args) - (PSet.add coq_id - (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with - | None -> PSet.empty - | Some s -> s)); - List.iter - (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) - (eq.eq_lhs :: eq.eq_args); - (if eq_depends_on_mem eq + (match flat_eq with + | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) -> + add_to_set_in_table rhs_table + (flat_eq_op, flat_eq_args) coq_id + | Flat_cond(flat_eq_cond, flat_eq_args) -> ()); + (match eq with + | Equ(lhs, sop, args) -> + List.iter + (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) + (lhs :: args); + (match sop, args with + | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id + | _, _ -> ()) + | Cond(cond, args) -> + List.iter + (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args + ); + (if eq_cond_depends_on_mem eq then cur_kill_mem := PSet.add coq_id !cur_kill_mem); - (if eq_depends_on_store eq + (if eq_cond_depends_on_store eq then cur_kill_store := PSet.add coq_id !cur_kill_store); - (match eq.eq_op, eq.eq_args with - | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id - | _, _ -> ()); Some coq_id end in @@ -238,17 +305,15 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = eq_kill_store = (fun () -> !cur_kill_store); 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 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 + let invariants = initial_analysis ctx tenv f in + 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 ;; |