Array creation annotation checks #928

thisisalexandercook · 2024-09-30T13:40:19Z

fixes #927 , added a warning if the first dimension (element type) of array creation is annotated with nullable. Warning will inform user that this annotation has been ignored. Also added a new error message to support the warning.

Ao-senXiong · 2024-09-30T21:46:40Z

You can use fix to link this PR to the issue. https://docs.github.com/en/issues/tracking-your-work-with-issues/using-issues/linking-a-pull-request-to-an-issue#linking-a-pull-request-to-an-issue-using-a-keyword

Ao-senXiong · 2024-09-30T21:47:22Z

@thisisalexandercook Please also add test case to show the the check is implemented correctly.

Ao-senXiong · 2024-09-30T21:48:12Z

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

+                TreeUtils.annotationsFromArrayCreation(tree, 0);
+        if (AnnotationUtils.containsSame(annotations, NULLABLE)) {
+            checker.reportWarning(tree, "new.array.nullable.ignored");
+        }


can we use this error message?
new.array.type.invalid=annotations %s may not be applied as component type for array "%s"

No, because it is not about the component type.

…-annotation-fix

wmdietl

Can you also look at checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java and see why visitNewArray and visitNewClass are slightly different? Is there a reason one doesn't call super?

In a separate PR, can you also look at why we backed out fb6cb61 12 years ago? Why doesn't the simpler check work?

wmdietl · 2024-10-02T18:15:58Z

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

+        List<? extends AnnotationMirror> annotations =
+                TreeUtils.annotationsFromArrayCreation(tree, 0);
+        if (AnnotationUtils.containsSame(annotations, NULLABLE)) {


Suggested change

List<? extends AnnotationMirror> annotations =

TreeUtils.annotationsFromArrayCreation(tree, 0);

if (AnnotationUtils.containsSame(annotations, NULLABLE)) {

if (type.hasAnnotation(NULLABLE)) {

type is the type of the NewArrayTree, so wouldn't this perform the check you want?

What about @PolyNull? Is that allowed? MonotonicNonNull?
Are some of these checks maybe in isValid?

type is holding what the annotation defaulted to (i.e. @NonNull) and I couldn't find a utility to retrieve the original @Nullable annotation (i.e. getExplicitonAnnotation() does not hold onto it), so I pull the annotations directly from the 0th dim of the tree.

Thanks for bringing up @PolyNull and @MonotonicNonNull, both suggest possible nullness so I think they should be disallowed.

checker/tests/nullness/ArrayMainModifierNullableAnnotation.java

wmdietl · 2024-10-02T19:40:44Z

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


Should we have a similar warning for object and array creations?
On the other hand, there is the -AwarnRedundantAnnotations option... so should we remove the special case for instanceof? If needed, please file a new issue for this.

I think it makes sense to move instanceof.nonnull.redundant to an -AwarnRedundantAnnotations flagged warning. When testing this flag I also noticed redundancy on enum isn't under this option either but is noted to be in testcase below. Will file an issue to move both of these and also do a check it see if there are any others.

checker-framework/checker/tests/nullness-warnredundantannotations/RedundantAnnotation.java

Lines 33 to 38 in 33399f9

enum InnerEnum {

// TODO :: warning: (redundant.anno)

// :: error: (nullness.on.enum)

@NonNull EXPLICIT,

IMPLICIT,

}

wmdietl · 2024-10-02T20:47:40Z

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

+                TreeUtils.annotationsFromArrayCreation(tree, 0);
+        if (AnnotationUtils.containsSame(annotations, NULLABLE)) {
+            checker.reportWarning(tree, "new.array.nullable.ignored");
+        }


No, because it is not about the component type.

checker/src/main/java/org/checkerframework/checker/nullness/messages.properties

thisisalexandercook · 2024-10-29T18:03:27Z

Can you also look at checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java and see why visitNewArray and visitNewClass are slightly different? Is there a reason one doesn't call super?

visitNewArray overrides a method in the PropagationTreeAnnotator class that looks at context and ensures consistent annotation on component types, whereas visitNewClass overrides the default method from SimpleTreeVisitor as it doesn't have a propagation method, so calling super here wouldn't do much.

…ssages.properties

wmdietl

Thanks! Let's discuss the error key some more.
Also, please add a changelog entry and see whether a note somewhere in the manual would be good.

wmdietl · 2024-11-08T01:18:55Z

checker/src/main/java/org/checkerframework/checker/nullness/messages.properties

+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


Suggested change

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

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.new.array=do not write nullness annotations on an array creation, which is always non-null

What do you think of using this key? It would follow the existing nullness.on errors.
All of these should be split into the invalid use of @Nullable and the redundant use of @NonNull #966.

An alternative would be to go with the earlier suggestion of new.array.type.invalid and split that up/reword to allow errors on the created object or the component type.
In general, it would probably have been nicer to consistently use xxx.type.invalid for all of these...

The new ignored category I don't like so much - we should just raise an error for the misuse of @Nullable and not ignore it.

wmdietl · 2024-11-08T01:20:36Z

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

@@ -349,6 +349,13 @@ public Void visitNewArray(NewArrayTree tree, Void p) {
                    type.toString());
        }

+        List<? extends AnnotationMirror> annotations =
+                TreeUtils.annotationsFromArrayCreation(tree, 0);


Can you add a comment why this doesn't use type? That is already the type of the array creation. Was it because @PolyNull would already be substituted?

wmdietl · 2024-11-08T01:21:07Z

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

+        if (AnnotationUtils.containsSame(annotations, NULLABLE)
+                || AnnotationUtils.containsSame(annotations, MONOTONIC_NONNULL)
+                || AnnotationUtils.containsSame(annotations, POLYNULL)) {
+            checker.reportWarning(tree, "new.array.nullable.ignored");


Suggested change

checker.reportWarning(tree, "new.array.nullable.ignored");

checker.reportError(tree, "new.array.nullable.ignored");

Related to the discussion of the error key, the other nullness.on messages are errors.

wmdietl · 2024-11-08T01:42:27Z

checker/tests/nullness/ArrayMainModifierNullableAnnotation.java

@@ -0,0 +1,8 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class ArrayMainModifierNullableAnnotation {


I would probably put the two test cases into one file and name it ArrayCreation or something like that.

thisisalexandercook and others added 2 commits September 30, 2024 09:24

added logic to ignore nullable element type during array creation

13ba984

Merge branch 'eisop:master' into array-annotation-fix

04f7dc3

Ao-senXiong suggested changes Sep 30, 2024

View reviewed changes

thisisalexandercook added 3 commits October 1, 2024 14:45

added ArrayElementAnnotation test case

beff18b

Merge remote-tracking branch 'origin/array-annotation-fix' into array…

6f8ee2a

…-annotation-fix

collapsed main modifier test case into nullness test suite

398ca37

Ao-senXiong requested a review from wmdietl October 2, 2024 03:58

Ao-senXiong assigned wmdietl Oct 2, 2024

wmdietl changed the title ~~Array element nullable annotation warning~~ Array creation annotation checks Oct 2, 2024

wmdietl requested changes Oct 2, 2024

View reviewed changes

wmdietl assigned thisisalexandercook and unassigned wmdietl Oct 2, 2024

thisisalexandercook added 2 commits October 3, 2024 12:15

added checks for monotonic nonnull and polynull

95b896d

added multi dimension test case

a8351aa

Update checker/src/main/java/org/checkerframework/checker/nullness/me…

e7db307

…ssages.properties

thisisalexandercook requested a review from wmdietl October 30, 2024 18:29

thisisalexandercook mentioned this pull request Nov 3, 2024

Move all redundant annotation warnings to -AwarnRedundantAnnotations #966

Open

Merge branch 'master' into array-annotation-fix

eb46944

wmdietl requested changes Nov 8, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Array creation annotation checks #928

Array creation annotation checks #928

thisisalexandercook commented Sep 30, 2024 •

edited

Loading

Ao-senXiong commented Sep 30, 2024

Ao-senXiong commented Sep 30, 2024

Ao-senXiong Sep 30, 2024

wmdietl Oct 2, 2024

wmdietl left a comment

wmdietl Oct 2, 2024

wmdietl Oct 2, 2024

thisisalexandercook Oct 3, 2024

wmdietl Oct 2, 2024

thisisalexandercook Oct 30, 2024

wmdietl Oct 2, 2024

thisisalexandercook commented Oct 29, 2024

wmdietl left a comment

wmdietl Nov 8, 2024

wmdietl Nov 8, 2024

wmdietl Nov 8, 2024

wmdietl Nov 8, 2024

		@@ -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

	enum InnerEnum {
	// TODO :: warning: (redundant.anno)
	// :: error: (nullness.on.enum)
	@NonNull EXPLICIT,
	IMPLICIT,
	}

	checker.reportWarning(tree, "new.array.nullable.ignored");
	checker.reportError(tree, "new.array.nullable.ignored");

		@@ -0,0 +1,8 @@
		import org.checkerframework.checker.nullness.qual.Nullable;

		public class ArrayMainModifierNullableAnnotation {

Array creation annotation checks #928

Are you sure you want to change the base?

Array creation annotation checks #928

Conversation

thisisalexandercook commented Sep 30, 2024 • edited Loading

Ao-senXiong commented Sep 30, 2024

Ao-senXiong commented Sep 30, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wmdietl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thisisalexandercook commented Oct 29, 2024

wmdietl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thisisalexandercook commented Sep 30, 2024 •

edited

Loading