Fix RLC unsoundness with explicit @MustCallUnknown annotation#6994
Fix RLC unsoundness with explicit @MustCallUnknown annotation#6994kelloggm wants to merge 33 commits into
@MustCallUnknown annotation#6994Conversation
|
@mernst I think you should review this again to make sure that the new Also, this change could introduce user-facing behavior in the form of new warnings (as shown by the need to add those annotations). Does that warrant a changelog entry? If so, I don't mind adding one. |
|
@kelloggm CI is not passing. Could you fix that? Then I will review. |
|
@kelloggm Ping. |
There was a problem hiding this comment.
Pull Request Overview
This pull request fixes an RLC (Resource Leak Checker) unsoundness issue by adding explicit @MustCallUnknown annotations to prevent incorrect behavior when handling owning parameters with unknown must-call obligations.
- Adds proper error detection for
@Owningparameters with@MustCallUnknownannotations - Improves must-call type resolution by using hierarchy-aware annotation lookup
- Adds type annotations to initialization classes to ensure proper type checking
Reviewed Changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| DropOwning.java | New test case demonstrating the fix for issue #6990 with expected error |
| CrashForTempVar.java | Adds suppression annotation to focus testing on crash detection |
| MustCallConsistencyAnalyzer.java | Updates annotation lookup logic and fixes typo in comment |
| InitializationTransfer.java | Adds @MustCall type annotations to class declaration |
| InitializationStore.java | Adds @MustCall type annotations and improves class documentation |
…ion/InitializationStore.java Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
|
PR changed again? Review this PR in Change Stack to compare snapshots and stay oriented. No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (1)
📝 WalkthroughWalkthroughTightens Possibly related PRs
🚥 Pre-merge checks | ❌ 2❌ Failed checks (2 warnings)
✏️ 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}
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
`@checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java`:
- Around line 59-62: The generic type V in InitializationTransfer is bound as
CFAbstractValue<V> but InitializationStore is parameterized with `@MustCall`({})
V, causing an annotated type-argument mismatch; change V's bound to
CFAbstractValue<@MustCall({}) V> so the value type annotation matches
InitializationStore's value parameter (update the type parameter declaration on
class InitializationTransfer accordingly, keeping T and S as-is and preserving
references to InitializationStore and `@MustCall`).
🪄 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: 65fb28ac-d3eb-4c99-8f99-9320be6dabc6
📒 Files selected for processing (7)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.javachecker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.javachecker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.javachecker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
There was a problem hiding this comment.
♻️ Duplicate comments (1)
checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java (1)
60-60:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winAlign
V's bound withInitializationStore.Line 63 passes
@MustCall({}) VtoInitializationStore, but line 60 bindsVasCFAbstractValue<V>instead ofCFAbstractValue<@MustCall({}) V>. This creates a type-argument mismatch withInitializationStore's declaration (see context snippet), which expects the value bound to beCFAbstractValue<@MustCall({}) V>.Proposed fix
public class InitializationTransfer< - V extends CFAbstractValue<V>, + V extends CFAbstractValue<`@MustCall`({}) V>, T extends InitializationTransfer<V, T, S>, S extends InitializationStore<`@MustCall`({}) V, `@MustCall`({}) S>>🤖 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 `@checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java` at line 60, The generic type parameter V on InitializationTransfer is bounded incorrectly: change the bound from CFAbstractValue<V> to CFAbstractValue<`@MustCall`({}) V> so it matches the expected type used when constructing/using InitializationStore; update the class declaration's type parameter (InitializationTransfer<... V ...>) to use CFAbstractValue<`@MustCall`({}) V> and any related declarations that reference V to preserve the `@MustCall` annotation so InitializationStore's type-argument constraints align with CFAbstractValue<`@MustCall`({}) V>.
🤖 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.
Duplicate comments:
In
`@checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java`:
- Line 60: The generic type parameter V on InitializationTransfer is bounded
incorrectly: change the bound from CFAbstractValue<V> to
CFAbstractValue<`@MustCall`({}) V> so it matches the expected type used when
constructing/using InitializationStore; update the class declaration's type
parameter (InitializationTransfer<... V ...>) to use
CFAbstractValue<`@MustCall`({}) V> and any related declarations that reference V
to preserve the `@MustCall` annotation so InitializationStore's type-argument
constraints align with CFAbstractValue<`@MustCall`({}) V>.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: b0b83557-a0fa-4255-8fa7-32accdb89c43
📒 Files selected for processing (3)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.javachecker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.javachecker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.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
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java`:
- Around line 296-297: The Javadoc has a duplicated generic `@param` tag: it
documents both keys and values as `@param` <K>; update the second tag to `@param`
<V> to correctly document the method/type parameters K and V in SceneOps (where
the method/type declares <K, V>), ensuring the value type parameter is
documented as V rather than K.
🪄 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: 45bd2e18-19b2-466f-9e0f-712e76d638c0
📒 Files selected for processing (3)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.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)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java (1)
616-621:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winFix remaining
Main.temporaryDebugreferences (field missing inMain.java).
annotation-file-utilities/.../Main.javano longer containstemporaryDebug, but there are still manyMain.temporaryDebugusages (e.g.,IndexFileSpecification.java:522,Insertion.java:209,TreeFinder.javamultiple sites,Insertions.javamultiple sites). Restore the field or update those call sites to the new debug flag so the build doesn’t fail.🤖 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 `@annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java` around lines 616 - 621, Several files still reference Main.temporaryDebug which was removed; add back a compatible flag in Main or update all call sites to the current debug mechanism. Either restore a public static boolean temporaryDebug = false in Main (so IndexFileSpecification, Insertion, TreeFinder, Insertions continue to compile), or replace each Main.temporaryDebug usage with the new debug check (for example Main.dbug.isEnabled() or the project's canonical debug flag) across the referenced classes (IndexFileSpecification, Insertion, TreeFinder, Insertions) so the build no longer fails.
🤖 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
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java`:
- Around line 616-621: Several files still reference Main.temporaryDebug which
was removed; add back a compatible flag in Main or update all call sites to the
current debug mechanism. Either restore a public static boolean temporaryDebug =
false in Main (so IndexFileSpecification, Insertion, TreeFinder, Insertions
continue to compile), or replace each Main.temporaryDebug usage with the new
debug check (for example Main.dbug.isEnabled() or the project's canonical debug
flag) across the referenced classes (IndexFileSpecification, Insertion,
TreeFinder, Insertions) so the build no longer fails.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: a98093c0-8d74-44c2-ab4e-d117e9050e31
📒 Files selected for processing (2)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java
|
@mernst this change triggers a huge number of false positive warnings that need to be resolved via a meaningless-seeming annotation (>150) in the Checker Framework itself, so I think we need to revisit it - is this really the right fix to prevent the false negative in #6990? It will be pretty disruptive for users of the RLC who have already annotated their programs. In particular, the vast majority of the false positives are caused by this PR's interaction with the defaulting rules for generics. Consider the following example, from Before this change, neither of the two There are a lot of similar examples throughout the Checker Framework, although the most sites affected by far are in "analysis" classes that have type parameters for their Value, Store, and Analysis types. Each one of these declarations needs to be modified from (e.g.) One option would be to change the default bound on such types from top (i.e., |
|
@kelloggm Thanks for your analysis. I agree that this change requires an unacceptable number of annotations, for no gain. I don't have a suggestion, and I don't know whether generics defaulting rules would improve the situation. |
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java (1)
411-424:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winPrevent infinite loop in AST parent traversal.
At Line 415 and Line 416,
pathis not advanced forVARIABLE/METHOD, so the loop can spin forever on the same node.Proposed fix
while (path != null) { Tree leaf = path.getLeaf(); switch (leaf.getKind()) { // TODO: Is this an infinite loop if leaf is a VARIABLE or METHOD? - case VARIABLE -> varTree = (JCTree.JCVariableDecl) leaf; - case METHOD -> { - // This assignment is not used. - // methTree = (JCTree.JCMethodDecl) leaf; - } + case VARIABLE -> { + varTree = (JCTree.JCVariableDecl) leaf; + path = path.getParentPath(); + } + case METHOD -> path = path.getParentPath(); case ANNOTATION_TYPE, CLASS, ENUM, INTERFACE -> { break loop; } default -> path = path.getParentPath(); } }🤖 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 `@annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java` around lines 411 - 424, The while loop in Main.java that walks parent paths can hang because in the VARIABLE and METHOD cases you don't advance path; modify the switch handling for leaf kinds (VARIABLE / METHOD) so after setting varTree (and assigning methTree if needed) you also set path = path.getParentPath() (or otherwise advance the traversal) so the loop progresses; ensure the loop label/behaviour (break loop) remains unchanged and remove or fix the commented-out unused methTree assignment as appropriate.
🤖 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
`@checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java`:
- Around line 1510-1527: Update the comment in MustCallConsistencyAnalyzer.java
near the constructor-handling branch (the block that checks
TreeUtils.isConstructor(enclosingMethodTree)) to fix the typo: change the phrase
"owning file reassignment error" to "owning field reassignment error"; the
relevant symbols to locate the code are enclosingMethodTree,
enclosingClassElement, receiverTypeElement, lhsElement and the call to
ConstructorFirstWriteAnalysis.isFirstWriteToFieldInConstructor(node.getTree(),
lhsElement, enclosingMethodTree, cmAtf).
---
Outside diff comments:
In
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java`:
- Around line 411-424: The while loop in Main.java that walks parent paths can
hang because in the VARIABLE and METHOD cases you don't advance path; modify the
switch handling for leaf kinds (VARIABLE / METHOD) so after setting varTree (and
assigning methTree if needed) you also set path = path.getParentPath() (or
otherwise advance the traversal) so the loop progresses; ensure the loop
label/behaviour (break loop) remains unchanged and remove or fix the
commented-out unused methTree assignment as appropriate.
🪄 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: fd5c53fe-e626-4bd4-b8d9-88e8094a9cb3
📒 Files selected for processing (6)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.javachecker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
There was a problem hiding this comment.
Caution
Inline review comments failed to post. This is likely due to GitHub's internal server error or limits when posting large numbers of comments. If you are seeing this consistently it is likely a permissions issue. Please check "Moderation" -> "Code review limits" under your organization settings.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java (1)
411-424:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winPrevent infinite loop in AST parent traversal.
At Line 415 and Line 416,
pathis not advanced forVARIABLE/METHOD, so the loop can spin forever on the same node.Proposed fix
while (path != null) { Tree leaf = path.getLeaf(); switch (leaf.getKind()) { // TODO: Is this an infinite loop if leaf is a VARIABLE or METHOD? - case VARIABLE -> varTree = (JCTree.JCVariableDecl) leaf; - case METHOD -> { - // This assignment is not used. - // methTree = (JCTree.JCMethodDecl) leaf; - } + case VARIABLE -> { + varTree = (JCTree.JCVariableDecl) leaf; + path = path.getParentPath(); + } + case METHOD -> path = path.getParentPath(); case ANNOTATION_TYPE, CLASS, ENUM, INTERFACE -> { break loop; } default -> path = path.getParentPath(); } }🤖 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 `@annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java` around lines 411 - 424, The while loop in Main.java that walks parent paths can hang because in the VARIABLE and METHOD cases you don't advance path; modify the switch handling for leaf kinds (VARIABLE / METHOD) so after setting varTree (and assigning methTree if needed) you also set path = path.getParentPath() (or otherwise advance the traversal) so the loop progresses; ensure the loop label/behaviour (break loop) remains unchanged and remove or fix the commented-out unused methTree assignment as appropriate.
🤖 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
`@checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java`:
- Around line 1510-1527: Update the comment in MustCallConsistencyAnalyzer.java
near the constructor-handling branch (the block that checks
TreeUtils.isConstructor(enclosingMethodTree)) to fix the typo: change the phrase
"owning file reassignment error" to "owning field reassignment error"; the
relevant symbols to locate the code are enclosingMethodTree,
enclosingClassElement, receiverTypeElement, lhsElement and the call to
ConstructorFirstWriteAnalysis.isFirstWriteToFieldInConstructor(node.getTree(),
lhsElement, enclosingMethodTree, cmAtf).
---
Outside diff comments:
In
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java`:
- Around line 411-424: The while loop in Main.java that walks parent paths can
hang because in the VARIABLE and METHOD cases you don't advance path; modify the
switch handling for leaf kinds (VARIABLE / METHOD) so after setting varTree (and
assigning methTree if needed) you also set path = path.getParentPath() (or
otherwise advance the traversal) so the loop progresses; ensure the loop
label/behaviour (break loop) remains unchanged and remove or fix the
commented-out unused methTree assignment as appropriate.
🪄 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: fd5c53fe-e626-4bd4-b8d9-88e8094a9cb3
📒 Files selected for processing (6)
annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.javaannotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.javachecker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
🛑 Comments failed to post (1)
checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java (1)
1510-1527:
⚠️ Potential issue | 🟡 Minor | ⚡ Quick win🧩 Analysis chain
🏁 Script executed:
#!/bin/bash # Description: Verify ConstructorFirstWriteAnalysis class exists and has the expected method # Search for the class definition rg -n "class ConstructorFirstWriteAnalysis" --type java # Search for the method signature rg -n "isFirstWriteToFieldInConstructor" --type java -A 3Repository: typetools/checker-framework
Length of output: 2030
Fix typo in comment
Line 1513: change “owning file reassignment error” to “owning field reassignment error”.
📝 Fix typo
- // (If the field is not private, conservatively throw the owning file reassignment error.) + // (If the field is not private, conservatively throw the owning field reassignment error.)📝 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.} else if (TreeUtils.isConstructor(enclosingMethodTree)) { // If this assignment is the first write to the private field in this constructor, // then do not throw non-final owning field reassignment error. // (If the field is not private, conservatively throw the owning field reassignment error.) ExecutableElement elementFromDeclaration = TreeUtils.elementFromDeclaration(enclosingMethodTree); `@SuppressWarnings`("nullness:dereference.of.nullable") // a constructor has an enclosing class Element enclosingClassElement = elementFromDeclaration.getEnclosingElement(); Element receiverTypeElement = TypesUtils.getTypeElement(receiver.getType()); if (Objects.equals(enclosingClassElement, receiverTypeElement)) { VariableElement lhsElement = lhs.getElement(); if (lhsElement.getModifiers().contains(Modifier.PRIVATE) && ConstructorFirstWriteAnalysis.isFirstWriteToFieldInConstructor( node.getTree(), lhsElement, enclosingMethodTree, cmAtf)) { // Safe; first assignment in constructor. return; } }🤖 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 `@checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java` around lines 1510 - 1527, Update the comment in MustCallConsistencyAnalyzer.java near the constructor-handling branch (the block that checks TreeUtils.isConstructor(enclosingMethodTree)) to fix the typo: change the phrase "owning file reassignment error" to "owning field reassignment error"; the relevant symbols to locate the code are enclosingMethodTree, enclosingClassElement, receiverTypeElement, lhsElement and the call to ConstructorFirstWriteAnalysis.isFirstWriteToFieldInConstructor(node.getTree(), lhsElement, enclosingMethodTree, cmAtf).
fixes #6990