Fix static field access

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java

@@ -361,9 +361,11 @@ public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitMethodAcces
             MethodAccessNode n, TransferInput<NullnessNoInitValue, NullnessNoInitStore> p) {
         TransferResult<NullnessNoInitValue, NullnessNoInitStore> 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());
+        // 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());
+        }
         return result;
     }
 
@@ -372,7 +374,11 @@ public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitFieldAccess
             FieldAccessNode n, TransferInput<NullnessNoInitValue, NullnessNoInitStore> p) {
         TransferResult<NullnessNoInitValue, NullnessNoInitStore> result =
                 super.visitFieldAccess(n, p);
-        makeNonNull(result, n.getReceiver());
+        // 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());
+        }
         return result;
     }
 

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)
 ~~~~~~~~~

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();
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java

@@ -24,13 +24,17 @@
  * </pre>
  */
 public class FieldAccessNode extends Node {
-
+    /** The tree of the field access. */
     protected final Tree tree;
+
+    /** The element of the accessed field. */
     protected final VariableElement element;
+
+    /** The name of the accessed field. */
     protected final String field;
-    protected final Node receiver;
 
-    // TODO: add method to get modifiers (static, access level, ..)
+    /** The receiver node of the field access. */
+    protected final Node receiver;
 
     /**
      * Creates a new FieldAccessNode.
@@ -93,7 +97,11 @@ public String toString() {
         return getReceiver() + "." + field;
     }
 
-    /** Is this a static field? */
+    /**
+     * Determine whether the field is static or not.
+     *
+     * @return whether the field is static or not
+     */
     public boolean isStatic() {
         return ElementUtils.isStatic(getElement());
     }

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;
@@ -22,12 +23,14 @@
  * </pre>
  */
 public class MethodAccessNode extends Node {
-
+    /** The tree of the method access. */
     protected final ExpressionTree tree;
+
+    /** The element of the accessed method. */
     protected final ExecutableElement method;
-    protected final Node receiver;
 
-    // TODO: add method to get modifiers (static, access level, ..)
+    /** The receiver node of the method access. */
+    protected final Node receiver;
 
     /**
      * Create a new MethodAccessNode.
@@ -90,4 +93,13 @@ public int hashCode() {
     public Collection<Node> getOperands() {
         return Collections.singletonList(receiver);
     }
+
+    /**
+     * Determine whether the method is static or not.
+     *
+     * @return whether the method is static or not
+     */
+    public boolean isStatic() {
+        return ElementUtils.isStatic(getMethod());
+    }
 }

docs/CHANGELOG.md

@@ -13,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
@@ -32,8 +36,7 @@ Changed the return types of
 
 **Closed issues:**
 
-eisop#297, eisop#376, eisop#400, eisop#532, typetools#1590.
-
+eisop#297, eisop#376, eisop#400, eisop#532, eisop#533, typetools#1590.
 
 Version 3.34.0-eisop1 (May 9, 2023)
 -----------------------------------