[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

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

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

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

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

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)

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);
+  }
+
+}

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