[Cost] Add a Java model for functions to be considered invariant

fbshipit-source-id: e2fa74b19

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

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

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 =

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

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

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

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