Skip to content

RLC extension for resource collection#7602

Open
iamsanjaymalakar wants to merge 464 commits intotypetools:masterfrom
iamsanjaymalakar:rlc-for-collections
Open

RLC extension for resource collection#7602
iamsanjaymalakar wants to merge 464 commits intotypetools:masterfrom
iamsanjaymalakar:rlc-for-collections

Conversation

@iamsanjaymalakar
Copy link
Copy Markdown
Member

@iamsanjaymalakar iamsanjaymalakar commented Mar 31, 2026

This is the new PR for #7166

Sascha Kehrli and others added 30 commits June 24, 2025 22:30
…CreatesMustCallFor anno on enclosing method
Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 3

♻️ Duplicate comments (5)
checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java (4)

904-906: ⚠️ Potential issue | 🟠 Major

Don't use reference equality on Name when locating the parameter slot.

getSimpleName() does not guarantee identical object references for equal names. When the Name instances differ, the parameter's ownership qualifier is never propagated to the use site.

Minimal fix
-            if (params.get(i).getSimpleName() == elt.getSimpleName()) {
+            if (params.get(i).getSimpleName().equals(elt.getSimpleName())) {
               type.replaceAnnotation(paramTypes.get(i).getAnnotationInHierarchy(TOP));
               break;
             }
In Java annotation processing, do javax.lang.model.element.Name values returned by Element.getSimpleName() guarantee reference equality, or should they be compared with equals/contentEquals instead of ==?

Based on learnings: In MustCallVisitor.java (Checker Framework), prefer using Name.equals(...) or Objects.equals(...) for com.sun.source.util.Name comparisons (instead of ==/!=). This should be the default unless the Interning Checker is explicitly used to guarantee reference equality.

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 904 - 906, The loop that matches parameter slots uses reference
equality on Name (params.get(i).getSimpleName() == elt.getSimpleName()), which
can fail; change the comparison to test name equality (e.g., use .equals(...) or
.contentEquals(...)) so the branch that calls
type.replaceAnnotation(paramTypes.get(i).getAnnotationInHierarchy(TOP)) runs
reliably; update the condition in the for-loop that compares
params.get(i).getSimpleName() with elt.getSimpleName() to use a content-equality
check.

363-364: ⚠️ Potential issue | 🟡 Minor

Guard elt before dereferencing it.

Both helpers call elt.getKind() or elt.asType() without the null check that isOwningCollectionField(...) already uses, so a defensive caller gets an immediate NPE instead of false.

Minimal fix
   public boolean isResourceCollectionField(Element elt) {
+    if (elt == null) {
+      return false;
+    }
     if (elt.getKind().isField()) {
       if (isResourceCollection(elt.asType())) {
         return true;
@@
   public boolean isOwningCollectionParameter(Element elt) {
+    if (elt == null) {
+      return false;
+    }
     if (isResourceCollection(elt.asType())) {
       if (elt.getKind() == ElementKind.PARAMETER) {

Also applies to: 381-382

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 363 - 364, Guard against null Element inputs in the
collection-check helpers: add an early null check in isResourceCollectionField
(and the other helper(s) that call elt.getKind() or elt.asType(), analogous to
isOwningCollectionField) and return false if elt is null, so callers that
defensively pass null don't get an NPE.

156-176: ⚠️ Potential issue | 🟠 Major

Make the fulfilling-loop caches instance-scoped.

These maps are mutable, keyed by AST and CFG objects, and shared across all checker instances. That lets stale graphs survive between analyses and can mix one run's verified loops into another.

Based on learnings: In checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java, prefer instance fields over static state for analysis caches (e.g., maps keyed by Tree/Block). There is at most one ATF per running checker, so static mutable fields are discouraged.

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 156 - 176, The two caches conditionToVerifiedFulfillingLoopMap and
conditionalBlockToVerifiedFulfillingLoopMap are static and must be instance
fields on CollectionOwnershipAnnotatedTypeFactory to avoid leaking AST/CFG state
across checker instances; change their declarations to non-static instance
members, initialize them in the class constructor (or at declaration time per
instance), and update all usages — including
markFulfillingLoop(ResolvedPotentiallyFulfillingCollectionLoop) and any reads of
these maps — to reference the instance fields
(this.conditionToVerifiedFulfillingLoopMap /
this.conditionalBlockToVerifiedFulfillingLoopMap) instead of the static ones so
each ATF gets its own cache.

575-576: ⚠️ Potential issue | 🔴 Critical

Return null for unsupported trees instead of crashing.

This public helper calls mcAtf.getAnnotatedType(tree) unguarded. Unsupported tree shapes still throw BugInCF here, which bypasses the "no obligations" fallback expected by the consistency analysis.

Minimal fix
   public List<String> getMustCallValuesOfResourceCollectionComponent(Tree tree) {
-    return getMustCallValuesOfResourceCollectionComponent(mcAtf.getAnnotatedType(tree));
+    if (tree == null) {
+      return null;
+    }
+    try {
+      return getMustCallValuesOfResourceCollectionComponent(mcAtf.getAnnotatedType(tree));
+    } catch (BugInCF e) {
+      return null;
+    }
   }
Based on learnings: In MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn, treat a null result from CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...) as “no obligations” and skip creating CollectionObligation(s). This can occur for OwningCollection over non-resource element types.
🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 575 - 576, The helper
CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent
currently calls mcAtf.getAnnotatedType(tree) unguarded and lets BugInCF
propagate; change getMustCallValuesOfResourceCollectionComponent to catch the
BugInCF (and return null if mcAtf.getAnnotatedType(tree) is null or if the tree
shape is unsupported) so unsupported trees yield null instead of throwing, and
then update MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn
to treat a null return from getMustCallValuesOfResourceCollectionComponent(...)
as “no obligations” (i.e., skip creating CollectionObligation instances and
return early).
checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java (1)

226-230: ⚠️ Potential issue | 🔴 Critical

Don't cast the no-CMCF checker to CollectionOwnershipChecker.

This branch accepts MustCallNoCreatesMustCallForChecker, but the body always casts referenceChecker to CollectionOwnershipChecker. Any lookup through that path will fail with ClassCastException; recurse to the parent for the no-CMCF case instead.

🤖 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/resourceleak/ResourceLeakUtils.java`
around lines 226 - 230, The branch in ResourceLeakUtils that checks className
and accepts MustCallNoCreatesMustCallForChecker incorrectly casts
referenceChecker to CollectionOwnershipChecker; change the logic so when
className equals "MustCallNoCreatesMustCallForChecker" you do not cast to
CollectionOwnershipChecker but instead recurse to the parent path (i.e., call
the same lookup on referenceChecker.getParent() or equivalent) to obtain the
correct type factory; only cast to CollectionOwnershipChecker when className
equals "CollectionOwnershipChecker" and use its getTypeFactory() for the
CollectionOwnershipAnnotatedTypeFactory return value.
🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`:
- Around line 545-552: The code treats any type where
ResourceLeakUtils.isCollection(atm.getUnderlyingType()) is true as a collection
but only extracts a component when there's exactly one type argument, which
silently skips Map<K,V>; update CollectionOwnershipAnnotatedTypeFactory to
detect when atm is an AnnotatedDeclaredType representing java.util.Map (or any
two-arg declared type) and, for maps, choose the appropriate component type
(typically the value type, i.e., typeArgs.get(1)) instead of leaving
componentType null; apply the same change to the other similar block (the second
occurrence around the other branch) so Map value types are inspected for
obligations rather than ignored.

In
`@checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java`:
- Around line 261-266: The helper getRlccAtfIfPartOfHierarchy incorrectly treats
a standalone MustCallChecker as part of the RLC hierarchy because
ResourceLeakUtils.rlcCheckers includes MustCallChecker; to fix, change the
search so it does not consider the initial checker itself—start the while loop
from checker.getParent() (or otherwise ignore a match equal to the original
checker) and only call
ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this) when a true
ancestor in the checker hierarchy is found; this ensures
getRlccAtfIfPartOfHierarchy, ResourceLeakUtils.rlcCheckers, and
ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory are only invoked for
actual enclosing RLC checkers (not standalone MustCallChecker).

In
`@checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java`:
- Around line 454-463: The helper hasManualMustCallUnknownAnno treats a
defaulted TOP as if `@MustCallUnknown` were explicitly present because it uses
annotatedTypeMirror.getPrimaryAnnotationInHierarchy(mcAtf.TOP); change this to
detect only explicit annotations: inspect the underlying TypeMirror's annotation
mirrors (annotatedTypeMirror.getUnderlyingType().getAnnotationMirrors()) or call
the existing TypeMirror overload that checks for a manual MustCallUnknown
instead of using mcAtf.TOP; specifically, in hasManualMustCallUnknownAnno
replace the getPrimaryAnnotationInHierarchy-based check (manualMcAnno) with a
loop over the underlying type's AnnotationMirror list and return true only when
an annotation with the canonical name MustCallUnknown is actually present.

---

Duplicate comments:
In
`@checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`:
- Around line 904-906: The loop that matches parameter slots uses reference
equality on Name (params.get(i).getSimpleName() == elt.getSimpleName()), which
can fail; change the comparison to test name equality (e.g., use .equals(...) or
.contentEquals(...)) so the branch that calls
type.replaceAnnotation(paramTypes.get(i).getAnnotationInHierarchy(TOP)) runs
reliably; update the condition in the for-loop that compares
params.get(i).getSimpleName() with elt.getSimpleName() to use a content-equality
check.
- Around line 363-364: Guard against null Element inputs in the collection-check
helpers: add an early null check in isResourceCollectionField (and the other
helper(s) that call elt.getKind() or elt.asType(), analogous to
isOwningCollectionField) and return false if elt is null, so callers that
defensively pass null don't get an NPE.
- Around line 156-176: The two caches conditionToVerifiedFulfillingLoopMap and
conditionalBlockToVerifiedFulfillingLoopMap are static and must be instance
fields on CollectionOwnershipAnnotatedTypeFactory to avoid leaking AST/CFG state
across checker instances; change their declarations to non-static instance
members, initialize them in the class constructor (or at declaration time per
instance), and update all usages — including
markFulfillingLoop(ResolvedPotentiallyFulfillingCollectionLoop) and any reads of
these maps — to reference the instance fields
(this.conditionToVerifiedFulfillingLoopMap /
this.conditionalBlockToVerifiedFulfillingLoopMap) instead of the static ones so
each ATF gets its own cache.
- Around line 575-576: The helper
CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent
currently calls mcAtf.getAnnotatedType(tree) unguarded and lets BugInCF
propagate; change getMustCallValuesOfResourceCollectionComponent to catch the
BugInCF (and return null if mcAtf.getAnnotatedType(tree) is null or if the tree
shape is unsupported) so unsupported trees yield null instead of throwing, and
then update MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn
to treat a null return from getMustCallValuesOfResourceCollectionComponent(...)
as “no obligations” (i.e., skip creating CollectionObligation instances and
return early).

In
`@checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java`:
- Around line 226-230: The branch in ResourceLeakUtils that checks className and
accepts MustCallNoCreatesMustCallForChecker incorrectly casts referenceChecker
to CollectionOwnershipChecker; change the logic so when className equals
"MustCallNoCreatesMustCallForChecker" you do not cast to
CollectionOwnershipChecker but instead recurse to the parent path (i.e., call
the same lookup on referenceChecker.getParent() or equivalent) to obtain the
correct type factory; only cast to CollectionOwnershipChecker when className
equals "CollectionOwnershipChecker" and use its getTypeFactory() for the
CollectionOwnershipAnnotatedTypeFactory return value.
🪄 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: 27bb3f4a-43cb-4c4c-8315-6d85fe69ca0b

📥 Commits

Reviewing files that changed from the base of the PR and between 1b3f47e and 5c6eeef.

📒 Files selected for processing (3)
  • checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java
  • checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java
  • checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java

Comment on lines +545 to +552
boolean isCollectionType = ResourceLeakUtils.isCollection(atm.getUnderlyingType());

AnnotatedTypeMirror componentType = null;
if (isCollectionType) {
List<? extends AnnotatedTypeMirror> typeArgs =
((AnnotatedDeclaredType) atm).getTypeArguments();
if (typeArgs.size() == 1) {
componentType = typeArgs.get(0);
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

Map is classified as a collection, but never gets a component type here.

ResourceLeakUtils.isCollection(...) returns true for Map, but both overloads below only extract a component when there is exactly one type argument. Every Map<K, V> therefore falls through as "no obligations", so map-backed resources are silently skipped. Either handle the key/value choice explicitly here or stop treating Map as a collection in ResourceLeakUtils.

Also applies to: 590-597

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 545 - 552, The code treats any type where
ResourceLeakUtils.isCollection(atm.getUnderlyingType()) is true as a collection
but only extracts a component when there's exactly one type argument, which
silently skips Map<K,V>; update CollectionOwnershipAnnotatedTypeFactory to
detect when atm is an AnnotatedDeclaredType representing java.util.Map (or any
two-arg declared type) and, for maps, choose the appropriate component type
(typically the value type, i.e., typeArgs.get(1)) instead of leaving
componentType null; apply the same change to the other similar block (the second
occurrence around the other branch) so Map value types are inspected for
obligations rather than ignored.

Comment on lines +261 to +266
private @Nullable RLCCalledMethodsAnnotatedTypeFactory getRlccAtfIfPartOfHierarchy() {
SourceChecker currentChecker = checker;
while (currentChecker != null) {
String currentCheckerName = currentChecker.getClass().getCanonicalName();
if (ResourceLeakUtils.rlcCheckers.contains(currentCheckerName)) {
return ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this);
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🔴 Critical

Don't treat every MustCallChecker as if it were inside RLC.

ResourceLeakUtils.rlcCheckers contains MustCallChecker, so a standalone Must Call run makes this helper return non-null. The next call to ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this) then walks to a missing parent and throws, violating the "do nothing outside the hierarchy" contract of the new public record methods.

Possible fix
-      if (ResourceLeakUtils.rlcCheckers.contains(currentCheckerName)) {
+      if ("org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsChecker"
+              .equals(currentCheckerName)
+          || "org.checkerframework.checker.collectionownership.CollectionOwnershipChecker"
+              .equals(currentCheckerName)
+          || "org.checkerframework.checker.resourceleak.ResourceLeakChecker"
+              .equals(currentCheckerName)) {
         return ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this);
       }
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
private @Nullable RLCCalledMethodsAnnotatedTypeFactory getRlccAtfIfPartOfHierarchy() {
SourceChecker currentChecker = checker;
while (currentChecker != null) {
String currentCheckerName = currentChecker.getClass().getCanonicalName();
if (ResourceLeakUtils.rlcCheckers.contains(currentCheckerName)) {
return ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this);
private `@Nullable` RLCCalledMethodsAnnotatedTypeFactory getRlccAtfIfPartOfHierarchy() {
SourceChecker currentChecker = checker;
while (currentChecker != null) {
String currentCheckerName = currentChecker.getClass().getCanonicalName();
if ("org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsChecker"
.equals(currentCheckerName)
|| "org.checkerframework.checker.collectionownership.CollectionOwnershipChecker"
.equals(currentCheckerName)
|| "org.checkerframework.checker.resourceleak.ResourceLeakChecker"
.equals(currentCheckerName)) {
return ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this);
🤖 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, The helper getRlccAtfIfPartOfHierarchy incorrectly
treats a standalone MustCallChecker as part of the RLC hierarchy because
ResourceLeakUtils.rlcCheckers includes MustCallChecker; to fix, change the
search so it does not consider the initial checker itself—start the while loop
from checker.getParent() (or otherwise ignore a match equal to the original
checker) and only call
ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(this) when a true
ancestor in the checker hierarchy is found; this ensures
getRlccAtfIfPartOfHierarchy, ResourceLeakUtils.rlcCheckers, and
ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory are only invoked for
actual enclosing RLC checkers (not standalone MustCallChecker).

Comment on lines +454 to +463
public static boolean hasManualMustCallUnknownAnno(
AnnotatedTypeMirror annotatedTypeMirror, MustCallAnnotatedTypeFactory mcAtf) {
if (annotatedTypeMirror == null) {
return false;
}
AnnotationMirror manualMcAnno = annotatedTypeMirror.getPrimaryAnnotationInHierarchy(mcAtf.TOP);
if (manualMcAnno == null) {
return false;
}
if (AnnotationUtils.areSameByName(manualMcAnno, MustCallUnknown.class.getCanonicalName())) {
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

This helper treats defaulted @MustCallUnknown as if it were written explicitly.

getPrimaryAnnotationInHierarchy(mcAtf.TOP) returns the effective qualifier, so an unannotated upper bound that merely defaults to TOP also makes this return true. That makes the new collection-element rewrite preserve @MustCallUnknown for cases like List<T> instead of resetting them to bottom. Reuse the TypeMirror overload or inspect annotatedTypeMirror.getUnderlyingType().getAnnotationMirrors() here.

🤖 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/resourceleak/ResourceLeakUtils.java`
around lines 454 - 463, The helper hasManualMustCallUnknownAnno treats a
defaulted TOP as if `@MustCallUnknown` were explicitly present because it uses
annotatedTypeMirror.getPrimaryAnnotationInHierarchy(mcAtf.TOP); change this to
detect only explicit annotations: inspect the underlying TypeMirror's annotation
mirrors (annotatedTypeMirror.getUnderlyingType().getAnnotationMirrors()) or call
the existing TypeMirror overload that checks for a manual MustCallUnknown
instead of using mcAtf.TOP; specifically, in hasManualMustCallUnknownAnno
replace the getPrimaryAnnotationInHierarchy-based check (manualMcAnno) with a
loop over the underlying type's AnnotationMirror list and return true only when
an annotation with the canonical name MustCallUnknown is actually present.

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 2

♻️ Duplicate comments (19)
checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipTransfer.java (2)

256-283: ⚠️ Potential issue | 🔴 Critical

Guard argElem before the field-ownership branch.

TreeUtils.elementFromTree(arg.getTree()) is still nullable for synthetic/temp argument shapes. argElem.getKind() can therefore NPE before the non-field fallback runs. Treat a null element like a non-field temp/result and take the replaceInStores(...) path.

🤖 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/collectionownership/CollectionOwnershipTransfer.java`
around lines 256 - 283, The code currently assumes argElem from
TreeUtils.elementFromTree(arg.getTree()) is non-null before calling
argElem.getKind(), which can NPE for synthetic/temp argument shapes; guard the
null case by checking if argElem == null before the field branch and treat null
the same as a non-field (i.e., do not call argElem.getKind().isField(), instead
execute the replaceInStores(res, argJE, atypeFactory.NOTOWNINGCOLLECTION) path
when argElem is null), keeping the existing behavior for when transferOwnership
is true and argElem is a real field (use checker.reportError(arg.getTree(),
"transfer.owningcollection.field.ownership", arg.getTree().toString())).

128-131: ⚠️ Potential issue | 🔴 Critical

Handle non-resource collection elements without throwing.

getMustCallValuesOfResourceCollectionComponent(...) can still be null here. containsAll(null) will crash the transfer instead of treating the collection as having no element obligations and leaving the store unchanged.

Based on learnings: treat a null result from CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(..) as “no obligations” and skip creating CollectionObligation(s); do not throw.

🤖 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/collectionownership/CollectionOwnershipTransfer.java`
around lines 128 - 131, The call to
CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...)
can return null, and calling containsAll on mustCallValuesOfElements will throw;
update the transfer logic around verifiedFulfillingLoop to treat a null
mustCallValuesOfElements as "no obligations" by checking for null before using
containsAll and by only creating CollectionObligation(s) when
mustCallValuesOfElements is non-null and non-empty; reference the
variables/methods mustCallValuesOfElements,
verifiedFulfillingLoop.getCalledMethods(),
getMustCallValuesOfResourceCollectionComponent(...), and the code path that
constructs CollectionObligation so it is skipped when the factory returns null.
checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java (7)

907-914: ⚠️ Potential issue | 🔴 Critical

Don't throw on a missing component must-call list.

@OwningCollection can still appear over element types with no must-call obligation. Throwing BugInCF here aborts analysis instead of meaning “no collection obligations for this return value”.

Based on learnings: in MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn, treat a null result from CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...) as “no obligations” and skip creating CollectionObligation(s).

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 907 - 914, The code in
MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn currently
throws BugInCF when
CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...)
returns null; instead treat a null mustCallValues as “no obligations” and skip
creating any CollectionObligation(s). Modify the logic around the mustCallValues
variable so that if mustCallValues == null you simply return/continue (do not
construct CollectionObligation objects or throw), otherwise proceed to create
obligations from the returned list; keep references to the node and existing
CollectionObligation creation code unchanged.

3740-3743: ⚠️ Potential issue | 🟠 Major

Null-check cmValOfIce before reading its called methods.

store.getValue(ice) can still be null here. getCalledMethods(cmValOfIce) dereferences it immediately and will abort the loop-body analysis.

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 3740 - 3743, The code calls getCalledMethods(cmValOfIce) without
ensuring cmValOfIce is non-null; after obtaining AccumulationValue cmValOfIce =
store.getValue(ice) add a null-check (e.g., if (cmValOfIce == null) continue; or
otherwise skip/handle) before calling getCalledMethods so you never dereference
a null AccumulationValue; update the block around the variables ice, cmValOfIce,
store.getValue(ice), and getCalledMethods to handle the null case safely.

3573-3586: ⚠️ Potential issue | 🔴 Critical

A null back-edge summary must invalidate the whole loop.

When one back edge returns null from analyzeTypeOfCollectionElement(...), skipping the intersection leaves previously learned methods intact. A single unsatisfied path can therefore still let the loop be marked fulfilling.

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 3573 - 3586, The code treats a null result from
analyzeTypeOfCollectionElement(...) as ignorable, which keeps previously
accumulated calledMethodsInLoop and can incorrectly mark the loop fulfilling;
change the logic in the isLastBlockOfBody branch so that when
calledMethodsAfterBlock is null you set calledMethodsInLoop to null
(invalidating the whole loop) instead of leaving the prior set intact (and then
short-circuit further intersection handling as appropriate). Refer to
analyzeTypeOfCollectionElement, calledMethodsAfterBlock, and calledMethodsInLoop
to locate and implement this null-path invalidation.

2059-2065: ⚠️ Potential issue | 🟠 Major

Guard the element-method lookup before building the diagnostic.

Both error paths still call .get(0) on getMustCallValuesOfResourceCollectionComponent(...) without a null/empty check. That can NPE or throw IndexOutOfBoundsException instead of reporting the reassignment error. Fall back to "Unknown" when the list is absent.

Based on learnings: when constructing diagnostics that reference an element method name, fall back to "Unknown" if the list is null/empty.

Also applies to: 2140-2143

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 2059 - 2065, The diagnostic construction calls
coAtf.getMustCallValuesOfResourceCollectionComponent(...) and immediately
.get(0) which can NPE/IndexOutOfBounds; change MustCallConsistencyAnalyzer to
guard the lookup by retrieving the list into a local (e.g., names =
coAtf.getMustCallValuesOfResourceCollectionComponent(lhs.getTree())), check for
null or empty and use the string "Unknown" when building the checker.reportError
call (instead of unguarded .get(0)); apply the same fix to the other occurrence
around the reported range (the similar block at ~2140-2143) so both error paths
safely fall back to "Unknown".

967-975: ⚠️ Potential issue | 🟠 Major

Don't consume the source obligation after checkEnclosingMethodIsCreatesMustCallFor(...) reports an error.

Both call sites still remove the inserted/RHS obligation even when checkEnclosingMethodIsCreatesMustCallFor(...) returns false. That makes the analysis behave as though ownership moved into the collection/field anyway.

Also applies to: 2127-2135

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 967 - 975, The code currently calls
consumeInsertedArgumentObligationIfSingleElementInsert(obligations, node)
unconditionally even after
checkEnclosingMethodIsCreatesMustCallFor(receiverNode, enclosingMethodTree)
returns false; capture the boolean result of
checkEnclosingMethodIsCreatesMustCallFor and only call
consumeInsertedArgumentObligationIfSingleElementInsert when that result is true
(i.e., ownership was transferred), and make the same change at the other
identical call site so the source obligation is not removed when the check
reports an error.

2092-2118: ⚠️ Potential issue | 🔴 Critical

Treat OwningCollectionBottom as the null-field case, not a BugInCF.

The comment on Lines 2113-2117 already says bottom means null, but this branch still aborts analysis. Reassigning an owning collection into a field that currently holds null should take the safe first-assignment / @CreatesMustCallFor path instead of crashing.

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 2092 - 2118, The code currently throws a BugInCF when lhsCoType ==
CollectionOwnershipType.OwningCollectionBottom, but OwningCollectionBottom
represents null and should be treated like the "first assignment into a null
field" case; update the MustCallConsistencyAnalyzer logic so that when lhsCoType
== CollectionOwnershipType.OwningCollectionBottom you follow the same safe
first-assignment/@CreatesMustCallFor handling (e.g., call
getObligationsForVar(rhs.getTree()), remove those obligations from obligations,
and return) instead of throwing; ensure you reference lhsCoType,
CollectionOwnershipType.OwningCollectionBottom,
enclosingMethodTree/isOwningCollectionField, getObligationsForVar, rhs, and
obligations so the change is applied in the same conditional branch.

933-960: ⚠️ Potential issue | 🟠 Major

Model @CreatesCollectionObligation only on the normal edge, and enforce it on every later exit.

This helper is still invoked from updateObligationsForInvocation(...) on exceptional successors, and it still creates the new obligation via CollectionObligation.fromTree(...), which gives it NORMAL_RETURN. That can fabricate obligations in catch paths and also miss leaks when insertion succeeds but the enclosing method later exits exceptionally.

Also applies to: 1087-1089

🤖 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/resourceleak/MustCallConsistencyAnalyzer.java`
around lines 933 - 960, The helper
addObligationsForCreatesCollectionObligationAnno is being run on exceptional
successor edges and creates obligations with CollectionObligation.fromTree(...),
which sets NORMAL_RETURN and thus can fabricate obligations on catch paths and
miss leaks on later exceptional exits; fix by only invoking
addObligationsForCreatesCollectionObligationAnno from
updateObligationsForInvocation when handling the normal successor edge (skip
calling it for exceptional successors), and when constructing the obligation
ensure you create it with a return-kind that enforces on every later exit rather
than NORMAL_RETURN (replace the CollectionObligation.fromTree(...) call or use
the API overload that accepts a ReturnKind/all-returns flag so the created
obligation applies to all subsequent exits).
checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java (3)

1130-1143: ⚠️ Potential issue | 🔴 Critical

Bail out when the CFG lookup doesn't produce the expected shape.

collectionEltNodes.iterator().next() still assumes a non-empty mapping, and the casts to SingleSuccessorBlock / ConditionalBlock still trust one lowering. A slightly different CFG shape should conservatively skip the match, not crash the 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/MustCallVisitor.java`
around lines 1130 - 1143, The code assumes collectionEltNodes non-empty and
specific CFG shapes; change MustCallVisitor so it bails out conservatively when
assumptions fail: check collectionEltNodes != null &&
!collectionEltNodes.isEmpty() before calling
collectionEltNodes.iterator().next() (so nodeForCollectionElt is only set when
present), and verify the CFG shapes by testing types and successors before
casting—i.e., confirm loopConditionBlock is an instance of SingleSuccessorBlock
and its getSuccessor() is non-null and an instance of ConditionalBlock (or that
conditionalBlock.getThenSuccessor() is non-null) before assigning
conditionalBlock and loopBodyEntryBlock; if any check fails, return early
instead of casting or dereferencing.

968-1050: ⚠️ Potential issue | 🟠 Major

Reject abrupt control flow in matched loop bodies.

These scanners still don't invalidate the match on continue, and the same problem applies to other abrupt-control-flow exits in this code. Any such path can skip the extraction/required calls for the current element while the loop is still recorded as fulfilling.

Also applies to: 1239-1300

🤖 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/MustCallVisitor.java`
around lines 968 - 1050, The loop-body scanner in
findSingleExtractionInWhileBody fails to invalidate matches when an abrupt
control flow (continue/break/return/throw) can skip the extraction; override the
TreeScanner handlers for ContinueTree, BreakTree, ReturnTree, and ThrowTree (and
any other abrupt-exit tree types used elsewhere) to set illegal.set(true) so any
such path marks the match invalid, and apply the same changes to the analogous
scanner referenced in the other block (the code around visit methods at the
second location).

981-985: ⚠️ Potential issue | 🟠 Major

Use value equality for Name objects.

These comparisons still rely on ==/!= for Name. That silently depends on interning and can miss iterator/collection matches, making the loop matcher unstable across compiler implementations.

Based on learnings: in MustCallVisitor.java, prefer using Name.equals(...) or Objects.equals(...) for com.sun.source.util.Name comparisons (instead of ==/!=).

Also applies to: 1076-1077, 1202-1207, 1253-1275, 1284-1286, 1396-1397

🤖 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/MustCallVisitor.java`
around lines 981 - 985, The code in MustCallVisitor methods (e.g.,
markWriteIfTargetsHeaderOrCollection) uses reference equality (==/!=) for
com.sun.source.util.Name comparisons which is unsafe; change those checks to
value equality using Objects.equals(...) (or Name.equals(...))—for example
replace "if (assigned == headerVar)" with "if (Objects.equals(assigned,
headerVar))" and similarly for collectionVarName and all other occurrences
listed (around lines ~1076, ~1202-1207, ~1253-1275, ~1284-1286, ~1396-1397); add
the import for java.util.Objects if not present.
checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java (3)

1372-1377: ⚠️ Potential issue | 🟠 Major

Use Name.equals(...) when matching the enhanced-for variable.

Line 1376 compares Name instances with ==. If interning does not line up, enhanced-for resolution never finds the loop-variable assignment and the loop is silently skipped.

Does `javax.lang.model.element.Name` guarantee reference equality for equal names, or should annotation processors compare `Name` values with `.equals(...)` / `.contentEquals(...)` instead of `==`?
Suggested fix
-          isAssignmentOfLoopVariable =
-              iteratorVariableDeclaration.getName() == loopVariable.getName();
+          isAssignmentOfLoopVariable =
+              iteratorVariableDeclaration.getName().equals(loopVariable.getName());

Based on learnings: In MustCallVisitor.java (Checker Framework), prefer using Name.equals(...) or Objects.equals(...) for com.sun.source.util.Name comparisons (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 1372 - 1377, The comparison of enhanced-for variable names uses
reference equality (==) which can fail; in RLCCalledMethodsAnnotatedTypeFactory
replace the identity check in the AssignmentNode/VariableTree branch so that
isAssignmentOfLoopVariable compares names with .equals(...) (or
Objects.equals(...)/contentEquals(...)) against loopVariable.getName() when
computing isAssignmentOfLoopVariable for loopVariableNode, ensuring proper
detection of the loop-variable assignment.

390-409: ⚠️ Potential issue | 🟠 Major

Key loop state by the actual CFG owner, not just MethodTree.

getMethodCollectionLoopState(...) only handles UnderlyingAST.Kind.METHOD, so loops discovered inside lambdas never become visible to the lambda CFG's store seeding or postAnalyze(...). The enclosing-method cleanup at Line 1200 then drops that state before the lambda can be analyzed. Consider keying this state by the actual UnderlyingAST/lambda instead of only the enclosing method.

Also applies to: 450-469, 1188-1200

🤖 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 390 - 409, The loop state map is keyed only by MethodTree so loops
inside lambdas are lost before the lambda CFG is seeded; update the logic to key
loop state by the actual CFG owner (UnderlyingAST) rather than only the
enclosing MethodTree: change getOrCreateMethodCollectionLoopState /
getMethodCollectionLoopState to accept an UnderlyingAST (or to compute a unique
key from getEnclosingMethodTree(underlyingAST) fallbacking to the underlyingAST
for lambdas), store MethodCollectionLoopState in a map keyed by that
UnderlyingAST (or its unique owner id) instead of
collectionLoopStateByEnclosingMethod, and adjust the enclosing-method cleanup
(the cleanup code around postAnalyze) to remove entries by that same
UnderlyingAST key so lambda loop state remains available until the lambda CFG is
analyzed.

1515-1531: ⚠️ Potential issue | 🟠 Major

Record the latch block as loopUpdateBlock.

For a back edge source -> target, target is the loop header. Using it here makes later store reads observe header/condition state instead of the post-iteration latch state.

Suggested fix
         if (naturalLoop.size() < bestLoopSize) {
           bestLoopSize = naturalLoop.size();
-          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 1515 - 1531, The code picks the loop header (backEdge.targetBlock)
as the update/latch block which makes later reads see header/condition state;
instead record the latch block instead: when selecting the best loop in the
loop-selection loop over WhileLoopResolutionCache.BlockEdge from
whileLoopCache.getBackEdges(), set bestLoopUpdateBlock (aka loopUpdateBlock) to
the back edge's source (the latch) rather than backEdge.targetBlock (the
header), keeping the same loop-size comparison using naturalLoop.size() and the
same containment checks against bodyEntryBlock and conditionalBlock.
checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java (4)

156-177: ⚠️ Potential issue | 🟠 Major

Make the fulfilling-loop caches instance-scoped.

These maps are static, mutable, and keyed by AST/CFG objects. They can retain old graphs for the lifetime of the JVM and share stale state across checker instances. markFulfillingLoop(...) and the lookup APIs should live on the ATF instance instead.

Suggested fix
-  private static final Map<Tree, ResolvedPotentiallyFulfillingCollectionLoop>
+  private final Map<Tree, ResolvedPotentiallyFulfillingCollectionLoop>
       conditionToVerifiedFulfillingLoopMap = new HashMap<>();
@@
-  private static final Map<Block, ResolvedPotentiallyFulfillingCollectionLoop>
+  private final Map<Block, ResolvedPotentiallyFulfillingCollectionLoop>
       conditionalBlockToVerifiedFulfillingLoopMap = new HashMap<>();
@@
-  public static void markFulfillingLoop(
+  public void markFulfillingLoop(
       ResolvedPotentiallyFulfillingCollectionLoop verifiedFulfillingLoop) {
@@
-  public static ResolvedPotentiallyFulfillingCollectionLoop getFulfillingLoopForCondition(
+  public ResolvedPotentiallyFulfillingCollectionLoop getFulfillingLoopForCondition(
       Tree tree) {

Based on learnings: In checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java, prefer instance fields over static state for analysis caches (e.g., maps keyed by Tree/Block). There is at most one ATF per running checker, so static mutable fields are discouraged.

Also applies to: 185-200

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 156 - 177, The two static mutable maps
conditionToVerifiedFulfillingLoopMap and
conditionalBlockToVerifiedFulfillingLoopMap and the method markFulfillingLoop in
CollectionOwnershipAnnotatedTypeFactory should be converted to instance-level
state/methods: remove the static modifier from both maps and from
markFulfillingLoop (and any lookup APIs that access these maps), initialize the
maps in the ATF constructor (or inline as instance fields), and update all call
sites to use the ATF instance instead of referencing static members so the
caches are tied to the ATF instance and do not leak/stale across checkers.

545-553: ⚠️ Potential issue | 🟠 Major

Handle Map<K,V> consistently with isCollection(...).

Both overloads only extract a component when there is exactly one type argument. If ResourceLeakUtils.isCollection(...) still includes Map, every map value obligation is silently dropped here.

Verify whether isCollection(...) still classifies maps as collections:

#!/bin/bash
sed -n '541,606p' checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java
rg -n -C3 'isCollection\s*\(' checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java

Also applies to: 590-597

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 545 - 553, The code assumes collections have exactly one type
argument and sets componentType only when typeArgs.size() == 1, which drops Map
value obligations if ResourceLeakUtils.isCollection(...) classifies maps as
collections; update the logic in CollectionOwnershipAnnotatedTypeFactory (the
block using ResourceLeakUtils.isCollection(atm.getUnderlyingType()), atm, and
componentType) to detect Map types (or typeArgs.size() == 2) and in that case
extract the value type argument (typeArgs.get(1)) as the componentType, while
keeping the existing behavior for single-argument collections; apply the same
fix to the other overload/section referenced around the 590-597 region so maps
are handled consistently.

907-909: ⚠️ Potential issue | 🟠 Major

Don't use == on parameter Names.

Line 908 compares Name instances by reference. When that misses, the parameter's ownership qualifier is not propagated to the use site.

Does `javax.lang.model.element.Name` guarantee reference equality for equal names, or should annotation processors compare `Name` values with `.equals(...)` / `.contentEquals(...)` instead of `==`?
Suggested fix
-            if (params.get(i).getSimpleName() == elt.getSimpleName()) {
+            if (params.get(i).getSimpleName().equals(elt.getSimpleName())) {
               type.replaceAnnotation(paramTypes.get(i).getAnnotationInHierarchy(TOP));
               break;
             }

Based on learnings: In MustCallVisitor.java (Checker Framework), prefer using Name.equals(...) or Objects.equals(...) for com.sun.source.util.Name comparisons (instead of ==/!=). This should be the default unless the Interning Checker is explicitly used to guarantee reference equality.

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 907 - 909, In CollectionOwnershipAnnotatedTypeFactory (inside the
loop over params where params.get(i).getSimpleName() is compared to
elt.getSimpleName()), replace the reference equality check using == with a
proper value comparison (e.g., .equals(...) or .contentEquals(...)) so Name
instances are compared by content; keep the rest of the logic (using
paramTypes.get(i).getAnnotationInHierarchy(TOP) and type.replaceAnnotation(...))
unchanged so the parameter ownership qualifier is correctly propagated to the
use site.

575-576: ⚠️ Potential issue | 🔴 Critical

Return null for unsupported trees instead of crashing.

The Tree overload is still unguarded, so mcAtf.getAnnotatedType(tree) can throw BugInCF here even though callers use null to mean “no obligations”.

Verify that isResourceCollection(Tree) already guards this path and that callers depend on the null-return contract:

#!/bin/bash
sed -n '410,423p' checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java
sed -n '571,577p' checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java
rg -n -C2 'getMustCallValuesOfResourceCollectionComponent\(' checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
Suggested fix
   public List<String> getMustCallValuesOfResourceCollectionComponent(Tree tree) {
-    return getMustCallValuesOfResourceCollectionComponent(mcAtf.getAnnotatedType(tree));
+    if (tree == null) {
+      return null;
+    }
+    try {
+      return getMustCallValuesOfResourceCollectionComponent(mcAtf.getAnnotatedType(tree));
+    } catch (BugInCF e) {
+      return null;
+    }
   }

Based on learnings: In MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn, treat a null result from CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...) as “no obligations” and skip creating CollectionObligation(s); do not throw. This can occur for OwningCollection over non-resource element types.

🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 575 - 576, The Tree overload
getMustCallValuesOfResourceCollectionComponent(Tree) currently calls
mcAtf.getAnnotatedType(tree) unguarded and can throw BugInCF; change it to
return null for unsupported trees by either first checking
isResourceCollection(tree) and returning null if false, or catching the
exception from mcAtf.getAnnotatedType(tree) and returning null; update callers
(notably MustCallConsistencyAnalyzer.addObligationsForOwningCollection) to treat
a null return as “no obligations” and skip creating CollectionObligation(s)
rather than throwing.
🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`:
- Around line 492-503: The checks in CollectionOwnershipAnnotatedTypeFactory use
Element.getAnnotation on insertedElement for NotOwning and Owning, which
bypasses stub-aware logic; change those checks to use the
RLCCalledMethodsAnnotatedTypeFactory helpers
(rlAtf.hasNotOwning(insertedElement) and rlAtf.hasOwning(insertedElement)) so
stub annotations are respected and the returned CollectionMutatorArgumentKind
(DEFINITELY_NON_OWNING or MAY_BE_OWNING) is correct.

In
`@checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java`:
- Around line 1179-1223: In nameOfCollectionThatAllElementsAreCalledOn(...), add
a check that condition.getKind() is Tree.Kind.LESS_THAN (i.e., a '<' comparison)
before proceeding to inspect left/right operands; if the kind is not LESS_THAN
return null. Place this check near the start of the condition-handling block
(before using condition.getLeftOperand()/getRightOperand()) so loops with other
operators (==, >, <=, etc.) are not classified as "all elements".

---

Duplicate comments:
In
`@checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`:
- Around line 156-177: The two static mutable maps
conditionToVerifiedFulfillingLoopMap and
conditionalBlockToVerifiedFulfillingLoopMap and the method markFulfillingLoop in
CollectionOwnershipAnnotatedTypeFactory should be converted to instance-level
state/methods: remove the static modifier from both maps and from
markFulfillingLoop (and any lookup APIs that access these maps), initialize the
maps in the ATF constructor (or inline as instance fields), and update all call
sites to use the ATF instance instead of referencing static members so the
caches are tied to the ATF instance and do not leak/stale across checkers.
- Around line 545-553: The code assumes collections have exactly one type
argument and sets componentType only when typeArgs.size() == 1, which drops Map
value obligations if ResourceLeakUtils.isCollection(...) classifies maps as
collections; update the logic in CollectionOwnershipAnnotatedTypeFactory (the
block using ResourceLeakUtils.isCollection(atm.getUnderlyingType()), atm, and
componentType) to detect Map types (or typeArgs.size() == 2) and in that case
extract the value type argument (typeArgs.get(1)) as the componentType, while
keeping the existing behavior for single-argument collections; apply the same
fix to the other overload/section referenced around the 590-597 region so maps
are handled consistently.
- Around line 907-909: In CollectionOwnershipAnnotatedTypeFactory (inside the
loop over params where params.get(i).getSimpleName() is compared to
elt.getSimpleName()), replace the reference equality check using == with a
proper value comparison (e.g., .equals(...) or .contentEquals(...)) so Name
instances are compared by content; keep the rest of the logic (using
paramTypes.get(i).getAnnotationInHierarchy(TOP) and type.replaceAnnotation(...))
unchanged so the parameter ownership qualifier is correctly propagated to the
use site.
- Around line 575-576: The Tree overload
getMustCallValuesOfResourceCollectionComponent(Tree) currently calls
mcAtf.getAnnotatedType(tree) unguarded and can throw BugInCF; change it to
return null for unsupported trees by either first checking
isResourceCollection(tree) and returning null if false, or catching the
exception from mcAtf.getAnnotatedType(tree) and returning null; update callers
(notably MustCallConsistencyAnalyzer.addObligationsForOwningCollection) to treat
a null return as “no obligations” and skip creating CollectionObligation(s)
rather than throwing.

In
`@checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipTransfer.java`:
- Around line 256-283: The code currently assumes argElem from
TreeUtils.elementFromTree(arg.getTree()) is non-null before calling
argElem.getKind(), which can NPE for synthetic/temp argument shapes; guard the
null case by checking if argElem == null before the field branch and treat null
the same as a non-field (i.e., do not call argElem.getKind().isField(), instead
execute the replaceInStores(res, argJE, atypeFactory.NOTOWNINGCOLLECTION) path
when argElem is null), keeping the existing behavior for when transferOwnership
is true and argElem is a real field (use checker.reportError(arg.getTree(),
"transfer.owningcollection.field.ownership", arg.getTree().toString())).
- Around line 128-131: The call to
CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...)
can return null, and calling containsAll on mustCallValuesOfElements will throw;
update the transfer logic around verifiedFulfillingLoop to treat a null
mustCallValuesOfElements as "no obligations" by checking for null before using
containsAll and by only creating CollectionObligation(s) when
mustCallValuesOfElements is non-null and non-empty; reference the
variables/methods mustCallValuesOfElements,
verifiedFulfillingLoop.getCalledMethods(),
getMustCallValuesOfResourceCollectionComponent(...), and the code path that
constructs CollectionObligation so it is skipped when the factory returns null.

In
`@checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java`:
- Around line 1130-1143: The code assumes collectionEltNodes non-empty and
specific CFG shapes; change MustCallVisitor so it bails out conservatively when
assumptions fail: check collectionEltNodes != null &&
!collectionEltNodes.isEmpty() before calling
collectionEltNodes.iterator().next() (so nodeForCollectionElt is only set when
present), and verify the CFG shapes by testing types and successors before
casting—i.e., confirm loopConditionBlock is an instance of SingleSuccessorBlock
and its getSuccessor() is non-null and an instance of ConditionalBlock (or that
conditionalBlock.getThenSuccessor() is non-null) before assigning
conditionalBlock and loopBodyEntryBlock; if any check fails, return early
instead of casting or dereferencing.
- Around line 968-1050: The loop-body scanner in findSingleExtractionInWhileBody
fails to invalidate matches when an abrupt control flow
(continue/break/return/throw) can skip the extraction; override the TreeScanner
handlers for ContinueTree, BreakTree, ReturnTree, and ThrowTree (and any other
abrupt-exit tree types used elsewhere) to set illegal.set(true) so any such path
marks the match invalid, and apply the same changes to the analogous scanner
referenced in the other block (the code around visit methods at the second
location).
- Around line 981-985: The code in MustCallVisitor methods (e.g.,
markWriteIfTargetsHeaderOrCollection) uses reference equality (==/!=) for
com.sun.source.util.Name comparisons which is unsafe; change those checks to
value equality using Objects.equals(...) (or Name.equals(...))—for example
replace "if (assigned == headerVar)" with "if (Objects.equals(assigned,
headerVar))" and similarly for collectionVarName and all other occurrences
listed (around lines ~1076, ~1202-1207, ~1253-1275, ~1284-1286, ~1396-1397); add
the import for java.util.Objects if not present.

In
`@checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java`:
- Around line 907-914: The code in
MustCallConsistencyAnalyzer.addObligationsForOwningCollectionReturn currently
throws BugInCF when
CollectionOwnershipAnnotatedTypeFactory.getMustCallValuesOfResourceCollectionComponent(...)
returns null; instead treat a null mustCallValues as “no obligations” and skip
creating any CollectionObligation(s). Modify the logic around the mustCallValues
variable so that if mustCallValues == null you simply return/continue (do not
construct CollectionObligation objects or throw), otherwise proceed to create
obligations from the returned list; keep references to the node and existing
CollectionObligation creation code unchanged.
- Around line 3740-3743: The code calls getCalledMethods(cmValOfIce) without
ensuring cmValOfIce is non-null; after obtaining AccumulationValue cmValOfIce =
store.getValue(ice) add a null-check (e.g., if (cmValOfIce == null) continue; or
otherwise skip/handle) before calling getCalledMethods so you never dereference
a null AccumulationValue; update the block around the variables ice, cmValOfIce,
store.getValue(ice), and getCalledMethods to handle the null case safely.
- Around line 3573-3586: The code treats a null result from
analyzeTypeOfCollectionElement(...) as ignorable, which keeps previously
accumulated calledMethodsInLoop and can incorrectly mark the loop fulfilling;
change the logic in the isLastBlockOfBody branch so that when
calledMethodsAfterBlock is null you set calledMethodsInLoop to null
(invalidating the whole loop) instead of leaving the prior set intact (and then
short-circuit further intersection handling as appropriate). Refer to
analyzeTypeOfCollectionElement, calledMethodsAfterBlock, and calledMethodsInLoop
to locate and implement this null-path invalidation.
- Around line 2059-2065: The diagnostic construction calls
coAtf.getMustCallValuesOfResourceCollectionComponent(...) and immediately
.get(0) which can NPE/IndexOutOfBounds; change MustCallConsistencyAnalyzer to
guard the lookup by retrieving the list into a local (e.g., names =
coAtf.getMustCallValuesOfResourceCollectionComponent(lhs.getTree())), check for
null or empty and use the string "Unknown" when building the checker.reportError
call (instead of unguarded .get(0)); apply the same fix to the other occurrence
around the reported range (the similar block at ~2140-2143) so both error paths
safely fall back to "Unknown".
- Around line 967-975: The code currently calls
consumeInsertedArgumentObligationIfSingleElementInsert(obligations, node)
unconditionally even after
checkEnclosingMethodIsCreatesMustCallFor(receiverNode, enclosingMethodTree)
returns false; capture the boolean result of
checkEnclosingMethodIsCreatesMustCallFor and only call
consumeInsertedArgumentObligationIfSingleElementInsert when that result is true
(i.e., ownership was transferred), and make the same change at the other
identical call site so the source obligation is not removed when the check
reports an error.
- Around line 2092-2118: The code currently throws a BugInCF when lhsCoType ==
CollectionOwnershipType.OwningCollectionBottom, but OwningCollectionBottom
represents null and should be treated like the "first assignment into a null
field" case; update the MustCallConsistencyAnalyzer logic so that when lhsCoType
== CollectionOwnershipType.OwningCollectionBottom you follow the same safe
first-assignment/@CreatesMustCallFor handling (e.g., call
getObligationsForVar(rhs.getTree()), remove those obligations from obligations,
and return) instead of throwing; ensure you reference lhsCoType,
CollectionOwnershipType.OwningCollectionBottom,
enclosingMethodTree/isOwningCollectionField, getObligationsForVar, rhs, and
obligations so the change is applied in the same conditional branch.
- Around line 933-960: The helper
addObligationsForCreatesCollectionObligationAnno is being run on exceptional
successor edges and creates obligations with CollectionObligation.fromTree(...),
which sets NORMAL_RETURN and thus can fabricate obligations on catch paths and
miss leaks on later exceptional exits; fix by only invoking
addObligationsForCreatesCollectionObligationAnno from
updateObligationsForInvocation when handling the normal successor edge (skip
calling it for exceptional successors), and when constructing the obligation
ensure you create it with a return-kind that enforces on every later exit rather
than NORMAL_RETURN (replace the CollectionObligation.fromTree(...) call or use
the API overload that accepts a ReturnKind/all-returns flag so the created
obligation applies to all subsequent exits).

In
`@checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java`:
- Around line 1372-1377: The comparison of enhanced-for variable names uses
reference equality (==) which can fail; in RLCCalledMethodsAnnotatedTypeFactory
replace the identity check in the AssignmentNode/VariableTree branch so that
isAssignmentOfLoopVariable compares names with .equals(...) (or
Objects.equals(...)/contentEquals(...)) against loopVariable.getName() when
computing isAssignmentOfLoopVariable for loopVariableNode, ensuring proper
detection of the loop-variable assignment.
- Around line 390-409: The loop state map is keyed only by MethodTree so loops
inside lambdas are lost before the lambda CFG is seeded; update the logic to key
loop state by the actual CFG owner (UnderlyingAST) rather than only the
enclosing MethodTree: change getOrCreateMethodCollectionLoopState /
getMethodCollectionLoopState to accept an UnderlyingAST (or to compute a unique
key from getEnclosingMethodTree(underlyingAST) fallbacking to the underlyingAST
for lambdas), store MethodCollectionLoopState in a map keyed by that
UnderlyingAST (or its unique owner id) instead of
collectionLoopStateByEnclosingMethod, and adjust the enclosing-method cleanup
(the cleanup code around postAnalyze) to remove entries by that same
UnderlyingAST key so lambda loop state remains available until the lambda CFG is
analyzed.
- Around line 1515-1531: The code picks the loop header (backEdge.targetBlock)
as the update/latch block which makes later reads see header/condition state;
instead record the latch block instead: when selecting the best loop in the
loop-selection loop over WhileLoopResolutionCache.BlockEdge from
whileLoopCache.getBackEdges(), set bestLoopUpdateBlock (aka loopUpdateBlock) to
the back edge's source (the latch) rather than backEdge.targetBlock (the
header), keeping the same loop-size comparison using naturalLoop.size() and the
same containment checks against bodyEntryBlock and conditionalBlock.
🪄 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: 6fe9b8e3-4b79-4089-b66e-7196cab1564e

📥 Commits

Reviewing files that changed from the base of the PR and between 5c6eeef and 91e9f76.

📒 Files selected for processing (5)
  • checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java
  • checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipTransfer.java
  • checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java
  • checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
  • checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java

Comment on lines +492 to +503
// If the inserted element annotated as @NotOwning, then it's definitely not owning
Element insertedElement = TreeUtils.elementFromTree(insertedArgumentTree);
if (insertedElement != null && insertedElement.getAnnotation(NotOwning.class) != null) {
return CollectionMutatorArgumentKind.DEFINITELY_NON_OWNING;
}

// If the inserted element is a parameter, and it has no explicit @Owning annotation, then it's
// definitely not owning.
if (insertedElement != null && insertedElement.getKind() == ElementKind.PARAMETER) {
return insertedElement.getAnnotation(Owning.class) == null
? CollectionMutatorArgumentKind.DEFINITELY_NON_OWNING
: CollectionMutatorArgumentKind.MAY_BE_OWNING;
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
sed -n '489,524p' checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java
sed -n '942,960p' checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java

Repository: typetools/checker-framework

Length of output: 2752


Use stub-aware helper methods for checking annotations on inserted elements.

The code directly calls Element.getAnnotation(...) for @NotOwning and @Owning, which bypasses the stub-aware helpers in RLCCalledMethodsAnnotatedTypeFactory. A parameter with @Owning in a stub file will be incorrectly classified as DEFINITELY_NON_OWNING, breaking soundness of collection obligation transfer.

Use rlAtf.hasNotOwning(insertedElement) and rlAtf.hasOwning(insertedElement) instead, which properly check stub files via getDeclAnnotation.

Suggested fix
-    if (insertedElement != null && insertedElement.getAnnotation(NotOwning.class) != null) {
+    if (insertedElement != null && rlAtf.hasNotOwning(insertedElement)) {
       return CollectionMutatorArgumentKind.DEFINITELY_NON_OWNING;
     }
@@
     if (insertedElement != null && insertedElement.getKind() == ElementKind.PARAMETER) {
-      return insertedElement.getAnnotation(Owning.class) == null
+      return !rlAtf.hasOwning(insertedElement)
           ? CollectionMutatorArgumentKind.DEFINITELY_NON_OWNING
           : CollectionMutatorArgumentKind.MAY_BE_OWNING;
     }
🤖 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/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java`
around lines 492 - 503, The checks in CollectionOwnershipAnnotatedTypeFactory
use Element.getAnnotation on insertedElement for NotOwning and Owning, which
bypasses stub-aware logic; change those checks to use the
RLCCalledMethodsAnnotatedTypeFactory helpers
(rlAtf.hasNotOwning(insertedElement) and rlAtf.hasOwning(insertedElement)) so
stub annotations are respected and the returned CollectionMutatorArgumentKind
(DEFINITELY_NON_OWNING or MAY_BE_OWNING) is correct.

Comment on lines +1179 to +1223
protected Name nameOfCollectionThatAllElementsAreCalledOn(
StatementTree init, BinaryTree condition, ExpressionStatementTree update) {
Tree.Kind updateKind = update.getExpression().getKind();
if (updateKind == Tree.Kind.PREFIX_INCREMENT || updateKind == Tree.Kind.POSTFIX_INCREMENT) {
UnaryTree inc = (UnaryTree) update.getExpression();

// Verify update is of form i++ or ++i and init is variable initializer.
if (!(init instanceof VariableTree) || !(inc.getExpression() instanceof IdentifierTree))
return null;
VariableTree initVar = (VariableTree) init;

// Verify that intializer is i=0.
if (!(initVar.getInitializer() instanceof LiteralTree)
|| !((LiteralTree) initVar.getInitializer()).getValue().equals(0)) {
return null;
}

// Verify that condition is of the form: i < something.
if (!(condition.getLeftOperand() instanceof IdentifierTree)) {
return null;
}

// Verify that i=0, i<n, and i++ have the same "i".
Name initVarName = initVar.getName();
if (initVarName != ((IdentifierTree) condition.getLeftOperand()).getName()) {
return null;
}
if (initVarName != ((IdentifierTree) inc.getExpression()).getName()) {
return null;
}

if ((condition.getRightOperand() instanceof MethodInvocationTree)
&& TreeUtils.isSizeAccess(condition.getRightOperand())) {
ExpressionTree methodSelect =
((MethodInvocationTree) condition.getRightOperand()).getMethodSelect();
if (methodSelect instanceof MemberSelectTree) {
MemberSelectTree mst = (MemberSelectTree) methodSelect;
Element elt = TreeUtils.elementFromTree(mst.getExpression());
if (ResourceLeakUtils.isCollection(elt, atypeFactory)) {
return getNameFromExpressionTree(mst.getExpression());
}
}
}
}
return null;
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

Require a < condition before classifying the loop as “all elements”.

nameOfCollectionThatAllElementsAreCalledOn(...) never checks condition.getKind(). Headers like i == list.size() or i > list.size() can therefore slip through the matcher even though they do not satisfy the “iterate over all elements” precondition.

Suggested fix
   protected Name nameOfCollectionThatAllElementsAreCalledOn(
       StatementTree init, BinaryTree condition, ExpressionStatementTree update) {
+    if (condition.getKind() != Tree.Kind.LESS_THAN) {
+      return null;
+    }
     Tree.Kind updateKind = update.getExpression().getKind();
🤖 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/MustCallVisitor.java`
around lines 1179 - 1223, In nameOfCollectionThatAllElementsAreCalledOn(...),
add a check that condition.getKind() is Tree.Kind.LESS_THAN (i.e., a '<'
comparison) before proceeding to inspect left/right operands; if the kind is not
LESS_THAN return null. Place this check near the start of the condition-handling
block (before using condition.getLeftOperand()/getRightOperand()) so loops with
other operators (==, >, <=, etc.) are not classified as "all elements".

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

♻️ Duplicate comments (1)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java (1)

111-122: ⚠️ Potential issue | 🟠 Major

Make both add overloads explicitly @OwningCollection receivers.

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
    done

Expected result: all insertion/removal mutators in LinkedHashKeyedSet consistently require @OwningCollection receivers, and signatures remain compatible with KeyedSet.


ℹ️ Review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: 093f6549-bc61-47fc-85ee-156eb7fbf153

📥 Commits

Reviewing files that changed from the base of the PR and between 91e9f76 and 2e03c50.

📒 Files selected for processing (1)
  • annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

♻️ Duplicate comments (4)
annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java (1)

126-127: ⚠️ Potential issue | 🟠 Major

Declare an explicit receiver qualifier on add(@owning V 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 | 🟠 Major

Compare the loop-variable Name with .equals(...).

On Line 1379, VariableTree.getName() is a Name; == 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(...) or Objects.equals(...) for com.sun.source.util.Name comparisons 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 | 🟠 Major

Pick the latch, not the header, as loopUpdateBlock.

On Line 1533, backEdge.targetBlock is 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. Record backEdge.sourceBlock instead.

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 | 🟠 Major

Lambda-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(...) return null for UnderlyingAST.Kind.LAMBDA, and analyzeResolvedPotentiallyFulfillingCollectionLoops(...) 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 reaches postAnalyze(...). 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

📥 Commits

Reviewing files that changed from the base of the PR and between 2e03c50 and 2c2468a.

📒 Files selected for processing (2)
  • annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java
  • checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

📥 Commits

Reviewing files that changed from the base of the PR and between 2c2468a and 34c5027.

📒 Files selected for processing (1)
  • annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java

Comment on lines +119 to 120
public boolean add(@Owning V o) {
return add(o, THROW_EXCEPTION, IGNORE) == null;
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

🧩 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.java

Repository: 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 @Owning to add(V, int, int) parameter
  • Add @Owning to replace(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.

@iamsanjaymalakar
Copy link
Copy Markdown
Member Author

@mernst CI jobs are failing on [daikon_part3_jdk25) due to missing annotations. How do I resolve them (add annotations)?

@mernst
Copy link
Copy Markdown
Member

mernst commented Apr 5, 2026

@iamsanjaymalakar
Copy link
Copy Markdown
Member Author

@mernst
Copy link
Copy Markdown
Member

mernst commented Apr 5, 2026

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 #2222 is from fork ORG (that is, GitHub organization ORG) and branch B. The pull request is to organization typetools, project checker-framework, and branch master.

  1. Create a fork of the relevant project (such as daikon or plume-util) in GitHub organization ORG.
  2. Create a branch, in ORG, with exactly the same name as B.
  3. Create a pull request for the new branch. In the description of that pull request, write "Merge with https://github.com/typetools/checker-framework/pull/2222".
  4. Edit the description of pull request #2222 to refer back to the newly-created pull request: "Merge with https://github.com/UPSTREAM_ORG/PROJECT/pull/NNN".

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.

Copy link
Copy Markdown
Contributor

@msridhar msridhar left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Couple of very initial comments. My rough review plan:

  1. Review CollectionOwnershipChecker and related code in the collectionownership package, starting with the transfer functions
  2. Review MustCallConsistencyAnalyzer changes
  3. 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}
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the reference to java.util.Iterator here out of date? Or does our checker actually treats Iterators as potentially owning collections?

Comment on lines +36 to +37
* 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
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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);
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is this super.visitAssignment call that does the ownership transfer from rhs to lhs, correct? If so, add a comment to that effect

Comment on lines +94 to +97
replaceInStores(
res,
hasExplicitNotOwningCollectionDeclaration(node) ? lhsJE : rhsJE,
atypeFactory.NOTOWNINGCOLLECTION);
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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"

@msridhar
Copy link
Copy Markdown
Contributor

msridhar commented Apr 8, 2026

This PR is still incomplete. Significant documentation and restructuring remain.

@iamsanjaymalakar is this still true? If not, update the PR description?

Also, looks like there are some conflicts with the latest master branch.

@msridhar
Copy link
Copy Markdown
Contributor

msridhar commented Apr 8, 2026

@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: MustCallVisitor#detectCollectionObligationFulfillingWhileLoop, MustCallConsistencyAnalyzer#analyzeResolvedPotentiallyFulfillingCollectionLoop, RLCCalledMethodsAnnotatedTypeFactory#analyzeResolvedPotentiallyFulfillingCollectionLoops, CollectionOwnershipTransfer#updateStoreForVerifiedFulfillingCollectionLoop, possibly other places. I was expecting most of this logic to live inside the Collection Ownership Checker.

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?

@iamsanjaymalakar
Copy link
Copy Markdown
Member Author

@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: MustCallVisitor#detectCollectionObligationFulfillingWhileLoop, MustCallConsistencyAnalyzer#analyzeResolvedPotentiallyFulfillingCollectionLoop, RLCCalledMethodsAnnotatedTypeFactory#analyzeResolvedPotentiallyFulfillingCollectionLoops, CollectionOwnershipTransfer#updateStoreForVerifiedFulfillingCollectionLoop, possibly other places. I was expecting most of this logic to live inside the Collection Ownership Checker.

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.

MustCallVisitor is where the initial match happens because that step is purely syntactic. It sees the original Java source form before CFG lowering, and recognizes loops that iterate over a collection (for, while, etc.). This stage only asks whether the code is a candidate traversal over a resource collection. It does not try to prove anything.

RLCCalledMethodsAnnotatedTypeFactory is the next stage because AST matching is not enough. We still need CFG facts to certify the traversal:

  • enhanced for is desugared, so we need CFG reconstruction to find the actual body/update structure
  • while loops need CFG resolution to choose the correct loop-update block
  • certification must run after called-methods analysis has produced the relevant stores

RLCCalledMethodsAnnotatedTypeFactory#analyzeResolvedPotentiallyFulfillingCollectionLoops method is doing orchestration, not proof: it knows which candidates belong to the current analysis root, which ones have already been resolved, and when called-methods analysis has completed so loop certification can run.

MustCallConsistencyAnalyzer is doing proof. The proof is not a collection-ownership proof; it is a resource-leak proof. That is why the verification lives in MCCA rather than in the Collection Ownership Checker.

CollectionOwnershipTransfer is only the consumer of that proof. Once a loop traversal has been verified, collection ownership uses that fact to change the collection from @OwningCollection to @OwningCollectionWithoutObligation.

I'm not sure about how can I move all of them into CollectionOwnershipChecker. Let me know if you have any suggestions. @msridhar

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 | 🔵 Trivial

Annotate get(int) explicitly to match the new accessor contract.

peek() and pop() now spell out the receiver qualifier, but Line 1498 get(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 | 🔴 Critical

Guard empty argument lists before indexing getArguments().get(0).

Line 1731 can throw IndexOutOfBoundsException for zero-arg get() 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 | 🟠 Major

Resolve the static-field rule conflict for @NotOwningCollection.

Lines 825-826 say any static resource-collection field is rejected, but Lines 888-893 say @NotOwningCollection fields behave like ordinary non-owning references. Those rules conflict unless static @NotOwningCollection fields 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 | 🟡 Minor

Remove 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 | 🟠 Major

Document @CreatesCollectionObligation alongside 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 | 🟠 Major

Don’t describe @NotOwningCollection as 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 | 🟡 Minor

This section still under-documents the accepted loop shapes.

It only documents enhanced for and one indexed-for pattern. If iterator/while traversals 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 | 🟠 Major

Invalidate iterated-element facts on mutations, too.

iteratedCollectionElements is now first-class store state, but the mutation paths still never evict it. Side-effecting calls and the removeConflicting(...) 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 | 🟡 Minor

Require both key components to match in getIteratedCollectionElement.

This || chain is looser than IteratedCollectionElement.equals(...), which keys entries on both tree and node. Two distinct keys that share only one component can therefore resolve to the wrong store entry, and the result depends on HashMap iteration 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

📥 Commits

Reviewing files that changed from the base of the PR and between d2d1a36 and ae959a1.

📒 Files selected for processing (7)
  • annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java
  • dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
  • docs/manual/resource-leak-checker.tex
  • framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
  • framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java
  • framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java
  • javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java

Comment on lines +665 to +672
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.
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

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.

Comment on lines +1199 to +1214
/**
* 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();
}
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

🧩 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.java

Repository: 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.java

Repository: 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 -20

Repository: 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.java

Repository: 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 -10

Repository: 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 java

Repository: 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.java

Repository: 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.java

Repository: 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.java

Repository: 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.

@msridhar
Copy link
Copy Markdown
Contributor

msridhar commented Apr 8, 2026

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:

  1. For each loop back edge (from a node inside the loop to the loop head), at the source of the back edge, all @MustCall methods for the loop variable are in its inferred @CalledMethods set.
  2. There are no early exits in the loop, due to break, throwing an exception (modulo our list of ignored exception types), etc.

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 c is @OwningCollection, and there is a certified disposal loop over c, then immediately after the loop (there should be only one relevant loop exit edge), c becomes @OwningCollectionWithoutObligation.

I think it's also useful to keep in mind the current sub-checker relationships for the RLC:

ResourceLeakChecker -> CollectionOwnershipChecker -> RLCCalledMethodsChecker -> MustCallChecker

Now to your comment:

MustCallVisitor is where the initial match happens because that step is purely syntactic. It sees the original Java source form before CFG lowering, and recognizes loops that iterate over a collection (for, while, etc.). This stage only asks whether the code is a candidate traversal over a resource collection. It does not try to prove anything.

All checkers can have a visitor that operates over ASTs. Why does this logic need to live in the MustCallVisitor?

RLCCalledMethodsAnnotatedTypeFactory is the next stage because AST matching is not enough. We still need CFG facts to certify the traversal:

  • enhanced for is desugared, so we need CFG reconstruction to find the actual body/update structure
  • while loops need CFG resolution to choose the correct loop-update block
  • certification must run after called-methods analysis has produced the relevant stores

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.

RLCCalledMethodsAnnotatedTypeFactory#analyzeResolvedPotentiallyFulfillingCollectionLoops method is doing orchestration, not proof: it knows which candidates belong to the current analysis root, which ones have already been resolved, and when called-methods analysis has completed so loop certification can run.

I don't understand what "orchestration" or "resolved" mean in this sentence.

MustCallConsistencyAnalyzer is doing proof. The proof is not a collection-ownership proof; it is a resource-leak proof. That is why the verification lives in MCCA rather than in the Collection Ownership Checker.

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.

CollectionOwnershipTransfer is only the consumer of that proof. Once a loop traversal has been verified, collection ownership uses that fact to change the collection from @OwningCollection to @OwningCollectionWithoutObligation.

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?

@iamsanjaymalakar
Copy link
Copy Markdown
Member Author

iamsanjaymalakar commented Apr 9, 2026

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.

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 for and the supported while forms, things like the actual body/update blocks come from the CFG resolution step, not from the visitor.

All checkers can have a visitor that operates over ASTs. Why does this logic need to live in the MustCallVisitor?

There is no fundamental reason it has to be in MustCallVisitor; it could also be done in CollectionOwnershipVisitor. I kept it in MustCallVisitor mainly because that is where the initial implementation already did the source-level matching.

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.

This does not inherently have to live in RLCCalledMethodsAnnotatedTypeFactory. I kept it there because that was already the place in the existing structure that owned the per-method loop state in collectionLoopStateByEnclosingMethod and whose postAnalyze(...) runs after Called Methods analysis has produced the stores that certification needs. So the choice was mostly about reusing that lifecycle, not about the other checkers lacking CFG access. Let me know if you have any suggestions on this.

I don't understand what "orchestration" or "resolved" mean in this sentence.

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.

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.

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.

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?

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.

@msridhar

@msridhar
Copy link
Copy Markdown
Contributor

msridhar commented Apr 9, 2026

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?

@iamsanjaymalakar
Copy link
Copy Markdown
Member Author

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.

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

♻️ Duplicate comments (1)
checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java (1)

261-266: ⚠️ Potential issue | 🔴 Critical

Skip the current checker when probing for an enclosing RLC hierarchy.

Starting the scan at checker still makes a standalone MustCallChecker look like it is inside the RLC hierarchy, so this helper can call the RLCC factory lookup when no enclosing RLC checker exists. Start from checker.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

📥 Commits

Reviewing files that changed from the base of the PR and between ae959a1 and b48eba3.

📒 Files selected for processing (2)
  • checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java
  • checker/tests/resourceleak-collections/ArraysAsListZeroArgs.java

Comment on lines +293 to +337
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);
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

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.

Suggested change
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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants