From 4a53079816f937cf94a048083a64acba90c52045 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Wed, 6 Dec 2023 10:21:12 -0800 Subject: [PATCH 1/9] Added functionality to handle nullability of array contents in JSpecify mode. --- .../main/java/com/uber/nullaway/NullAway.java | 18 ++++++++++++- .../nullaway/NullAwayJSpecifyArrayTests.java | 25 +++++++++++++++++-- 2 files changed, 40 insertions(+), 3 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index f7ee780e5b..af6f2483ae 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -83,10 +83,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; @@ -2283,7 +2285,21 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { // obviously null return true; case ARRAY_ACCESS: - // unsound! we cannot check for nullness of array contents yet + 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) { + return true; + } + } + } + } + } + return false; case NEW_CLASS: case NEW_ARRAY: // for string concatenation, auto-boxing diff --git a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java index 54267859fb..5cc72b330e 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,27 @@ 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 [] fizz = {\"1\"};", + " static Object foo = new Object();", + " static void foo() {", + " if (fizz != null) {", + " String s = fizz[0];", + " // TODO: This should report due to dereference of @Nullable s", + " int l = s.length();", + " }", + " }", + "}") + .doTest(); + } + private CompilationTestHelper makeHelper() { return makeTestHelperWithArgs( Arrays.asList( From 627f64e2a894ffac12b139c2536cb0402fa4bb59 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Sun, 7 Jan 2024 01:05:22 +0530 Subject: [PATCH 2/9] Update nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java Co-authored-by: Manu Sridharan --- .../test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java index 5cc72b330e..f126693062 100644 --- a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java @@ -118,7 +118,7 @@ public void arrayContentsAndTopLevelAnnotation() { "package com.uber;", "import org.jspecify.annotations.Nullable;", "class Test {", - " static @Nullable String [] fizz = {\"1\"};", + " static @Nullable String @Nullable [] fizz = {\"1\"};", " static Object foo = new Object();", " static void foo() {", " if (fizz != null) {", From e429aba29456ad4182d87d158a9ab90630c2fbd1 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Wed, 24 Jan 2024 17:41:53 +0530 Subject: [PATCH 3/9] testing alternative array_access case --- .../main/java/com/uber/nullaway/NullAway.java | 34 ++++++++++--------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index 5071e60d45..dd72c40ce6 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -2288,22 +2288,6 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { case NULL_LITERAL: // obviously null return true; - case ARRAY_ACCESS: - 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) { - return true; - } - } - } - } - } - return false; case NEW_CLASS: case NEW_ARRAY: // for string concatenation, auto-boxing @@ -2361,6 +2345,24 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { Symbol exprSymbol = ASTHelpers.getSymbol(expr); boolean exprMayBeNull; switch (expr.getKind()) { + case ARRAY_ACCESS: + exprMayBeNull = false; + 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( From 4b640ef15d6c1c79e1d4fe188bd2a2334072d8ad Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Mon, 5 Feb 2024 15:57:54 +0530 Subject: [PATCH 4/9] Updated dataflow to handle nullable array elements. --- .../AccessPathNullnessPropagation.java | 29 +++++++++++++++++-- .../nullaway/NullAwayJSpecifyArrayTests.java | 2 +- 2 files changed, 28 insertions(+), 3 deletions(-) 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..6d321ec07c 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/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 visitMethodAccess( 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 = Nullness.NONNULL; + + 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) { + break; + } + } + resultNullness = isElementNullable ? Nullness.NULLABLE : Nullness.NONNULL; + } + } + + // Update the store based on the result nullness determined above + 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 f126693062..1eac8c6ea5 100644 --- a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java @@ -123,7 +123,7 @@ public void arrayContentsAndTopLevelAnnotation() { " static void foo() {", " if (fizz != null) {", " String s = fizz[0];", - " // TODO: This should report due to dereference of @Nullable s", + " // BUG: Diagnostic contains: dereferenced expression s is @Nullable", " int l = s.length();", " }", " }", From 0af1d28e8bb3c73faf29f1100207987ad6f0e686 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Mon, 5 Feb 2024 16:02:34 +0530 Subject: [PATCH 5/9] Revert "Updated dataflow to handle nullable array elements." This reverts commit 4b640ef15d6c1c79e1d4fe188bd2a2334072d8ad. --- .../AccessPathNullnessPropagation.java | 29 ++----------------- .../nullaway/NullAwayJSpecifyArrayTests.java | 2 +- 2 files changed, 3 insertions(+), 28 deletions(-) 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 6d321ec07c..b68665ad0b 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -31,10 +31,8 @@ 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; @@ -796,32 +794,9 @@ public TransferResult visitMethodAccess( public TransferResult visitArrayAccess( ArrayAccessNode node, TransferInput input) { ReadableUpdates updates = new ReadableUpdates(); - setNonnullIfAnalyzeable(updates, node.getArray()); - - Nullness resultNullness = Nullness.NONNULL; - - 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) { - break; - } - } - resultNullness = isElementNullable ? Nullness.NULLABLE : Nullness.NONNULL; - } - } - - // Update the store based on the result nullness determined above - return updateRegularStore(resultNullness, input, updates); + // this is unsound + return updateRegularStore(defaultAssumption, 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 1eac8c6ea5..f126693062 100644 --- a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java @@ -123,7 +123,7 @@ public void arrayContentsAndTopLevelAnnotation() { " static void foo() {", " if (fizz != null) {", " String s = fizz[0];", - " // BUG: Diagnostic contains: dereferenced expression s is @Nullable", + " // TODO: This should report due to dereference of @Nullable s", " int l = s.length();", " }", " }", From 08e79e93c6faa07d7dea11e733e483b7953abe69 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Mon, 5 Feb 2024 16:12:15 +0530 Subject: [PATCH 6/9] Minor updates to logic --- .../main/java/com/uber/nullaway/NullAway.java | 1 + .../AccessPathNullnessPropagation.java | 29 +++++++++++++++++-- .../nullaway/NullAwayJSpecifyArrayTests.java | 2 +- 3 files changed, 29 insertions(+), 3 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index dd72c40ce6..ba53be91b0 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -2347,6 +2347,7 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { switch (expr.getKind()) { case ARRAY_ACCESS: exprMayBeNull = false; + // TODO: export to utility method if (config.isJSpecifyMode()) { ArrayAccessTree arrayAccess = (ArrayAccessTree) expr; ExpressionTree arrayExpr = arrayAccess.getExpression(); 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..3239b2afb0 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/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 visitMethodAccess( 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 = 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 diff --git a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java index f126693062..5a5706d7a5 100644 --- a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java @@ -123,7 +123,7 @@ public void arrayContentsAndTopLevelAnnotation() { " static void foo() {", " if (fizz != null) {", " String s = fizz[0];", - " // TODO: This should report due to dereference of @Nullable s", + " // BUG: Diagnostic contains: dereferenced expression s is @Nullable", " int l = s.length();", " }", " }", From 08aac838f7d889b5eaeb01c2b54ebc3c1fa18658 Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Mon, 5 Feb 2024 16:27:56 +0530 Subject: [PATCH 7/9] Added nullcheck case --- .../com/uber/nullaway/NullAwayJSpecifyArrayTests.java | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java index 5a5706d7a5..8141be9877 100644 --- a/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java @@ -122,9 +122,13 @@ public void arrayContentsAndTopLevelAnnotation() { " static Object foo = new Object();", " static void foo() {", " if (fizz != null) {", - " String s = fizz[0];", - " // BUG: Diagnostic contains: dereferenced expression s is @Nullable", - " int l = s.length();", + " 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();", + " }", " }", " }", "}") From 2ea7d86778b7a85fe3294f621e393722ab7c29ea Mon Sep 17 00:00:00 2001 From: Md Armughanuddin Date: Tue, 6 Feb 2024 01:55:26 +0530 Subject: [PATCH 8/9] Exported utility method and added nullable annotation check. --- .../main/java/com/uber/nullaway/NullAway.java | 12 +--------- .../com/uber/nullaway/NullabilityUtil.java | 21 ++++++++++++++++ .../AccessPathNullnessPropagation.java | 24 ++++--------------- 3 files changed, 26 insertions(+), 31 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index 09b24d2c6d..86b5613f05 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -85,12 +85,10 @@ 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; @@ -2370,20 +2368,12 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { 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; - } - } - } + exprMayBeNull = NullabilityUtil.isArrayElementNullable(arraySymbol, config); } } break; diff --git a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java index cca114b296..9914754376 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,24 @@ public static T castToNonNull(@Nullable T obj) { } return obj; } + + /** + * Checks if the given array symbol has a nullable annotation. + * + * @param arraySymbol The symbol of the array to check. + * @param config NullAway configuration. + * @return true if the array symbol has a nullable annotation, 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.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 3239b2afb0..831dac4b96 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -31,10 +31,8 @@ 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; @@ -796,31 +794,17 @@ public TransferResult visitMethodAccess( public TransferResult visitArrayAccess( ArrayAccessNode node, TransferInput input) { ReadableUpdates updates = new ReadableUpdates(); - setNonnullIfAnalyzeable(updates, node.getArray()); - - Nullness resultNullness = defaultAssumption; - - // TODO: export to utility method + Nullness resultNullness; + boolean isElementNullable = false; 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; - } - } + isElementNullable = NullabilityUtil.isArrayElementNullable(arraySymbol, config); } } + resultNullness = isElementNullable ? Nullness.NULLABLE : defaultAssumption; return updateRegularStore(resultNullness, input, updates); } From 87d3cc6bdbf1957494e348e17d749b85713028f3 Mon Sep 17 00:00:00 2001 From: Manu Sridharan Date: Mon, 5 Feb 2024 20:00:40 -0800 Subject: [PATCH 9/9] improve docs and minor fix --- nullaway/src/main/java/com/uber/nullaway/NullAway.java | 2 ++ .../src/main/java/com/uber/nullaway/NullabilityUtil.java | 7 ++++--- .../nullaway/dataflow/AccessPathNullnessPropagation.java | 1 + 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index 86b5613f05..b437623b29 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -2367,8 +2367,10 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree 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); diff --git a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java index 9914754376..b1528c40ea 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java @@ -416,17 +416,18 @@ public static T castToNonNull(@Nullable T obj) { } /** - * Checks if the given array symbol has a nullable annotation. + * 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 nullable annotation, false otherwise. + * @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.toString(), config)) { + if (Nullness.isNullableAnnotation(t.type.toString(), config)) { return true; } } 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 831dac4b96..299645079a 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -796,6 +796,7 @@ public TransferResult visitArrayAccess( ReadableUpdates updates = new ReadableUpdates(); setNonnullIfAnalyzeable(updates, node.getArray()); 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());