From cc18f9883d6be70fbe8d46144d3713e9d87ead1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 16 Aug 2018 14:35:54 -0700 Subject: [PATCH] [Cost] Fix invariant variable analysis to be based on all reaching defns Reviewed By: mbouaziz Differential Revision: D9337572 fbshipit-source-id: f7f5f7572 --- infer/src/IR/Var.ml | 2 + infer/src/IR/Var.mli | 2 + infer/src/checkers/cost.ml | 3 +- infer/src/checkers/loopInvariant.ml | 6 +- infer/src/checkers/reachingDefs.ml | 8 +++ .../java/performance/Invariant.java | 62 +++++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 7 +++ 7 files changed, 86 insertions(+), 4 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/performance/Invariant.java diff --git a/infer/src/IR/Var.ml b/infer/src/IR/Var.ml index f6e2a4ac3..741b80fa2 100644 --- a/infer/src/IR/Var.ml +++ b/infer/src/IR/Var.ml @@ -36,6 +36,8 @@ let is_return = function ProgramVar pvar -> Pvar.is_return pvar | LogicalVar _ - let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id +let is_none = function LogicalVar id -> Ident.is_none id | _ -> false + let get_all_vars_in_exp e = let acc = Exp.free_vars e |> Sequence.map ~f:of_id in Exp.program_vars e |> Sequence.map ~f:of_pvar |> Sequence.append acc diff --git a/infer/src/IR/Var.mli b/infer/src/IR/Var.mli index 94e447bba..6fd30d728 100644 --- a/infer/src/IR/Var.mli +++ b/infer/src/IR/Var.mli @@ -33,6 +33,8 @@ val is_return : t -> bool val is_footprint : t -> bool +val is_none : t -> bool + val appears_in_source_code : t -> bool (** return true if this variable appears in source code (i.e., is not a LogicalVar or a frontend-generated ProgramVar) *) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 68791abb9..2b0f9bb33 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -749,7 +749,8 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = let proc_data = ProcData.make_default proc_desc tenv in (* computes reaching defs: node -> (var -> node set) *) let reaching_defs_invariant_map = - ReachingDefs.Analyzer.exec_cfg node_cfg proc_data ~initial:ReachingDefs.ReachingDefsMap.empty + ReachingDefs.Analyzer.exec_cfg node_cfg proc_data + ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc) ~debug:false in (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index de162e058..db2592292 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -75,7 +75,7 @@ let get_inv_vars_in_loop 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) *) - if InvariantVars.mem var inv_vars then (inv_vars, false) + if InvariantVars.mem var inv_vars || Var.is_none var then (inv_vars, false) else let loop_head_id = Procdesc.Node.get_id loop_head in ReachingDefs.Analyzer.extract_post loop_head_id reaching_defs_invariant_map @@ -87,12 +87,12 @@ 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 in_loop_defs + is_def_unique_and_satisfy var def_nodes (is_exp_invariant inv_vars loop_nodes reaching_defs) then (InvariantVars.add var inv_vars, true) else (inv_vars, false) ) |> Option.value (* if a var is not declared, it must be invariant *) - ~default:(InvariantVars.add var inv_vars, true) ) + ~default:(inv_vars, false) ) |> Option.value ~default:(inv_vars, false) in let vars_in_loop = get_vars_in_loop loop_nodes in diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index 98861b69f..b3e58c9aa 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -56,4 +56,12 @@ module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct F.fprintf fmt "reaching defs analysis %a" CFG.Node.pp_id (CFG.Node.id node) end +(* initialize formal parameters to have start node as reaching def *) +let init_reaching_defs_with_formals pdesc = + let start_node_defs = Defs.singleton (Procdesc.get_start_node pdesc) in + BufferOverrunSemantics.get_formals pdesc + |> List.fold_left ~init:ReachingDefsMap.empty ~f:(fun acc (pvar, _) -> + ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc ) + + module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctionsReachingDefs) diff --git a/infer/tests/codetoanalyze/java/performance/Invariant.java b/infer/tests/codetoanalyze/java/performance/Invariant.java new file mode 100644 index 000000000..13d39c751 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/Invariant.java @@ -0,0 +1,62 @@ +/* + * 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 Invariant { + + // x is invariant + void x_is_invariant_ok(int size) { + int i = 0, x; + if (size > 10) { + x = 10; + } else { + x = 20; + } + while (i < size + x) { + i++; + } + } + + // x shouldn't be invariant since it can have two different values + // depending on whether the inner conditional is executed or not + // Currently, we are getting T because of a problem in InferBo, see + // T32798161 + void formal_not_invariant_FP(int size, int x) { + int i = 0; + while (i < size + x) { + if (x > i) { + x = 0; + } + i++; + } + } + + // x shouldn't be invariant since it can have two different values + // depending on whether the inner conditional is executed or not + // Currently, we are getting T because of a problem in InferBo, see + // T32798161 + void local_not_invariant_FP(int size) { + int i = 0; + int x = 5; + while (i < size + x) { + if (x > i) { + x = 0; + } + i++; + } + } + + + // m will be invariant + void do_while_invariant(int m, int k){ + int i = 0; + do{ + m = k; + i++; + } + while (i < m); + } + +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 521cf316a..1e122a18c 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -84,6 +84,13 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] 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.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +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] codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 2 * (parts.length.ub + -1) + 4 * parts.length.ub, degree = 1] codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 0 + 2 * (parts.length.ub + -1) + 4 * parts.length.ub, degree = 1] codetoanalyze/java/performance/JsonArray.java, libraries.marauder.analytics.utils.json.JsonArray.addStringEntry(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []