From 5b6430e739a379be6786f926db680a8b1c064b96 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 12 Jun 2018 07:01:58 -0700 Subject: [PATCH] Cost solver Reviewed By: ddino Differential Revision: D8348319 fbshipit-source-id: 9274da6 --- infer/src/bufferoverrun/itv.ml | 10 +- infer/src/checkers/cost.ml | 252 ++++++++++++++---- infer/src/istd/ImperativeUnionFind.ml | 10 +- infer/src/istd/ImperativeUnionFind.mli | 4 + .../java/performance/EvilCfg.java | 35 +++ .../codetoanalyze/java/performance/issues.exp | 1 + 6 files changed, 253 insertions(+), 59 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/performance/EvilCfg.java diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5cea7d2d0..9520b57e9 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -1144,7 +1144,9 @@ module MakePolynomial (S : NonNegativeSymbol) = struct (* assumes symbols are not comparable *) let rec ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs ~rhs -> - NonNegativeInt.( <= ) ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:( <= ) lhs.terms rhs.terms + phys_equal lhs rhs + || NonNegativeInt.( <= ) ~lhs:lhs.const ~rhs:rhs.const + && M.le ~le_elt:( <= ) lhs.terms rhs.terms let rec xcompare ~lhs ~rhs = @@ -1158,8 +1160,10 @@ module MakePolynomial (S : NonNegativeSymbol) = struct (* Possible optimization for later: x join x^2 = x^2 instead of x + x^2 *) let rec join : t -> t -> t = fun p1 p2 -> - { const= NonNegativeInt.max p1.const p2.const - ; terms= M.increasing_union ~f:join p1.terms p2.terms } + if phys_equal p1 p2 then p1 + else + { const= NonNegativeInt.max p1.const p2.const + ; terms= M.increasing_union ~f:join p1.terms p2.terms } (* assumes symbols are not comparable *) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 83d79b391..aca630485 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -23,6 +23,8 @@ end) Currently it's set randomly to 200. *) let expensive_threshold = BasicCost.of_int_exn 200 +let solver = `ConstraintSolver + (* CFG modules used in several other modules *) module InstrCFG = ProcCfg.NormalOneInstrPerNode module NodeCFG = ProcCfg.Normal @@ -280,10 +282,16 @@ module ControlFlowCost = struct Some (e :> [Item.t | t]) | Some l -> Some (`Sum (len - 1, l)) + + + let cost ~of_item (`Sum (_, l)) = + List.fold l ~init:BasicCost.zero ~f:(fun cost item -> BasicCost.plus cost (of_item item)) end type t = [Item.t | Sum.t] + let is_node = function `Node nid -> Some nid | _ -> None + let assert_node = function `Node nid -> nid | _ -> assert false let compare : t -> t -> int = @@ -314,7 +322,11 @@ module ControlFlowCost = struct module Set = struct type elt = t [@@deriving compare] - type t = {mutable size: int; mutable items: Item.t ARList.t; mutable sums: Sum.t ARList.t} + type t = + { mutable size: int + ; mutable items: Item.t ARList.t + ; mutable sums: Sum.t ARList.t + ; mutable cost: BasicCost.astate } let create e = let items, sums = @@ -324,7 +336,7 @@ module ControlFlowCost = struct | #Sum.t as sum -> (ARList.empty, ARList.singleton sum) in - {size= 1; items; sums} + {size= 1; items; sums; cost= BasicCost.top} let compare_size {size= size1} {size= size2} = Int.compare size1 size2 @@ -332,6 +344,8 @@ module ControlFlowCost = struct (* Invalidation is just a sanity check, union-find already takes care of it. *) let is_valid {size} = size >= 1 + let cost {cost} = cost + (* move semantics, should not be called with aliases *) let merge ~from ~to_ = assert (not (phys_equal from to_)) ; @@ -364,22 +378,54 @@ module ControlFlowCost = struct |> IContainer.iter_consecutive ~fold:List.fold ~f:on_infer + let sum_items t = + t.sums + |> ARList.fold_unordered ~init:ARList.empty ~f:(fun acc sum -> + sum |> Sum.items |> ARList.of_list |> ARList.append acc ) + |> IContainer.to_rev_list ~fold:ARList.fold_unordered + |> List.dedup_and_sort ~compare:Item.compare + + let infer_equalities_from_sums : on_infer:(elt -> elt -> unit) -> normalizer:(elt -> elt) -> t -> unit = fun ~on_infer ~normalizer t -> normalize_sums ~normalizer t ; - let all_items = - t.sums - |> ARList.fold_unordered ~init:ARList.empty ~f:(fun acc sum -> - sum |> Sum.items |> ARList.of_list |> ARList.append acc ) - |> IContainer.to_rev_list ~fold:ARList.fold_unordered - |> List.dedup_and_sort ~compare:Item.compare - in (* Keep in mind that [on_infer] can modify [t]. It happens only if we merge a node while infering equalities from it, i.e. in the case an item appears in an equality class both alone and in two sums, i.e. X = A + X = A + B. This is not a problem here (we could stop if it happens but it is not necessary as existing equalities still remain true after merges) *) (* Also keep in mind that the current version, in the worst-case scenario, is quadratic-ish in the size of the CFG *) - List.iter all_items ~f:(fun item -> infer_equalities_by_removing_item ~on_infer t item) + sum_items t |> List.iter ~f:(fun item -> infer_equalities_by_removing_item ~on_infer t item) + + + let init_cost : of_node:(Node.id -> BasicCost.astate) -> t -> unit = + fun ~of_node t -> + let min_if_node cost item = + match item with `Node node -> BasicCost.min_default_left cost (of_node node) | _ -> cost + in + t.cost <- ARList.fold_unordered t.items ~init:t.cost ~f:min_if_node + + + let improve_cost_from_sums + : on_improve:(Sum.t -> BasicCost.astate -> BasicCost.astate -> unit) + -> of_item:(Item.t -> BasicCost.astate) -> t -> unit = + fun ~on_improve ~of_item t -> + let f sum = + let cost_of_sum = Sum.cost ~of_item sum in + let new_cost = BasicCost.min_default_left t.cost cost_of_sum in + if not (BasicCost.( <= ) ~lhs:t.cost ~rhs:new_cost) then ( + on_improve sum cost_of_sum new_cost ; + t.cost <- new_cost ) + in + Container.iter t.sums ~fold:ARList.fold_unordered ~f + + + let improve_cost_with t cost' = + let old_cost = t.cost in + let new_cost = BasicCost.min_default_left old_cost cost' in + if not (BasicCost.( <= ) ~lhs:old_cost ~rhs:new_cost) then ( + t.cost <- new_cost ; + Some old_cost ) + else None end end @@ -398,6 +444,13 @@ module ConstraintSolver = struct IContainer.pp_collection ~fold:fold_sets ~pp_item fmt equalities + let pp_costs fmt equalities = + let pp_item fmt (repr, set) = + F.fprintf fmt "%a --> %a" pp_repr repr BasicCost.pp (ControlFlowCost.Set.cost set) + in + IContainer.pp_collection ~fold:fold_sets ~pp_item fmt equalities + + let log_union equalities e1 e2 = match union equalities e1 e2 with | None -> @@ -410,6 +463,26 @@ module ConstraintSolver = struct true + let try_to_improve ~on_improve ~f equalities ~max = + let f did_improve repr_set = + if did_improve then ( + f ~did_improve:(fun () -> ()) repr_set ; + true ) + else + let did_improve = ref false in + f ~did_improve:(fun () -> did_improve := true) repr_set ; + !did_improve + in + let rec loop max = + if fold_sets equalities ~init:false ~f then ( + on_improve () ; + if max > 0 then loop (max - 1) + else + L.(debug Analysis Verbose) "[ConstraintSolver] Maximum number of iterations reached@\n" ) + in + loop max + + (** Infer equalities from sums, like this: (1) A + sum1 = A + sum2 => sum1 = sum2 @@ -424,20 +497,14 @@ module ConstraintSolver = struct *) let infer_equalities_from_sums equalities ~max = let normalizer = normalizer equalities in - let f did_infer (_repr, set) = - let did_infer = ref did_infer in - let on_infer e1 e2 = if log_union equalities e1 e2 then did_infer := true in - ControlFlowCost.Set.infer_equalities_from_sums ~on_infer ~normalizer set ; - !did_infer + let f ~did_improve (_repr, set) = + let on_infer e1 e2 = if log_union equalities e1 e2 then did_improve () in + ControlFlowCost.Set.infer_equalities_from_sums ~on_infer ~normalizer set in - let rec loop max = - if fold_sets equalities ~init:false ~f then ( - L.(debug Analysis Verbose) "[ConstraintSolver] %a@\n" pp_equalities equalities ; - if max > 0 then loop (max - 1) - else - L.(debug Analysis Verbose) "[ConstraintSolver] Maximum number of iterations reached@\n" ) + let on_improve () = + L.(debug Analysis Verbose) "[ConstraintSolver][EInfe] %a@\n" pp_equalities equalities in - loop max + try_to_improve ~on_improve ~f equalities ~max let normalize_sums equalities = @@ -449,6 +516,55 @@ module ConstraintSolver = struct let union equalities e1 e2 = let _ : bool = log_union equalities e1 e2 in () + + + let init_costs bound_map equalities = + let of_node node_id = BoundMap.upperbound bound_map node_id in + Container.iter equalities ~fold:fold_sets ~f:(fun (_repr, set) -> + ControlFlowCost.Set.init_cost ~of_node set ) + + + (** + From sums: if A = B + C, do cost(A) = min(cost(A), cost(B) + cost(C)) + From inequalities: if A = B + C, then B <= A, do cost(B) = min(cost(B), cost(A)) + *) + let improve_costs equalities ~max = + let of_item (item: ControlFlowCost.Item.t) = + (item :> ControlFlowCost.t) |> find equalities |> find_set equalities + |> Option.value_map ~f:ControlFlowCost.Set.cost ~default:BasicCost.top + in + let f ~did_improve (repr, set) = + let on_improve sum cost_of_sum new_cost = + L.(debug Analysis Verbose) + "[ConstraintSolver][CImpr] Improved cost of %a using %a (cost: %a), from %a to %a@\n" + pp_repr repr ControlFlowCost.Sum.pp sum BasicCost.pp cost_of_sum BasicCost.pp + (ControlFlowCost.Set.cost set) BasicCost.pp new_cost ; + did_improve () + in + ControlFlowCost.Set.improve_cost_from_sums ~on_improve ~of_item set ; + let try_from_inequality (sum_item: ControlFlowCost.Item.t) = + let sum_item_set = + (sum_item :> ControlFlowCost.t) |> find equalities |> find_create_set equalities + in + match + ControlFlowCost.Set.improve_cost_with sum_item_set (ControlFlowCost.Set.cost set) + with + | Some previous_cost -> + L.(debug Analysis Verbose) + "[ConstraintSolver][CImpr] Improved cost of %a <= %a (cost: %a), from %a to %a@\n" + ControlFlowCost.Item.pp sum_item pp_repr repr BasicCost.pp + (ControlFlowCost.Set.cost set) BasicCost.pp previous_cost BasicCost.pp + (ControlFlowCost.Set.cost sum_item_set) ; + did_improve () + | None -> + () + in + ControlFlowCost.Set.sum_items set |> List.iter ~f:try_from_inequality + in + let on_improve () = + L.(debug Analysis Verbose) "[ConstraintSolver][CImpr] %a@\n" pp_costs equalities + in + try_to_improve ~on_improve ~f equalities ~max end let add_constraints equalities node get_nodes make = @@ -474,12 +590,30 @@ module ConstraintSolver = struct L.(debug Analysis Verbose) "[ConstraintSolver] Procedure %a @@ %a@\n" Typ.Procname.pp (Procdesc.get_proc_name node_cfg) Location.pp_file_pos (Procdesc.get_loc node_cfg) ; - L.(debug Analysis Verbose) "[ConstraintSolver] %a@\n" Equalities.pp_equalities equalities ; + L.(debug Analysis Verbose) + "[ConstraintSolver][EInit] %a@\n" Equalities.pp_equalities equalities ; Equalities.normalize_sums equalities ; - L.(debug Analysis Verbose) "[ConstraintSolver] %a@\n" Equalities.pp_equalities equalities ; + L.(debug Analysis Verbose) + "[ConstraintSolver][ENorm] %a@\n" Equalities.pp_equalities equalities ; Equalities.infer_equalities_from_sums equalities ~max:10 ; - L.(debug Analysis Verbose) "[ConstraintSolver] %a@\n" Equalities.pp_equalities equalities ; + L.(debug Analysis Verbose) + "[ConstraintSolver][EInfe] %a@\n" Equalities.pp_equalities equalities ; equalities + + + let compute_costs bound_map equalities = + Equalities.init_costs bound_map equalities ; + L.(debug Analysis Verbose) "[ConstraintSolver][CInit] %a@\n" Equalities.pp_costs equalities ; + Equalities.improve_costs equalities ~max:10 ; + L.(debug Analysis Verbose) "[ConstraintSolver][CImpr] %a@\n" Equalities.pp_costs equalities + + + let get_node_nb_exec equalities node_id = + let set = + node_id |> ControlFlowCost.make_node |> Equalities.find equalities + |> Equalities.find_set equalities + in + Option.value_exn set |> ControlFlowCost.Set.cost end (* Structural Constraints are expressions of the kind: @@ -704,16 +838,19 @@ module MinTree = struct let min_trees = ConstraintSolver.Equalities.fold_sets eqs ~init:Node.IdMap.empty ~f: (fun acc_trees (rep, _eq_cl) -> - let rep_id = ControlFlowCost.assert_node (rep :> ControlFlowCost.t) in - let tree = - if ConstraintSolver.Equalities.Repr.equal start_node_repr rep then - (* for any node in the same equivalence class as the start node we give the trivial MinTree: + match ControlFlowCost.is_node (rep :> ControlFlowCost.t) with + | None -> + acc_trees + | Some rep_id -> + let tree = + if ConstraintSolver.Equalities.Repr.equal start_node_repr 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 ) + 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 ) in Node.IdMap.iter (fun nid t -> L.(debug Analysis Medium) "@\n node %a = %a @\n" Node.pp_id nid pp t) @@ -872,27 +1009,34 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = in let pp_extra, get_node_nb_exec = let equalities = ConstraintSolver.collect_constraints node_cfg in - let min_trees = - let constraints = StructuralConstraints.compute_structural_constraints node_cfg in - MinTree.compute_trees_from_contraints bound_map node_cfg equalities constraints - in - let trees_valuation = - 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 ) - min_trees Node.IdMap.empty - in - let pp_extra fmt = F.fprintf fmt "|Trees|=%i" (Node.IdMap.cardinal min_trees) in - let get_node_nb_exec node_id = - match Node.IdMap.find_opt node_id trees_valuation with - | Some t -> - t - | None -> - MinTree.find_tree_eq_rel node_id trees_valuation equalities - in - (pp_extra, get_node_nb_exec) + match solver with + | `MinTree -> + let min_trees = + let constraints = StructuralConstraints.compute_structural_constraints node_cfg in + MinTree.compute_trees_from_contraints bound_map node_cfg equalities constraints + in + let trees_valuation = + 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 ) + min_trees Node.IdMap.empty + in + let pp_extra fmt = F.fprintf fmt "|Trees|=%i" (Node.IdMap.cardinal min_trees) in + let get_node_nb_exec node_id = + match Node.IdMap.find_opt node_id trees_valuation with + | Some t -> + t + | None -> + MinTree.find_tree_eq_rel node_id trees_valuation equalities + in + (pp_extra, get_node_nb_exec) + | `ConstraintSolver -> + let () = ConstraintSolver.compute_costs bound_map equalities in + let pp_extra _ = () in + (pp_extra, ConstraintSolver.get_node_nb_exec equalities) in let initWCET = (BasicCost.zero, ReportedOnNodes.empty) in match diff --git a/infer/src/istd/ImperativeUnionFind.ml b/infer/src/istd/ImperativeUnionFind.ml index 1847c583e..ef6405f53 100644 --- a/infer/src/istd/ImperativeUnionFind.ml +++ b/infer/src/istd/ImperativeUnionFind.ml @@ -75,6 +75,8 @@ module Make (Set : Set) = struct let create () = H.create 1 + let find t r = H.find_opt t r + let find_create t (r: Repr.t) = match H.find_opt t r with | Some set -> @@ -111,13 +113,15 @@ module Make (Set : Set) = struct else t.to_remove <- from_r :: t.to_remove + let find_create_set t repr = Sets.find_create t.sets repr + let union t e1 e2 = let repr1 = find t e1 in let repr2 = find t e2 in if Repr.equal repr1 repr2 then None else - let set1 = Sets.find_create t.sets repr1 in - let set2 = Sets.find_create t.sets repr2 in + let set1 = find_create_set t repr1 in + let set2 = find_create_set t repr2 in let cmp_size = Set.compare_size set1 set2 in if cmp_size < 0 || (Int.equal cmp_size 0 && Repr.is_simpler_than repr2 repr1) then ( (* A desired side-effect of using [is_simpler_than] is that the representative for a set will always be a [`Node]. For now. *) @@ -138,6 +142,8 @@ module Make (Set : Set) = struct t.to_remove <- [] ) + let find_set t r = Sets.find t.sets r + let fold_sets t ~init ~f = t.nb_iterators <- t.nb_iterators + 1 ; match IContainer.filter ~fold:Sets.fold ~filter:(is_still_a_repr t) t.sets ~init ~f with diff --git a/infer/src/istd/ImperativeUnionFind.mli b/infer/src/istd/ImperativeUnionFind.mli index 9397c9459..057f05193 100644 --- a/infer/src/istd/ImperativeUnionFind.mli +++ b/infer/src/istd/ImperativeUnionFind.mli @@ -35,6 +35,10 @@ module Make (Set : Set) : sig val union : t -> Set.elt -> Set.elt -> (Set.elt * Set.elt) option (** [union t e1 e2] returns [None] if [e1] and [e2] were already in the same set, [Some (a, b)] if [a] is merged into [b] (were [(a, b)] is either [(e1, e2)] or [(e2, e1)]). *) + val find_create_set : t -> Repr.t -> Set.t + + val find_set : t -> Repr.t -> Set.t option + val fold_sets : (t, Repr.t * Set.t, 'accum) Container.fold (** It is safe to call [find] or [union] while folding. *) end diff --git a/infer/tests/codetoanalyze/java/performance/EvilCfg.java b/infer/tests/codetoanalyze/java/performance/EvilCfg.java new file mode 100644 index 000000000..03f0c43d3 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/EvilCfg.java @@ -0,0 +1,35 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class EvilCfg { + public void foo(int i, int j, boolean b) { + int k, l, m, n; + + k = b ? i : j; + l = b ? k : i; + m = b ? k : l; + n = b ? m : k; + for (; n < 10; n++) {} + + k = b ? i : j; + l = b ? k : i; + m = b ? k : l; + n = b ? m : k; + for (; n < 10; n++) {} + + k = b ? i : j; + l = b ? k : i; + m = b ? k : l; + n = b ? m : k; + for (; n < 10; n++) {} + + k = b ? i : j; + l = b ? k : i; + m = b ? k : l; + n = b ? m : k; + for (; n < 10; n++) {} + } +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 32389b096..3b7c1a5f6 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -43,6 +43,7 @@ codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.two_loops codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.two_loops(), 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545] codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608] codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 607] +codetoanalyze/java/performance/EvilCfg.java, void EvilCfg.foo(int,int,boolean), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,Object), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []