Issue error if top is used in a contract annotation#6429
Open
mernst wants to merge 11 commits intotypetools:masterfrom
Open
Issue error if top is used in a contract annotation#6429mernst wants to merge 11 commits intotypetools:masterfrom
mernst wants to merge 11 commits intotypetools:masterfrom
Conversation
smillst
requested changes
Jan 30, 2024
Member
smillst
left a comment
smillst
left a comment
There was a problem hiding this comment.
I still don't think these changes are right. I propose that I take over this pull request and make the changes I want.
| } | ||
| } | ||
|
|
||
| // Check for type-system specific annotations. These are the annotations that are |
Member
There was a problem hiding this comment.
It's strange that this code is reading the meta-annotations every time it encounters a declaration annotation rather than just when the checker is initialized. I want to rewrite this.
| String methodString = " on method " + executableElement.getSimpleName(); | ||
| factory | ||
| .getChecker() | ||
| .reportWarning( |
Member
There was a problem hiding this comment.
Warnings should only be issued in the BaseTypeVisitor. Specifically, this code belongs in BaseTypeVisitor#checkContractsAtMethodDeclaration.
Member
Author
|
OK, you can take over. |
Contributor
📝 WalkthroughWalkthroughThis pull request adds detection and diagnostics for contract annotations that use top-level qualifiers. ContractsFromMethod.java now issues a warning when a contract annotation is a top qualifier and throws a TypeSystemError when an enforced qualifier resolves to a top qualifier. Javadoc for PreconditionAnnotation, PostconditionAnnotation, and ConditionalPostconditionAnnotation was expanded to explain why top qualifiers are ineffective. A new message key Possibly related PRs
Suggested reviewers
🚥 Pre-merge checks | ❌ 1❌ Failed checks (1 warning)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In
`@framework/src/main/java/org/checkerframework/common/basetype/messages.properties`:
- Line 93: Update the user-facing message string for the diagnostics key
contracts.toptype by fixing the typo "qualifer" to "qualifier" so the message
reads "the top qualifier %s in contract annotation %s has no effect"; modify the
value for contracts.toptype in messages.properties (the literal string on that
key) to reflect the corrected spelling.
In
`@framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java`:
- Around line 147-166: The loop over per-expression contracts in
ContractsFromMethod causes duplicate "contracts.toptype" warnings for the same
contract annotation; fix by deduplicating before reporting: create a Set to
track seen annotations (e.g., seenAnnos) and for each T contract check if its
contract.annotation is already represented in seenAnnos (use
AnnotationUtils.containsSame to compare AnnotationMirror equality) and skip
reporting if present, otherwise add it to seenAnnos and call
factory.getChecker().reportWarning(...) as currently done; keep checks using
tops, executableElement, and the existing contract.contractAnnotation +
methodString message and the "contracts.toptype" key.
ℹ️ Review info
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (10)
annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaifchecker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.javachecker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.javachecker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.javachecker/tests/nullness/PreconditionFieldNotInStore.javaframework/src/main/java/org/checkerframework/common/basetype/messages.propertiesframework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.javaframework/tests/flow/ContractsOverridingSubtyping.javaframework/tests/flow/Postcondition.javaframework/tests/flow/Precondition.java
💤 Files with no reviewable changes (1)
- annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif
| flowexpr.parameter.not.final=parameter %s in '%s' is not effectively final (i.e., it gets re-assigned) | ||
| contracts.precondition=precondition of %s is not satisfied.%nfound : %s%nrequired: %s | ||
| contracts.postcondition=postcondition of %s is not satisfied.%nfound : %s%nrequired: %s | ||
| contracts.toptype=the top qualifer %s in contract annotation %s has no effect |
Contributor
There was a problem hiding this comment.
Fix typo in user-facing diagnostic message.
Line 93 has "qualifer" instead of "qualifier".
📝 Proposed fix
-contracts.toptype=the top qualifer %s in contract annotation %s has no effect
+contracts.toptype=the top qualifier %s in contract annotation %s has no effect📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| contracts.toptype=the top qualifer %s in contract annotation %s has no effect | |
| contracts.toptype=the top qualifier %s in contract annotation %s has no effect |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@framework/src/main/java/org/checkerframework/common/basetype/messages.properties`
at line 93, Update the user-facing message string for the diagnostics key
contracts.toptype by fixing the typo "qualifer" to "qualifier" so the message
reads "the top qualifier %s in contract annotation %s has no effect"; modify the
value for contracts.toptype in messages.properties (the literal string on that
key) to reflect the corrected spelling.
Comment on lines
+147
to
+166
| // At this point, `result` contains only framework-defined contract annotations. | ||
| Set<AnnotationMirror> tops = factory.getQualifierHierarchy().getTopAnnotations(); | ||
| for (T contract : result) { | ||
| AnnotationMirror anno = contract.annotation; | ||
| if (AnnotationUtils.containsSame(tops, anno)) { | ||
| // TODO: issue a warning on the annotation itself rather than on the method declaration. | ||
| // This requires iterating over the annotation trees on the method declaration to determine | ||
| // which one led tho the given AnnotationMirror. | ||
| if (executableElement != null) { | ||
| String methodString = " on method " + executableElement.getSimpleName(); | ||
| factory | ||
| .getChecker() | ||
| .reportWarning( | ||
| executableElement, | ||
| "contracts.toptype", | ||
| anno, | ||
| contract.contractAnnotation + methodString); | ||
| } | ||
| } | ||
| } |
Contributor
There was a problem hiding this comment.
Deduplicate contracts.toptype warnings per contract annotation.
At Line 149, iteration is over per-expression contracts, so one annotation with multiple expressions can trigger repeated identical warnings.
🔧 Proposed fix
Set<AnnotationMirror> tops = factory.getQualifierHierarchy().getTopAnnotations();
+ Set<AnnotationMirror> warnedContractAnnotations = new LinkedHashSet<>();
for (T contract : result) {
AnnotationMirror anno = contract.annotation;
- if (AnnotationUtils.containsSame(tops, anno)) {
+ if (AnnotationUtils.containsSame(tops, anno)
+ && !AnnotationUtils.containsSame(
+ warnedContractAnnotations, contract.contractAnnotation)) {
// TODO: issue a warning on the annotation itself rather than on the method declaration.
// This requires iterating over the annotation trees on the method declaration to determine
// which one led tho the given AnnotationMirror.
if (executableElement != null) {
String methodString = " on method " + executableElement.getSimpleName();
factory
.getChecker()
.reportWarning(
executableElement,
"contracts.toptype",
anno,
contract.contractAnnotation + methodString);
+ warnedContractAnnotations.add(contract.contractAnnotation);
}
}
}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| // At this point, `result` contains only framework-defined contract annotations. | |
| Set<AnnotationMirror> tops = factory.getQualifierHierarchy().getTopAnnotations(); | |
| for (T contract : result) { | |
| AnnotationMirror anno = contract.annotation; | |
| if (AnnotationUtils.containsSame(tops, anno)) { | |
| // TODO: issue a warning on the annotation itself rather than on the method declaration. | |
| // This requires iterating over the annotation trees on the method declaration to determine | |
| // which one led tho the given AnnotationMirror. | |
| if (executableElement != null) { | |
| String methodString = " on method " + executableElement.getSimpleName(); | |
| factory | |
| .getChecker() | |
| .reportWarning( | |
| executableElement, | |
| "contracts.toptype", | |
| anno, | |
| contract.contractAnnotation + methodString); | |
| } | |
| } | |
| } | |
| // At this point, `result` contains only framework-defined contract annotations. | |
| Set<AnnotationMirror> tops = factory.getQualifierHierarchy().getTopAnnotations(); | |
| Set<AnnotationMirror> warnedContractAnnotations = new LinkedHashSet<>(); | |
| for (T contract : result) { | |
| AnnotationMirror anno = contract.annotation; | |
| if (AnnotationUtils.containsSame(tops, anno) | |
| && !AnnotationUtils.containsSame( | |
| warnedContractAnnotations, contract.contractAnnotation)) { | |
| // TODO: issue a warning on the annotation itself rather than on the method declaration. | |
| // This requires iterating over the annotation trees on the method declaration to determine | |
| // which one led tho the given AnnotationMirror. | |
| if (executableElement != null) { | |
| String methodString = " on method " + executableElement.getSimpleName(); | |
| factory | |
| .getChecker() | |
| .reportWarning( | |
| executableElement, | |
| "contracts.toptype", | |
| anno, | |
| contract.contractAnnotation + methodString); | |
| warnedContractAnnotations.add(contract.contractAnnotation); | |
| } | |
| } | |
| } |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java`
around lines 147 - 166, The loop over per-expression contracts in
ContractsFromMethod causes duplicate "contracts.toptype" warnings for the same
contract annotation; fix by deduplicating before reporting: create a Set to
track seen annotations (e.g., seenAnnos) and for each T contract check if its
contract.annotation is already represented in seenAnnos (use
AnnotationUtils.containsSame to compare AnnotationMirror equality) and skip
reporting if present, otherwise add it to seenAnnos and call
factory.getChecker().reportWarning(...) as currently done; keep checks using
tops, executableElement, and the existing contract.contractAnnotation +
methodString message and the "contracts.toptype" key.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@framework/tests/flow/Postcondition.java`:
- Line 317: Rename the misleading section comment "/** *** errors for invalid
postconditions ***** */" in Postcondition.java to reflect that the tests expect
warnings rather than errors (for example change it to "/** *** warnings for
top-qualifier postconditions ***** */"); update only the comment text near the
Postcondition test cases so future maintainers won't be confused by the mismatch
between the heading and the assertions.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 99ea6df3-7f68-4fa3-99ea-af988ec6b48e
📒 Files selected for processing (3)
checker/tests/nullness/PreconditionFieldNotInStore.javaframework/tests/flow/Postcondition.javaframework/tests/flow/Precondition.java
| } | ||
| } | ||
|
|
||
| /** *** errors for invalid postconditions ***** */ |
Contributor
There was a problem hiding this comment.
Section comment says “errors” but assertions expect warnings.
Please rename the heading to avoid confusion during future maintenance (e.g., “warnings for top-qualifier postconditions”).
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@framework/tests/flow/Postcondition.java` at line 317, Rename the misleading
section comment "/** *** errors for invalid postconditions ***** */" in
Postcondition.java to reflect that the tests expect warnings rather than errors
(for example change it to "/** *** warnings for top-qualifier postconditions
***** */"); update only the comment text near the Postcondition test cases so
future maintainers won't be confused by the mismatch between the heading and the
assertions.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Merge atter #6432.