From 5068956b1d54acde3a1ad2e4fc67ec7d4a1e6d14 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Tue, 6 Feb 2024 09:38:45 +0530 Subject: [PATCH] JSpecify: Reason about nullability of reads from arrays (#875) This is a continuation of #850 where the behavior of `@Nullable` annotations on the array was modified. With this PR, the aim is to allow `@Nullable` annotations on array contents **in JSpecify mode**, and to process these annotations when handling _reads_ from arrays. This PR does not handle checking writes to array elements, nor does it support reasoning about null checks on array elements in local type refinement. --------- Co-authored-by: Manu Sridharan --- .../main/java/com/uber/nullaway/NullAway.java | 15 ++++++++-- .../com/uber/nullaway/NullabilityUtil.java | 22 ++++++++++++++ .../AccessPathNullnessPropagation.java | 14 +++++++-- .../nullaway/NullAwayJSpecifyArrayTests.java | 29 +++++++++++++++++-- 4 files changed, 74 insertions(+), 6 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index a23438ad3a..b437623b29 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/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( diff --git a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java index cca114b296..b1528c40ea 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java +++ b/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 @@ public static T castToNonNull(@Nullable T obj) { } 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; + } } diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java index b68665ad0b..299645079a 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -795,8 +795,18 @@ public TransferResult visitArrayAccess( ArrayAccessNode node, TransferInput 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 diff --git a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java index 54267859fb..8141be9877 100644 --- a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java +++ b/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(