pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cost solver

Browse Source 
Reviewed By: ddino

Differential Revision: D8348319

fbshipit-source-id: 9274da6
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 776e728b63
commit 5b6430e739
6 changed files with 253 additions and 59 deletions
Show Stats Download Patch File Download Diff File

10
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -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 *)

252
infer/src/checkers/cost.ml
Unescape View File

@ -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

10
infer/src/istd/ImperativeUnionFind.ml
Unescape View File

@ -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

4
infer/src/istd/ImperativeUnionFind.mli
Unescape View File

@ -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

35
infer/tests/codetoanalyze/java/performance/EvilCfg.java
Unescape View File

@ -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++) {}
}
}

1
infer/tests/codetoanalyze/java/performance/issues.exp
Unescape View File

@ -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, []

Write Preview
Loading…
Cancel
Save