Add @DoesNotUnrefineReceiver annotation#7640
Open
mernst wants to merge 12 commits intotypetools:masterfrom
Open
Add @DoesNotUnrefineReceiver annotation#7640mernst wants to merge 12 commits intotypetools:masterfrom
@DoesNotUnrefineReceiver annotation#7640mernst wants to merge 12 commits intotypetools:masterfrom
Conversation
Contributor
📝 WalkthroughWalkthroughThis pull request introduces a new 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: 8
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In
`@checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java`:
- Around line 12-13: Fix the Javadoc typos and clarify the semantics of the
annotation element: in the Javadoc for the annotation type
DoesNotUnrefineReceiver correct "unrefinde" to "unrefined" and reword the
description of the value() element to use plural/array wording (e.g., "the
receiver's types" or "one or more receiver types" and "an array of type
qualifiers" / "the annotation elements") so it accurately describes that value()
returns an array of qualifiers rather than a singular qualifier; update the
corresponding Javadoc occurrences (including the similar text around lines
25–29) to match this corrected spelling and pluralized/array-aware phrasing.
In `@checker/src/main/java/org/checkerframework/checker/lock/LockStore.java`:
- Line 169: The comment in LockStore.java refers to the type-qualifier
"LockPosssiblyHeld" which is a typo; update the comment to use the correct name
"LockPossiblyHeld" for consistency with the actual annotation/type and related
code (e.g., LockAnnotatedTypeFactory and the LockPossiblyHeld type hierarchy).
Locate the comment mentioning LockPosssiblyHeld and replace it with
LockPossiblyHeld so documentation matches the code symbols.
In `@docs/CHANGELOG.md`:
- Around line 12-13: Changelog entry is inconsistent: update the API line to
document the actual method signature added to AnnotationProvider as
hasDoesNotUnrefineReceiver(ExecutableElement methodElement) (and mention the new
method annotation DoesNotUnrefineReceiver) so the changelog reflects the real
interface contract; ensure the exact parameter type and name ExecutableElement
methodElement are shown in the entry to avoid ambiguity.
In
`@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java`:
- Around line 272-285: The doNotUnrefineField predicate is redundant; either
remove it and pass doNotUnrefine::test into updateFieldValuesForMethodCall or
broaden updateFieldValuesForMethodCall's parameter to Predicate<? super
FieldAccess> so you can pass doNotUnrefine directly; update the call site in
CFAbstractStore (replace doNotUnrefineField) and adjust
updateFieldValuesForMethodCall's signature and usages to accept Predicate<?
super FieldAccess> if you choose the signature-change option.
- Around line 388-390: The Javadoc for CFAbstractStore (parameter doNotUnrefine)
contains grammar errors; update the comment to read clearly and grammatically
(e.g., "if true for a field access, don't unrefine it" and "This predicate
indicates exceptions: fields that are not updated by this method") so that the
parameter description and the following sentence are correct and consistent;
edit the Javadoc block that documents the doNotUnrefine parameter in
CFAbstractStore to apply these fixes.
In
`@framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java`:
- Around line 5868-5880: The method hasDoesNotUnrefineReceiver currently treats
an empty `@DoesNotUnrefineReceiver` value as non-matching; update the logic in
hasDoesNotUnrefineReceiver (after obtaining typeSystems via
AnnotationUtils.getElementValueArray on doesNotUnrefineReceiverValueElement) to
treat an empty typeSystems list as applying to all checkers by returning true
when typeSystems.isEmpty(); otherwise keep the existing loop over
checker.getSuppressWarningsPrefixes() to check membership and then return false
if none match. Use the existing helpers getDeclAnnotations and areSameByClass to
locate the correct annotation handling block.
In
`@javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java`:
- Around line 61-62: The Javadoc for the method in AnnotationProvider contains
duplicated wording "does not does not"; update the method's Javadoc comment to
remove the duplicate so the sentence reads "Returns true if the given method may
have side effects but does not unrefine its receiver." Locate the Javadoc above
the method declaration in class AnnotationProvider and edit the comment text
accordingly, leaving the rest of the docblock intact.
In
`@javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java`:
- Around line 90-92: Update the Javadoc in BasicAnnotationProvider that
documents the `@DoesNotUnrefineReceiver` annotation: change the incorrect element
name "values" to the correct "value" (i.e., refer to the annotation element as
"value") so the comment matches the actual annotation API used by methods like
those in BasicAnnotationProvider that check for `@DoesNotUnrefineReceiver`.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 4deb6027-a139-4c0d-91f8-04817984db32
📒 Files selected for processing (8)
checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.javachecker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.javachecker/src/main/java/org/checkerframework/checker/lock/LockStore.javadocs/CHANGELOG.mdframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.javajavacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.javajavacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java
checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java
Outdated
Show resolved
Hide resolved
checker/src/main/java/org/checkerframework/checker/lock/LockStore.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
Show resolved
Hide resolved
javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java
Outdated
Show resolved
Hide resolved
javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java
Show resolved
Hide resolved
Contributor
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (1)
checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java (1)
25-29:⚠️ Potential issue | 🟡 MinorPluralize the
@returnJavadoc to matchString[] value().Line 28 still describes a singular checker name, but
value()returns an array. Please use plural wording for consistency with Line 25 and the method signature.📝 Suggested doc patch
- * `@return` the name of the checker that this annotation affects + * `@return` the names of the checkers that this annotation affects🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java` around lines 25 - 29, Update the Javadoc for the annotation's value() method in DoesNotUnrefineReceiver.java to use plural wording: change the `@return` text from a singular "the name of the checker that this annotation affects" to a plural form such as "the names of the checkers that this annotation affects" (or "the checkers affected by this annotation") so it matches the String[] return type and the class-level wording.
🤖 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/framework/flow/CFAbstractStore.java`:
- Around line 267-269: The code clears thisValue whenever
sideEffectsUnrefineAliases is true except when receiverJe is a ThisReference,
but it also needs to preserve thisValue for SuperReference (since annotated
super.method() uses the same backing store); update the conditional in
CFAbstractStore around sideEffectsUnrefineAliases to exempt both ThisReference
and SuperReference (i.e., check receiverJe instanceof ThisReference ||
receiverJe instanceof SuperReference) so thisValue is not nulled for super
calls.
In
`@framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java`:
- Around line 1391-1392: The unlabeled boolean arguments in the second
analyze(...) call should be replaced with the same labeled-argument style used
earlier to improve readability; update the analyze(...) invocation (the one
currently passing true, true) to use /* isInitializationCode= */ true and /*
updateInitializationStore= */ true so it matches the first analyze(...) call in
GenericAnnotatedTypeFactory and makes the purpose of each flag explicit.
---
Duplicate comments:
In
`@checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java`:
- Around line 25-29: Update the Javadoc for the annotation's value() method in
DoesNotUnrefineReceiver.java to use plural wording: change the `@return` text from
a singular "the name of the checker that this annotation affects" to a plural
form such as "the names of the checkers that this annotation affects" (or "the
checkers affected by this annotation") so it matches the String[] return type
and the class-level wording.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 3a73dccf-9ac6-4be3-8934-ee85b09e7afc
📒 Files selected for processing (5)
checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.javajavacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.javajavacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java
Show resolved
Hide resolved
…AbstractStore.java Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
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/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java`:
- Around line 247-254: The current doNotUnrefine predicate preserves any
receiver expression that equals receiverJe, which unsafely keeps unstable
receivers (ArrayAccess, MethodCall, FieldAccess chains) and can leave stale
facts; modify the logic that computes receiverJe and doNotUnrefine to only grant
the exemption when the receiver is a stable form: create or call
isStableReceiverExpression(Node receiver) and set receiverJe =
hasDoesNotUnrefineReceiver && isStableReceiverExpression(receiver) ?
JavaExpression.fromNode(receiver) : null, and keep doNotUnrefine = receiverJe !=
null ? je -> je.equals(receiverJe) : je -> false; ensure
isStableReceiverExpression rejects ArrayAccess and MethodCall (and any
lookup-varying forms) so those receivers fall back to the existing invalidation
logic; apply the same change to the other doNotUnrefine sites in this class (the
other occurrences noted).
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 101a627d-91a9-49b2-ae7d-34103a97bc59
📒 Files selected for processing (1)
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Show resolved
Hide resolved
Contributor
There was a problem hiding this comment.
♻️ Duplicate comments (2)
framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java (1)
1399-1408: 🧹 Nitpick | 🔵 TrivialApply the same labeled-argument style in the sibling
analyze(...)call.
true, truein this call is still unlabeled, so readability is inconsistent within the same method.♻️ Suggested consistency update
ControlFlowGraph cfg = analyze( classQueue, lambdaQueue, new CFGStatement(b, ct), fieldValues, null, - true, - true, + /* isInitializationCode= */ true, + /* updateInitializationStore= */ true, b.isStatic(), capturedStore);🤖 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/type/GenericAnnotatedTypeFactory.java` around lines 1399 - 1408, The analyze(...) call that starts with new CFGStatement(b, ct) passes two unlabeled boolean literals ("true, true"), which breaks consistency with the sibling call; update that invocation to use the same labeled-argument style used by the other analyze(...) call by replacing those two positional booleans with the corresponding named parameters from analyze's signature (use the exact parameter names used in the sibling analyze call so the call reads like analyze(classQueue, lambdaQueue, new CFGStatement(b, ct), fieldValues, null, <paramName1>: true, <paramName2>: true, b.isStatic(), capturedStore)).framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java (1)
5865-5881:⚠️ Potential issue | 🟠 MajorHandle empty
@DoesNotUnrefineReceivervalue as “applies to all checkers.”On Lines 5869-5877, an empty
typeSystemslist currently falls through toreturn false. This rejects@DoesNotUnrefineReceiver({}), which should apply universally.💡 Proposed fix
`@Override` public boolean hasDoesNotUnrefineReceiver(ExecutableElement methodElement) { for (AnnotationMirror am : getDeclAnnotations(methodElement)) { if (areSameByClass(am, org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver.class)) { List<String> typeSystems = AnnotationUtils.getElementValueArray( am, doesNotUnrefineReceiverValueElement, String.class); + if (typeSystems.isEmpty()) { + return true; + } for (String prefix : checker.getSuppressWarningsPrefixes()) { if (typeSystems.contains(prefix)) { return true; } } return false; } } return false; }🤖 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/type/AnnotatedTypeFactory.java` around lines 5865 - 5881, The method hasDoesNotUnrefineReceiver currently treats an empty List returned from AnnotationUtils.getElementValueArray (from the `@DoesNotUnrefineReceiver` annotation) as “does not apply”, but an empty value should mean “applies to all checkers”; in hasDoesNotUnrefineReceiver, after obtaining typeSystems from AnnotationUtils.getElementValueArray (and before iterating checker.getSuppressWarningsPrefixes()), add a check if typeSystems.isEmpty() and return true to indicate universal applicability; keep the rest of the logic (matching prefixes via checker.getSuppressWarningsPrefixes() and returning false only when a non-empty list does not contain any prefix).
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In
`@framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java`:
- Around line 5865-5881: The method hasDoesNotUnrefineReceiver currently treats
an empty List returned from AnnotationUtils.getElementValueArray (from the
`@DoesNotUnrefineReceiver` annotation) as “does not apply”, but an empty value
should mean “applies to all checkers”; in hasDoesNotUnrefineReceiver, after
obtaining typeSystems from AnnotationUtils.getElementValueArray (and before
iterating checker.getSuppressWarningsPrefixes()), add a check if
typeSystems.isEmpty() and return true to indicate universal applicability; keep
the rest of the logic (matching prefixes via
checker.getSuppressWarningsPrefixes() and returning false only when a non-empty
list does not contain any prefix).
In
`@framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java`:
- Around line 1399-1408: The analyze(...) call that starts with new
CFGStatement(b, ct) passes two unlabeled boolean literals ("true, true"), which
breaks consistency with the sibling call; update that invocation to use the same
labeled-argument style used by the other analyze(...) call by replacing those
two positional booleans with the corresponding named parameters from analyze's
signature (use the exact parameter names used in the sibling analyze call so the
call reads like analyze(classQueue, lambdaQueue, new CFGStatement(b, ct),
fieldValues, null, <paramName1>: true, <paramName2>: true, b.isStatic(),
capturedStore)).
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 28cdfd76-0ea5-4160-94b8-b2229b736381
📒 Files selected for processing (3)
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.javaframework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java
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.
This feature is tested via
yukiyang:modifiability.