RLC extension for resource collection#7602
RLC extension for resource collection#7602iamsanjaymalakar wants to merge 464 commits intotypetools:masterfrom
Conversation
…CreatesMustCallFor anno on enclosing method
…-framework into rlc-collections-redesign
…-framework into rlc-collections-redesign
… into rlc-collections-redesign
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
♻️ Duplicate comments (1)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java (1)
111-122:⚠️ Potential issue | 🟠 MajorMake both
addoverloads explicitly@OwningCollectionreceivers.Line 111 and Line 121 currently leave insertion receiver ownership weaker/implicit, while other mutators (
checkAdd,remove) are explicit. This creates an inconsistent ownership contract on the public insertion paths.💡 Proposed fix
- public V add(LinkedHashKeyedSet<K, V> this, V o, int conflictBehavior, int equalBehavior) { + public V add(`@OwningCollection` LinkedHashKeyedSet<K, V> this, V o, int conflictBehavior, int equalBehavior) { K key = keyer.getKeyFor(o); V old = theMap.get(key); if (old == null || (eq(o, old) ? checkAdd(equalBehavior, old) : checkAdd(conflictBehavior, old))) theMap.put(key, o); return old; } - public boolean add(`@Owning` V o) { + public boolean add(`@OwningCollection` LinkedHashKeyedSet<K, V> this, `@Owning` V o) { return add(o, THROW_EXCEPTION, IGNORE) == null; }#!/bin/bash set -euo pipefail TARGET="annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java" echo "== Mutator signatures in LinkedHashKeyedSet ==" nl -ba "$TARGET" | rg -n "public .* add\\(|public .* remove\\(|private .* checkAdd\\(" -C1 echo echo "== KeyedSet interface method signatures (for override compatibility) ==" fd -p "KeyedSet.java" annotation-file-utilities/src/main/java \ | while read -r f; do echo "-- $f" nl -ba "$f" | rg -n "add\\(|remove\\(" -C1 doneExpected result: all insertion/removal mutators in
LinkedHashKeyedSetconsistently require@OwningCollectionreceivers, and signatures remain compatible withKeyedSet.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 093f6549-bc61-47fc-85ee-156eb7fbf153
📒 Files selected for processing (1)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java
There was a problem hiding this comment.
♻️ Duplicate comments (4)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java (1)
126-127:⚠️ Potential issue | 🟠 MajorDeclare an explicit receiver qualifier on
add(@owningV o)for contract consistency.Line 126 is the only public insertion mutator without an explicit receiver qualifier. Please make the receiver explicit to keep ownership contracts consistent across mutators.
💡 Proposed fix
- public boolean add(`@Owning` V o) { + public boolean add(`@OwningCollection` LinkedHashKeyedSet<K, V> this, `@Owning` V o) { return add(o, THROW_EXCEPTION, IGNORE) == null; }#!/bin/bash # Verify receiver-qualifier consistency for mutators in LinkedHashKeyedSet. FILE="annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java" rg -nP 'public\s+(boolean|V)\s+add\s*\(|public\s+boolean\s+remove\s*\(' "$FILE" -A2 -B1 # Expected: each public mutator signature shows an explicit receiver qualifier.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java` around lines 126 - 127, The public mutator add(`@Owning` V o) is missing an explicit receiver qualifier, breaking ownership-contract consistency with other mutators; update the method signature for add to include the same explicit receiver qualifier used on other mutators (e.g. the qualifier pattern applied to remove/other insertion methods) so its ownership contract is explicit and consistent with LinkedHashKeyedSet's other public mutators (refer to the add(`@Owning` V o) method and the signatures of public remove/... methods to match the qualifier).checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java (3)
1375-1379:⚠️ Potential issue | 🟠 MajorCompare the loop-variable
Namewith.equals(...).On Line 1379,
VariableTree.getName()is aName;==relies on interning and can miss the assignment that binds the enhanced-for variable, so valid loops never resolve.Suggested fix
- isAssignmentOfLoopVariable = - iteratorVariableDeclaration.getName() == loopVariable.getName(); + isAssignmentOfLoopVariable = + iteratorVariableDeclaration.getName().equals(loopVariable.getName());Does javax.lang.model.element.Name guarantee reference equality for equal names, or should compiler code use .equals(...) / contentEquals(...) instead of ==?Based on learnings: prefer using
Name.equals(...)orObjects.equals(...)forcom.sun.source.util.Namecomparisons instead of==/!=.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java` around lines 1375 - 1379, The comparison of loop variable Names in RLCCalledMethodsAnnotatedTypeFactory uses reference equality (VariableTree.getName() == loopVariable.getName()) which can fail; change the check in the block handling AssignmentNode/VariableTree so that isAssignmentOfLoopVariable compares Names by value (e.g., call .equals(...) or use Objects.equals(...)) when comparing iteratorVariableDeclaration.getName() and loopVariable.getName() to reliably detect the enhanced-for binding; leave loopVariableNode and other logic unchanged.
1518-1534:⚠️ Potential issue | 🟠 MajorPick the latch, not the header, as
loopUpdateBlock.On Line 1533,
backEdge.targetBlockis the loop header/condition block, not the block after one full iteration. Using it makes later store reads observe pre-iteration state and can miss methods called in the body. RecordbackEdge.sourceBlockinstead.Suggested fix
- bestLoopUpdateBlock = backEdge.targetBlock; + bestLoopUpdateBlock = backEdge.sourceBlock;🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java` around lines 1518 - 1534, The loop selection stores the wrong block as the update point: in the loop scan inside RLCCalledMethodsAnnotatedTypeFactory you set bestLoopUpdateBlock to backEdge.targetBlock (the loop header/condition) which makes later reads see pre-iteration state; change the assignment to use backEdge.sourceBlock (the latch/block that flows back into the header) so bestLoopUpdateBlock (and ultimately loopUpdateBlock) points to the post-iteration update location; update any related comments to reflect that WhileLoopResolutionCache.BlockEdge.sourceBlock is the intended latch.
383-397:⚠️ Potential issue | 🟠 MajorLambda-body collection loops are still dropped before lambda analysis.
Lines 517-535 deliberately defer lambda CFGs to later iterations, but the loop-state map is still keyed only by
MethodTree.getMethodCollectionLoopState(...)/removeMethodCollectionLoopState(...)returnnullforUnderlyingAST.Kind.LAMBDA, andanalyzeResolvedPotentiallyFulfillingCollectionLoops(...)only processes loops whose trees are in the current CFG. The enclosing-method pass therefore skips lambda-body loops and Line 1203 clears their state before the lambda CFG reachespostAnalyze(...). Use a method/lambda-aware key throughout the record/get/remove path.Also applies to: 405-471, 517-535, 559-624, 1187-1203, 1227-1247
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java`:
- Around line 126-127: The public mutator add(`@Owning` V o) is missing an
explicit receiver qualifier, breaking ownership-contract consistency with other
mutators; update the method signature for add to include the same explicit
receiver qualifier used on other mutators (e.g. the qualifier pattern applied to
remove/other insertion methods) so its ownership contract is explicit and
consistent with LinkedHashKeyedSet's other public mutators (refer to the
add(`@Owning` V o) method and the signatures of public remove/... methods to match
the qualifier).
In
`@checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java`:
- Around line 1375-1379: The comparison of loop variable Names in
RLCCalledMethodsAnnotatedTypeFactory uses reference equality
(VariableTree.getName() == loopVariable.getName()) which can fail; change the
check in the block handling AssignmentNode/VariableTree so that
isAssignmentOfLoopVariable compares Names by value (e.g., call .equals(...) or
use Objects.equals(...)) when comparing iteratorVariableDeclaration.getName()
and loopVariable.getName() to reliably detect the enhanced-for binding; leave
loopVariableNode and other logic unchanged.
- Around line 1518-1534: The loop selection stores the wrong block as the update
point: in the loop scan inside RLCCalledMethodsAnnotatedTypeFactory you set
bestLoopUpdateBlock to backEdge.targetBlock (the loop header/condition) which
makes later reads see pre-iteration state; change the assignment to use
backEdge.sourceBlock (the latch/block that flows back into the header) so
bestLoopUpdateBlock (and ultimately loopUpdateBlock) points to the
post-iteration update location; update any related comments to reflect that
WhileLoopResolutionCache.BlockEdge.sourceBlock is the intended latch.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 4857c8da-78d4-4245-a838-e0420cdd1ca1
📒 Files selected for processing (2)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.javachecker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java
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
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java`:
- Around line 119-120: The ownership contract is inconsistent: add(V) is
annotated `@Owning` but the other insertion APIs are not, allowing bypasses via
theMap.put; update the KeyedSet interface and LinkedHashKeyedSet implementation
so the parameter on add(V, int, int) and replace(V) is annotated `@Owning`
(matching add(V)), and adjust the method signatures in both KeyedSet and
LinkedHashKeyedSet (where add(V,int,int) and replace(V) call theMap.put(...)) to
enforce the same ownership contract; also add any necessary imports or
annotations to compile.
🪄 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: fbe65c73-cab4-4b9e-b610-c380d134b382
📒 Files selected for processing (1)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java
| public boolean add(@Owning V o) { | ||
| return add(o, THROW_EXCEPTION, IGNORE) == null; |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Verify ownership annotations on all mutators that can insert/replace elements.
fd -t f "LinkedHashKeyedSet.java" annotation-file-utilities \
--exec sed -n '100,170p' {}
# Verify interface declarations for add/replace contract context.
fd -t f "KeyedSet.java" annotation-file-utilities \
--exec sed -n '1,120p' {}
# Inspect all add/replace declarations in the concrete class.
rg -n --type=java '\b(public\s+)?(boolean|V)\s+(add|replace)\s*\(' \
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.javaRepository: typetools/checker-framework
Length of output: 7389
Ownership contract is inconsistent across insertion APIs.
Line 119 requires @Owning for add(V), but insertion still occurs through add(V, int, int) (Line 109) and replace(V) (Line 148) without ownership annotations. Both methods call theMap.put(), creating bypass paths that weaken ownership/RLC guarantees.
Update both KeyedSet interface and LinkedHashKeyedSet implementation:
- Add
@Owningtoadd(V, int, int)parameter - Add
@Owningtoreplace(V)parameter
💡 Changes needed
In KeyedSet.java:
- public abstract V add(V v, int conflictBehavior, int equalBehavior);
+ public abstract V add(`@Owning` V v, int conflictBehavior, int equalBehavior);- public abstract V replace(V v);
+ public abstract V replace(`@Owning` V v);In LinkedHashKeyedSet.java:
- public V add(V o, int conflictBehavior, int equalBehavior) {
+ public V add(`@Owning` V o, int conflictBehavior, int equalBehavior) {- public V replace(V v) {
+ public V replace(`@Owning` V v) {🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java`
around lines 119 - 120, The ownership contract is inconsistent: add(V) is
annotated `@Owning` but the other insertion APIs are not, allowing bypasses via
theMap.put; update the KeyedSet interface and LinkedHashKeyedSet implementation
so the parameter on add(V, int, int) and replace(V) is annotated `@Owning`
(matching add(V)), and adjust the method signatures in both KeyedSet and
LinkedHashKeyedSet (where add(V,int,int) and replace(V) call theMap.put(...)) to
enforce the same ownership contract; also add any necessary imports or
annotations to compile.
|
@mernst CI jobs are failing on |
|
@iamsanjaymalakar Good question. Please see https://htmlpreview.github.io/?https://github.com/mernst/checker-framework/ci-related-projects/docs/developer/developer-manual.html#ci-related-projects and let me know if anything is unclear. |
@mernst I can't access the link. |
|
That's weird. I can do so, even in an incognito tab. Here is the text: Continuous Integration failures in related projects (daikon, plume-lib, etc.) Continuous integration type-checks external projects such as daikon and plume-lib libraries. If you change the Checker Framework, then you might need to change code being type-checked — for example, to fix a newly-revealed defect (bug) or to remove a warning suppression that is no longer necessary. Suppose that Checker Framework pull request
When CI runs for the new pull request, it will use your fork and branch of the Checker Framework. When CI runs for your Checker Framework pull request, it will typecheck the newly-created branch. When all the CI runs pass, merge all the branches in quick succession — that is, click the squash-and-merge buttons one after another. |
msridhar
left a comment
msridhar
left a comment
There was a problem hiding this comment.
Couple of very initial comments. My rough review plan:
- Review
CollectionOwnershipCheckerand related code in thecollectionownershippackage, starting with the transfer functions - Review
MustCallConsistencyAnalyzerchanges - Review any other stuff that wasn't covered by 1 or 2
| * the receiver. | ||
| * | ||
| * <p>This annotation should only be used on method declarations of collections, as defined by the | ||
| * CollectionOwnershipChecker, that is, {@code java.lang.Iterable} and {@code java.util.Iterator} |
There was a problem hiding this comment.
Is the reference to java.util.Iterator here out of date? Or does our checker actually treats Iterators as potentially owning collections?
| * Transfer function for the collection ownership type system. Its primary purpose is to create | ||
| * temporary variables for expressions (which allow those expressions to have refined information in |
There was a problem hiding this comment.
Is this really the primary purpose? Doesn't this code contain the primary logic for ownership inference, and isn't that just as important as temporary variables?
| @Override | ||
| public TransferResult<CFValue, CollectionOwnershipStore> visitAssignment( | ||
| AssignmentNode node, TransferInput<CFValue, CollectionOwnershipStore> in) { | ||
| TransferResult<CFValue, CollectionOwnershipStore> res = super.visitAssignment(node, in); |
There was a problem hiding this comment.
It is this super.visitAssignment call that does the ownership transfer from rhs to lhs, correct? If so, add a comment to that effect
| replaceInStores( | ||
| res, | ||
| hasExplicitNotOwningCollectionDeclaration(node) ? lhsJE : rhsJE, | ||
| atypeFactory.NOTOWNINGCOLLECTION); |
There was a problem hiding this comment.
This is a bit subtle. I'd add a comment like, "Make the RHS @NotOwningCollection to reflect the ownership transfer, unless there is a @NotOwningCollection annotation, in which case there is no transfer and the lhs should be @NotOwningCollection"
@iamsanjaymalakar is this still true? If not, update the PR description? Also, looks like there are some conflicts with the latest master branch. |
|
@iamsanjaymalakar I have a high-level question. The logic for detecting loops that satisfy collection obligation and using them seems spread across many different places: Can you explain why the code is split up in the way that it is? Could we possibly consolidate more of it into the Collection Ownership Checker? |
The split is mostly by responsibility, not by checker ownership.
I'm not sure about how can I move all of them into CollectionOwnershipChecker. Let me know if you have any suggestions. @msridhar |
There was a problem hiding this comment.
Actionable comments posted: 2
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/scenelib/io/ASTPath.java (1)
1460-1465: 🧹 Nitpick | 🔵 TrivialAnnotate
get(int)explicitly to match the new accessor contract.
peek()andpop()now spell out the receiver qualifier, but Line 1498get(int)still exposes the same element-access path via defaults alone. For a checker-facing API, that inconsistency makes the ownership surface harder to audit and easier to regress.♻️ Proposed fix
- public E get(int index) { + public E get(`@NotOwningCollection` ImmutableStack<E> this, int index) {Also applies to: 1472-1476
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java` around lines 1460 - 1465, The get(int) accessor must be annotated the same as peek() and pop(): add the explicit receiver qualifier "@NotOwningCollection ImmutableStack<E> this" to the get(int) method signature(s) so the ownership contract is spelled out (match the annotations on peek() and pop()), ensuring the ImmutableStack<E> receiver is annotated for checker-facing consistency.
♻️ Duplicate comments (8)
javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java (1)
1728-1732:⚠️ Potential issue | 🔴 CriticalGuard empty argument lists before indexing
getArguments().get(0).Line 1731 can throw
IndexOutOfBoundsExceptionfor zero-argget()calls, which can crash analysis paths.🐛 Proposed fix
public static `@Nullable` ExpressionTree getIdxForGetCall(Tree tree) { - if ((tree instanceof MethodInvocationTree) - && isNamedMethodCall("get", (MethodInvocationTree) tree)) { - return ((MethodInvocationTree) tree).getArguments().get(0); + if (tree instanceof MethodInvocationTree) { + MethodInvocationTree invocationTree = (MethodInvocationTree) tree; + if (isNamedMethodCall("get", invocationTree) && !invocationTree.getArguments().isEmpty()) { + return invocationTree.getArguments().get(0); + } } return null; }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java` around lines 1728 - 1732, getIdxForGetCall can throw IndexOutOfBoundsException when a zero-argument "get" call is encountered; update the method to check the argument list size before calling getArguments().get(0) (e.g., test ((MethodInvocationTree) tree).getArguments().isEmpty() or size() > 0) and only return the first argument when present; keep the existing isNamedMethodCall("get", (MethodInvocationTree) tree) check and return null for empty-arg cases to avoid the exception.docs/manual/resource-leak-checker.tex (5)
825-826:⚠️ Potential issue | 🟠 MajorResolve the static-field rule conflict for
@NotOwningCollection.Lines 825-826 say any static resource-collection field is rejected, but Lines 888-893 say
@NotOwningCollectionfields behave like ordinary non-owning references. Those rules conflict unless static@NotOwningCollectionfields are explicitly carved out as legal, or forbidden in both places.Also applies to: 888-893
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/manual/resource-leak-checker.tex` around lines 825 - 826, The documentation currently contradicts itself about static resource-collection fields: the paragraph around the rule for resource collection ownership rejects any static resource-collection field, while the later section describing `@NotOwningCollection` implies such fields behave like ordinary non-owning references; fix by reconciling the policy and making it explicit — either allow static fields when annotated `@NotOwningCollection` or forbid static fields universally. Update the text around the general rule (the “static fields are not supported” sentence) and the `@NotOwningCollection` section so they state the same policy, e.g., “Static resource-collection fields are forbidden except when annotated `@NotOwningCollection`, which makes them legal non-owning references” or “Static resource-collection fields are forbidden, and `@NotOwningCollection` is not permitted on static fields,” and ensure both places reference `@NotOwningCollection` by name for clarity.
963-964:⚠️ Potential issue | 🟡 MinorRemove the rendered TODO before merge.
This placeholder will ship as unfinished manual text. Replace it with the intended table or drop the subsection for now.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/manual/resource-leak-checker.tex` around lines 963 - 964, The rendered TODO inside the subsection \subsectionAndLabel{JDK Method Signatures}{resource-leak-collections-jdk-methods} must be removed before merge; either replace the placeholder "[[TODO: Add a table with a number of collection/iterable methods and their collection ownership annotations]]" with the actual table of JDK collection/iterable methods and their ownership annotations, or delete the entire subsection header and its placeholder content if the table is not ready, ensuring no TODO/unrendered placeholder remains in the final document.
146-163:⚠️ Potential issue | 🟠 MajorDocument
@CreatesCollectionObligationalongside the other collection annotations.This overview still omits
@CreatesCollectionObligation, so readers never learn how methods that add new per-element obligations to an existing collection are modeled or how that differs from@CollectionFieldDestructor.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/manual/resource-leak-checker.tex` around lines 146 - 163, Add documentation for `@CreatesCollectionObligation` alongside the existing collection annotations (OwningCollection, NotOwningCollection, CollectionFieldDestructor): state that `@CreatesCollectionObligation` marks methods that create per-element obligations for an existing resource collection, document its parameters (if any) and intended targets, give an example and explicitly contrast its semantics with CollectionFieldDestructor (which cleans up whole fields) and with owning/not-owning defaults, and link to the relevant Section~\ref{resource-leak-collections} and the elements subsection so readers can find details on per-element obligation modeling.
661-662:⚠️ Potential issue | 🟠 MajorDon’t describe
@NotOwningCollectionas completely non-mutating.These paragraphs still say non-owning references cannot add, remove, or overwrite elements. That overstates the restriction: the checker permits mutations that insert non-owning/safe elements. Please document that exception so the manual matches the checker.
Also applies to: 728-729
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/manual/resource-leak-checker.tex` around lines 661 - 662, Update the two paragraphs describing non-owning references to avoid saying they are completely non-mutating: state that references annotated with `@NotOwningCollection` (or otherwise non-owning) are restricted from arbitrary mutation but may perform mutations that only insert or replace elements that are themselves non-owning/safe (e.g., elements annotated as non-owning or otherwise provably safe); revise the wording to mention this permitted exception and mirror the same clarification in the other occurrence of the paragraph to keep the manual consistent.
775-812:⚠️ Potential issue | 🟡 MinorThis section still under-documents the accepted loop shapes.
It only documents enhanced
forand one indexed-forpattern. If iterator/whiletraversals are now certified too, spell out those forms and their checks here; otherwise narrow the wording so the manual matches the implementation.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/manual/resource-leak-checker.tex` around lines 775 - 812, The docs currently only describe enhanced for and one indexed-for pattern for satisfying collection obligations but the implementation also accepts additional traversal shapes (or conversely the docs overclaim); update docs in resource-leak-checker.tex to either (a) enumerate the exact accepted loop shapes and checks (include iterator/while traversals and their required properties: no early termination, no writes to loop variable/collection, accesses via iterator.next() or collection.get(i) as appropriate, and reliance on CalledMethods/@EnsuresCalledMethods for per-element calls) or (b) narrow the wording to only claim enhanced-for and the indexed-for pattern shown; reference the same terminology used in the text (CalledMethods, `@EnsuresCalledMethods`("m"), `@OwningCollection`, `@OwningCollectionWithoutObligation`) so the manual matches the implementation.framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java (2)
78-79:⚠️ Potential issue | 🟠 MajorInvalidate iterated-element facts on mutations, too.
iteratedCollectionElementsis now first-class store state, but the mutation paths still never evict it. Side-effecting calls and theremoveConflicting(...)paths for field/array/local assignments can all change the iterator or backing collection state, so keeping these entries makes the store stale and can leak called-method facts across iterations.Minimal soundness fix
@@ if (hasSideEffect) { + iteratedCollectionElements.clear(); @@ protected void removeConflicting(FieldAccess fieldAccess, `@Nullable` V val) { + iteratedCollectionElements.clear(); @@ protected void removeConflicting(ArrayAccess arrayAccess, `@Nullable` V val) { + iteratedCollectionElements.clear(); @@ protected void removeConflicting(LocalVariable var) { + iteratedCollectionElements.clear();Also applies to: 632-638
🤖 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/flow/CFAbstractStore.java` around lines 78 - 79, The iteratedCollectionElements map must be cleared/updated whenever the store is mutated so iterator-related facts don't leak; modify all mutation/assignment paths (including removeConflicting(...), field/array/local assignment handlers, and any side-effecting call paths) to remove or invalidate entries in iteratedCollectionElements when the target or its backing collection/element could change. Locate uses of iteratedCollectionElements and add logic in CFAbstractStore mutation methods (and in removeConflicting(...)) to evict affected IteratedCollectionElement keys (or clear the map on broad-unknown mutations) so iterator facts are not preserved across mutations.
817-820:⚠️ Potential issue | 🟡 MinorRequire both key components to match in
getIteratedCollectionElement.This
||chain is looser thanIteratedCollectionElement.equals(...), which keys entries on bothtreeandnode. Two distinct keys that share only one component can therefore resolve to the wrong store entry, and the result depends onHashMapiteration order.Suggested fix
public `@Nullable` IteratedCollectionElement getIteratedCollectionElement(Node node, Tree tree) { for (IteratedCollectionElement ice : iteratedCollectionElements.keySet()) { - if (ice.tree == tree || ice.node == node || ice.tree.equals(tree) || ice.node.equals(node)) { + boolean treeMatches = ice.tree == tree || ice.tree.equals(tree); + boolean nodeMatches = ice.node == node || ice.node.equals(node); + if (treeMatches && nodeMatches) { return ice; } } return null; }🤖 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/flow/CFAbstractStore.java` around lines 817 - 820, getIteratedCollectionElement currently matches a key if either the node or tree matches, which can return the wrong IteratedCollectionElement; change the matching logic in getIteratedCollectionElement to require both components match (i.e., tree AND node) using null-safe equality (e.g., Objects.equals) against iteratedCollectionElements' keys (IteratedCollectionElement ice), so replace the || chain with a conjunction that checks both ice.tree vs tree and ice.node vs node (or delegating to IteratedCollectionElement.equals(...) if appropriate).
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/manual/resource-leak-checker.tex`:
- Around line 665-672: The definition of "resource collection" is inconsistent
with the example: update the rule so the type parameter upper bound can be
either a non-empty `@MustCall` type or `@MustCallUnknown` (i.e., treat
`@MustCallUnknown` as a valid must-call obligation for the purposes of the
checker), and then keep the example Iterable<? extends `@MustCallUnknown` Object>
as-is; reference the "resource collection" term and the `@MustCall` /
`@MustCallUnknown` type parameter upper bound in the sentence to make the intent
explicit.
In
`@framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java`:
- Around line 1199-1214: The method getRegularStore(Block) may dereference a
null TransferInput because flowResult.getInput(block) and
analysis.getInput(block) are `@Nullable`; change the method to return `@Nullable`
Store and defend against null by checking if input is null and returning null
(rather than calling input.getRegularStore()), keeping the existing behavior
when input is non-null; update the method signature and any Javadoc to reflect
`@Nullable` and reference getRegularStore(Block), flowResult.getInput,
analysis.getInput, and TransferInput<Value, Store> in your changes.
---
Outside diff comments:
In
`@annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java`:
- Around line 1460-1465: The get(int) accessor must be annotated the same as
peek() and pop(): add the explicit receiver qualifier "@NotOwningCollection
ImmutableStack<E> this" to the get(int) method signature(s) so the ownership
contract is spelled out (match the annotations on peek() and pop()), ensuring
the ImmutableStack<E> receiver is annotated for checker-facing consistency.
---
Duplicate comments:
In `@docs/manual/resource-leak-checker.tex`:
- Around line 825-826: The documentation currently contradicts itself about
static resource-collection fields: the paragraph around the rule for resource
collection ownership rejects any static resource-collection field, while the
later section describing `@NotOwningCollection` implies such fields behave like
ordinary non-owning references; fix by reconciling the policy and making it
explicit — either allow static fields when annotated `@NotOwningCollection` or
forbid static fields universally. Update the text around the general rule (the
“static fields are not supported” sentence) and the `@NotOwningCollection` section
so they state the same policy, e.g., “Static resource-collection fields are
forbidden except when annotated `@NotOwningCollection`, which makes them legal
non-owning references” or “Static resource-collection fields are forbidden, and
`@NotOwningCollection` is not permitted on static fields,” and ensure both places
reference `@NotOwningCollection` by name for clarity.
- Around line 963-964: The rendered TODO inside the subsection
\subsectionAndLabel{JDK Method
Signatures}{resource-leak-collections-jdk-methods} must be removed before merge;
either replace the placeholder "[[TODO: Add a table with a number of
collection/iterable methods and their collection ownership annotations]]" with
the actual table of JDK collection/iterable methods and their ownership
annotations, or delete the entire subsection header and its placeholder content
if the table is not ready, ensuring no TODO/unrendered placeholder remains in
the final document.
- Around line 146-163: Add documentation for `@CreatesCollectionObligation`
alongside the existing collection annotations (OwningCollection,
NotOwningCollection, CollectionFieldDestructor): state that
`@CreatesCollectionObligation` marks methods that create per-element obligations
for an existing resource collection, document its parameters (if any) and
intended targets, give an example and explicitly contrast its semantics with
CollectionFieldDestructor (which cleans up whole fields) and with
owning/not-owning defaults, and link to the relevant
Section~\ref{resource-leak-collections} and the elements subsection so readers
can find details on per-element obligation modeling.
- Around line 661-662: Update the two paragraphs describing non-owning
references to avoid saying they are completely non-mutating: state that
references annotated with `@NotOwningCollection` (or otherwise non-owning) are
restricted from arbitrary mutation but may perform mutations that only insert or
replace elements that are themselves non-owning/safe (e.g., elements annotated
as non-owning or otherwise provably safe); revise the wording to mention this
permitted exception and mirror the same clarification in the other occurrence of
the paragraph to keep the manual consistent.
- Around line 775-812: The docs currently only describe enhanced for and one
indexed-for pattern for satisfying collection obligations but the implementation
also accepts additional traversal shapes (or conversely the docs overclaim);
update docs in resource-leak-checker.tex to either (a) enumerate the exact
accepted loop shapes and checks (include iterator/while traversals and their
required properties: no early termination, no writes to loop
variable/collection, accesses via iterator.next() or collection.get(i) as
appropriate, and reliance on CalledMethods/@EnsuresCalledMethods for per-element
calls) or (b) narrow the wording to only claim enhanced-for and the indexed-for
pattern shown; reference the same terminology used in the text (CalledMethods,
`@EnsuresCalledMethods`("m"), `@OwningCollection`,
`@OwningCollectionWithoutObligation`) so the manual matches the implementation.
In
`@framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java`:
- Around line 78-79: The iteratedCollectionElements map must be cleared/updated
whenever the store is mutated so iterator-related facts don't leak; modify all
mutation/assignment paths (including removeConflicting(...), field/array/local
assignment handlers, and any side-effecting call paths) to remove or invalidate
entries in iteratedCollectionElements when the target or its backing
collection/element could change. Locate uses of iteratedCollectionElements and
add logic in CFAbstractStore mutation methods (and in removeConflicting(...)) to
evict affected IteratedCollectionElement keys (or clear the map on broad-unknown
mutations) so iterator facts are not preserved across mutations.
- Around line 817-820: getIteratedCollectionElement currently matches a key if
either the node or tree matches, which can return the wrong
IteratedCollectionElement; change the matching logic in
getIteratedCollectionElement to require both components match (i.e., tree AND
node) using null-safe equality (e.g., Objects.equals) against
iteratedCollectionElements' keys (IteratedCollectionElement ice), so replace the
|| chain with a conjunction that checks both ice.tree vs tree and ice.node vs
node (or delegating to IteratedCollectionElement.equals(...) if appropriate).
In `@javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java`:
- Around line 1728-1732: getIdxForGetCall can throw IndexOutOfBoundsException
when a zero-argument "get" call is encountered; update the method to check the
argument list size before calling getArguments().get(0) (e.g., test
((MethodInvocationTree) tree).getArguments().isEmpty() or size() > 0) and only
return the first argument when present; keep the existing
isNamedMethodCall("get", (MethodInvocationTree) tree) check and return null for
empty-arg cases to avoid the exception.
🪄 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: 106e3096-831b-4d3d-8be4-0c36f754abe3
📒 Files selected for processing (7)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.javadataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.javadocs/manual/resource-leak-checker.texframework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.javaframework/src/main/java/org/checkerframework/framework/stub/StubGenerator.javaframework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.javajavacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
| For the purposes of this checker, \textit{resource collections} are precisely defined, as the objects of interest for both the type system and obligation tracking. A Java expression is a \textit{resource collection} if it is: | ||
|
|
||
| \begin{enumerate} | ||
| \item A \texttt{java.util.Iterable} or implementation thereof (which includes the entire Java Collections framework), and:%, or a \texttt{java.util.Iterator} | ||
| \item Its type parameter upper bound has non-empty \texttt{MustCall} type. | ||
| \end{enumerate} | ||
|
|
||
| For example, expressions of type \texttt{List<Socket>} or \texttt{Iterable<? extends @MustCallUnknown Object>} are both resource collections, but one of type \texttt{Set<String>} is not. |
There was a problem hiding this comment.
Align the formal definition with the example.
Line 669 says a resource collection must have an element upper bound with a non-empty @MustCall type, but Line 672 then lists Iterable<? extends @MustCallUnknown Object> as an example. Please either broaden the definition to cover unknown must-call obligations or replace the example.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@docs/manual/resource-leak-checker.tex` around lines 665 - 672, The definition
of "resource collection" is inconsistent with the example: update the rule so
the type parameter upper bound can be either a non-empty `@MustCall` type or
`@MustCallUnknown` (i.e., treat `@MustCallUnknown` as a valid must-call obligation
for the purposes of the checker), and then keep the example Iterable<? extends
`@MustCallUnknown` Object> as-is; reference the "resource collection" term and the
`@MustCall` / `@MustCallUnknown` type parameter upper bound in the sentence to make
the intent explicit.
| /** | ||
| * Returns the regular store for a given block. | ||
| * | ||
| * @param block a block whose regular store to return | ||
| * @return the regular store of {@code block} | ||
| */ | ||
| public Store getRegularStore(Block block) { | ||
| TransferInput<Value, Store> input; | ||
| if (!analysis.isRunning()) { | ||
| input = flowResult.getInput(block); | ||
| } else { | ||
| input = analysis.getInput(block); | ||
| } | ||
|
|
||
| return input.getRegularStore(); | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Check how similar store-retrieval methods handle null
# Look for getInput calls and null handling patterns
rg -n -A5 -B2 'getInput\(' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java
# Check if TransferInput getInput can return null based on its declaration
ast-grep --pattern 'TransferInput<$_, $_> getInput($_) { $$$ }'Repository: typetools/checker-framework
Length of output: 335
🏁 Script executed:
# Find and examine the getStoreBefore method to compare
rg -n -A10 'getStoreBefore\(Tree' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.javaRepository: typetools/checker-framework
Length of output: 1414
🏁 Script executed:
# Find the class definition of flowResult and analysis to understand their types
rg -n 'flowResult\s*=' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java | head -5
rg -n 'analysis\s*=' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java | head -5
# Also look for field declarations
rg -n -B2 'private.*flowResult\|protected.*flowResult\|public.*flowResult' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java
rg -n -B2 'private.*analysis\|protected.*analysis\|public.*analysis' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.javaRepository: typetools/checker-framework
Length of output: 352
🏁 Script executed:
# Check for `@Nullable` annotations in the file to understand the pattern
rg -n '@Nullable' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java | head -20Repository: typetools/checker-framework
Length of output: 1562
🏁 Script executed:
# Search for any usage of getInput with null checking
rg -n -B2 -A2 'getInput.*null\|null.*getInput' framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.javaRepository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
# Search for getInput method definitions in the codebase
fd -t f '\.java$' | xargs rg -l 'getInput\(' | head -10Repository: typetools/checker-framework
Length of output: 881
🏁 Script executed:
# Look for TransferResult or FlowResult class definitions
fd -t f 'TransferResult.java|FlowResult.java|AnalysisResult.java' framework/Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
# Search for method signature of getInput in analysis and flowResult related classes
rg -n 'TransferInput.*getInput|AnalysisResult.*getInput' framework/ -t javaRepository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
# Find the AnalysisResult class and look for getInput method
rg -n -A10 'public.*getInput\(Block' dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.javaRepository: typetools/checker-framework
Length of output: 404
🏁 Script executed:
# Also search in Analysis class
rg -n -A10 'public.*getInput\(Block' dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.javaRepository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
# Check AbstractAnalysis as well
rg -n -A10 'getInput\(Block' dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.javaRepository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
# Look for the return type annotation on getInput methods
rg -n '@Nullable.*getInput\(|getInput.*@Nullable' dataflow/src/main/java/org/checkerframework/dataflow/analysis/Repository: typetools/checker-framework
Length of output: 651
Potential null pointer dereference on input.getRegularStore().
Both flowResult.getInput(block) and analysis.getInput(block) can return null (confirmed by @Nullable annotation in their signatures), but there is no null check before calling input.getRegularStore(). This is inconsistent with similar methods in this class like getStoreBefore(Tree), getStoreAfter(Tree), getRegularExitStore(Tree), and getExceptionalExitStore(Tree), which all return @Nullable Store.
Consider either adding a null check and returning @Nullable Store, or documenting a precondition that the block must have a valid input. Given the pattern in this class, returning @Nullable Store is more consistent with related methods.
Suggested fix
- public Store getRegularStore(Block block) {
+ public `@Nullable` Store getRegularStore(Block block) {
TransferInput<Value, Store> input;
if (!analysis.isRunning()) {
input = flowResult.getInput(block);
} else {
input = analysis.getInput(block);
}
+ if (input == null) {
+ return null;
+ }
return input.getRegularStore();
}🤖 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 1199 - 1214, The method getRegularStore(Block) may dereference a
null TransferInput because flowResult.getInput(block) and
analysis.getInput(block) are `@Nullable`; change the method to return `@Nullable`
Store and defend against null by checking if input is null and returning null
(rather than calling input.getRegularStore()), keeping the existing behavior
when input is non-null; update the method signature and any Javadoc to reflect
`@Nullable` and reference getRegularStore(Block), flowResult.getInput,
analysis.getInput, and TransferInput<Value, Store> in your changes.
|
Thanks, @iamsanjaymalakar. To make sure we are on the same page, here's what I think needs to happen at a high level. We need to identify loops that iterate over a (resource) collection. When we identify a loop, I'm assuming we know all CFG nodes in the loop, the loop head, and the loop variable corresponding to an element of the collection. For each such loop, we need to check two things:
If a loop over a resource collection satisfies 1 and 2, it is a certified disposal loop. Then, in inference of collection ownership types, if a reference to a collection I think it's also useful to keep in mind the current sub-checker relationships for the RLC: Now to your comment:
All checkers can have a visitor that operates over ASTs. Why does this logic need to live in the
Again, all checkers usually do inference and have access to CFGs (including the Must Call Checker). I don't understand why the bullets listed above need to happen in the RLC Called Methods Checker.
I don't understand what "orchestration" or "resolved" mean in this sentence.
This one I don't understand either. Is the idea that the check being performed at back edges is a consistency check, so it's somehow nice to re-use the consistency analyzer logic for this? Do we handle cases like must-aliases of the loop variable then? I guess that idea makes sense, but I still don't know why it's getting called from the RLC Called Methods Checker.
This makes sense. I just don't understand why the orchestration is so complicated. Is it because the Collection Ownership Checker cannot easily access the types inferred by the sub-checkers? |
Not at the initial match point. There we only know the source-level loop shape and the relevant trees. The full CFG structure is recovered later; for enhanced
There is no fundamental reason it has to be in
This does not inherently have to live in
The AST match gives us a candidate loop, but not all of the CFG information that MCCA needs to certify it. After the missing CFG pieces are filled in, the loop is in a resolved state. By “orchestration”, I mean that RLCCalledMethodsAnnotatedTypeFactory is doing the bookkeeping around that process: it tracks the candidates, resolves the missing CFG pieces, and then calls MCCA on the resolved loops.
Yes, the reason it is in MCCA is basically that this is already using the same consistency machinery: it seeds an obligation for the iterated element, propagates obligations through the loop body, updates aliases through assignments, and then checks the @CalledMethods information for the element and its aliases at the relevant back edges.
I agree with you on this. I think we'll need a seprate place/class that does all the orchestration. The matched/resolved loop state is tracked on the RLCC Called Methods side, and the certification needs to run in a postAnalyze(...) phase after Called Methods analysis has finished, so that is where the orchestration ended up. |
|
Quick question, why do we need to do AST matching to find source-level loop shapes? Why can't everything be done at the CFG level? |
@msridhar I'm not too sure about how hard that would be. I extended following the initial implementation (indexed-for in AST, enhanced for via CFG) to while loops. Matching in the AST stage seemed natuaral to find the loop condition and the collection being iterated (just to identify the potential loops). I don't know how complicated it would be to do so from CFG. |
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java (1)
261-266:⚠️ Potential issue | 🔴 CriticalSkip the current checker when probing for an enclosing RLC hierarchy.
Starting the scan at
checkerstill makes a standaloneMustCallCheckerlook like it is inside the RLC hierarchy, so this helper can call the RLCC factory lookup when no enclosing RLC checker exists. Start fromchecker.getParentChecker()or otherwise ignore the initial checker.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java` around lines 261 - 266, getRlccAtfIfPartOfHierarchy incorrectly begins scanning at the current checker, causing a standalone MustCallChecker to be treated as part of the RLC hierarchy; change the probe to skip the current checker by initializing currentChecker to checker.getParentChecker() (or otherwise start from the parent) and then iterate while currentChecker != null, checking ResourceLeakUtils.rlcCheckers for currentChecker.getClass().getCanonicalName() and calling ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this) only when an enclosing RLC checker is found.
🤖 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/mustcall/MustCallAnnotatedTypeFactory.java`:
- Around line 293-337: The current loop in MustCallAnnotatedTypeFactory only
recurses into nested declared type arguments when
ResourceLeakUtils.isCollection(adt.getUnderlyingType()) is true, so declared
inner collections (e.g., Optional<List<?>>) aren't visited; change the logic so
that the handling that forces wildcard/typevar element annotations to BOTTOM
remains when the outer type is a collection, but the recursive call to
replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg)
is executed for any AnnotatedDeclaredType type argument regardless of the outer
isCollection check—i.e., move or duplicate the branch that checks
typeArg.getKind() == TypeKind.DECLARED out of the isCollection guard (or add a
second pass over adt.getTypeArguments() that calls
replaceCollectionTypeVarsWithBottomIfTop for DECLARED args) so nested declared
types are always descended into.
---
Duplicate comments:
In
`@checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java`:
- Around line 261-266: getRlccAtfIfPartOfHierarchy incorrectly begins scanning
at the current checker, causing a standalone MustCallChecker to be treated as
part of the RLC hierarchy; change the probe to skip the current checker by
initializing currentChecker to checker.getParentChecker() (or otherwise start
from the parent) and then iterate while currentChecker != null, checking
ResourceLeakUtils.rlcCheckers for currentChecker.getClass().getCanonicalName()
and calling ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this) only
when an enclosing RLC checker is found.
🪄 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: 5217275d-7bce-4d89-8cd5-3b72ed0670d4
📒 Files selected for processing (2)
checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.javachecker/tests/resourceleak-collections/ArraysAsListZeroArgs.java
| if (ResourceLeakUtils.isCollection(adt.getUnderlyingType())) { | ||
| for (AnnotatedTypeMirror typeArg : adt.getTypeArguments()) { | ||
| if (typeArg == null) { | ||
| continue; | ||
| } | ||
| if (typeArg.getKind() == TypeKind.WILDCARD || typeArg.getKind() == TypeKind.TYPEVAR) { | ||
| if (tree != null && tree instanceof NewClassTree) { | ||
| if (((NewClassTree) tree).getTypeArguments().isEmpty()) { | ||
| // Diamond [new Class()<>]. Not explicit generic type param. | ||
| // This will be inferred later. Don't put it to bottom here. | ||
| continue; | ||
| } | ||
| } | ||
| AnnotationMirror mcAnno = typeArg.getAnnotationInHierarchy(TOP); | ||
| boolean typeArgIsMcUnknown = | ||
| mcAnno != null | ||
| && processingEnv | ||
| .getTypeUtils() | ||
| .isSameType(mcAnno.getAnnotationType(), TOP.getAnnotationType()); | ||
| if (typeArgIsMcUnknown) { | ||
| // check whether the upper bounds have manual MustCallUnknown annotations, in which case | ||
| // they should | ||
| // not be reset to bottom. For example like this: | ||
| // void m(List<? extends @MustCallUnknown Object>) {} | ||
|
|
||
| if (typeArg.getUnderlyingType() instanceof WildcardType) { | ||
| TypeMirror extendsBound = | ||
| ((WildcardType) typeArg.getUnderlyingType()).getExtendsBound(); | ||
| if (!ResourceLeakUtils.hasManualMustCallUnknownAnno(extendsBound)) { | ||
| typeArg.replaceAnnotation(BOTTOM); | ||
| } | ||
| } else if (typeArg instanceof AnnotatedTypeVariable) { | ||
| AnnotatedTypeMirror upperBound = ((AnnotatedTypeVariable) typeArg).getUpperBound(); | ||
| // set back to bottom if the type var is a captured wildcard | ||
| // or if it doesn't have a manual MustCallUnknown anno | ||
| if (typeArg.containsCapturedTypes() | ||
| || !ResourceLeakUtils.hasManualMustCallUnknownAnno(upperBound, this)) { | ||
| typeArg.replaceAnnotation(BOTTOM); | ||
| } | ||
| } else { | ||
| typeArg.replaceAnnotation(BOTTOM); | ||
| } | ||
| } | ||
| } else if (typeArg.getKind() == TypeKind.DECLARED) { | ||
| replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg); |
There was a problem hiding this comment.
Recurse into nested declared type arguments even when the outer type is not a collection.
The ResourceLeakUtils.isCollection(...) guard currently wraps both the rewrite and the recursive descent. As a result, types like Optional<List<?>> or Holder<Iterator<?>> never visit their inner collection/iterator arguments, so those element types keep @MustCallUnknown instead of being forced to bottom.
♻️ Suggested fix
private void replaceCollectionTypeVarsWithBottomIfTop(Tree tree, AnnotatedDeclaredType adt) {
- if (ResourceLeakUtils.isCollection(adt.getUnderlyingType())) {
- for (AnnotatedTypeMirror typeArg : adt.getTypeArguments()) {
+ boolean currentIsCollection = ResourceLeakUtils.isCollection(adt.getUnderlyingType());
+ for (AnnotatedTypeMirror typeArg : adt.getTypeArguments()) {
if (typeArg == null) {
continue;
}
- if (typeArg.getKind() == TypeKind.WILDCARD || typeArg.getKind() == TypeKind.TYPEVAR) {
+ if (currentIsCollection
+ && (typeArg.getKind() == TypeKind.WILDCARD || typeArg.getKind() == TypeKind.TYPEVAR)) {
...
} else if (typeArg.getKind() == TypeKind.DECLARED) {
replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg);
}
- }
}
}📝 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.
| if (ResourceLeakUtils.isCollection(adt.getUnderlyingType())) { | |
| for (AnnotatedTypeMirror typeArg : adt.getTypeArguments()) { | |
| if (typeArg == null) { | |
| continue; | |
| } | |
| if (typeArg.getKind() == TypeKind.WILDCARD || typeArg.getKind() == TypeKind.TYPEVAR) { | |
| if (tree != null && tree instanceof NewClassTree) { | |
| if (((NewClassTree) tree).getTypeArguments().isEmpty()) { | |
| // Diamond [new Class()<>]. Not explicit generic type param. | |
| // This will be inferred later. Don't put it to bottom here. | |
| continue; | |
| } | |
| } | |
| AnnotationMirror mcAnno = typeArg.getAnnotationInHierarchy(TOP); | |
| boolean typeArgIsMcUnknown = | |
| mcAnno != null | |
| && processingEnv | |
| .getTypeUtils() | |
| .isSameType(mcAnno.getAnnotationType(), TOP.getAnnotationType()); | |
| if (typeArgIsMcUnknown) { | |
| // check whether the upper bounds have manual MustCallUnknown annotations, in which case | |
| // they should | |
| // not be reset to bottom. For example like this: | |
| // void m(List<? extends @MustCallUnknown Object>) {} | |
| if (typeArg.getUnderlyingType() instanceof WildcardType) { | |
| TypeMirror extendsBound = | |
| ((WildcardType) typeArg.getUnderlyingType()).getExtendsBound(); | |
| if (!ResourceLeakUtils.hasManualMustCallUnknownAnno(extendsBound)) { | |
| typeArg.replaceAnnotation(BOTTOM); | |
| } | |
| } else if (typeArg instanceof AnnotatedTypeVariable) { | |
| AnnotatedTypeMirror upperBound = ((AnnotatedTypeVariable) typeArg).getUpperBound(); | |
| // set back to bottom if the type var is a captured wildcard | |
| // or if it doesn't have a manual MustCallUnknown anno | |
| if (typeArg.containsCapturedTypes() | |
| || !ResourceLeakUtils.hasManualMustCallUnknownAnno(upperBound, this)) { | |
| typeArg.replaceAnnotation(BOTTOM); | |
| } | |
| } else { | |
| typeArg.replaceAnnotation(BOTTOM); | |
| } | |
| } | |
| } else if (typeArg.getKind() == TypeKind.DECLARED) { | |
| replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg); | |
| boolean currentIsCollection = ResourceLeakUtils.isCollection(adt.getUnderlyingType()); | |
| for (AnnotatedTypeMirror typeArg : adt.getTypeArguments()) { | |
| if (typeArg == null) { | |
| continue; | |
| } | |
| if (currentIsCollection | |
| && (typeArg.getKind() == TypeKind.WILDCARD || typeArg.getKind() == TypeKind.TYPEVAR)) { | |
| if (tree != null && tree instanceof NewClassTree) { | |
| if (((NewClassTree) tree).getTypeArguments().isEmpty()) { | |
| // Diamond [new Class()<>]. Not explicit generic type param. | |
| // This will be inferred later. Don't put it to bottom here. | |
| continue; | |
| } | |
| } | |
| AnnotationMirror mcAnno = typeArg.getAnnotationInHierarchy(TOP); | |
| boolean typeArgIsMcUnknown = | |
| mcAnno != null | |
| && processingEnv | |
| .getTypeUtils() | |
| .isSameType(mcAnno.getAnnotationType(), TOP.getAnnotationType()); | |
| if (typeArgIsMcUnknown) { | |
| // check whether the upper bounds have manual MustCallUnknown annotations, in which case | |
| // they should | |
| // not be reset to bottom. For example like this: | |
| // void m(List<? extends `@MustCallUnknown` Object>) {} | |
| if (typeArg.getUnderlyingType() instanceof WildcardType) { | |
| TypeMirror extendsBound = | |
| ((WildcardType) typeArg.getUnderlyingType()).getExtendsBound(); | |
| if (!ResourceLeakUtils.hasManualMustCallUnknownAnno(extendsBound)) { | |
| typeArg.replaceAnnotation(BOTTOM); | |
| } | |
| } else if (typeArg instanceof AnnotatedTypeVariable) { | |
| AnnotatedTypeMirror upperBound = ((AnnotatedTypeVariable) typeArg).getUpperBound(); | |
| // set back to bottom if the type var is a captured wildcard | |
| // or if it doesn't have a manual MustCallUnknown anno | |
| if (typeArg.containsCapturedTypes() | |
| || !ResourceLeakUtils.hasManualMustCallUnknownAnno(upperBound, this)) { | |
| typeArg.replaceAnnotation(BOTTOM); | |
| } | |
| } else { | |
| typeArg.replaceAnnotation(BOTTOM); | |
| } | |
| } | |
| } else if (typeArg.getKind() == TypeKind.DECLARED) { | |
| replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg); | |
| } | |
| } |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java`
around lines 293 - 337, The current loop in MustCallAnnotatedTypeFactory only
recurses into nested declared type arguments when
ResourceLeakUtils.isCollection(adt.getUnderlyingType()) is true, so declared
inner collections (e.g., Optional<List<?>>) aren't visited; change the logic so
that the handling that forces wildcard/typevar element annotations to BOTTOM
remains when the outer type is a collection, but the recursive call to
replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg)
is executed for any AnnotatedDeclaredType type argument regardless of the outer
isCollection check—i.e., move or duplicate the branch that checks
typeArg.getKind() == TypeKind.DECLARED out of the isCollection guard (or add a
second pass over adt.getTypeArguments() that calls
replaceCollectionTypeVarsWithBottomIfTop for DECLARED args) so nested declared
types are always descended into.
|
@msridhar I agree the current structure is more scattered than ideal, and I also agree that the long-term direction should be to consolidate more of the orchestration under Collection Ownership checker. But I do not think the right end state is to move all of the logic there. The refactoring I have in mind is not “move everything into Collection Ownership”, but rather: Collection Ownership should own the traversal bookkeeping/lifecycle, while MCCA remains the proof engine. Concretely, I think a cleaner design would be to introduce a separate coordination layer owned by the Collection Ownership side. That layer would own the candidate loops (via own visitor, instead of I think the certification trigger still has to happen at the Called Methods post-analysis point, or at an equivalent lifecycle point where the Called Methods stores are already available. If we instead wait and do the certification in Collection Ownership’s own post-analysis, then the normal Collection Ownership transfer for that same analysis has already run by that point, so the certified result arrives too late to affect the current CO flow pass. In other words, doing certification there would mean we would need to run Collection Ownership flow again, or introduce some second pass just to consume the newly certified loops. So in summary the proposed direction: add a CollectionOwnershipCoordinator to own bookkeeping for loops and the API used by CollectionOwnershipTransfer, while keeping certification in MCCA. Certification should still be triggered at CM postAnalyze, since that is when the Called Methods stores are definetly available (I can't think of a better point); doing it in CO post-analysis would require rerunning CO or adding a second pass. |
|
@iamsanjaymalakar didn't we discuss overriding some pre-analysis hook in our meeting last week? What happened to that? I don't really know what you mean by a coordination layer. That is not standard terminology for the Checker Framework. Please be more concrete about what you are proposing. |
@msridhar There is not currently a standard pre-analysis hook in the CF lifecycle. The relevant lifecycle points are: analyze(...), then postAnalyzeAfterFirstMethodAnalysis(...) for methods, and finally postAnalyze(...). As the pre-analysis hook needs to run before flow analysis, but after the CFG exists phase, I'll need to override
One note: I can't just call Let me know if this answers your question. |
5 participants
This is the new PR for #7166