From e04f0a0ffad0abcefac34c5f096ad43a2c5d42f8 Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Thu, 28 Jan 2021 01:44:32 -0800 Subject: [PATCH] [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 | 10 +++ .../java/pulse/CheckNotNullExample.java | 63 +++++++++++++++++++ .../tests/codetoanalyze/java/pulse/issues.exp | 1 + 3 files changed, 74 insertions(+) create mode 100644 infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 46b816a86..5cfe6bf12 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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" diff --git a/infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java b/infer/tests/codetoanalyze/java/pulse/CheckNotNullExample.java new file mode 100644 index 000000000..2504a5b2e --- /dev/null +++ b/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(); + } +} diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 3769df8d0..678a6f7ec 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/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]