JSpecify: Reason about nullability of reads from arrays

nullaway/src/main/java/com/uber/nullaway/NullAway.java

@@ -2309,8 +2309,6 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) {
       case NULL_LITERAL:
         // obviously null
         return true;
-      case ARRAY_ACCESS:
-        // unsound!  we cannot check for nullness of array contents yet
       case NEW_CLASS:
       case NEW_ARRAY:
         // for string concatenation, auto-boxing
@@ -2368,6 +2366,19 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) {
     Symbol exprSymbol = ASTHelpers.getSymbol(expr);
     boolean exprMayBeNull;
     switch (expr.getKind()) {
+      case ARRAY_ACCESS:
+        // Outside JSpecify mode, we assume array contents are always non-null
+        exprMayBeNull = false;
+        if (config.isJSpecifyMode()) {
+          // In JSpecify mode, we check if the array element type is nullable
+          ArrayAccessTree arrayAccess = (ArrayAccessTree) expr;
+          ExpressionTree arrayExpr = arrayAccess.getExpression();
+          Symbol arraySymbol = ASTHelpers.getSymbol(arrayExpr);
+          if (arraySymbol != null) {
+            exprMayBeNull = NullabilityUtil.isArrayElementNullable(arraySymbol, config);
+          }
+        }
+        break;
       case MEMBER_SELECT:
         if (exprSymbol == null) {
           throw new IllegalStateException(

nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

@@ -41,6 +41,7 @@
 import com.sun.tools.javac.code.Symbol;
 import com.sun.tools.javac.code.TargetType;
 import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.TypeAnnotationPosition;
 import com.sun.tools.javac.code.TypeAnnotationPosition.TypePathEntry;
 import com.sun.tools.javac.code.Types;
 import com.sun.tools.javac.tree.JCTree;
@@ -413,4 +414,25 @@
     }
     return obj;
   }
+
+  /**
+   * Checks if the given array symbol has a {@code @Nullable} annotation for its elements.
+   *
+   * @param arraySymbol The symbol of the array to check.
+   * @param config NullAway configuration.
+   * @return true if the array symbol has a {@code @Nullable} annotation for its elements, false
+   *     otherwise
+   */
+  public static boolean isArrayElementNullable(Symbol arraySymbol, Config config) {
+    for (Attribute.TypeCompound t : arraySymbol.getRawTypeAttributes()) {
+      for (TypeAnnotationPosition.TypePathEntry entry : t.position.location) {
+        if (entry.tag == TypeAnnotationPosition.TypePathEntryKind.ARRAY) {
+          if (Nullness.isNullableAnnotation(t.type.toString(), config)) {
+            return true;
+          }
+        }
+      }
+    }
+    return false;
+  }
 }

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java

@@ -795,8 +795,18 @@ public TransferResult<Nullness, NullnessStore> visitArrayAccess(
       ArrayAccessNode node, TransferInput<Nullness, NullnessStore> input) {
     ReadableUpdates updates = new ReadableUpdates();
     setNonnullIfAnalyzeable(updates, node.getArray());
-    // this is unsound
-    return updateRegularStore(defaultAssumption, input, updates);
+    Nullness resultNullness;
+    // Unsoundly assume @NonNull, except in JSpecify mode where we check the type
+    boolean isElementNullable = false;
+    if (config.isJSpecifyMode()) {
+      Symbol arraySymbol = ASTHelpers.getSymbol(node.getArray().getTree());
+      if (arraySymbol != null) {
+        isElementNullable = NullabilityUtil.isArrayElementNullable(arraySymbol, config);
+      }
+    }
+
+    resultNullness = isElementNullable ? Nullness.NULLABLE : defaultAssumption;
+    return updateRegularStore(resultNullness, input, updates);
   }
 
   @Override

nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java

@@ -55,7 +55,7 @@ public void arrayContentsAnnotationDereference() {
             "  static @Nullable String [] fizz = {\"1\"};",
             "  static Object foo = new Object();",
             "  static void foo() {",
-            "      // TODO: This should report an error due to dereference of @Nullable fizz[0]",
+            "      // BUG: Diagnostic contains: dereferenced expression fizz[0] is @Nullable",
             "      int bar = fizz[0].length();",
             "      // OK: valid dereference since only elements of the array can be null",
             "      foo = fizz.length;",
@@ -74,7 +74,7 @@ public void arrayContentsAnnotationAssignment() {
             "class Test {",
             "  Object fizz = new Object();",
             "  void m( @Nullable Integer [] foo) {",
-            "      // TODO: This should report an error due to assignment of @Nullable foo[0] to @NonNull field",
+            "      // BUG: Diagnostic contains: assigning @Nullable expression to @NonNull field",
             "      fizz = foo[0];",
             "      // OK: valid assignment since only elements can be null",
             "      fizz = foo;",
@@ -110,6 +110,31 @@ public void arrayDeclarationAnnotation() {
         .doTest();
   }
 
+  @Test
+  public void arrayContentsAndTopLevelAnnotation() {
+    makeHelper()
+        .addSourceLines(
+            "Test.java",
+            "package com.uber;",
+            "import org.jspecify.annotations.Nullable;",
+            "class Test {",
+            "  static @Nullable String @Nullable [] fizz = {\"1\"};",
+            "  static Object foo = new Object();",
+            "  static void foo() {",
+            "     if (fizz != null) {",
+            "        String s = fizz[0];",
+            "        // BUG: Diagnostic contains: dereferenced expression s is @Nullable",
+            "        int l1 = s.length();",
+            "        if (s != null){",
+            "           // OK: handled by null check",
+            "           int l2 = s.length();",
+            "        }",
+            "     }",
+            "  }",
+            "}")
+        .doTest();
+  }
+
   private CompilationTestHelper makeHelper() {
     return makeTestHelperWithArgs(
         Arrays.asList(