From be39e74bd40cf6ce0e9e8aeb7c4e296263b7bbfb Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Thu, 28 Jan 2021 08:07:00 -0800 Subject: [PATCH] [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 | 9 ++++ ...Example.java => PreconditionsExample.java} | 43 +++++++++++++++++-- .../tests/codetoanalyze/java/pulse/issues.exp | 4 +- 3 files changed, 51 insertions(+), 5 deletions(-) rename infer/tests/codetoanalyze/java/pulse/{CheckNotNullExample.java => PreconditionsExample.java} (58%) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 5cfe6bf12..64da377bc 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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" diff --git a/infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java b/infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java similarity index 58% rename from infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java rename to infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java index 2504a5b2e..e358ac6f0 100644 --- a/infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java +++ b/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(); + } } diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 678a6f7ec..bdb31f420 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/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.()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `OtherClass.()`,assigned,return from call to `OtherClass.()`,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.(), 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]