[pulse] Modeling checkNotNull function

Summary: Creating model for the checkNotNull function from the Preconditions class in Pulse (Java). Whenever `checkNotNull(x)` is called, Pulse will assume that `x!= null`.

Reviewed By: ezgicicek

Differential Revision: D26075176

fbshipit-source-id: 40dcd395b

infer/src/pulse/PulseModels.ml

@@ -1021,6 +1021,14 @@ module JavaInteger = struct
     [ExecutionDomain.continue astate]
 end
 
+module JavaPreconditions = struct
+  let check_not_null (address, hist) : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model "Preconditions.checkNotNull"; location; in_call= []} in
+    let astate = PulseArithmetic.and_positive address astate in
+    PulseOperations.write_id ret_id (address, event :: hist) astate |> ok_continue
+end
+
 module StringSet = Caml.Set.Make (String)
 
 module ProcNameDispatcher = struct
@@ -1308,6 +1316,8 @@ module ProcNameDispatcher = struct
           &:: "intValue" <>$ capt_arg_payload $--> JavaInteger.int_val
         ; +map_context_tenv (PatternMatch.Java.implements_lang "Integer")
           &:: "valueOf" <>$ capt_arg_payload $--> JavaInteger.value_of
+        ; +map_context_tenv (PatternMatch.Java.implements_google "common.base.Preconditions")
+          &:: "checkNotNull" $ capt_arg_payload $+...$--> JavaPreconditions.check_not_null
         ; +map_context_tenv PatternMatch.Java.implements_iterator
           &:: "remove" <>$ capt_arg_payload
           $+...$--> JavaIterator.remove ~desc:"remove"

infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java

@@ -0,0 +1,63 @@
+/*
+ * 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.
+ */
+package codetoanalyze.java.infer;
+
+import com.google.common.base.Preconditions;
+
+public class CheckNotNullExample {
+
+  Integer i1;
+
+  /*
+   * Note: Although the Guava checkNotNull method throws a NullPointerException when a given
+   * value x is null, Pulse will simply try to go ahead assuming that x != null.
+   * This means that it will not report NPEs on values passed to checkNotNull.
+   */
+
+  void testCheckNotNullOnNullValueOk() {
+    CheckNotNullExample x = null;
+    // This should not be reported due to the use of checkNotNull
+    Preconditions.checkNotNull(x);
+    Integer i1 = x.i1;
+  }
+
+  void testCheckNotNullOnNonNullValueOk() {
+    CheckNotNullExample x = new CheckNotNullExample();
+    x.i1 = new Integer(10);
+    CheckNotNullExample y = Preconditions.checkNotNull(x);
+    // This should not cause bug, as y.i1 should be equal to x.i1
+    if (!y.i1.equals(10)) {
+      Object o = null;
+      o.toString();
+    }
+  }
+
+  void testCheckNotNullPassingFurtherArgsOk() {
+    Object x = null;
+    Preconditions.checkNotNull(x, "errorMsg");
+    x.toString();
+  }
+
+  void testCheckNotNullOtherDerefOk() {
+    Object x = null;
+    Object y = null;
+    Preconditions.checkNotNull(x, "errorMsg");
+    y.toString();
+  }
+
+  void testCheckNotNullArgOk(Object x) {
+    Object y = null;
+    Preconditions.checkNotNull(x);
+    x.toString();
+  }
+
+  void testCheckNotNullArgBad(Object x) {
+    Object y = null;
+    Preconditions.checkNotNull(x);
+    y.toString();
+  }
+}

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

@@ -5,6 +5,7 @@ codetoanalyze/java/pulse/Builtins.java, codetoanalyze.java.infer.Builtins.FP_blo
 codetoanalyze/java/pulse/Builtins.java, codetoanalyze.java.infer.Builtins.FP_blockErrorOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/Builtins.java, codetoanalyze.java.infer.Builtins.doNotBlockErrorBad(java.lang.Object):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/Builtins.java, codetoanalyze.java.infer.Builtins.doNotBlockErrorBad(java.lang.Object):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/CheckNotNullExample.java, codetoanalyze.java.infer.CheckNotNullExample.testCheckNotNullArgBad(java.lang.Object):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$A.defaultCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$B.overridenCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE_latent(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]