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.

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

Don't write irrelevant annotations in .ajava files #6254

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

Conversation

mernst
Copy link
Member

@mernst mernst commented Oct 22, 2023

No description provided.

Copy link
Contributor

@kelloggm kelloggm left a comment

Choose a reason for hiding this comment

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

Overall this is a nice change, but I have a few concerns that I think need to be addressed before it's ready to merge.

} else if (clazz.isArray()) {
throw new TypeSystemError(
"Don't use arrays other than Object[] in @RelevantJavaTypes on "
+ this.getClass().getSimpleName());
} else {
TypeMirror relevantType = TypesUtils.typeFromClass(clazz, types, elements);
relevantJavaTypes.add(types.erasure(relevantType));
TypeMirror erased = types.erasure(relevantType);
Copy link
Contributor

Choose a reason for hiding this comment

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

relevantJavaTypesNames, at least, is only used by WPI (i.e., in this PR). That means that most (all?) of this computation is wasted for non-WPI runs of the checker, which makes me a bit uncomfortable: it does not seem reasonable to slow down the checker in the non-WPI case to speed it up in the WPI case. Can we guard some of this work behind a check that WPI is actually running?

I think this will also complicate the specification of relevantJavaTypeNames, which will need to say something like "always null if WPI is not enabled"

Copy link
Member Author

Choose a reason for hiding this comment

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

There are 71 instances of extends BaseTypeChecker in the Checker Framework (excluding checkers used only for testing). Of those:

58 have 0 classes in a @RelevantJavaTypes annotation
5 have 1 class in a @RelevantJavaTypes annotation
2 have 3 classes in a @RelevantJavaTypes annotation
1 has 6 classes in a @RelevantJavaTypes annotation
1 has 8 classes in a @RelevantJavaTypes annotation
4 have 10 classes in a @RelevantJavaTypes annotation

So, I don't think this is a heavy cost, either in time to compute the strings nor in space to store the strings.
But if @smillst agrees with the efficiency concern, I will implement it.

@@ -59,13 +59,11 @@ public static void testThisInference(

public void compute5(
DependentTypesViewpointAdaptationTest this, DependentTypesViewpointAdaptationTest other) {
// :: warning: (assignment)
@SameLen("this") DependentTypesViewpointAdaptationTest myOther = other;
DependentTypesViewpointAdaptationTest myOther = other;
Copy link
Contributor

Choose a reason for hiding this comment

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

Why were these annotations removed?

If DependentTypesViewpointAdapationTest isn't being considered a relevant Java type for @SameLen at this location, I think that's a problem with either @SameLen's definition of its relevant types or with the implementation in this PR, not with this test.

Copy link
Member Author

Choose a reason for hiding this comment

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

SameLenChecker.java contains:

@RelevantJavaTypes({CharSequence.class, Object[].class, Object.class})

Is that incorrect? Why is @SameLen applicable to an arbitrary class?

Copy link
Contributor

Choose a reason for hiding this comment

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

The @RelevantJavaTypes annotation is probably incorrect. The pattern that this test is testing is documented in the manual here: https://checkerframework.org/manual/#index-annotating-fixed-size

int dotIndex = typeString.lastIndexOf('.');
if (dotIndex != -1) {
// It's a fully-qualified name. Add the simple name as well.
// TODO: This might not handle a user writing a nested class like "Map.Entry".
Copy link
Contributor

Choose a reason for hiding this comment

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

Given the TODO comments here and about handling type variables (at WholeProgramInferenceJavaParserStorage line 1100 or so), I think it's clear we need a test case for this change where an annotation's relevant Java types include at least one class like Map.Entry: it has a type parameter, and it is an inner class (and is usually referenced that way).

Probably the easiest way to test that would be to add another annotation to the AinferTestChecker with the appropriate relevant type, and a corresponding test that ensures it can be inferred in the appropriate place.

@smillst smillst assigned mernst and unassigned kelloggm and smillst Oct 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Optional checker: implicit @MaybePresent annotations are inserted in .ajava files
3 participants