Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Array creation annotation checks #928

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Array creation annotation checks #928

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
13ba984
added logic to ignore nullable element type during array creation
thisisalexandercook Sep 30, 2024
04f7dc3
Merge branch 'eisop:master' into array-annotation-fix
thisisalexandercook Sep 30, 2024
beff18b
added ArrayElementAnnotation test case
thisisalexandercook Oct 1, 2024
6f8ee2a
Merge remote-tracking branch 'origin/array-annotation-fix' into array…
thisisalexandercook Oct 1, 2024
398ca37
collapsed main modifier test case into nullness test suite
thisisalexandercook Oct 1, 2024
95b896d
added checks for monotonic nonnull and polynull
thisisalexandercook Oct 3, 2024
a8351aa
added multi dimension test case
thisisalexandercook Oct 3, 2024
e7db307
Update checker/src/main/java/org/checkerframework/checker/nullness/me…
thisisalexandercook Oct 30, 2024
eb46944
Merge branch 'master' into array-annotation-fix
wmdietl Nov 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -348,7 +348,11 @@ public Void visitNewArray(NewArrayTree tree, Void p) {
componentType.getAnnotations(),
type.toString());
}

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

if (AnnotationUtils.containsSame(annotations, NULLABLE)) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.reportWarning(tree, "new.array.nullable.ignored");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, because it is not about the component type.

return super.visitNewArray(tree, p);
}

Expand Down
1 change: 1 addition & 0 deletions checker/src/main/java/org/checkerframework/checker/nullness/messages.properties
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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,
}

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
Expand Down