JSpecify: Reason about nullability of reads from arrays

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

@@ -85,10 +85,12 @@
 import com.sun.source.tree.WhileLoopTree;
 import com.sun.source.util.TreePath;
 import com.sun.source.util.Trees;
+import com.sun.tools.javac.code.Attribute;
 import com.sun.tools.javac.code.Symbol;
 import com.sun.tools.javac.code.Symbol.ClassSymbol;
 import com.sun.tools.javac.code.Symbol.VarSymbol;
 import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.TypeAnnotationPosition;
 import com.sun.tools.javac.processing.JavacProcessingEnvironment;
 import com.sun.tools.javac.tree.JCTree;
 import com.uber.nullaway.ErrorMessage.MessageTypes;
@@ -2309,8 +2311,6 @@
       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 +2368,25 @@
     Symbol exprSymbol = ASTHelpers.getSymbol(expr);
     boolean exprMayBeNull;
     switch (expr.getKind()) {
+      case ARRAY_ACCESS:
+        exprMayBeNull = false;
+        // TODO: export to utility method
+        if (config.isJSpecifyMode()) {
+          ArrayAccessTree arrayAccess = (ArrayAccessTree) expr;
+          ExpressionTree arrayExpr = arrayAccess.getExpression();
+          Symbol arraySymbol = ASTHelpers.getSymbol(arrayExpr);
+          if (arraySymbol != null) {
+            for (Attribute.TypeCompound t : arraySymbol.getRawTypeAttributes()) {
+              for (TypeAnnotationPosition.TypePathEntry entry : t.position.location) {
+                if (entry.tag == TypeAnnotationPosition.TypePathEntryKind.ARRAY) {
+                  exprMayBeNull = true;
+                  break;
+                }
+              }
+            }
+          }
+        }
+        break;
       case MEMBER_SELECT:
         if (exprSymbol == null) {
           throw new IllegalStateException(

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

@@ -31,8 +31,10 @@
 import com.google.errorprone.suppliers.Suppliers;
 import com.google.errorprone.util.ASTHelpers;
 import com.sun.source.tree.MethodInvocationTree;
+import com.sun.tools.javac.code.Attribute;
 import com.sun.tools.javac.code.Symbol;
 import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.TypeAnnotationPosition;
 import com.sun.tools.javac.code.TypeTag;
 import com.uber.nullaway.CodeAnnotationInfo;
 import com.uber.nullaway.Config;
@@ -794,9 +796,32 @@
   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 = defaultAssumption;
+
+    // TODO: export to utility method
+    if (config.isJSpecifyMode()) {
+      Symbol arraySymbol = ASTHelpers.getSymbol(node.getArray().getTree());
+      if (arraySymbol != null) {
+        boolean isElementNullable = false;
+        for (Attribute.TypeCompound t : arraySymbol.getRawTypeAttributes()) {
+          for (TypeAnnotationPosition.TypePathEntry entry : t.position.location) {
+            if (entry.tag == TypeAnnotationPosition.TypePathEntryKind.ARRAY) {
+              isElementNullable = true;
+              break;
+            }
+          }
+          if (isElementNullable) {
+            resultNullness = Nullness.NULLABLE;
+            break;
+          }
+        }
+      }
+    }
+
+    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(