JSpecify: Modify Array Type Use Annotation Syntax (#850)

Added unit tests for annotations on array in JSpecify mode and modified
behavior.

Currently, NullAway does not support `@Nullable` annotations on array
elements (#708). Both `@Nullable String[]` and `String @Nullable []` are
currently treated identically, and NullAway considers both annotations
as the array itself might be null.

This is the first step to bring the annotation syntax in line with
JSpecify norms, which treats `@Nullable String[]` as the array elements
could be null while `String @Nullable []` implies the array itself could
be null.

After this change, NullAway completely ignores type-use annotations on array element types, such
as `@Nullable String[]`, and only considers type-use annotations in the correct position for the top-level type, i.e.,
`String @Nullable []`. This is an intermediary change, and support for
type annotations will be extended eventually. Additionally, this
**only** applies to **JSpecify mode**

Unit tests currently conform to the current behavior of NullAway after
the changes and some tests have TODOs until we support annotations on
type and are able to detect the nullability of array elements.

---------

Co-authored-by: Manu Sridharan <msridhar@gmail.com>
Co-authored-by: Lázaro Clapp <lazaro.clapp@gmail.com>

4 files changed, 153 insertions, 12 deletions

diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java
index 5d8dc83..d4ce4e8 100644
--- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java
+++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java
@@ -1962,7 +1962,8 @@ public class NullAway extends BugChecker
   }
 
   private boolean symbolHasExternalInitAnnotation(Symbol symbol) {
-    return StreamSupport.stream(NullabilityUtil.getAllAnnotations(symbol).spliterator(), false)
+    return StreamSupport.stream(
+            NullabilityUtil.getAllAnnotations(symbol, config).spliterator(), false)
         .map((anno) -> anno.getAnnotationType().toString())
         .anyMatch(config::isExternalInitClassAnnotation);
   }
@@ -2219,7 +2220,7 @@ public class NullAway extends BugChecker
   }
 
   private boolean skipDueToFieldAnnotation(Symbol fieldSymbol) {
-    return NullabilityUtil.getAllAnnotations(fieldSymbol)
+    return NullabilityUtil.getAllAnnotations(fieldSymbol, config)
         .map(anno -> anno.getAnnotationType().toString())
         .anyMatch(config::isExcludedFieldAnnotation);
   }
