From 68b4b5cc27bdd44c5dd39e92b6b526b80521ac60 Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Fri, 26 Mar 2021 09:48:00 -0700 Subject: [PATCH] [pulse] IsInstanceOf simplification for null obj Summary: Fixing `IsInstanceOf` term simplification for null case. Before, this was only being done if value was known to be null at the moment of the call to `instanceof`. Otherwise, the `IsInstanceOf` term would remain in the formula unnecessarily. Reviewed By: jvillard Differential Revision: D27361025 fbshipit-source-id: 2d958a757 --- infer/src/pulse/PulseFormula.ml | 2 ++ infer/src/pulse/PulseModels.ml | 5 +---- .../java/pulse/InstanceOfExample.java | 18 +++++++++++++++++- .../tests/codetoanalyze/java/pulse/issues.exp | 1 + 4 files changed, 21 insertions(+), 5 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 196e9b988..c302237ef 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -545,6 +545,8 @@ module Term = struct match op with | VarSubst v' when not (Var.equal v v') -> IsInstanceOf (v', typ) + | QSubst q when Q.is_zero q -> + zero | QSubst _ | VarSubst _ | LinSubst _ -> t in diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 5ad85e8bb..180e051cd 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -960,10 +960,7 @@ module Java = struct let res_addr = AbstractValue.mk_fresh () in match typeexpr with | Exp.Sizeof {typ} -> - let<+> astate = - PulseArithmetic.and_equal_instanceof res_addr argv typ astate - >>= PulseArithmetic.prune_positive argv - in + let<+> astate = PulseArithmetic.and_equal_instanceof res_addr argv typ astate in PulseOperations.write_id ret_id (res_addr, event :: hist) astate (* The type expr is sometimes a Var expr but this is not expected. This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *) diff --git a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java index 1cbf623e2..8a6cd587c 100644 --- a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java +++ b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java @@ -56,7 +56,7 @@ public class InstanceOfExample { } } - public void testInstanceOfNullOk() { + public void testInstanceOfNullInterOk() { Person p = new Professor(); // p is null after this call p = updatePerson(p); @@ -66,6 +66,22 @@ public class InstanceOfExample { } } + public void testInstanceOfNullIntraOk() { + Person p = null; + if (p instanceof Professor) { + Object o = null; + o.toString(); + } + } + + public void testInstanceOfNullIntraBad() { + Person p = null; + if (!(p instanceof Professor)) { + Object o = null; + o.toString(); + } + } + public void checkInstanceArray(Object array) { Object o = null; if (array instanceof int[]) { diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index ce46dc44c..992346493 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -20,6 +20,7 @@ codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapEx codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getOneIntegerWithoutCheckBad():int, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.checkInstanceArray(java.lang.Object):void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfBooleanArrayBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `void InstanceOfExample.checkInstanceArray(Object)`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfNullIntraBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfObjProfessorBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerBuiltInEqualOperatorCachedValuesOk():void, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]