From 54c3dafef8c345b2c97ca5f76cadda51a4954eaa Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Fri, 12 Feb 2021 01:09:25 -0800 Subject: [PATCH] [pulse] Modeling Java instanceof operator as returning true Summary: Modeling Java instanceof operator in Pulse. This implementation does not yet provide the proper semantics for instanceof. For now, it will always return true. This is temporary and should reduce the false positive rate. Reviewed By: da319 Differential Revision: D26317089 fbshipit-source-id: 494e3dec5 --- infer/src/pulse/PulseModels.ml | 1 + .../java/pulse/InstanceOfExample.java | 68 +++++++++++++++++++ .../tests/codetoanalyze/java/pulse/issues.exp | 2 + 3 files changed, 71 insertions(+) create mode 100644 infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index e7316135e..878581df0 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1359,6 +1359,7 @@ module ProcNameDispatcher = struct ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "next" <>$ capt_arg_payload $!--> JavaIterator.next ~desc:"Iterator.next()" + ; +match_builtin BuiltinDecl.__instanceof &--> Misc.return_positive ~desc:"instanceof" ; ( +map_context_tenv PatternMatch.Java.implements_enumeration &:: "nextElement" <>$ capt_arg_payload $!--> fun x -> diff --git a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java new file mode 100644 index 000000000..778da668e --- /dev/null +++ b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java @@ -0,0 +1,68 @@ +/* + * 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. + */ +public class InstanceOfExample { + abstract class Person {} + + class Faculty extends Person {} + + class Professor extends Faculty {} + + class Student extends Person {} + + public void testInstanceOfObjFacultyOk() { + Person p = new Professor(); + Person p2 = null; + if (p instanceof Faculty) { + p2 = new Student(); + } + p2.toString(); + } + + public Person updatePerson(Person p) { + Person new_p = null; + if (p instanceof Student) { + new_p = p; + } + + if (p instanceof Professor) { + new_p = null; + } + + return new_p; + } + + public void FP_testInstanceOfObjProfessorOk() { + Person p = new Professor(); + if (p instanceof Student) { + String x = updatePerson(p).toString(); + } + } + + public void FP_testInstanceOfObjStudentOk() { + Person p = new Student(); + Person new_p = updatePerson(p); + new_p.toString(); + } + + public Object checkInstanceArray(Object array) { + Object o = null; + if (array instanceof boolean[]) { + o = new Object(); + } + + if (array instanceof int[]) { + o.toString(); + } + + return o; + } + + public void FN_testInstanceOfArrayIntBad() { + int arr[] = new int[10]; + checkInstanceArray(arr); + } +} diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index bdb31f420..4143a5fa6 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -14,6 +14,8 @@ codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicD codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Subtype.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Subtype.foo()`,return from call to `Object DynamicDispatch$Subtype.foo()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicResolutionWithVariadicMethodBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,return from call to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Impl.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Impl.foo()`,return from call to `Object DynamicDispatch$Impl.foo()`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.FP_testInstanceOfObjProfessorOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime 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/InstanceOfExample.java, InstanceOfExample.FP_testInstanceOfObjStudentOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime 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, [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/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, 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/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodBad():void, 6, 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]