diff --git a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java
index ba4be9f..2a04d46 100644
--- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java
+++ b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java
@@ -180,9 +180,9 @@ public class NullabilityUtil {
    * @param symbol the symbol
    * @return all annotations on the symbol and on the type of the symbol
    */
-  public static Stream<? extends AnnotationMirror> getAllAnnotations(Symbol symbol) {
+  public static Stream<? extends AnnotationMirror> getAllAnnotations(Symbol symbol, Config config) {
     // for methods, we care about annotations on the return type, not on the method type itself
-    Stream<? extends AnnotationMirror> typeUseAnnotations = getTypeUseAnnotations(symbol);
+    Stream<? extends AnnotationMirror> typeUseAnnotations = getTypeUseAnnotations(symbol, config);
     return Stream.concat(symbol.getAnnotationMirrors().stream(), typeUseAnnotations);
   }
 
@@ -277,27 +277,44 @@ public class NullabilityUtil {
    * Gets the type use annotations on a symbol, ignoring annotations on components of the type (type
    * arguments, wildcards, etc.)
    */
-  private static Stream<? extends AnnotationMirror> getTypeUseAnnotations(Symbol symbol) {
+  private static Stream<? extends AnnotationMirror> getTypeUseAnnotations(
+      Symbol symbol, Config config) {
     Stream<Attribute.TypeCompound> rawTypeAttributes = symbol.getRawTypeAttributes().stream();
     if (symbol instanceof Symbol.MethodSymbol) {
       // for methods, we want annotations on the return type
       return rawTypeAttributes.filter(
-          (t) -> t.position.type.equals(TargetType.METHOD_RETURN) && isDirectTypeUseAnnotation(t));
+          (t) ->
+              t.position.type.equals(TargetType.METHOD_RETURN)
+                  && isDirectTypeUseAnnotation(t, config));
     } else {
       // filter for annotations directly on the type
-      return rawTypeAttributes.filter(NullabilityUtil::isDirectTypeUseAnnotation);
+      return rawTypeAttributes.filter(t -> NullabilityUtil.isDirectTypeUseAnnotation(t, config));
     }
   }
 
-  private static boolean isDirectTypeUseAnnotation(Attribute.TypeCompound t) {
+  /**
+   * Check whether a type-use annotation should be treated as applying directly to the top-level
+   * type
+   *
+   * <p>For example {@code @Nullable List<T> lst} is a direct type use annotation of {@code lst},
+   * but {@code List<@Nullable T> lst} is not.
+   *
+   * @param t the annotation and its position in the type
+   * @param config NullAway configuration
+   * @return {@code true} if the annotation should be treated as applying directly to the top-level
+   *     type, false otherwise
+   */
+  private static boolean isDirectTypeUseAnnotation(Attribute.TypeCompound t, Config config) {
     // location is a list of TypePathEntry objects, indicating whether the annotation is
     // on an array, inner type, wildcard, or type argument. If it's empty, then the
     // annotation is directly on the type.
     // We care about both annotations directly on the outer type and also those directly
     // on an inner type or array dimension, but wish to discard annotations on wildcards,
     // or type arguments.
-    // For arrays, we treat annotations on the outer type and on any dimension of the array
-    // as applying to the nullability of the array itself, not the elements.
+    // For arrays, outside JSpecify mode, we treat annotations on the outer type and on any
+    // dimension of the array as applying to the nullability of the array itself, not the elements.
+    // In JSpecify mode, annotations on array dimensions are *not* treated as applying to the
+    // top-level type, consistent with the JSpecify spec.
     // We don't allow mixing of inner types and array dimensions in the same location
     // (i.e. `Foo.@Nullable Bar []` is meaningless).
     // These aren't correct semantics for type use annotations, but a series of hacky
@@ -313,6 +330,11 @@ public class NullabilityUtil {
           locationHasInnerTypes = true;
           break;
         case ARRAY:
+          if (config.isJSpecifyMode()) {
+            // In JSpecify mode, annotations on array element types do not apply to the top-level
+            // type
+            return false;
+          }
           locationHasArray = true;
           break;
         default:
diff --git a/nullaway/src/main/java/com/uber/nullaway/Nullness.java b/nullaway/src/main/java/com/uber/nullaway/Nullness.java
index c1b8198..845d547 100644
--- a/nullaway/src/main/java/com/uber/nullaway/Nullness.java
+++ b/nullaway/src/main/java/com/uber/nullaway/Nullness.java
@@ -192,7 +192,7 @@ public enum Nullness implements AbstractValue<Nullness> {
    * Config)}
    */
   public static boolean hasNonNullAnnotation(Symbol symbol, Config config) {
-    return hasNonNullAnnotation(NullabilityUtil.getAllAnnotations(symbol), config);
+    return hasNonNullAnnotation(NullabilityUtil.getAllAnnotations(symbol, config), config);
   }
 
   /**
@@ -203,7 +203,7 @@ public enum Nullness implements AbstractValue<Nullness> {
    * Config)}
    */
   public static boolean hasNullableAnnotation(Symbol symbol, Config config) {
-    return hasNullableAnnotation(NullabilityUtil.getAllAnnotations(symbol), config);
+    return hasNullableAnnotation(NullabilityUtil.getAllAnnotations(symbol, config), config);
   }
 
   /**
diff --git a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java
new file mode 100644
index 0000000..5426785
--- /dev/null
+++ b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java
@@ -0,0 +1,118 @@
+package com.uber.nullaway;
+
+import com.google.errorprone.CompilationTestHelper;
+import java.util.Arrays;
+import org.junit.Test;
+
+public class NullAwayJSpecifyArrayTests extends NullAwayTestsBase {
+
+  @Test
+  public void arrayTopLevelAnnotationDereference() {
+    makeHelper()
+        .addSourceLines(
+            "Test.java",
+            "package com.uber;",
+            "import org.jspecify.annotations.Nullable;",
+            "class Test {",
+            "  static Integer @Nullable [] fizz = {1};",
+            "  static void foo() {",
+            "    // BUG: Diagnostic contains: dereferenced expression fizz is @Nullable",
+            "    int bar = fizz.length;",
+            "  }",
+            "  static void bar() {",
+            "    // BUG: Diagnostic contains: dereferenced expression fizz is @Nullable",
+            "    int bar = fizz[0];",
+            "  }",
+            "}")
+        .doTest();
+  }
+
+  @Test
+  public void arrayTopLevelAnnotationAssignment() {
+    makeHelper()
+        .addSourceLines(
+            "Test.java",
+            "package com.uber;",
+            "import org.jspecify.annotations.Nullable;",
+            "class Test {",
+            "  Object foo = new Object();",
+            "  void m( Integer @Nullable [] bar) {",
+            "      // BUG: Diagnostic contains: assigning @Nullable expression to @NonNull field",
+            "      foo = bar;",
+            "  }",
+            "}")
+        .doTest();
+  }
+
+  @Test
+  public void arrayContentsAnnotationDereference() {
+    makeHelper()
+        .addSourceLines(
+            "Test.java",
+            "package com.uber;",
+            "import org.jspecify.annotations.Nullable;",
+            "class Test {",
+            "  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]",
+            "      int bar = fizz[0].length();",
+            "      // OK: valid dereference since only elements of the array can be null",
+            "      foo = fizz.length;",
+            "  }",
+            "}")
+        .doTest();
+  }
+
+  @Test
+  public void arrayContentsAnnotationAssignment() {
+    makeHelper()
+        .addSourceLines(
+            "Test.java",
+            "package com.uber;",
+            "import org.jspecify.annotations.Nullable;",
+            "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",
+            "      fizz = foo[0];",
+            "      // OK: valid assignment since only elements can be null",
+            "      fizz = foo;",
+            "  }",
+            "}")
+        .doTest();
+  }
+
+  /**
+   * Currently in JSpecify mode, JSpecify syntax only applies to type-use annotations. Declaration
+   * annotations preserve their existing behavior, with annotations being treated on the top-level
+   * type. We will very likely revisit this design in the future.
+   */
+  @Test
+  public void arrayDeclarationAnnotation() {
+    makeHelper()
+        .addSourceLines(
+            "Test.java",
+            "package com.uber;",
+            "import javax.annotation.Nullable;",
+            "class Test {",
+            "  static @Nullable String [] fizz = {\"1\"};",
+            "  static Object o1 = new Object();",
+            "  static void foo() {",
+            "      // This should not report an error while using JSpecify type-use annotation",
+            "      // BUG: Diagnostic contains: assigning @Nullable expression to @NonNull field",
+            "      o1 = fizz;",
+            "      // This should not report an error while using JSpecify type-use annotation",
+            "      // BUG: Diagnostic contains: dereferenced expression fizz is @Nullable",
+            "      o1 = fizz.length;",
+            "  }",
+            "}")
+        .doTest();
+  }
+
+  private CompilationTestHelper makeHelper() {
+    return makeTestHelperWithArgs(
+        Arrays.asList(
+            "-XepOpt:NullAway:AnnotatedPackages=com.uber", "-XepOpt:NullAway:JSpecifyMode=true"));
+  }
+}