[inferbo] Add models for Preconditions.checkNotNull and Preconditions.checkState

Reviewed By: ngorogiannis

Differential Revision: D19346368

fbshipit-source-id: 643327802

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -347,6 +347,14 @@ let cast exp size_exp =
   {exec; check= no_check}
 
 
+let id exp =
+  let exec {integer_type_widths} ~ret:(ret_id, _) mem =
+    let v = Sem.eval integer_type_widths exp mem in
+    model_by_value v ret_id mem
+  in
+  {exec; check= no_check}
+
+
 let by_value =
   let exec ~value _ ~ret:(ret_id, _) mem = model_by_value value ret_id mem in
   fun value -> {exec= exec ~value; check= no_check}
@@ -1398,7 +1406,11 @@ module Call = struct
         &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $!--> Collection.addAll_at_index
       ; +PatternMatch.implements_collection &:: "size" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.implements_google "common.base.Preconditions"
-        &:: "checkArgument" <>$ capt_exp $--> Preconditions.check_argument
+        &:: "checkArgument" <>$ capt_exp $+...$--> Preconditions.check_argument
+      ; +PatternMatch.implements_google "common.base.Preconditions"
+        &:: "checkState" <>$ capt_exp $+...$--> Preconditions.check_argument
+      ; +PatternMatch.implements_google "common.base.Preconditions"
+        &:: "checkNotNull" <>$ capt_exp $+...$--> id
       ; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.implements_org_json "JSONArray"
         &:: "length" <>$ capt_exp $!--> Collection.size

infer/tests/codetoanalyze/java/performance/PreconditionTest.java

@@ -9,11 +9,17 @@ import java.util.ArrayList;
 
 class PreconditionTest {
   // should be constant
-  public void constant(ArrayList<Integer> list) {
+  public void checkArgument_constant(ArrayList<Integer> list) {
     Preconditions.checkArgument(list.size() == 2);
     for (int i = 0; i < list.size(); i++) {}
   }
 
+  // should be constant
+  public void checkState_constant(ArrayList<Integer> list) {
+    Preconditions.checkState(list.size() == 2);
+    for (int i = 0; i < list.size(); i++) {}
+  }
+
   public class get_five {
     public static final int FIVE = 5;
   }
@@ -25,4 +31,9 @@ class PreconditionTest {
       Preconditions.checkArgument(i >= 0);
     }
   }
+
+  public void checkNotNull_linear(ArrayList<Integer> list, Object o) {
+    ArrayList<Integer> mediaList = Preconditions.checkNotNull(list, o);
+    for (Integer el : mediaList) {}
+  }
 }

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -195,6 +195,7 @@ codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.Mat
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ p, O(p), degree = 1,{p},Loop at line 28]
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max2_symbolic(int,int):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (max(x, y)), O((max(x, y))), degree = 1,{max(x, y)},Loop at line 20]
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 16,{arr.length},Loop at line 16]
+codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkNotNull_linear(java.util.ArrayList,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 37,{list.length},Loop at line 37]
 codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + this.mId.length, O(this.mId.length), degree = 1,{this.mId.length},call to int StringTest.indexof_linear(String),Modeled call to String.indexOf]
 codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(java.lang.String,int):int, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + (-j + m.length), O((-j + m.length)), degree = 1,{-j + m.length},Modeled call to String.indexOf]
 codetoanalyze/java/performance/StringTest.java, StringTest.indexof_linear(java.lang.String):int, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + m.length, O(m.length), degree = 1,{m.length},Modeled call to String.indexOf]