[pulse] Modeling checkState and checkArgument

Summary:
providing models for the checkState and checkArgument
functions, both used in Java code.

Reviewed By: da319

Differential Revision: D26101726

fbshipit-source-id: 0cc73d252

infer/src/pulse/PulseModels.ml

@@ -1027,6 +1027,11 @@ module JavaPreconditions = struct
     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
+
+
+  let check_state_argument (address, _) : model =
+   fun _ ~callee_procname:_ _ ~ret:_ astate ->
+    PulseArithmetic.and_positive address astate |> ok_continue
 end
 
 module StringSet = Caml.Set.Make (String)
@@ -1318,6 +1323,10 @@ module ProcNameDispatcher = struct
           &:: "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_google "common.base.Preconditions")
+          &:: "checkState" $ capt_arg_payload $+...$--> JavaPreconditions.check_state_argument
+        ; +map_context_tenv (PatternMatch.Java.implements_google "common.base.Preconditions")
+          &:: "checkArgument" $ capt_arg_payload $+...$--> JavaPreconditions.check_state_argument
         ; +map_context_tenv PatternMatch.Java.implements_iterator
           &:: "remove" <>$ capt_arg_payload
           $+...$--> JavaIterator.remove ~desc:"remove"

infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java

@@ -8,7 +8,7 @@ package codetoanalyze.java.infer;
 
 import com.google.common.base.Preconditions;
 
-public class CheckNotNullExample {
+public class PreconditionsExample {
 
   Integer i1;
 
@@ -16,19 +16,20 @@ public class CheckNotNullExample {
    * 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.
+   * The analogous approach has been taken for checkState and checkArgument.
    */
 
   void testCheckNotNullOnNullValueOk() {
-    CheckNotNullExample x = null;
+    PreconditionsExample 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();
+    PreconditionsExample x = new PreconditionsExample();
     x.i1 = new Integer(10);
-    CheckNotNullExample y = Preconditions.checkNotNull(x);
+    PreconditionsExample 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;
@@ -60,4 +61,38 @@ public class CheckNotNullExample {
     Preconditions.checkNotNull(x);
     y.toString();
   }
+
+  void checkStateConditionSatBad() {
+    PreconditionsExample x = new PreconditionsExample();
+    PreconditionsExample y = null;
+    x.i1 = 1000;
+    Preconditions.checkState(x.i1.equals(1000));
+    y.toString();
+  }
+
+  void checkStateConditionUnsatOk() {
+    PreconditionsExample x = new PreconditionsExample();
+    PreconditionsExample y = null;
+    x.i1 = 1000;
+    Preconditions.checkState(x.i1.equals(100), "errorMsg");
+    y.toString();
+  }
+
+  void checkArgumentUnsatOk() {
+    int age = -18;
+    Object x = null;
+    Preconditions.checkArgument(age > 0);
+    x.getClass();
+  }
+
+  void checkAgeOver18(int age) {
+    Preconditions.checkArgument(age > 18, "errorMsg");
+  }
+
+  void checkArgumentSatBad() {
+    int age = 20;
+    Object x = null;
+    checkAgeOver18(age);
+    x.getClass();
+  }
 }

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

@@ -5,7 +5,6 @@ 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]
@@ -55,6 +54,9 @@ codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.Nu
 codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP():void, 10, 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/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.stringVarEqualsFalseNPE():void, 5, 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/NullSafeExample.java, OtherClass.buggyMethodBad():java.lang.String, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `OtherClass.<init>()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `OtherClass.<init>()`,assigned,return from call to `OtherClass.<init>()`,passed as argument to `OtherClass OtherClass.canReturnNull()`,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.checkArgumentSatBad():void, 4, 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/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.checkStateConditionSatBad():void, 5, 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/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.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/SuppressLintExample.java, codetoanalyze.java.infer.SuppressAllWarnigsInTheClass.shouldNotReportNPE():void, 2, 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/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.<init>(), 2, 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/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.FP_shouldNotReportNPE():void, 2, 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]