From 13ba984602444cf39964296a4d06c6db03c1c50a Mon Sep 17 00:00:00 2001 From: Alex Cook Date: Mon, 30 Sep 2024 09:24:08 -0400 Subject: [PATCH 1/6] added logic to ignore nullable element type during array creation --- .../checker/nullness/NullnessNoInitVisitor.java | 6 +++++- .../checkerframework/checker/nullness/messages.properties | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java index bdd2be147e5..3be057456ba 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -348,7 +348,11 @@ public Void visitNewArray(NewArrayTree tree, Void p) { componentType.getAnnotations(), type.toString()); } - + List annotations = + TreeUtils.annotationsFromArrayCreation(tree, 0); + if (AnnotationUtils.containsSame(annotations, NULLABLE)) { + checker.reportWarning(tree, "new.array.nullable.ignored"); + } return super.visitNewArray(tree, p); } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties index f1ccf838bf4..e80b1f0dfd3 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties @@ -22,6 +22,7 @@ nulltest.redundant=redundant test against null; "%s" is non-null instanceof.nullable=instanceof is only true for a non-null expression instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof new.array.type.invalid=annotations %s may not be applied as component type for array "%s" +new.array.nullable.ignored=nullable annotation on array element type ignored, must be nonnull new.class.type.invalid=the annotations %s do not need be applied in object creations nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null nullness.on.enum=do not write nullness annotations on an enum constant, which is always non-null From beff18ba94d4c0f91f7e009434ab55bbf6770d40 Mon Sep 17 00:00:00 2001 From: Alex Cook Date: Tue, 1 Oct 2024 14:45:12 -0400 Subject: [PATCH 2/6] added ArrayElementAnnotation test case --- .../junit/ArrayElementAnnotationTest.java | 27 +++++++++++++++++++ .../NonNullElementAnnotation.java | 8 ++++++ 2 files changed, 35 insertions(+) create mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java create mode 100644 checker/tests/array-element-annotation/NonNullElementAnnotation.java diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java new file mode 100644 index 00000000000..e7c814434a4 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java @@ -0,0 +1,27 @@ +package org.checkerframework.checker.test.junit; + +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +import java.io.File; +import java.util.List; + +public class ArrayElementAnnotationTest extends CheckerFrameworkPerDirectoryTest { + + /** + * Create an ArrayElementAnnotationTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public ArrayElementAnnotationTest(List testFiles) { + super( + testFiles, + org.checkerframework.checker.nullness.NullnessChecker.class, + "array-element-annotation"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"array-element-annotation"}; + } +} diff --git a/checker/tests/array-element-annotation/NonNullElementAnnotation.java b/checker/tests/array-element-annotation/NonNullElementAnnotation.java new file mode 100644 index 00000000000..84d16aaddc8 --- /dev/null +++ b/checker/tests/array-element-annotation/NonNullElementAnnotation.java @@ -0,0 +1,8 @@ +import org.checkerframework.checker.nullness.qual.Nullable; + +public class NonNullElementAnnotation { + void foo() { + // :: warning: (new.array.nullable.ignored) + int[] o = new int @Nullable [10]; + } +} From 398ca37a0e1a88e2c96a6d9e0a4f2154561ba0b0 Mon Sep 17 00:00:00 2001 From: Alex Cook Date: Tue, 1 Oct 2024 17:40:44 -0400 Subject: [PATCH 3/6] collapsed main modifier test case into nullness test suite --- .../checker/nullness/messages.properties | 2 +- .../junit/ArrayElementAnnotationTest.java | 27 ------------------- .../ArrayMainModifierNullableAnnotation.java} | 2 +- 3 files changed, 2 insertions(+), 29 deletions(-) delete mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java rename checker/tests/{array-element-annotation/NonNullElementAnnotation.java => nullness/ArrayMainModifierNullableAnnotation.java} (77%) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties index e80b1f0dfd3..868ceec6645 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties @@ -22,7 +22,7 @@ nulltest.redundant=redundant test against null; "%s" is non-null instanceof.nullable=instanceof is only true for a non-null expression instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof new.array.type.invalid=annotations %s may not be applied as component type for array "%s" -new.array.nullable.ignored=nullable annotation on array element type ignored, must be nonnull +new.array.nullable.ignored=nullable annotation on new array main modifier ignored, must be nonnull new.class.type.invalid=the annotations %s do not need be applied in object creations nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null nullness.on.enum=do not write nullness annotations on an enum constant, which is always non-null diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java deleted file mode 100644 index e7c814434a4..00000000000 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/ArrayElementAnnotationTest.java +++ /dev/null @@ -1,27 +0,0 @@ -package org.checkerframework.checker.test.junit; - -import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; -import org.junit.runners.Parameterized.Parameters; - -import java.io.File; -import java.util.List; - -public class ArrayElementAnnotationTest extends CheckerFrameworkPerDirectoryTest { - - /** - * Create an ArrayElementAnnotationTest. - * - * @param testFiles the files containing test code, which will be type-checked - */ - public ArrayElementAnnotationTest(List testFiles) { - super( - testFiles, - org.checkerframework.checker.nullness.NullnessChecker.class, - "array-element-annotation"); - } - - @Parameters - public static String[] getTestDirs() { - return new String[] {"array-element-annotation"}; - } -} diff --git a/checker/tests/array-element-annotation/NonNullElementAnnotation.java b/checker/tests/nullness/ArrayMainModifierNullableAnnotation.java similarity index 77% rename from checker/tests/array-element-annotation/NonNullElementAnnotation.java rename to checker/tests/nullness/ArrayMainModifierNullableAnnotation.java index 84d16aaddc8..ce660772cbf 100644 --- a/checker/tests/array-element-annotation/NonNullElementAnnotation.java +++ b/checker/tests/nullness/ArrayMainModifierNullableAnnotation.java @@ -1,6 +1,6 @@ import org.checkerframework.checker.nullness.qual.Nullable; -public class NonNullElementAnnotation { +public class ArrayMainModifierNullableAnnotation { void foo() { // :: warning: (new.array.nullable.ignored) int[] o = new int @Nullable [10]; From 95b896dd27925708f238b965751d74ae2e3d969c Mon Sep 17 00:00:00 2001 From: Alex Cook Date: Thu, 3 Oct 2024 12:15:08 -0400 Subject: [PATCH 4/6] added checks for monotonic nonnull and polynull --- .../checker/nullness/NullnessNoInitVisitor.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java index 3be057456ba..869405c840c 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -348,9 +348,12 @@ public Void visitNewArray(NewArrayTree tree, Void p) { componentType.getAnnotations(), type.toString()); } + List annotations = TreeUtils.annotationsFromArrayCreation(tree, 0); - if (AnnotationUtils.containsSame(annotations, NULLABLE)) { + if (AnnotationUtils.containsSame(annotations, NULLABLE) + || AnnotationUtils.containsSame(annotations, MONOTONIC_NONNULL) + || AnnotationUtils.containsSame(annotations, POLYNULL)) { checker.reportWarning(tree, "new.array.nullable.ignored"); } return super.visitNewArray(tree, p); From a8351aa3032ef9e337a49d1b74e7ee0becfe451c Mon Sep 17 00:00:00 2001 From: Alex Cook Date: Thu, 3 Oct 2024 12:29:17 -0400 Subject: [PATCH 5/6] added multi dimension test case --- .../tests/nullness/ArrayComponentNullableAnnotation.java | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 checker/tests/nullness/ArrayComponentNullableAnnotation.java diff --git a/checker/tests/nullness/ArrayComponentNullableAnnotation.java b/checker/tests/nullness/ArrayComponentNullableAnnotation.java new file mode 100644 index 00000000000..366bab11984 --- /dev/null +++ b/checker/tests/nullness/ArrayComponentNullableAnnotation.java @@ -0,0 +1,7 @@ +import org.checkerframework.checker.nullness.qual.Nullable; + +public class ArrayComponentNullableAnnotation { + void foo() { + int[] @Nullable [] o = new int[10] @Nullable []; + } +} From e7db307f0a26ef7cf5fb18752e7344dbb88412f9 Mon Sep 17 00:00:00 2001 From: Alex Cook <43047600+thisisalexandercook@users.noreply.github.com> Date: Wed, 30 Oct 2024 14:28:40 -0400 Subject: [PATCH 6/6] Update checker/src/main/java/org/checkerframework/checker/nullness/messages.properties --- .../org/checkerframework/checker/nullness/messages.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties index 868ceec6645..c701fb26f61 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties @@ -22,7 +22,7 @@ nulltest.redundant=redundant test against null; "%s" is non-null instanceof.nullable=instanceof is only true for a non-null expression instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof new.array.type.invalid=annotations %s may not be applied as component type for array "%s" -new.array.nullable.ignored=nullable annotation on new array main modifier ignored, must be nonnull +new.array.nullable.ignored=array type annotation must be non-null new.class.type.invalid=the annotations %s do not need be applied in object creations nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null nullness.on.enum=do not write nullness annotations on an enum constant, which is always non-null