From 083ee1ea978f148145ed3048e5c1bb4fd2ad3794 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 12 Aug 2023 22:46:03 -0400 Subject: [PATCH 01/17] first attempt --- .../checker/nullness/NullnessTransfer.java | 9 +++++++-- checker/tests/nullness/EISOPIssue553.java | 10 ++++++++++ .../dataflow/cfg/node/FieldAccessNode.java | 11 +++++++++++ .../dataflow/cfg/node/MethodAccessNode.java | 11 +++++++++++ 4 files changed, 39 insertions(+), 2 deletions(-) create mode 100644 checker/tests/nullness/EISOPIssue553.java diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java index 5e594dc0cc9..1fa57a81652 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java @@ -42,6 +42,7 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; @@ -344,7 +345,9 @@ public TransferResult visitMethodAccess( TransferResult result = super.visitMethodAccess(n, p); // In contrast to the conditional makeNonNull in visitMethodInvocation, this // makeNonNull is unconditional, as the receiver is definitely non-null after the access. - makeNonNull(result, n.getReceiver()); + if (!n.getMethodModifiers().contains(Modifier.STATIC)) { + makeNonNull(result, n.getReceiver()); + } return result; } @@ -352,7 +355,9 @@ public TransferResult visitMethodAccess( public TransferResult visitFieldAccess( FieldAccessNode n, TransferInput p) { TransferResult result = super.visitFieldAccess(n, p); - makeNonNull(result, n.getReceiver()); + if (!n.getMethodModifiers().contains(Modifier.STATIC)) { + makeNonNull(result, n.getReceiver()); + } return result; } diff --git a/checker/tests/nullness/EISOPIssue553.java b/checker/tests/nullness/EISOPIssue553.java new file mode 100644 index 00000000000..2b3fecdd2fb --- /dev/null +++ b/checker/tests/nullness/EISOPIssue553.java @@ -0,0 +1,10 @@ +public class EISOPIssue553 { + static Object sfield = ""; + Object field = ""; + + public static void main(String[] args) { + EISOPIssue553 x = null; + Object o = x.sfield; + o = x.field; + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 3051ed91755..49a02d8c2c3 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -13,7 +13,9 @@ import java.util.Collection; import java.util.Collections; import java.util.Objects; +import java.util.Set; +import javax.lang.model.element.Modifier; import javax.lang.model.element.VariableElement; /** @@ -118,4 +120,13 @@ public int hashCode() { public Collection getOperands() { return Collections.singletonList(receiver); } + + /** + * Retrieves the modifiers of the method. + * + * @return the set of modifiers of the method + */ + public Set getMethodModifiers() { + return element.getModifiers(); + } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index c3e8509f42e..649c36a53a1 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -11,8 +11,10 @@ import java.util.Collection; import java.util.Collections; import java.util.Objects; +import java.util.Set; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; /** * A node for a method access, including a receiver: @@ -90,4 +92,13 @@ public int hashCode() { public Collection getOperands() { return Collections.singletonList(receiver); } + + /** + * Retrieves the modifiers of the method. + * + * @return the set of modifiers of the method + */ + public Set getMethodModifiers() { + return method.getModifiers(); + } } From cfa9c3af14773c9f1ef43df47402c91f5bf10779 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 12 Aug 2023 23:06:51 -0400 Subject: [PATCH 02/17] finish TODO --- .../checker/nullness/NullnessTransfer.java | 11 ++++++----- .../dataflow/cfg/node/FieldAccessNode.java | 8 +++++--- .../dataflow/cfg/node/MethodAccessNode.java | 12 ++++++++++-- 3 files changed, 21 insertions(+), 10 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java index 1fa57a81652..6ced439dba0 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java @@ -42,7 +42,6 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.Modifier; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; @@ -343,9 +342,9 @@ public TransferResult visitInstanceOf( public TransferResult visitMethodAccess( MethodAccessNode n, TransferInput p) { TransferResult result = super.visitMethodAccess(n, p); - // In contrast to the conditional makeNonNull in visitMethodInvocation, this - // makeNonNull is unconditional, as the receiver is definitely non-null after the access. - if (!n.getMethodModifiers().contains(Modifier.STATIC)) { + // MethodAccess makeNonNull should be conditional and only for accessing method is an + // instance method, not static method. + if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); } return result; @@ -355,7 +354,9 @@ public TransferResult visitMethodAccess( public TransferResult visitFieldAccess( FieldAccessNode n, TransferInput p) { TransferResult result = super.visitFieldAccess(n, p); - if (!n.getMethodModifiers().contains(Modifier.STATIC)) { + // FieldAccess makeNonNull should be conditional and only for accessing field is an instance + // field, not static field. + if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); } return result; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 49a02d8c2c3..9f5e11a51f4 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -32,8 +32,6 @@ public class FieldAccessNode extends Node { protected final String field; protected final Node receiver; - // TODO: add method to get modifiers (static, access level, ..) - /** * Creates a new FieldAccessNode. * @@ -95,7 +93,11 @@ public String toString() { return getReceiver() + "." + field; } - /** Is this a static field? */ + /** + * Check the field is a static or not. + * + * @return A boolean indicates whether the field is static. + */ public boolean isStatic() { return ElementUtils.isStatic(getElement()); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index 649c36a53a1..8c725053b91 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -6,6 +6,7 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; import java.util.Collection; @@ -29,8 +30,6 @@ public class MethodAccessNode extends Node { protected final ExecutableElement method; protected final Node receiver; - // TODO: add method to get modifiers (static, access level, ..) - /** * Create a new MethodAccessNode. * @@ -101,4 +100,13 @@ public Collection getOperands() { public Set getMethodModifiers() { return method.getModifiers(); } + + /** + * Check the method is a static or not. + * + * @return A boolean indicates whether the method is static. + */ + public boolean isStatic() { + return ElementUtils.isStatic(getMethod()); + } } From 0f09989f16fbcd922253d216313fda0aeb82a972 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 12 Aug 2023 23:11:22 -0400 Subject: [PATCH 03/17] refine javadoc --- .../org/checkerframework/dataflow/cfg/node/FieldAccessNode.java | 2 +- .../checkerframework/dataflow/cfg/node/MethodAccessNode.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 9f5e11a51f4..57252c217cb 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -96,7 +96,7 @@ public String toString() { /** * Check the field is a static or not. * - * @return A boolean indicates whether the field is static. + * @return a boolean indicates whether the field is static */ public boolean isStatic() { return ElementUtils.isStatic(getElement()); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index 8c725053b91..2b282f4e5fd 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -104,7 +104,7 @@ public Set getMethodModifiers() { /** * Check the method is a static or not. * - * @return A boolean indicates whether the method is static. + * @return a boolean indicates whether the method is static */ public boolean isStatic() { return ElementUtils.isStatic(getMethod()); From a4851005ef30a50d934c28c0b0f4774066111e71 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 13 Aug 2023 00:11:26 -0400 Subject: [PATCH 04/17] refine javadoc --- .../dataflow/cfg/node/FieldAccessNode.java | 8 +++++++- .../dataflow/cfg/node/MethodAccessNode.java | 6 +++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 57252c217cb..81edce046ec 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -26,10 +26,16 @@ * */ public class FieldAccessNode extends Node { - + /** The corresponding tree for fieldaccessnode. */ protected final Tree tree; + + /** The VariableElement. */ protected final VariableElement element; + + /** The name of the field accessed by the tree. */ protected final String field; + + /** The receiver node for field being accessed. */ protected final Node receiver; /** diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index 2b282f4e5fd..ecab9a55c3a 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -25,9 +25,13 @@ * */ public class MethodAccessNode extends Node { - + /** The corresponding Expression tree. */ protected final ExpressionTree tree; + + /** The ExecutatbleElement method. */ protected final ExecutableElement method; + + /** The receiver node for method being accessed. */ protected final Node receiver; /** From eb30d7b5fd056108d52438443ccb8b56793df084 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 13 Aug 2023 17:09:48 -0400 Subject: [PATCH 05/17] add error message --- checker/tests/nullness/EISOPIssue553.java | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/tests/nullness/EISOPIssue553.java b/checker/tests/nullness/EISOPIssue553.java index 2b3fecdd2fb..8b19eeb6217 100644 --- a/checker/tests/nullness/EISOPIssue553.java +++ b/checker/tests/nullness/EISOPIssue553.java @@ -5,6 +5,7 @@ public class EISOPIssue553 { public static void main(String[] args) { EISOPIssue553 x = null; Object o = x.sfield; + // :: error: (dereference.of.nullable) o = x.field; } } From 7a4d0e7a8d9f58616258ab6260b84c13f4636a2a Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 13 Aug 2023 17:12:02 -0400 Subject: [PATCH 06/17] edit the changelog --- docs/CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 96e99a77ef6..6a0dc7d074d 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -18,7 +18,7 @@ Changed the return types of **Closed issues:** -eisop#376, eisop#532. +eisop#376, eisop#532, eisop#553. Version 3.34.0-eisop1 (May 9, 2023) From 49fb4170fe9fb960459d5c6441cc462ca711fd06 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 13 Aug 2023 18:52:36 -0400 Subject: [PATCH 07/17] add header to test case --- checker/tests/nullness/EISOPIssue553.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/checker/tests/nullness/EISOPIssue553.java b/checker/tests/nullness/EISOPIssue553.java index 8b19eeb6217..c2262e0cee7 100644 --- a/checker/tests/nullness/EISOPIssue553.java +++ b/checker/tests/nullness/EISOPIssue553.java @@ -1,3 +1,6 @@ +// Test case for EISOP Issue 553: +// https://github.com/eisop/checker-framework/issues/553 + public class EISOPIssue553 { static Object sfield = ""; Object field = ""; From 3ceea9d65b7a24e97ee9a457cc03e32e9e37de92 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 13 Aug 2023 19:03:22 -0400 Subject: [PATCH 08/17] modify the cfg of issue5174 --- .../tests/nullness-extra/issue5174/Issue5174.out | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/checker/tests/nullness-extra/issue5174/Issue5174.out b/checker/tests/nullness-extra/issue5174/Issue5174.out index 7b73babfa78..694155abac4 100644 --- a/checker/tests/nullness-extra/issue5174/Issue5174.out +++ b/checker/tests/nullness-extra/issue5174/Issue5174.out @@ -513,7 +513,6 @@ Before: NullnessStore#79( 55: Before: NullnessStore#86( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -524,7 +523,6 @@ Issue5174Sub [ ClassName ] > NV{@Initialized @NonNull, Issue5174Sub, poly n 56: Before: NullnessStore#87( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -538,8 +536,6 @@ o [ LocalVariable ] 57: Before: NullnessStore#96( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@UnknownInitialization @NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -550,8 +546,6 @@ Issue5174Super [ ClassName ] > NV{@Initialized @NonNull, Issue5174Super, po 58: Before: NullnessStore#97( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@UnknownInitialization @NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -564,8 +558,6 @@ expression statement o = Issue5174Super.sf [ ExpressionStatement ] 49: Before: NullnessStore#106( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@UnknownInitialization @NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -1037,7 +1029,6 @@ Before: NullnessStore#209( 109: Before: NullnessStore#216( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -1048,7 +1039,6 @@ Issue5174Sub [ ClassName ] > NV{@Initialized @NonNull, Issue5174Sub, poly n 110: Before: NullnessStore#217( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -1062,8 +1052,6 @@ o [ LocalVariable ] 111: Before: NullnessStore#226( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@UnknownInitialization @NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -1074,8 +1062,6 @@ Issue5174Super [ ClassName ] > NV{@Initialized @NonNull, Issue5174Super, po 112: Before: NullnessStore#227( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@UnknownInitialization @NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false @@ -1088,8 +1074,6 @@ expression statement o = Issue5174Super.sf [ ExpressionStatement ] 103: Before: NullnessStore#236( o > NV{@Initialized @NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@UnknownInitialization @NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@UnknownInitialization @NonNull, Issue5174Super, poly nn/n=f/f} initialized fields = [] invariant fields = [] isPolyNullNonNull = false From ff70a6841f7f2ff8a20211367609925022f89b3e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 17 Aug 2023 14:40:13 -0400 Subject: [PATCH 09/17] resume comments --- .../checker/nullness/NullnessTransfer.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java index 6ced439dba0..15f4ec2e75f 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java @@ -342,8 +342,9 @@ public TransferResult visitInstanceOf( public TransferResult visitMethodAccess( MethodAccessNode n, TransferInput p) { TransferResult result = super.visitMethodAccess(n, p); - // MethodAccess makeNonNull should be conditional and only for accessing method is an - // instance method, not static method. + // In contrast to the makeNonNull in visitMethodInvocation, which checks the method is + // SideEffectFree or the receiver is unassignable, this makeNonNull is conditional and only + // for accessing method is an instance method, not a static method. if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); } @@ -354,8 +355,6 @@ public TransferResult visitMethodAccess( public TransferResult visitFieldAccess( FieldAccessNode n, TransferInput p) { TransferResult result = super.visitFieldAccess(n, p); - // FieldAccess makeNonNull should be conditional and only for accessing field is an instance - // field, not static field. if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); } From 4171e30c45fc40cf5aae9bc15fe28040531012a6 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 17 Aug 2023 15:52:42 -0400 Subject: [PATCH 10/17] add extra test for static method invocation --- checker/tests/nullness/EISOPIssue553.java | 14 ----------- .../tests/nullness/flow/EISOPIssue553.java | 25 +++++++++++++++++++ 2 files changed, 25 insertions(+), 14 deletions(-) delete mode 100644 checker/tests/nullness/EISOPIssue553.java create mode 100644 checker/tests/nullness/flow/EISOPIssue553.java diff --git a/checker/tests/nullness/EISOPIssue553.java b/checker/tests/nullness/EISOPIssue553.java deleted file mode 100644 index c2262e0cee7..00000000000 --- a/checker/tests/nullness/EISOPIssue553.java +++ /dev/null @@ -1,14 +0,0 @@ -// Test case for EISOP Issue 553: -// https://github.com/eisop/checker-framework/issues/553 - -public class EISOPIssue553 { - static Object sfield = ""; - Object field = ""; - - public static void main(String[] args) { - EISOPIssue553 x = null; - Object o = x.sfield; - // :: error: (dereference.of.nullable) - o = x.field; - } -} diff --git a/checker/tests/nullness/flow/EISOPIssue553.java b/checker/tests/nullness/flow/EISOPIssue553.java new file mode 100644 index 00000000000..acdf33bd716 --- /dev/null +++ b/checker/tests/nullness/flow/EISOPIssue553.java @@ -0,0 +1,25 @@ +// Test case for EISOP Issue 553: +// https://github.com/eisop/checker-framework/issues/553 +import org.checkerframework.checker.nullness.qual.Nullable; + +public class EisopIssue553 { + static @Nullable Object sfield = ""; + Object field = ""; + + static void n(Object o) { + sfield = null; + } + + public static void main(String[] args) { + EisopIssue553 x = null; + Object o = x.sfield; + // :: error: (dereference.of.nullable) + o = x.field; + if (x.sfield == null) { + return; + } + x.n(x.sfield); + // :: error: (dereference.of.nullable) + x.sfield.toString(); + } +} From ca1f4c6f90d7840726564e36ce83426adb2c62dc Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 17 Aug 2023 18:21:36 -0400 Subject: [PATCH 11/17] rename file name --- .../nullness/flow/{EISOPIssue553.java => EisopIssue553.java} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename checker/tests/nullness/flow/{EISOPIssue553.java => EisopIssue553.java} (100%) diff --git a/checker/tests/nullness/flow/EISOPIssue553.java b/checker/tests/nullness/flow/EisopIssue553.java similarity index 100% rename from checker/tests/nullness/flow/EISOPIssue553.java rename to checker/tests/nullness/flow/EisopIssue553.java From a0a1bcdb750b437c46acdb234431406be4685314 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 27 Sep 2023 15:21:13 -0400 Subject: [PATCH 12/17] change expected output --- .../tests/nullness-extra/issue5174/Issue5174.out | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/checker/tests/nullness-extra/issue5174/Issue5174.out b/checker/tests/nullness-extra/issue5174/Issue5174.out index 6eda5660b1e..ad3cd08c04d 100644 --- a/checker/tests/nullness-extra/issue5174/Issue5174.out +++ b/checker/tests/nullness-extra/issue5174/Issue5174.out @@ -1215,7 +1215,6 @@ Before: NullnessNoInitStore#326( 55: Before: NullnessNoInitStore#333( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1224,7 +1223,6 @@ Issue5174Sub [ ClassName ] > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} 56: Before: NullnessNoInitStore#334( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1236,8 +1234,6 @@ o [ LocalVariable ] 57: Before: NullnessNoInitStore#343( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1246,8 +1242,6 @@ Issue5174Super [ ClassName ] > NV{@NonNull, Issue5174Super, poly nn/n=f/f} 58: Before: NullnessNoInitStore#344( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1258,8 +1252,6 @@ expression statement o = Issue5174Super.sf [ ExpressionStatement ] 49: Before: NullnessNoInitStore#353( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1667,7 +1659,6 @@ Before: NullnessNoInitStore#456( 109: Before: NullnessNoInitStore#463( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1676,7 +1667,6 @@ Issue5174Sub [ ClassName ] > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} 110: Before: NullnessNoInitStore#464( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1688,8 +1678,6 @@ o [ LocalVariable ] 111: Before: NullnessNoInitStore#473( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1698,8 +1686,6 @@ Issue5174Super [ ClassName ] > NV{@NonNull, Issue5174Super, poly nn/n=f/f} 112: Before: NullnessNoInitStore#474( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ @@ -1710,8 +1696,6 @@ expression statement o = Issue5174Super.sf [ ExpressionStatement ] 103: Before: NullnessNoInitStore#483( o > NV{@NonNull, Object, poly nn/n=f/f} - Issue5174Sub.class > NV{@NonNull, Issue5174Sub, poly nn/n=f/f} - Issue5174Super.class > NV{@NonNull, Issue5174Super, poly nn/n=f/f} isPolyNullNonNull = false isPolyNullNull = false) ~~~~~~~~~ From 3b6d85f3b752d5fee117d3b2db44689200ab3137 Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Thu, 28 Sep 2023 13:03:05 -0400 Subject: [PATCH 13/17] Apply suggestions from code review Co-authored-by: Werner Dietl --- .../dataflow/cfg/node/MethodAccessNode.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index ecab9a55c3a..9aa21eb2d67 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -25,13 +25,13 @@ * */ public class MethodAccessNode extends Node { - /** The corresponding Expression tree. */ + /** The tree of the method access. */ protected final ExpressionTree tree; - /** The ExecutatbleElement method. */ + /** The element of the accessed method. */ protected final ExecutableElement method; - /** The receiver node for method being accessed. */ + /** The receiver node of the method access. */ protected final Node receiver; /** From 5eb68479a26e26137106e89fbddee93c456c703a Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Thu, 28 Sep 2023 13:10:03 -0400 Subject: [PATCH 14/17] Apply suggestions from code review Co-authored-by: Werner Dietl --- .../dataflow/cfg/node/FieldAccessNode.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 03d04745376..73f82d9e989 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -26,16 +26,16 @@ * */ public class FieldAccessNode extends Node { - /** The corresponding tree for fieldaccessnode. */ + /** The tree of the field access. */ protected final Tree tree; - /** The VariableElement. */ + /** The element of the accessed field. */ protected final VariableElement element; - /** The name of the field accessed by the tree. */ + /** The name of the accessed field. */ protected final String field; - /** The receiver node for field being accessed. */ + /** The receiver node of the field access. */ protected final Node receiver; /** @@ -100,9 +100,9 @@ public String toString() { } /** - * Check the field is a static or not. + * Determine whether the field is static or not. * - * @return a boolean indicates whether the field is static + * @return whether the field is static or not */ public boolean isStatic() { return ElementUtils.isStatic(getElement()); From 0f49b43335652e94719ce7a2464aedebf9f77fe0 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 28 Sep 2023 13:14:30 -0400 Subject: [PATCH 15/17] address comments --- .../checker/nullness/NullnessNoInitTransfer.java | 7 ++++--- .../dataflow/cfg/node/FieldAccessNode.java | 13 +------------ .../dataflow/cfg/node/MethodAccessNode.java | 11 ----------- 3 files changed, 5 insertions(+), 26 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java index 1638df70f0f..047728e81d8 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java @@ -361,9 +361,8 @@ public TransferResult visitMethodAcces MethodAccessNode n, TransferInput p) { TransferResult result = super.visitMethodAccess(n, p); - // In contrast to the makeNonNull in visitMethodInvocation, which checks the method is - // SideEffectFree or the receiver is unassignable, this makeNonNull is conditional and only - // for accessing method is an instance method, not a static method. + // The receiver of an instance method access is non-null. A static method access does not + // ensure that the receiver is non-null. if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); } @@ -375,6 +374,8 @@ public TransferResult visitFieldAccess FieldAccessNode n, TransferInput p) { TransferResult result = super.visitFieldAccess(n, p); + // The receiver of an instance field access is non-null. A static method access does not + // ensure that the receiver is non-null. if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 03d04745376..2323fe5650d 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -13,9 +13,7 @@ import java.util.Collection; import java.util.Collections; import java.util.Objects; -import java.util.Set; -import javax.lang.model.element.Modifier; import javax.lang.model.element.VariableElement; /** @@ -100,7 +98,7 @@ public String toString() { } /** - * Check the field is a static or not. + * Determine whether the field is a static or not. * * @return a boolean indicates whether the field is static */ @@ -128,13 +126,4 @@ public int hashCode() { public Collection getOperands() { return Collections.singletonList(receiver); } - - /** - * Retrieves the modifiers of the method. - * - * @return the set of modifiers of the method - */ - public Set getMethodModifiers() { - return element.getModifiers(); - } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index 9aa21eb2d67..50f2eb55d35 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -12,10 +12,8 @@ import java.util.Collection; import java.util.Collections; import java.util.Objects; -import java.util.Set; import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.Modifier; /** * A node for a method access, including a receiver: @@ -96,15 +94,6 @@ public Collection getOperands() { return Collections.singletonList(receiver); } - /** - * Retrieves the modifiers of the method. - * - * @return the set of modifiers of the method - */ - public Set getMethodModifiers() { - return method.getModifiers(); - } - /** * Check the method is a static or not. * From 1d05f52f9024179645dacb765c27e7fe32ff798e Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Thu, 28 Sep 2023 13:10:03 -0400 Subject: [PATCH 16/17] Apply suggestions from code review Co-authored-by: Werner Dietl address comments --- .../checker/nullness/NullnessNoInitTransfer.java | 2 +- .../dataflow/cfg/node/FieldAccessNode.java | 12 ++++++------ .../dataflow/cfg/node/MethodAccessNode.java | 4 ++-- docs/CHANGELOG.md | 4 +++- 4 files changed, 12 insertions(+), 10 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java index 047728e81d8..b1abdf13a55 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java @@ -374,7 +374,7 @@ public TransferResult visitFieldAccess FieldAccessNode n, TransferInput p) { TransferResult result = super.visitFieldAccess(n, p); - // The receiver of an instance field access is non-null. A static method access does not + // The receiver of an instance field access is non-null. A static field access does not // ensure that the receiver is non-null. if (!n.isStatic()) { makeNonNull(result, n.getReceiver()); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 2323fe5650d..1cf3af49fe3 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -24,16 +24,16 @@ * */ public class FieldAccessNode extends Node { - /** The corresponding tree for fieldaccessnode. */ + /** The tree of the field access. */ protected final Tree tree; - /** The VariableElement. */ + /** The element of the accessed field. */ protected final VariableElement element; - /** The name of the field accessed by the tree. */ + /** The name of the accessed field. */ protected final String field; - /** The receiver node for field being accessed. */ + /** The receiver node of the field access. */ protected final Node receiver; /** @@ -98,9 +98,9 @@ public String toString() { } /** - * Determine whether the field is a static or not. + * Determine whether the field is static or not. * - * @return a boolean indicates whether the field is static + * @return whether the field is static or not */ public boolean isStatic() { return ElementUtils.isStatic(getElement()); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java index 50f2eb55d35..a8ce5b71c53 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodAccessNode.java @@ -95,9 +95,9 @@ public Collection getOperands() { } /** - * Check the method is a static or not. + * Determine whether the method is static or not. * - * @return a boolean indicates whether the method is static + * @return whether the method is static or not */ public boolean isStatic() { return ElementUtils.isStatic(getMethod()); diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 047f2fae9e7..7b685d0c372 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,8 @@ Version 3.34.0-eisop2 (May ?, 2023) **User-visible changes:** +Fixed a bug in the Nullness Checker where the instance receiver is not necessarily non-null after a static method/field access. + The Initialization Checker is now separated from the Nullness Checker. To unsoundly use the Nullness Checker without initialization checking, use the new `-AassumeInitialized` command-line argument. @@ -32,7 +34,7 @@ Changed the return types of **Closed issues:** -eisop#297, eisop#376, eisop#400, eisop#532 eisop#533, typetools#1590. +eisop#297, eisop#376, eisop#400, eisop#532, eisop#533, typetools#1590. Version 3.34.0-eisop1 (May 9, 2023) ----------------------------------- From 1639bced648bb99462ed33b2abdfa910af096c1f Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Sat, 30 Sep 2023 12:51:59 -0400 Subject: [PATCH 17/17] Reword changelog --- docs/CHANGELOG.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 7b685d0c372..c911609d9b7 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,8 +3,6 @@ Version 3.34.0-eisop2 (May ?, 2023) **User-visible changes:** -Fixed a bug in the Nullness Checker where the instance receiver is not necessarily non-null after a static method/field access. - The Initialization Checker is now separated from the Nullness Checker. To unsoundly use the Nullness Checker without initialization checking, use the new `-AassumeInitialized` command-line argument. @@ -15,6 +13,10 @@ In this release, `nullness` continues to suppress warnings from the Initializati `nullnessnoinit` may be used to suppress warnings from the Nullness Checker only. A future release will make suppression behavior consistent with other checkers. +Fixed a bug in the Nullness Checker where an instance receiver is incorrectly marked non-null after +a static method or field access. This could lead to new nullness errors. The static access should be +changed to be through a class name. + **Implementation details:** Corrected the arguments to an `ObjectCreationNode` when the node refers to an