[inferbo] Add models of infer annotations

Reviewed By: jvillard

Differential Revision: D21226982

fbshipit-source-id: 4b63b19b8

infer/src/absint/PatternMatch.ml

@@ -101,6 +101,10 @@ let implements_google class_name = implements ("com.google." ^ class_name)
 
 let implements_android class_name = implements ("android." ^ class_name)
 
+let implements_infer_annotation class_name =
+  implements ("com.facebook.infer.annotation." ^ class_name)
+
+
 let implements_jackson class_name = implements ("com.fasterxml.jackson." ^ class_name)
 
 let implements_org_json class_name = implements ("org.json." ^ class_name)

infer/src/absint/PatternMatch.mli

@@ -91,6 +91,9 @@ val implements_google : string -> Tenv.t -> string -> bool
 val implements_android : string -> Tenv.t -> string -> bool
 (** Check whether class implements a class of Android *)
 
+val implements_infer_annotation : string -> Tenv.t -> string -> bool
+(** Check whether class implements a class of Infer annotation *)
+
 val implements_xmob_utils : string -> Tenv.t -> string -> bool
 (** Check whether class implements a class of xmod.utils *)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -915,6 +915,12 @@ module Collection = struct
       key is found in the map *)
   let put coll_id = {exec= change_size_by_incr_or_not coll_id; check= no_check}
 
+  let put_with_elem coll_id elem_exp =
+    let put_model = put coll_id in
+    let exec env ~ret mem = put_model.exec env ~ret mem |> set_elem_exec env coll_id elem_exp in
+    {put_model with exec}
+
+
   (* The return value is set by [set_itv_updated_by_addition] in order to be sure that it can be
      used as a control variable value in the cost checker. *)
   let size coll_exp =
@@ -1304,6 +1310,15 @@ module Object = struct
     {exec; check= no_check}
 end
 
+module InferAnnotation = struct
+  let assert_get index_exp coll_exp =
+    match coll_exp with
+    | Exp.Var coll_id ->
+        Collection.get_at_index coll_id index_exp
+    | _ ->
+        no_model
+end
+
 module Call = struct
   let dispatch : (Tenv.t, model, unit) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
@@ -1520,8 +1535,8 @@ module Call = struct
       ; +PatternMatch.implements_map &:: "entrySet" <>$ capt_exp $!--> Collection.iterator
       ; +PatternMatch.implements_map &:: "keySet" <>$ capt_exp $!--> Collection.iterator
       ; +PatternMatch.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator
-      ; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg
+      ; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ capt_exp
-        $--> Collection.put
+        $--> Collection.put_with_elem
       ; +PatternMatch.implements_org_json "JSONArray"
         &:: "put" <>$ capt_var_exn $+...$--> Collection.put
       ; +PatternMatch.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp
@@ -1569,5 +1584,14 @@ module Call = struct
         $--> eval_binop ~f:(Itv.min_sem ~use_minmax_bound:true)
       ; +PatternMatch.implements_lang "Enum" &:: "name" &::.*--> JavaString.inferbo_constant_string
       ; +PatternMatch.implements_lang "Class"
-        &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string ]
+        &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string
+      ; +PatternMatch.implements_infer_annotation "Assertions"
+        &:: "assertNotNull" <>$ capt_exp $+...$--> id
+      ; +PatternMatch.implements_infer_annotation "Assertions"
+        &:: "assumeNotNull" <>$ capt_exp $+...$--> id
+      ; +PatternMatch.implements_infer_annotation "Assertions"
+        &:: "nullsafeFIXME" <>$ capt_exp $+...$--> id
+      ; +PatternMatch.implements_infer_annotation "Assertions"
+        &:: "assertGet" <>$ capt_exp $+ capt_exp $--> InferAnnotation.assert_get
+      ; +PatternMatch.implements_infer_annotation "Assertions" &::.*--> no_model ]
 end

infer/tests/codetoanalyze/java/performance/InferAnnotationTest.java

@@ -0,0 +1,45 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import com.facebook.infer.annotation.Assertions;
+import java.util.ArrayList;
+import java.util.HashMap;
+
+public class InferAnnotationTest {
+
+  public void assert_not_null_linear(Integer x) {
+    for (int i = 0; i < Assertions.assertNotNull(x); i++) {}
+  }
+
+  public void assert_not_null_explanation_linear(Integer x) {
+    for (int i = 0; i < Assertions.assertNotNull(x, "explanation"); i++) {}
+  }
+
+  public void assume_not_null_linear(Integer x) {
+    for (int i = 0; i < Assertions.assumeNotNull(x); i++) {}
+  }
+
+  public void assume_not_null_explanation_linear(Integer x) {
+    for (int i = 0; i < Assertions.assumeNotNull(x, "explanation"); i++) {}
+  }
+
+  public void nullsafe_fixme_linear(Integer x) {
+    for (int i = 0; i < Assertions.nullsafeFIXME(x, "explanation"); i++) {}
+  }
+
+  public void assert_get_list_constant() {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(5);
+    for (int i = 0; i < Assertions.assertGet(0, a); i++) {}
+  }
+
+  public void assert_get_map_constant() {
+    HashMap<Integer, Integer> m = new HashMap<Integer, Integer>();
+    m.put(0, 5);
+    for (int i = 0; i < Assertions.assertGet(0, m); i++) {}
+  }
+}

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

@@ -118,6 +118,11 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 545, O(1), degree = 0]
 codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 15]
 codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, O(test.a), degree = 1,{test.a},Loop at line 16]
+codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assert_not_null_explanation_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 19,{x},Loop at line 19]
+codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assert_not_null_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 15,{x},Loop at line 15]
+codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assume_not_null_explanation_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 27,{x},Loop at line 27]
+codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assume_not_null_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 23,{x},Loop at line 23]
+codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.nullsafe_fixme_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 31,{x},Loop at line 31]
 codetoanalyze/java/performance/InheritanceTest.java, InheritanceTest$Impl1.foo(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 34]
 codetoanalyze/java/performance/InheritanceTest.java, InheritanceTest$UniqueImpl.foo(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 15]
 codetoanalyze/java/performance/InheritanceTest.java, InheritanceTest$UniqueImpl4.top_cost(InheritanceTest$MyInterface3):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 58]