From 527fb90bbe5732084d1095ab580839bfb97e7ea6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Sat, 18 Aug 2018 11:29:53 -0700 Subject: [PATCH] [Cost] Add a Java model for functions to be considered invariant fbshipit-source-id: e2fa74b19 --- infer/src/base/Config.ml | 7 +++++ infer/src/base/Config.mli | 2 ++ infer/src/checkers/cost.ml | 2 +- infer/src/checkers/invariantModels.ml | 23 ++++++++++++++++ infer/src/checkers/loopInvariant.ml | 27 ++++++++++++++----- .../java/performance/Invariant.java | 15 +++++++---- .../codetoanalyze/java/performance/issues.exp | 6 +++-- 7 files changed, 67 insertions(+), 15 deletions(-) create mode 100644 infer/src/checkers/invariantModels.ml diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 47138e106..e261bb215 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -959,6 +959,11 @@ and continue = a procedure was changed beforehand, keep the changed marking.)" +and cost_invariant_by_default = + CLOpt.mk_bool ~long:"invariant-by-default" ~default:false + "[Cost]Consider functions to be invariant by default" + + and current_to_previous_script = CLOpt.mk_string_opt ~long:"current-to-previous-script" ~in_help:InferCommand.[(Diff, manual_generic)] @@ -2523,6 +2528,8 @@ and continue_capture = !continue and cost = !cost +and cost_invariant_by_default = !cost_invariant_by_default + and current_to_previous_script = !current_to_previous_script and crashcontext = !crashcontext diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0b08b2135..e303d9cf5 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -287,6 +287,8 @@ val continue_capture : bool val cost : bool +val cost_invariant_by_default : bool + val crashcontext : bool val current_to_previous_script : string option diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 2b0f9bb33..b0e18b96f 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -770,7 +770,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = in (* compute loop invariant map for control var analysis *) let loop_inv_map = - LoopInvariant.get_loop_inv_var_map reaching_defs_invariant_map loop_head_to_loop_nodes + LoopInvariant.get_loop_inv_var_map tenv reaching_defs_invariant_map loop_head_to_loop_nodes in (* given the semantics computes the upper bound on the number of times a node could be executed *) let bound_map = diff --git a/infer/src/checkers/invariantModels.ml b/infer/src/checkers/invariantModels.ml new file mode 100644 index 000000000..6b5761960 --- /dev/null +++ b/infer/src/checkers/invariantModels.ml @@ -0,0 +1,23 @@ +(* + * 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. + *) + +open! IStd + +type model = Invariant | Variant + +let is_invariant = function Invariant -> true | Variant -> false + +module Call = struct + let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher = + let open ProcnameDispatcher.Call in + make_dispatcher + [ -"__cast" <>--> Invariant + ; +PatternMatch.implements_collection &:: "iterator" <>--> Variant + ; +PatternMatch.implements_iterator &:: "hasNext" <>--> Variant + ; +PatternMatch.implements_iterator &:: "next" <>--> Variant + ; +PatternMatch.implements_collection &:: "size" <>--> Invariant ] +end diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index db2592292..72837b6e1 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -8,6 +8,7 @@ open! IStd module L = Logging module InvariantVars = AbstractDomain.FiniteSet (Var) module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node) +module Models = InvariantModels (** Map loop header node -> all nodes in the loop *) module LoopHeadToLoopNodes = Procdesc.NodeMap @@ -19,7 +20,8 @@ let is_defined_outside loop_nodes reaching_defs var = (* check if the def of var is unique and satisfies function f_exp *) -let is_def_unique_and_satisfy var (loop_nodes: LoopNodes.t) f_exp = +let is_def_unique_and_satisfy tenv var (loop_nodes: LoopNodes.t) f_exp = + let equals_var id = Var.equal var (Var.of_id id) in (* Use O(1) is_singleton check *) (* tedious parameter wrangling to make IContainer's fold interface happy *) IContainer.is_singleton @@ -29,11 +31,22 @@ let is_def_unique_and_satisfy var (loop_nodes: LoopNodes.t) f_exp = (fun node -> Procdesc.Node.get_instrs node |> Instrs.exists ~f:(function - | Sil.Load (id, exp_rhs, _, _) when Var.equal (Var.of_id id) var && f_exp exp_rhs -> + | Sil.Load (id, exp_rhs, _, _) when equals_var id && f_exp exp_rhs -> true | Sil.Store (exp_lhs, _, exp_rhs, _) when Exp.equal exp_lhs (Var.to_exp var) && f_exp exp_rhs -> - true (* function calls are ignored at the moment *) + true + | Sil.Call ((id, _), Const (Cfun callee_pname), params, _, _) when equals_var id -> ( + match + (* Take into account invariance behavior of modeled + functions *) + Models.Call.dispatch tenv callee_pname params + with + | Some inv -> + InvariantModels.is_invariant inv + && List.for_all ~f:(fun (exp, _) -> f_exp exp) params + | None -> + Config.cost_invariant_by_default ) | _ -> false ) ) loop_nodes @@ -71,7 +84,7 @@ let get_vars_in_loop loop_nodes = (* A variable is invariant if - its reaching definition is outside of the loop - o.w. its definition is constant or invariant itself *) -let get_inv_vars_in_loop reaching_defs_invariant_map loop_head loop_nodes = +let get_inv_vars_in_loop tenv reaching_defs_invariant_map loop_head loop_nodes = let process_var_once var inv_vars = (* if a variable is marked invariant once, it can't be invalidated (i.e. invariance is monotonic) *) @@ -87,7 +100,7 @@ let get_inv_vars_in_loop reaching_defs_invariant_map loop_head loop_nodes = if LoopNodes.is_empty in_loop_defs then (InvariantVars.add var inv_vars, true) else if (* its definition is unique and invariant *) - is_def_unique_and_satisfy var def_nodes + is_def_unique_and_satisfy tenv var def_nodes (is_exp_invariant inv_vars loop_nodes reaching_defs) then (InvariantVars.add var inv_vars, true) else (inv_vars, false) ) @@ -114,11 +127,11 @@ let get_inv_vars_in_loop reaching_defs_invariant_map loop_head loop_nodes = (** Map loop head -> invariant vars in loop *) module LoopHeadToInvVars = Procdesc.NodeMap -let get_loop_inv_var_map reaching_defs_invariant_map loop_head_to_loop_nodes = +let get_loop_inv_var_map tenv reaching_defs_invariant_map loop_head_to_loop_nodes = LoopHeadToLoopNodes.fold (fun loop_head loop_nodes inv_map -> let inv_vars_in_loop = - get_inv_vars_in_loop reaching_defs_invariant_map loop_head loop_nodes + get_inv_vars_in_loop tenv reaching_defs_invariant_map loop_head loop_nodes in L.(debug Analysis Medium) "@\n>>> loop head: %a --> inv vars: %a @\n" Procdesc.Node.pp loop_head InvariantVars.pp diff --git a/infer/tests/codetoanalyze/java/performance/Invariant.java b/infer/tests/codetoanalyze/java/performance/Invariant.java index 13d39c751..09e352d96 100644 --- a/infer/tests/codetoanalyze/java/performance/Invariant.java +++ b/infer/tests/codetoanalyze/java/performance/Invariant.java @@ -4,6 +4,8 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ +import java.util.List; + class Invariant { // x is invariant @@ -48,15 +50,18 @@ class Invariant { } } - // m will be invariant - void do_while_invariant(int m, int k){ + void do_while_invariant(int m, int k) { int i = 0; - do{ + do { m = k; i++; - } - while (i < m); + } while (i < m); } + // before, we were getting items.size()^2 since all functions were + // assumed to be impure + void list_size_invariant(List items) { + for (int i = 0; i < items.size(); i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 1e122a18c..8a4b59641 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -85,9 +85,11 @@ codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * (k.ub + -1), degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * (k.ub + -1), degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * (k.ub + -1), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * items.length.ub, degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 * items.length.ub, degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * (size.ub + 20), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 * (size.ub + 20), degree = 1]