Type refinement at calls to @SideEffectsOnly methods - #7962
Conversation
containsAsReceiver() tests whether one expression is reached through another as a receiver. superToThis() rewrites every use of `super` as `this`.
Declare @SideEffectsOnly in checker-qual and register it as an inherited annotation, so that it can be released and the annotated JDK can use it. No checker consumes it yet. The Lock Checker deliberately ignores it: the annotation constrains which expressions a method modifies, but promises nothing about locks.
A call to a method annotated @SideEffectsOnly no longer discards every refinement, only those the annotation permits it to invalidate. The annotation is trusted here, not verified.
…mework into side-effects-only-2-6
…nto side-effects-only-2-7
…artial into side-effects-only-2-5
…AD into side-effects-only-2-7
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
📝 WalkthroughWalkthroughThis change adds 🚥 Pre-merge checks | ✅ 2 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (2 passed)
✨ 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}
There was a problem hiding this comment.
Actionable comments posted: 5
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/manual/called-methods-checker.tex`:
- Around line 222-234: The Called Methods Checker documentation must distinguish
`@SideEffectsOnly` from side-effect-free and pure annotations: explain that it
permits side effects and preserves a refinement only when its complete,
viewpoint-adapted list cannot affect the tracked expression, such as the
sock.close() fact; update docs/manual/called-methods-checker.tex lines 222-234
accordingly. Also update docs/manual/troubleshooting.tex line 350 to state that
the list must not affect currentOutgoing, including through an enclosing
expression.
In
`@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java`:
- Around line 191-199: Update getSideEffectsOnlyExpressions to derive the method
from methodInvocationNode.getTarget().getMethod() before checking or populating
sideEffectsOnlyExpressionsCache, eliminating the ambiguous method parameter from
the computation path while preserving the existing cache behavior.
In
`@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java`:
- Around line 355-370: Update mayChangeValue to use the existing alias
predicates for ArrayAccess and FieldAccess expressions, rather than relying only
on containsSyntacticEqualJavaExpression. Reuse containsModifiableAliasOf and
canAlias consistently with removeConflicting(FieldAccess, V) and
removeConflicting(ArrayAccess, V), while preserving the existing MethodCall
receiver and argument checks.
- Around line 264-272: Update thisIsSideEffected in CFAbstractStore so its
stream match treats both ThisReference and SuperReference as side-effecting
references. Keep the existing null/empty-expression behavior and
unrefinableReceiverJe exclusions unchanged.
In
`@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java`:
- Around line 1083-1084: Replace the TODO by updating constructor handling in
visitObjectCreation to invoke store.updateForMethodCall, as method-call handling
does, so constructor side effects—including `@SideEffectsOnly` invalidation and
mutations from unannotated constructors—are reflected in type refinement at new
expressions while preserving the existing processPostconditions behavior.
🪄 Autofix
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 Plus
Run ID: 8486f66e-700b-498d-ba7c-48fa8a504dc3
📒 Files selected for processing (27)
checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.javachecker/src/test/java/org/checkerframework/checker/test/junit/OptionalSideEffectsTest.javachecker/src/test/java/org/checkerframework/checker/test/junit/SideEffectsOnlyTest.javachecker/tests/lock/SideEffectsOnlyLock.javachecker/tests/nullness/SetIteratorTest.javachecker/tests/nullness/SideEffectsOnlySuper.javachecker/tests/optional-side-effects/OptionalSideEffectsLambda.javachecker/tests/optional-side-effects/OptionalSideEffectsPrecondition.javachecker/tests/sideeffectsonly/PureMethodCallRefinement.javachecker/tests/sideeffectsonly/SideEffectsMultiple.javachecker/tests/sideeffectsonly/SideEffectsOnlyField.javachecker/tests/sideeffectsonly/SideEffectsOnlyTest1.javachecker/tests/sideeffectsonly/SideEffectsOnlyTest2.javachecker/tests/sideeffectsonly/SideEffectsTest1.javachecker/tests/sideeffectsonly/StaticIteratorSE.javachecker/tests/sideeffectsonly/UnrepresentableArgument.javadocs/CHANGELOG.mddocs/manual/advanced-features.texdocs/manual/called-methods-checker.texdocs/manual/introduction.texdocs/manual/nullness-checker.texdocs/manual/purity-checker.texdocs/manual/troubleshooting.texframework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.javaframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
💤 Files with no reviewable changes (1)
- checker/tests/nullness/SetIteratorTest.java
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java (1)
359-385: 🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy liftInvalidate field and array entries that contain method-call subexpressions.
mayChangeValuefollows receiver and argument dependencies only whenexpris itself aMethodCall. A stored field such asc.getSelf().for array element such asc.getArray()[0]can also depend on a listed expression. With@SideEffectsOnly("#1.f"), the nested method-call entry can be removed while the composite field or array entry retains its refinement.Recurse through
FieldAccess.getReceiver(),ArrayAccess.getArray(), andArrayAccess.getIndex(). Add regression tests for these cases.Proposed fix
private static boolean mayChangeValue(JavaExpression expr, JavaExpression seOnlyExpr) { if (expr.containsSyntacticEqualJavaExpression(seOnlyExpr)) { return true; } + if (expr instanceof FieldAccess fieldAccess + && mayReach(seOnlyExpr, fieldAccess.getReceiver())) { + return true; + } + if (expr instanceof ArrayAccess arrayAccess + && (mayReach(seOnlyExpr, arrayAccess.getArray()) + || mayReach(seOnlyExpr, arrayAccess.getIndex()))) { + return true; + } if (expr instanceof MethodCall methodCall) {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java` around lines 359 - 385, Update mayChangeValue to recurse through composite expressions as well as MethodCall: for FieldAccess inspect its receiver, and for ArrayAccess inspect both its array and index, using mayReach or the same dependency checks. Ensure entries such as c.getSelf().f and c.getArray()[0] are invalidated when their nested method-call subexpressions may change, and add regression tests covering both cases.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In
`@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java`:
- Around line 359-385: Update mayChangeValue to recurse through composite
expressions as well as MethodCall: for FieldAccess inspect its receiver, and for
ArrayAccess inspect both its array and index, using mayReach or the same
dependency checks. Ensure entries such as c.getSelf().f and c.getArray()[0] are
invalidated when their nested method-call subexpressions may change, and add
regression tests covering both cases.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 892b2d1b-3237-4657-8153-17e90583b83b
📒 Files selected for processing (2)
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In
`@framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java`:
- Around line 4158-4212: Complete the SideEffectsOnly override enforcement by
invoking checkSideEffectsOnly() at the override-validation point before
returning the result, so the parseSideEffectsOnly and sideEffectsOnlyToString
helpers are reachable and the expected purity.sideeffectsonly.overriding
diagnostics are emitted.
🪄 Autofix
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 Plus
Run ID: 9ce15800-35d3-4d12-b96a-5fbabc0af1b5
📒 Files selected for processing (8)
checker/tests/sideeffectsonly/PureMethodCallRefinement.javachecker/tests/sideeffectsonly/SideEffectsOnlyInherit.javachecker/tests/sideeffectsonly/SideEffectsOnlyOverride.javachecker/tests/sideeffectsonly/SideEffectsOnlyParseError.javaframework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In
`@framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java`:
- Line 4173: Replace both `@SuppressWarnings` entries using the "UnusedMethod"
identifier with "PMD.UnusedPrivateMethod", including the suppression shown near
BaseTypeVisitor and the other matching suppression. Do not alter unrelated
suppressions.
🪄 Autofix
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 Plus
Run ID: f7d2244b-976d-46c6-a99b-f409df840b01
📒 Files selected for processing (1)
framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
docs/manual/introduction.tex (1)
621-629: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winRemove
SideEffectsOnlyfrom the-AcheckPurityAnnotationsdescription.The option checks purity annotations through
PurityChecker.SideEffectsOnlyhas noPurityKind, and its verifier remains deferred. Documenting it as checked can cause users to rely on an unchecked contract.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/manual/introduction.tex` around lines 621 - 629, Update the \-AcheckPurityAnnotations item in the introduction documentation to remove the \refqualclass{dataflow/qual}{SideEffectsOnly} annotation from the list of annotations whose bodies are checked. Keep the descriptions of SideEffectFree, Deterministic, and Pure unchanged.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@docs/manual/introduction.tex`:
- Around line 621-629: Update the \-AcheckPurityAnnotations item in the
introduction documentation to remove the
\refqualclass{dataflow/qual}{SideEffectsOnly} annotation from the list of
annotations whose bodies are checked. Keep the descriptions of SideEffectFree,
Deterministic, and Pure unchanged.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: a0692db6-4044-4ac1-8730-2b95387ece1f
📒 Files selected for processing (8)
checker/tests/sideeffectsonly/SideEffectsOnlyOverride.javadocs/manual/advanced-features.texdocs/manual/called-methods-checker.texdocs/manual/introduction.texdocs/manual/nullness-checker.texdocs/manual/purity-checker.texdocs/manual/troubleshooting.texframework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java
…AD into side-effects-only-2-7
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In
`@framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java`:
- Around line 815-820: Update the SideEffectsOnly annotation setup in postInit()
to pass the annotation element name "value" to sideEffectsOnlyBuilder.setValue
instead of "an arbitrary value". Keep the existing arbitrary String[] value and
addInheritedAnnotation flow unchanged.
🪄 Autofix
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 Plus
Run ID: bdbdef21-8c92-49f8-aba8-1a4b1dd054cd
📒 Files selected for processing (5)
dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpression.javaframework/src/main/java/org/checkerframework/common/basetype/messages.propertiesframework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.javaframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
|
@coderabbitai review |
✅ Action performedReview finished.
|
There was a problem hiding this comment.
🔇 Additional comments (10)
docs/manual/introduction.tex (1)
622-630: LGTM!Also applies to: 1583-1590
checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.java (2)
38-38: The PMDUnusedLocalVariablereports are false positives. The assignments toyare the assertions that exercise the refinement, so the variables must stay.Also applies to: 45-45
9-47: LGTM!framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java (2)
52-52: LGTM!Also applies to: 267-268, 729-730, 367-382, 832-835
4190-4246: LGTM!Also applies to: 4248-4283
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java (5)
98-135: LGTM!Also applies to: 181-184
186-214: LGTM!
271-295: 🩺 Stability & Availability
⚠️ Unverified finding
Sandbox verification was unavailable.Confirm that
getTreePath()is non-null for everyMethodInvocationNodethat reaches these reports.Lines 277 and 288 dereference
methodInvocationNode.getTreePath(). The comment at lines 274-275 states thatmethodInvocationNode.getTree()may be null for a call that corresponds to no AST tree, such as the desugaredIterator.next()of an enhanced for loop.addSideEffectsOnlyErrorReportedat line 314 also dereferences the tree path. If a node without a tree path can reach this code, the parse-error path and the warning path throw aNullPointerExceptioninstead of reporting a diagnostic.Confirm that
Node.getTreePath()is non-null for artificial nodes, or guard the two report sites.
216-270: LGTM!Also applies to: 296-301
309-320: 📐 Maintainability & Code Quality
⚠️ Unverified finding
Sandbox verification was unavailable.Verify that the reference comparison at line 315 passes the Interning Checker.
Line 315 compares two
CompilationUnitTreereferences with!=. The Checker Framework builds itself with the Interning Checker, and comparable deliberate identity comparisons in this codebase carry@SuppressWarnings("interning:not.interned"). If the Interning Checker runs overframework/src/main/java, this comparison needs a suppression or an@InternedDistinct-style declaration.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: cb91cea3-52d1-4b0e-bfa3-995001ce3f8e
📒 Files selected for processing (4)
checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.javadocs/manual/introduction.texframework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.javaframework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
2 participants
This pull request makes the annotations trusted; a subsequent PR will verify the annotations.