From ac872f4bb59fec4a4c43d5ae39b26a11c82178ee Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Fri, 8 Jun 2018 13:10:11 -0700 Subject: [PATCH] Building MinTrees with equivalence relation Reviewed By: mbouaziz Differential Revision: D8286589 fbshipit-source-id: a804bbb --- infer/src/checkers/cost.ml | 112 ++++++++++++++++++++++++++-------- infer/src/istd/IContainer.ml | 10 --- infer/src/istd/IContainer.mli | 5 -- 3 files changed, 86 insertions(+), 41 deletions(-) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 50344ead6..e03029dae 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -233,6 +233,11 @@ module ControlFlowCost = struct let normalize ~(normalizer: t -> [> t]) (x: t) : t = match normalizer x with #t as x -> x | _ -> assert false + + + let is_node i = match i with `Node nid -> Some nid | _ -> None + + let of_node i = `Node i end module Sum = struct @@ -281,6 +286,8 @@ module ControlFlowCost = struct type t = [Item.t | Sum.t] + let is_node i = match i with `Node nid -> Some nid | _ -> None + let compare : t -> t -> int = fun x y -> match (x, y) with @@ -500,6 +507,8 @@ struct let pp_equalities fmt t = H.pp_bindings Repr.pp Set.pp_equalities fmt t + let fold_equalities t ~init ~f = H.fold t ~init ~f + let normalize_sums ~normalizer t = H.iter (fun _repr set -> Set.normalize_sums ~normalizer set) t @@ -565,6 +574,8 @@ struct let pp_equalities fmt t = Sets.pp_equalities fmt t.sets + let fold_equalities t ~init ~f = Sets.fold_equalities t.sets ~init ~f + let normalizer t = Reprs.normalizer t.reprs let normalize_sums t = Sets.normalize_sums ~normalizer:(normalizer t) t.sets @@ -794,6 +805,7 @@ module MinTree = struct let branch = List.fold_left ~f:(fun branch set_addend -> + assert (Node.IdSet.cardinal set_addend >= 2) ; if Node.IdSet.is_empty (Node.IdSet.inter set_addend visited_acc') then SetOfSetsOfNodes.add set_addend branch else branch ) @@ -804,11 +816,9 @@ module MinTree = struct let node, branch, visited_res = build_min (Min []) SetOfSetsOfNodes.empty visited [q] in SetOfSetsOfNodes.fold (fun addend i_node -> - if Node.IdSet.cardinal addend < 2 then assert false - else ( - L.(debug Analysis Medium) "@\n\n|Set addends| = %i {" (Node.IdSet.cardinal addend) ; - Node.IdSet.iter (fun e -> L.(debug Analysis Medium) " %a, " Node.pp_id e) addend ; - L.(debug Analysis Medium) " }@\n " ) ; + L.(debug Analysis Medium) "@\n\n|Set addends| = %i {" (Node.IdSet.cardinal addend) ; + Node.IdSet.iter (fun e -> L.(debug Analysis Medium) " %a, " Node.pp_id e) addend ; + L.(debug Analysis Medium) " }@\n " ; let plus_node = Node.IdSet.fold (fun n acc -> @@ -836,29 +846,68 @@ module MinTree = struct Staged.stage f_with_cache + let find_tree_eq_rel n trees representative_map = + match Node.IdMap.find_opt n representative_map with + | Some representative -> ( + match Node.IdMap.find_opt representative trees with + | Some t -> + t + | _ -> + L.(die InternalError) "@\n Equivalent tree not found. Stop.@\n" ) + | _ -> + L.(die InternalError) + "@\n Equivalence-class representative for %a not found. Stop.@\n" Node.pp_id n + + + (* update map where every element of an equivalence class map to its representative *) + let update_representative_map (acc_representative: Node.id Node.IdMap.t) + ({items}: ControlFlowCost.Set.t) (rep: Node.id) = + ARList.fold_left items ~init:acc_representative ~f:(fun acc it -> + match ControlFlowCost.Item.is_node it with Some k -> Node.IdMap.add k rep acc | _ -> acc ) + + let compute_trees_from_contraints bound_map node_cfg constraints = + let start_node = Node.id (NodeCFG.start_node node_cfg) in + let start_node_item = ControlFlowCost.Item.of_node start_node in + let eqs = ConstraintSolver.collect_constraints node_cfg in + let start_node_reprs = ConstraintSolver.Equalities.Reprs.find eqs.reprs start_node_item in + L.(debug Analysis Verbose) "@\n =========== Computed Equalities ==========@\n" ; + L.(debug Analysis Verbose) "[Equalities] %a@\n" ConstraintSolver.Equalities.pp_equalities eqs ; let minimum_propagation = with_cache (minimum_propagation bound_map constraints) |> Staged.unstage in - let min_trees = - NodeCFG.fold_nodes node_cfg - ~f:(fun acc node -> - let nid = Node.id node in - let tree = minimum_propagation (nid, Node.IdSet.empty) in - (nid, tree) :: acc ) - ~init:[] + let min_trees, representative_map = + ConstraintSolver.Equalities.fold_equalities eqs ~init:(Node.IdMap.empty, Node.IdMap.empty) + ~f:(fun (acc_trees, acc_representative) (rep, eq_cl) -> + let rep_id = + match ControlFlowCost.is_node (rep :> ControlFlowCost.t) with + | Some nid -> + nid + | _ -> + assert false + in + let acc_representative' = update_representative_map acc_representative eq_cl rep_id in + let tree = + if ConstraintSolver.Equalities.Repr.equal start_node_reprs rep then + (* for any node in the same equivalence class as the start node we give the trivial MinTree: + min(1) + *) + add_leaf (Min []) rep_id (BoundMap.upperbound bound_map rep_id) + else minimum_propagation (rep_id, Node.IdSet.empty) + in + (Node.IdMap.add rep_id tree acc_trees, acc_representative') ) in - List.iter - ~f:(fun (nid, t) -> L.(debug Analysis Medium) "@\n node %a = %a @\n" Node.pp_id nid pp t) + Node.IdMap.iter + (fun nid t -> L.(debug Analysis Medium) "@\n node %a = %a @\n" Node.pp_id nid pp t) min_trees ; - min_trees + (min_trees, representative_map) end module ReportedOnNodes = AbstractDomain.FiniteSetOfPPSet (Node.IdSet) type extras_TransferFunctionsWCET = { basic_cost_map: AnalyzerNodesBasicCost.invariant_map - ; min_trees_map: BasicCost.astate Node.IdMap.t + ; min_trees_map: BasicCost.astate Node.IdMap.t * Node.id Node.IdMap.t ; summary: Summary.t } (* Calculate the final Worst Case Execution Time predicted for each node. @@ -911,10 +960,16 @@ module TransferFunctionsWCET = struct preds - let map_cost trees m : BasicCost.astate = + let map_cost (trees, representative_map) m : BasicCost.astate = CostDomain.NodeInstructionToCostMap.fold (fun ((node_id, _) as instr_node_id) c acc -> - let t = Node.IdMap.find node_id trees in + let t = + match Node.IdMap.find_opt node_id trees with + | Some t' -> + t' + | None -> + MinTree.find_tree_eq_rel node_id trees representative_map + in let c_node = BasicCost.mult c t in let c_node' = BasicCost.plus acc c_node in L.(debug Analysis Medium) @@ -1003,31 +1058,36 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = let bound_map = BoundMap.compute_upperbound_map node_cfg inferbo_invariant_map control_dep_invariant_map in - let _ = ConstraintSolver.collect_constraints node_cfg in let constraints = StructuralConstraints.compute_structural_constraints node_cfg in - let min_trees = MinTree.compute_trees_from_contraints bound_map node_cfg constraints in + let min_trees, representative_map = + MinTree.compute_trees_from_contraints bound_map node_cfg constraints + in let trees_valuation = - List.fold - ~f:(fun acc (nid, t) -> + Node.IdMap.fold + (fun nid t acc -> let res = MinTree.evaluate_tree t in L.(debug Analysis Medium) "@\n Tree %a eval to %a @\n" Node.pp_id nid BasicCost.pp res ; Node.IdMap.add nid res acc ) - ~init:Node.IdMap.empty min_trees + min_trees Node.IdMap.empty in let initWCET = (BasicCost.zero, ReportedOnNodes.empty) in match AnalyzerWCET.compute_post (ProcData.make proc_desc tenv - {basic_cost_map= invariant_map_NodesBasicCost; min_trees_map= trees_valuation; summary}) + { basic_cost_map= invariant_map_NodesBasicCost + ; min_trees_map= (trees_valuation, representative_map) + ; summary }) ~debug:true ~initial:initWCET with | Some (exit_cost, _) -> L.internal_error - "@\n[COST ANALYSIS] PROCESSING MIN_TREE for PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" + "@\n\ + [COST ANALYSIS] PROCESSING MIN_TREE for PROCEDURE '%a' |CFG| = %i |Trees|=%i FINAL COST \ + = %a @\n" Typ.Procname.pp (Procdesc.get_proc_name proc_desc) (Container.length ~fold:NodeCFG.fold_nodes node_cfg) - BasicCost.pp exit_cost ; + (Node.IdMap.cardinal min_trees) BasicCost.pp exit_cost ; check_and_report_infinity exit_cost proc_desc summary ; Payload.update_summary {post= exit_cost} summary | None -> diff --git a/infer/src/istd/IContainer.ml b/infer/src/istd/IContainer.ml index 79d5d67e0..b207f13b7 100644 --- a/infer/src/istd/IContainer.ml +++ b/infer/src/istd/IContainer.ml @@ -58,13 +58,3 @@ let pp_collection ~fold ~pp_item fmt c = in let pp_aux fmt c = fold c ~init:None ~f |> Option.iter ~f:(F.fprintf fmt "@[%a@] " pp_item) in F.fprintf fmt "@[{ %a}@]" pp_aux c - - -let pp_seq ~fold ~sep pp_item fmt c = - let f first item = - if not first then F.pp_print_string fmt sep ; - pp_item fmt item ; - false - in - let _is_empty : bool = fold c ~init:true ~f in - () diff --git a/infer/src/istd/IContainer.mli b/infer/src/istd/IContainer.mli index f42bbafe2..25f39876c 100644 --- a/infer/src/istd/IContainer.mli +++ b/infer/src/istd/IContainer.mli @@ -32,8 +32,3 @@ val iter_consecutive : val pp_collection : fold:('t, 'a, 'a option) Container.fold -> pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 't -> unit - -val pp_seq : - fold:('t, 'a, bool) Container.fold -> sep:string -> (F.formatter -> 'a -> unit) -> F.formatter - -> 't -> unit - [@@warning "-32"]