Fix WPI Non-Termination Issue with @UnknownInitialization Annotations#6657
Fix WPI Non-Termination Issue with @UnknownInitialization Annotations#6657erfan-arvan wants to merge 46 commits intotypetools:masterfrom
Conversation
|
@erfan-arvan Could you please make CI pass? Thanks. |
@mernst |
| Werner Dietl, | ||
| Zhiping Cai. | ||
| Zhiping Cai, | ||
| erfanarvan. |
There was a problem hiding this comment.
Please don't add your username here (just your name is sufficient).
| return; | ||
| } | ||
|
|
||
| // For parameters, If rhsmATM is Nullable or MonotonicNonNull and has the |
There was a problem hiding this comment.
This code is nullness/initialization-specific, so WholeProgramInferenceImplementation isn't the logical place for it: it should be in the Nullness Checker somewhere.
There was a problem hiding this comment.
WholeProgramInferenceImplementation has checker-specific callbacks, but we can add more if you need another one.
| // UnknownInitialization(java.lang.Object.class). This is because there is | ||
| // likely a constructor where it hasn't been initialized, and we haven't | ||
| // considered its effect. Otherwise, WPI might get stuck in a loop. | ||
| if (defLoc == TypeUseLocation.PARAMETER |
There was a problem hiding this comment.
Why is this only an issue for parameters? I'm especially surprised that you need to do this for parameters but not for fields - the underlying issue seems to be about fields.
There was a problem hiding this comment.
It used to be for all assignments and pseudo-assignments, but to narrow down the possible loss of information, I thought it might be better to merely block the propagation of potentially incorrect annotations to other places by filtering the parameters. This approach also stopped the loop problem in my test cases, just like the previous approach. However, to ensure accuracy, I am refining the entire approach, changing its application to field assignments, and transferring it to the Nullness Checker. After my tests pass, I will commit the changes. Thank you very much for your valuable feedback.
| if (anno.getAnnotationType() | ||
| .asElement() | ||
| .getSimpleName() | ||
| .contentEquals("UnknownInitialization") |
There was a problem hiding this comment.
Use AnnotationUtils.areSameByName instead.
…ols#6653) Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
Co-authored-by: Suzanne Millstein <smillst@cs.washington.edu> Co-authored-by: Michael Ernst <mernst@cs.washington.edu>
Co-authored-by: Michael Ernst <mernst@cs.washington.edu>
…ialization annotations to NullnessAnnotatedTypeFactory
7af34c0 to
118b771
Compare
| * @param rhsATM the type of the rhs of the pseudo-assignment, which is side-effected by this | ||
| * method | ||
| */ | ||
| public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {} |
There was a problem hiding this comment.
The name "wpiAdjustForInitializationAnnotations" doesn't convey the generic purpose of this method. Rather, it conveys the specific purpose that you've used the method for in the Nullness Checker.
The name here should be chosen to explain when this method is called and what it might be used for in the general case, not the specific case that you're trying to fix in this PR. I suggest choosing a name that will help someone reading WholeProgramInferenceImplementation#updateAnnotationSet to understand what this hook does.
| } | ||
|
|
||
| // Update Initialization Annotations in WPI. It is only applied to | ||
| // Nullness-related qualifiers' inference to prevent possible loops. |
There was a problem hiding this comment.
This comment is inappropriate, because it may not remain true. In particular, it is mixing implementation details of a specific checker (nullness) with the generic WPI algorithm (which is what this code implements). The comment should explain the general purpose of this callback hook, not the specific use in one checker.
…pdate method usage, and revise comments
…ation' into bugfix/wpi-loop-unknowninitialization
…e method to NullnessAnnotatedTypeFactory.java to make it local for Nullness-related inference rather than for all checkers. Also added a test case for the corresponding issue in the ainfer-nullness tests.
28ef5ab to
d7acb57
Compare
…b.com/erfan-arvan/checker-framework into bugfix/wpi-loop-unknowninitialization
I have added the required test file, and it works as requested on my local system. However, it causes some CI tests to fail. Specifically, in the CI tests, it causes the Checker Framework to crash. According to the logs, the issue is: I have made some changes, but the problem persists. Could you please guide me on how to solve this problem? |
|
@erfan-arvan the failures are in the mostly-deprecated JAIF-based WPI mode. I suspect that there is some problem in JAIF-based WPI that prevents it from handling the test file - probably something related to local classes. Regardless, this test should be excluded for non-ajava-based WPI, because it relies on input ajava files. You should add an exclusion similar to this one for both JAIF- and stub-based |
…ssue and add comments to the test file
0ababd3 to
217ba50
Compare
📝 WalkthroughWalkthroughAdds an initialization-aware helper to the nullness type factory to rewrite UnknownInitialization annotations and invokes it before field/non-field update adjustments. Adds an OptionalTransfer class that propagates Possibly related PRs
🚥 Pre-merge checks | ✅ 2 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (2 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
There was a problem hiding this comment.
Actionable comments posted: 5
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java (1)
612-618: 🧹 Nitpick | 🔵 TrivialThe TODO comment appears outdated.
The comment claims
containscosts linear time, but examining theWorklistclass below (lines 664, 722-724),contains()already delegates toqueueSet.contains(block)which is O(1) using theHashSet. The optimization mentioned in the TODO has already been implemented.Consider removing or updating this TODO comment to reflect the current implementation.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java` around lines 612 - 618, Remove or update the outdated TODO above the worklist.contains(b) check: the Worklist.contains() already delegates to Worklist.queueSet.contains(block) and is O(1), so delete the remark about linear cost or replace it with a short note stating that duplicates are prevented via Worklist.queueSet (HashSet) and that the alternative strategies are no longer necessary; reference the Worklist class and its contains()/queueSet implementation to locate the current behavior.
🤖 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/nullness/NullnessAnnotatedTypeFactory.java`:
- Around line 994-1007: The parameter defLoc in
wpiAdjustInitializationAnnotations is unused—either annotate it with
`@SuppressWarnings`("unused") or remove it—and avoid mutating rhsATM while
iterating its primary annotations: instead, iterate
rhsATM.getPrimaryAnnotations() and collect any AnnotationMirror matching
AnnotationUtils.areSameByName(... "UnknownInitialization") into a temporary
list, then after the loop call rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION)
for each collected annotation; this prevents ConcurrentModificationException
when modifying the annotation set during iteration.
In
`@checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java`:
- Around line 67-68: The class OptionalImplVisitor widens its BaseTypeVisitor
type parameter to BaseAnnotatedTypeFactory; change that generic to the concrete
OptionalImplAnnotatedTypeFactory to match OptionalTransfer and improve
type-safety. Update the class declaration (OptionalImplVisitor extends
BaseTypeVisitor<OptionalImplAnnotatedTypeFactory>), then remove any unnecessary
casts and adjust usages of getTypeFactory() and any fields/constructors that
assumed BaseAnnotatedTypeFactory so they use OptionalImplAnnotatedTypeFactory
directly (this will align with OptionalTransfer's use of
analysis.getTypeFactory()).
In
`@checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava`:
- Around line 86-90: The test() method accesses g1.game but
PlayerDependentMoveValidator declares game as private; change the visibility of
the game field in PlayerDependentMoveValidator to public to match the
non-annotated variant so test() can access g1.game, and add the same
`@org.checkerframework.dataflow.qual`.* annotation used on the other methods in
this file to the test() method (i.e., mirror the annotation applied to the other
methods) so its nullness/dataflow contract matches the rest of the class.
In
`@checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java`:
- Around line 62-63: Replace the unnecessary string concatenation "purity" +
".not.sideeffectfree.call" with the single literal
"purity.not.sideeffectfree.call" in the test class
WPIUnknownInitializationLoopTest (the suppression/keys list containing "purity"
+ ".not.sideeffectfree.call" and "contracts.postcondition"); update that entry
so the array/collection uses the consolidated string literal to improve
readability and avoid the pointless concatenation.
In `@framework/tests/all-systems/java8/memberref/VarArgs.java`:
- Around line 34-39: Rename the class MoreVarAgrgsTest to MoreVarArgsTest (fix
the typo) and update any references to it; also normalize the field names to the
expected sequence by adding or renaming the missing v3 so the fields read v1,
v2, v3 (or rename v4 to v3) while keeping their assignments to the method
reference MoreVarArgsTest::myObjectArgArg (ensure the method name myObjectArgArg
remains unchanged) so naming is consistent with MemberRefVarArgsTest.
---
Outside diff comments:
In
`@dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java`:
- Around line 612-618: Remove or update the outdated TODO above the
worklist.contains(b) check: the Worklist.contains() already delegates to
Worklist.queueSet.contains(block) and is O(1), so delete the remark about linear
cost or replace it with a short note stating that duplicates are prevented via
Worklist.queueSet (HashSet) and that the alternative strategies are no longer
necessary; reference the Worklist class and its contains()/queueSet
implementation to locate the current behavior.
ℹ️ Review info
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (10)
checker/build.gradlechecker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.javachecker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.javachecker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javachecker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajavachecker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajavachecker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.javadataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.javadocs/manual/contributors.texframework/tests/all-systems/java8/memberref/VarArgs.java
💤 Files with no reviewable changes (1)
- checker/build.gradle
| public void wpiAdjustInitializationAnnotations( | ||
| AnnotatedTypeMirror rhsATM, TypeUseLocation defLoc) { | ||
| // defLoc is defined to be used in the future if needed to differentiate between field and | ||
| // non-field locations | ||
| if ((rhsATM.hasPrimaryAnnotation(Nullable.class) | ||
| || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { | ||
| for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { | ||
| if (AnnotationUtils.areSameByName( | ||
| anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) { | ||
| rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION); | ||
| } | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
# First, let's verify the exact content of the method and check if defLoc is used
cat -n checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java | sed -n '994,1007p'Repository: typetools/checker-framework
Length of output: 820
🏁 Script executed:
# Check the AnnotatedTypeMirror class to understand getPrimaryAnnotations() return type
fd -e java -x grep -l "class AnnotatedTypeMirror" {}Repository: typetools/checker-framework
Length of output: 157
🏁 Script executed:
# Look for similar patterns where getPrimaryAnnotations is used in a loop with replaceAnnotation
rg -n "for.*getPrimaryAnnotations\(\)" --type java -A 5 -B 1Repository: typetools/checker-framework
Length of output: 31135
🏁 Script executed:
# Check if there are other methods that iterate over getPrimaryAnnotations and modify annotations
rg -n "getPrimaryAnnotations\(\)" --type java -A 2 -B 1 | grep -E "(for|while|replaceAnnotation)" -A 2 -B 2 | head -60Repository: typetools/checker-framework
Length of output: 6768
🏁 Script executed:
# Check getPrimaryAnnotations() return type in AnnotatedTypeMirror
rg -n "getPrimaryAnnotations\(\)" framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java -B 2 -A 2Repository: typetools/checker-framework
Length of output: 1802
🏁 Script executed:
# Check the actual implementation of getPrimaryAnnotations() method
sed -n '1,3000p' framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java | grep -n "getPrimaryAnnotations" -B 1 -A 5 | head -40Repository: typetools/checker-framework
Length of output: 1711
🏁 Script executed:
# Look at the replaceAnnotation implementation
rg -n "public.*replaceAnnotation" framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java -A 10Repository: typetools/checker-framework
Length of output: 1149
🏁 Script executed:
# Check if WholeProgramInferenceJavaParserStorage pattern at 574-576 has issues reported
sed -n '570,585p' framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.javaRepository: typetools/checker-framework
Length of output: 943
Unused parameter defLoc.
The defLoc parameter is never used in this method. The comment at lines 996-997 indicates it's "defined to be used in the future," but if it's truly needed later, consider using @SuppressWarnings("unused") to document intent explicitly.
Additionally, the loop pattern at lines 1000-1005 may cause ConcurrentModificationException. Iterating over getPrimaryAnnotations() while calling replaceAnnotation() modifies the underlying annotation set during iteration. See AnnotatedTypeReplacer.java (lines 112-117) for an explicit warning about this pattern. Collect items to process first, then modify after the loop:
Suggested fix
List<AnnotationMirror> annotationsToReplace = new ArrayList<>();
for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) {
if (AnnotationUtils.areSameByName(
anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) {
annotationsToReplace.add(anno);
}
}
for (AnnotationMirror anno : annotationsToReplace) {
rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION);
}🤖 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/nullness/NullnessAnnotatedTypeFactory.java`
around lines 994 - 1007, The parameter defLoc in
wpiAdjustInitializationAnnotations is unused—either annotate it with
`@SuppressWarnings`("unused") or remove it—and avoid mutating rhsATM while
iterating its primary annotations: instead, iterate
rhsATM.getPrimaryAnnotations() and collect any AnnotationMirror matching
AnnotationUtils.areSameByName(... "UnknownInitialization") into a temporary
list, then after the loop call rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION)
for each collected annotation; this prevents ConcurrentModificationException
when modifying the annotation set during iteration.
| public class OptionalImplVisitor | ||
| extends BaseTypeVisitor</* OptionalAnnotatedTypeFactory*/ BaseAnnotatedTypeFactory> { | ||
| extends BaseTypeVisitor</* OptionalImplAnnotatedTypeFactory*/ BaseAnnotatedTypeFactory> { |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Check if OptionalImplAnnotatedTypeFactory exists
fd -t f "OptionalImplAnnotatedTypeFactory.java"Repository: typetools/checker-framework
Length of output: 168
🏁 Script executed:
#!/bin/bash
# Find and examine OptionalTransfer.java around line 50
fd -t f "OptionalTransfer.java" --exec head -100 {} \;Repository: typetools/checker-framework
Length of output: 4747
🏁 Script executed:
#!/bin/bash
# Check the OptionalImplVisitor.java file to see the full context
fd -t f "OptionalImplVisitor.java" --exec cat -n {} \;Repository: typetools/checker-framework
Length of output: 46549
Consider using the specific type parameter for consistency with OptionalTransfer.
The type parameter is widened to BaseAnnotatedTypeFactory while the specific OptionalImplAnnotatedTypeFactory is commented out. This creates an inconsistency with OptionalTransfer, which explicitly casts analysis.getTypeFactory() to OptionalImplAnnotatedTypeFactory in its constructor. Since OptionalImplAnnotatedTypeFactory exists and is the actual runtime type, reverting to the specific type parameter would improve type safety and code clarity without affecting functionality.
🤖 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/optional/OptionalImplVisitor.java`
around lines 67 - 68, The class OptionalImplVisitor widens its BaseTypeVisitor
type parameter to BaseAnnotatedTypeFactory; change that generic to the concrete
OptionalImplAnnotatedTypeFactory to match OptionalTransfer and improve
type-safety. Update the class declaration (OptionalImplVisitor extends
BaseTypeVisitor<OptionalImplAnnotatedTypeFactory>), then remove any unnecessary
casts and adjust usages of getTypeFactory() and any fields/constructors that
assumed BaseAnnotatedTypeFactory so they use OptionalImplAnnotatedTypeFactory
directly (this will align with OptionalTransfer's use of
analysis.getTypeFactory()).
| public void test(){ | ||
| PlayerDependentMoveValidator g1 = | ||
| new PlayerDependentMoveValidator(game); | ||
| this.game = g1.game; | ||
| } |
There was a problem hiding this comment.
Same visibility issue as the NullnessChecker variant.
The test() method at line 89 accesses g1.game, but game is declared as private at line 44 in PlayerDependentMoveValidator. This should match the non-annotated version where game is public.
Additionally, the test() method lacks the @org.checkerframework.dataflow.qual.* annotation present on other methods.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava`
around lines 86 - 90, The test() method accesses g1.game but
PlayerDependentMoveValidator declares game as private; change the visibility of
the game field in PlayerDependentMoveValidator to public to match the
non-annotated variant so test() can access g1.game, and add the same
`@org.checkerframework.dataflow.qual`.* annotation used on the other methods in
this file to the test() method (i.e., mirror the annotation applied to the other
methods) so its nullness/dataflow contract matches the rest of the class.
| "purity" + ".not.sideeffectfree.call", | ||
| "contracts.postcondition", |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Minor: Unnecessary string concatenation.
The suppression key "purity" + ".not.sideeffectfree.call" could be simplified to "purity.not.sideeffectfree.call". Unless there's a specific tooling reason for this split.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In
`@checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java`
around lines 62 - 63, Replace the unnecessary string concatenation "purity" +
".not.sideeffectfree.call" with the single literal
"purity.not.sideeffectfree.call" in the test class
WPIUnknownInitializationLoopTest (the suppression/keys list containing "purity"
+ ".not.sideeffectfree.call" and "contracts.postcondition"); update that entry
so the array/collection uses the consolidated string literal to improve
readability and avoid the pointless concatenation.
| class MoreVarAgrgsTest { | ||
| static void myObjectArgArg(Object o, String... vararg) {} | ||
|
|
||
| RegularFunc v1 = MoreVarAgrgsTest::myObjectArgArg; | ||
| RegularFunc2 v2 = MoreVarAgrgsTest::myObjectArgArg; | ||
| RegularFunc3 v4 = MoreVarAgrgsTest::myObjectArgArg; |
There was a problem hiding this comment.
Typo in class name and inconsistent field naming.
MoreVarAgrgsTestshould beMoreVarArgsTest(missing 'a' in "Args").- Field numbering skips
v3(v1, v2, v4), which is inconsistent with the pattern inMemberRefVarArgsTest.
✏️ Proposed fix
-class MoreVarAgrgsTest {
+class MoreVarArgsTest {
static void myObjectArgArg(Object o, String... vararg) {}
- RegularFunc v1 = MoreVarAgrgsTest::myObjectArgArg;
- RegularFunc2 v2 = MoreVarAgrgsTest::myObjectArgArg;
- RegularFunc3 v4 = MoreVarAgrgsTest::myObjectArgArg;
+ RegularFunc v1 = MoreVarArgsTest::myObjectArgArg;
+ RegularFunc2 v2 = MoreVarArgsTest::myObjectArgArg;
+ RegularFunc3 v3 = MoreVarArgsTest::myObjectArgArg;
}🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@framework/tests/all-systems/java8/memberref/VarArgs.java` around lines 34 -
39, Rename the class MoreVarAgrgsTest to MoreVarArgsTest (fix the typo) and
update any references to it; also normalize the field names to the expected
sequence by adding or renaming the missing v3 so the fields read v1, v2, v3 (or
rename v4 to v3) while keeping their assignments to the method reference
MoreVarArgsTest::myObjectArgArg (ensure the method name myObjectArgArg remains
unchanged) so naming is consistent with MemberRefVarArgsTest.
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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/optional/OptionalTransfer.java`:
- Around line 74-75: The condition uses lambdaParent.getKind() instanceof
MethodInvocationTree which is wrong because getKind() returns a Tree.Kind enum;
change the check to either test the node type or the kind: replace the condition
with (lambdaParent instanceof MethodInvocationTree) and cast to
MethodInvocationTree when assigning invok, or alternatively compare
lambdaParent.getKind() == Tree.Kind.METHOD_INVOCATION and then cast
(MethodInvocationTree) lambdaParent to invok; update the surrounding code to use
the chosen correct check and cast.
- Around line 72-73: The code assumes getParentPath() on the TreePath returned
by optionalTypeFactory.getPath(lambdaTree) is non-null; add a defensive
null-check after obtaining TreePath lambdaPath (from
optionalTypeFactory.getPath(lambdaTree)) and handle a null parentPath before
calling getLeaf(): if lambdaPath.getParentPath() is null, either return early
(e.g., skip processing this lambda) or log/throw a clear error, otherwise
proceed to assign lambdaParent = lambdaPath.getParentPath().getLeaf(); this
prevents a potential NPE when computing lambdaParent.
ℹ️ Review info
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (1)
checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java
| TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); | ||
| Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); |
There was a problem hiding this comment.
Potential NPE if getParentPath() returns null.
While unlikely in practice (a lambda should always have a parent), getParentPath() can return null for root elements. Adding a null check would make the code more defensive.
🛡️ Proposed fix
TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree);
- Tree lambdaParent = lambdaPath.getParentPath().getLeaf();
+ TreePath parentPath = lambdaPath.getParentPath();
+ if (parentPath == null) {
+ return result;
+ }
+ Tree lambdaParent = parentPath.getLeaf();📝 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.
| TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); | |
| Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); | |
| TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); | |
| TreePath parentPath = lambdaPath.getParentPath(); | |
| if (parentPath == null) { | |
| return result; | |
| } | |
| Tree lambdaParent = parentPath.getLeaf(); |
🤖 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/optional/OptionalTransfer.java`
around lines 72 - 73, The code assumes getParentPath() on the TreePath returned
by optionalTypeFactory.getPath(lambdaTree) is non-null; add a defensive
null-check after obtaining TreePath lambdaPath (from
optionalTypeFactory.getPath(lambdaTree)) and handle a null parentPath before
calling getLeaf(): if lambdaPath.getParentPath() is null, either return early
(e.g., skip processing this lambda) or log/throw a clear error, otherwise
proceed to assign lambdaParent = lambdaPath.getParentPath().getLeaf(); this
prevents a potential NPE when computing lambdaParent.
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java (1)
72-73:⚠️ Potential issue | 🟡 MinorGuard
TreePath/parent path dereferences to avoid NPE.At Line 72-73, both
optionalTypeFactory.getPath(lambdaTree)andgetParentPath()are dereferenced without null checks. This was previously flagged and still appears unresolved.Proposed defensive fix
TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); - Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); + if (lambdaPath == null) { + return result; + } + TreePath parentPath = lambdaPath.getParentPath(); + if (parentPath == null) { + return result; + } + Tree lambdaParent = parentPath.getLeaf();🤖 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/optional/OptionalTransfer.java` around lines 72 - 73, Guard against null TreePath and null parent path before dereferencing: check the result of optionalTypeFactory.getPath(lambdaTree) (variable lambdaPath) for null and also check lambdaPath.getParentPath() for null before calling getLeaf(); if either is null, return or skip the current processing branch in OptionalTransfer::visitLambda (or wherever this code lives) so you avoid NPEs. Update the code around the two expressions optionalTypeFactory.getPath(lambdaTree) and lambdaPath.getParentPath().getLeaf() to perform these null checks and handle the null case gracefully (e.g., early return or continue).
🤖 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/optional/OptionalTransfer.java`:
- Line 50: OptionalTransfer is dead duplicated code; remove it to eliminate
redundancy. Delete the OptionalTransfer class entirely (including the cast
optionalTypeFactory = (OptionalImplAnnotatedTypeFactory)
analysis.getTypeFactory(); and its initialStore() implementation) and ensure no
callers reference it — the factory
OptionalImplAnnotatedTypeFactory.createFlowTransferFunction() already constructs
OptionalImplTransfer, so rely on OptionalImplTransfer (and keep its
initialStore() implementation at lines referenced in that class) as the single
transfer implementation; if there was intended special behavior, consolidate
that behavior into OptionalImplTransfer instead of keeping OptionalTransfer.
---
Duplicate comments:
In
`@checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java`:
- Around line 72-73: Guard against null TreePath and null parent path before
dereferencing: check the result of optionalTypeFactory.getPath(lambdaTree)
(variable lambdaPath) for null and also check lambdaPath.getParentPath() for
null before calling getLeaf(); if either is null, return or skip the current
processing branch in OptionalTransfer::visitLambda (or wherever this code lives)
so you avoid NPEs. Update the code around the two expressions
optionalTypeFactory.getPath(lambdaTree) and lambdaPath.getParentPath().getLeaf()
to perform these null checks and handle the null case gracefully (e.g., early
return or continue).
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: cb5db739-ed92-47c5-8c09-db79e27f87a3
📒 Files selected for processing (2)
checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javachecker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java
| */ | ||
| public OptionalTransfer(CFAbstractAnalysis<CFValue, CFStore, CFTransfer> analysis) { | ||
| super(analysis); | ||
| optionalTypeFactory = (OptionalImplAnnotatedTypeFactory) analysis.getTypeFactory(); |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# First, let's locate and examine the OptionalTransfer file
find . -name "OptionalTransfer.java" -type fRepository: typetools/checker-framework
Length of output: 154
🏁 Script executed:
#!/bin/bash
# Execute the verification commands from the review comment
rg -nP --type=java -C3 '\bnew\s+OptionalTransfer\s*\(|\bnew\s+OptionalImplTransfer\s*\('Repository: typetools/checker-framework
Length of output: 862
🏁 Script executed:
#!/bin/bash
# Search for class definitions
rg -nP --type=java -C3 'class\s+OptionalTransfer\b|class\s+OptionalImplTransfer\b'Repository: typetools/checker-framework
Length of output: 1925
🏁 Script executed:
#!/bin/bash
# Search for the cast in question
rg -nP --type=java -C3 '\(OptionalImplAnnotatedTypeFactory\)\s*analysis\.getTypeFactory\(\)'Repository: typetools/checker-framework
Length of output: 2077
🏁 Script executed:
#!/bin/bash
# Read OptionalTransfer.java to understand the full context
cat -n checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java | head -80Repository: typetools/checker-framework
Length of output: 4603
🏁 Script executed:
#!/bin/bash
# Search for where OptionalTransfer is instantiated
rg -nP --type=java 'createFlowTransferFunction|new OptionalTransfer' checker/src/main/java/org/checkerframework/checker/optional/Repository: typetools/checker-framework
Length of output: 220
🏁 Script executed:
#!/bin/bash
# Check if OptionalTransfer or OptionalImplTransfer are subclassed
rg -nP --type=java 'extends OptionalTransfer|extends OptionalImplTransfer'Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/bin/bash
# Get the full OptionalTransfer.java file to analyze its methods
wc -l checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javaRepository: typetools/checker-framework
Length of output: 156
🏁 Script executed:
#!/bin/bash
# Search more broadly for OptionalTransfer usage and instantiation
rg -nP --type=java 'OptionalTransfer' checker/src/main/java/org/checkerframework/checker/optional/Repository: typetools/checker-framework
Length of output: 496
🏁 Script executed:
#!/bin/bash
# Check if there's a base OptionalAnnotatedTypeFactory that might wire OptionalTransfer
rg -nP --type=java 'class.*OptionalAnnotatedTypeFactory|createFlowTransferFunction' checker/src/main/java/org/checkerframework/checker/optional/Repository: typetools/checker-framework
Length of output: 220
🏁 Script executed:
#!/bin/bash
# Look for all TypeFactory classes in the optional checker
fd -e java checker/src/main/java/org/checkerframework/checker/optional/ | xargs grep -l 'class.*TypeFactory'Repository: typetools/checker-framework
Length of output: 618
🏁 Script executed:
#!/bin/bash
# Look for all TypeFactory classes in the optional checker
fd . 'checker/src/main/java/org/checkerframework/checker/optional/' -e java | xargs grep -l 'class.*TypeFactory'Repository: typetools/checker-framework
Length of output: 168
🏁 Script executed:
#!/bin/bash
# List all Java files in the optional checker directory
fd . 'checker/src/main/java/org/checkerframework/checker/optional/' -e javaRepository: typetools/checker-framework
Length of output: 587
🏁 Script executed:
#!/bin/bash
# Check OptionalImplAnnotatedTypeFactory to see if it wires OptionalTransfer or OptionalImplTransfer
cat -n checker/src/main/java/org/checkerframework/checker/optional/OptionalImplAnnotatedTypeFactory.java | sed -n '125,145p'Repository: typetools/checker-framework
Length of output: 392
🏁 Script executed:
#!/bin/bash
# Search for where OptionalTransfer or OptionalImplTransfer constructors are called
rg -nP --type=java '\(new\s+OptionalTransfer|new\s+OptionalImplTransfer|OptionalTransfer\(|OptionalImplTransfer\('Repository: typetools/checker-framework
Length of output: 571
🏁 Script executed:
#!/bin/bash
# Check OptionalChecker to see its structure and wiring
cat -n checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.javaRepository: typetools/checker-framework
Length of output: 1957
🏁 Script executed:
#!/bin/bash
# Look for OptionalAnnotatedTypeFactory (without "Impl")
fd . 'checker/src/main/java/org/checkerframework/checker/optional/' -e java | xargs grep -l 'OptionalAnnotatedTypeFactory' | grep -v ImplRepository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/bin/bash
# Search for who creates OptionalTransfer - maybe via inheritance or factory method
rg -nP --type=java 'class OptionalChecker|createFlowTransferFunction' checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.javaRepository: typetools/checker-framework
Length of output: 129
🏁 Script executed:
#!/bin/bash
# Look at the full OptionalChecker file
wc -l checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.javaRepository: typetools/checker-framework
Length of output: 154
🏁 Script executed:
#!/bin/bash
# Search across the entire codebase for any usage of OptionalTransfer
rg -nP --type=java 'OptionalTransfer' --max-count=20Repository: typetools/checker-framework
Length of output: 496
🏁 Script executed:
#!/bin/bash
# Check if OptionalTransfer is referenced in any imports or instantiations
rg -nP 'import.*OptionalTransfer|new OptionalTransfer'Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/bin/bash
# Look at OptionalImplChecker to understand the full architecture
cat -n checker/src/main/java/org/checkerframework/checker/optional/OptionalImplChecker.java | head -50Repository: typetools/checker-framework
Length of output: 1965
🏁 Script executed:
#!/bin/bash
# Check if there's a separate OptionalAnnotatedTypeFactory (without Impl)
rg -nP --type=java 'class OptionalAnnotatedTypeFactory'Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/bin/bash
# Search for all TypeFactory classes and their flow transfer functions
rg -nP --type=java 'class.*TypeFactory.*extends|createFlowTransferFunction' checker/src/main/java/org/checkerframework/checker/optional/Repository: typetools/checker-framework
Length of output: 402
🏁 Script executed:
#!/bin/bash
# Search in the NonEmptyChecker directory for any references to OptionalTransfer
rg -nP --type=java 'OptionalTransfer' checker/src/main/java/org/checkerframework/checker/nonempty/Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/bin/bash
# Get full context of OptionalImplAnnotatedTypeFactory file to understand inheritance
head -50 checker/src/main/java/org/checkerframework/checker/optional/OptionalImplAnnotatedTypeFactory.javaRepository: typetools/checker-framework
Length of output: 2113
🏁 Script executed:
#!/antml:bash
# Compare the two transfer classes more directly - get their full method lists
rg -nP --type=java '^\s+(public|private|protected).*\(' checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java | head -20Repository: typetools/checker-framework
Length of output: 260
🏁 Script executed:
#!/antml:bash
# Search entire codebase for any reference to OptionalTransfer outside the optional package
rg -nP 'OptionalTransfer' --type=java | grep -v 'OptionalImplTransfer'Repository: typetools/checker-framework
Length of output: 496
🏁 Script executed:
#!/antml:bash
# Check if OptionalTransfer is used as a parent class or referenced in tests
rg -nP 'OptionalTransfer' --type=javaRepository: typetools/checker-framework
Length of output: 496
🏁 Script executed:
#!/antml:bash
# Look at OptionalImplTransfer more carefully to see if it extends or duplicates OptionalTransfer
head -100 checker/src/main/java/org/checkerframework/checker/optional/OptionalImplTransfer.javaRepository: typetools/checker-framework
Length of output: 4629
🏁 Script executed:
#!/antml:bash
# Check the entire OptionalTransfer file to understand all methods
tail -n +60 checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javaRepository: typetools/checker-framework
Length of output: 2152
🏁 Script executed:
#!/antml:bash
# Compare OptionalTransfer and OptionalImplTransfer to see the full extent of duplication
diff <(sed -n '48,101p' checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java) <(sed -n '91,155p' checker/src/main/java/org/checkerframework/checker/optional/OptionalImplTransfer.java)Repository: typetools/checker-framework
Length of output: 158
🏁 Script executed:
#!/antml:bash
# Get the full length of OptionalImplTransfer to compare
wc -l checker/src/main/java/org/checkerframework/checker/optional/OptionalImplTransfer.javaRepository: typetools/checker-framework
Length of output: 160
🏁 Script executed:
#!/antml:bash
# Verify that OptionalTransfer is truly never referenced anywhere
rg -c 'OptionalTransfer' --type=java | grep -v ':0$'Repository: typetools/checker-framework
Length of output: 154
🏁 Script executed:
#!/antml:bash
# Do a comprehensive search for OptionalTransfer in the entire codebase including test files
find . -name "*.java" -type f | xargs grep -l 'OptionalTransfer' 2>/dev/null | head -20Repository: typetools/checker-framework
Length of output: 154
🏁 Script executed:
#!/antml:bash
# Check if OptionalTransfer appears in XML configuration files or annotation processors
find . -type f \( -name "*.xml" -o -name "*.properties" -o -name "*.txt" \) -exec grep -l 'OptionalTransfer' {} \; 2>/dev/nullRepository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/antml:bash
# Verify the complete initialization logic of both transfer classes side by side
echo "=== OptionalTransfer Constructor ===" && sed -n '48,57p' checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java
echo -e "\n=== OptionalImplTransfer Constructor ===" && sed -n '91,107p' checker/src/main/java/org/checkerframework/checker/optional/OptionalImplTransfer.javaRepository: typetools/checker-framework
Length of output: 1877
🏁 Script executed:
#!/antml:bash
# Search for test files related to Optional
find . -path "*/test*" -name "*Optional*.java" -type f | head -10Repository: typetools/checker-framework
Length of output: 703
🏁 Script executed:
#!/antml:bash
# Search for any dynamic instantiation or reflection-based creation of OptionalTransfer
rg -nP --type=java 'forName.*OptionalTransfer|Class\.forName|newInstance|invoke.*OptionalTransfer'Repository: typetools/checker-framework
Length of output: 16114
🏁 Script executed:
#!/antml:bash
# Check git history to see when OptionalTransfer was created and if it was ever used
git log --oneline --all -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java | head -5Repository: typetools/checker-framework
Length of output: 319
🏁 Script executed:
#!/antml:bash
# Check if there's any recent change or if OptionalTransfer is a new class
git log -1 --format="%H %ai %s" -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javaRepository: typetools/checker-framework
Length of output: 171
🏁 Script executed:
#!/antml:bash
# Look for commits that mention OptionalTransfer
git log --oneline --all --grep='OptionalTransfer' | head -5Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/antml:bash
# Verify that OptionalTransfer is truly dead code - check if there are any extension points or registrations
rg -nP --type=java 'extends OptionalTransfer|implements.*OptionalTransfer'Repository: typetools/checker-framework
Length of output: 53
🏁 Script executed:
#!/antml:bash
# Check the recent commit to see what OptionalTransfer was added for
git show 9c61e80c --stat | head -30Repository: typetools/checker-framework
Length of output: 1727
🏁 Script executed:
#!/antml:bash
# Get more detail on the commit that introduced OptionalTransfer
git show 9c61e80c --name-status | grep -i optionalRepository: typetools/checker-framework
Length of output: 1461
🏁 Script executed:
#!/antml:bash
# Check if OptionalTransfer was re-added after the deletion
git log --oneline -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java | head -10Repository: typetools/checker-framework
Length of output: 113
🏁 Script executed:
#!/antml:bash
# Get the full history including when it was re-added
git log --all --oneline --follow -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javaRepository: typetools/checker-framework
Length of output: 477
🏁 Script executed:
#!/antml:bash
# Check the recent commits to see when OptionalTransfer was added back
git log --oneline -20 -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.javaRepository: typetools/checker-framework
Length of output: 113
🏁 Script executed:
#!/antml:bash
# Check what commit a5eb5378 did - specifically regarding OptionalTransfer
git show a5eb5378 -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java | head -100Repository: typetools/checker-framework
Length of output: 4917
🏁 Script executed:
#!/antml:bash
# Get the full diff of that commit to understand the context
git show a5eb5378 --stat | grep -i optionalRepository: typetools/checker-framework
Length of output: 3917
🏁 Script executed:
#!/antml:bash
# Check if OptionalTransfer was added in a5eb5378
git show a5eb5378 --name-status | grep OptionalTransferRepository: typetools/checker-framework
Length of output: 154
🏁 Script executed:
#!/antml:bash
# Check if there's any plan to use OptionalTransfer or if it's truly abandoned
git log --all -p a5eb5378^..a5eb5378 -- checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java | tail -50Repository: typetools/checker-framework
Length of output: 112
OptionalTransfer is dead code that duplicates OptionalImplTransfer and should be removed.
OptionalTransfer is never instantiated anywhere in the codebase. The wiring chain OptionalImplAnnotatedTypeFactory.createFlowTransferFunction() returns only new OptionalImplTransfer(analysis), never OptionalTransfer. The cast at line 50 and the initialStore() method (lines 60–100) are identical to OptionalImplTransfer (lines 91–155), creating dead code duplication and maintenance burden. This class appears to be orphaned from a refactoring; either remove it or document its intended purpose.
🤖 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/optional/OptionalTransfer.java`
at line 50, OptionalTransfer is dead duplicated code; remove it to eliminate
redundancy. Delete the OptionalTransfer class entirely (including the cast
optionalTypeFactory = (OptionalImplAnnotatedTypeFactory)
analysis.getTypeFactory(); and its initialStore() implementation) and ensure no
callers reference it — the factory
OptionalImplAnnotatedTypeFactory.createFlowTransferFunction() already constructs
OptionalImplTransfer, so rely on OptionalImplTransfer (and keep its
initialStore() implementation at lines referenced in that class) as the single
transfer implementation; if there was intended special behavior, consolidate
that behavior into OptionalImplTransfer instead of keeping OptionalTransfer.
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java (1)
584-590:⚠️ Potential issue | 🟡 MinorTODO comment may be outdated.
The TODO suggests maintaining a HashSet to avoid linear-time containment checks, but this optimization is already implemented. The
Worklistclass maintainsqueueSet(line 636) alongside thequeue, and thecontains()method (line 694) usesqueueSet.contains(block), which is O(1). Consider removing this TODO or updating it to reflect the current implementation.📝 Proposed fix to remove the outdated TODO
- // TODO: This costs linear (!) time. Use a more efficient way to check if b is already present. - // Two possibilities: - // * add unconditionally, and detect duplicates when removing from the queue. - // * maintain a HashSet of the elements that are already in the queue. if (!worklist.contains(b)) { worklist.add(b); }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java` around lines 584 - 590, The TODO in AbstractAnalysis around the worklist.contains(b) check is outdated because Worklist already provides an O(1 contains via its internal queueSet); update the code by removing the misleading TODO comment (or rewrite it to note that Worklist.contains() is O(1 due to Worklist.queueSet) and explain any remaining performance considerations), referencing the worklist variable and the Worklist class methods (especially Worklist.contains and queueSet) so future readers know the optimization is implemented.
♻️ Duplicate comments (2)
checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java (1)
1004-1008:⚠️ Potential issue | 🟡 MinorAvoid mutating primary annotations while iterating them.
replaceAnnotationcan mutate the backing annotation set returned bygetPrimaryAnnotations(). Compute the match first, then replace after the loop.🐛 Proposed fix
- for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { - if (AnnotationUtils.areSameByName( - anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) { - rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION); - } - } + boolean hasUnknownInitialization = false; + for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) { + hasUnknownInitialization = true; + break; + } + } + if (hasUnknownInitialization) { + rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION); + }🤖 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/nullness/NullnessAnnotatedTypeFactory.java` around lines 1004 - 1008, Iterating rhsATM.getPrimaryAnnotations() and calling rhsATM.replaceAnnotation(...) can mutate the annotation set; instead, first detect whether any annotation matches "org.checkerframework.checker.initialization.qual.UnknownInitialization" by scanning rhsATM.getPrimaryAnnotations() (store a boolean or the matching AnnotationMirror), then after the loop call rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION) only if a match was found; reference rhsATM, getPrimaryAnnotations(), replaceAnnotation, and UNKNOWN_INITIALIZATION when making the change.checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java (1)
68-68: 🧹 Nitpick | 🔵 TrivialUse
OptionalImplAnnotatedTypeFactoryas the visitor factory type.
BaseAnnotatedTypeFactoryweakens the type contract, and the commented concrete type suggests the intended binding. Prefer:♻️ Proposed fix
- extends BaseTypeVisitor</* OptionalImplAnnotatedTypeFactory*/ BaseAnnotatedTypeFactory> { + extends BaseTypeVisitor<OptionalImplAnnotatedTypeFactory> {🤖 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/optional/OptionalImplVisitor.java` at line 68, The visitor class OptionalImplVisitor currently extends BaseTypeVisitor<BaseAnnotatedTypeFactory>, weakening the type contract; change its generic to the concrete OptionalImplAnnotatedTypeFactory so the class signature uses OptionalImplAnnotatedTypeFactory as the visitor factory type (replace BaseAnnotatedTypeFactory with OptionalImplAnnotatedTypeFactory in the extends clause of OptionalImplVisitor) to restore the intended binding and enable access to factory-specific APIs.
🤖 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/nullness/NullnessAnnotatedTypeFactory.java`:
- Around line 957-958: The call to wpiAdjustInitializationAnnotations(rhsATM,
TypeUseLocation.FIELD) is too broad and rewrites `@UnknownInitialization` for
non-parameter updates; move this WPI initialization rewrite so it only runs for
parameter updates (i.e., at the site that has TypeUseLocation.PARAMETER) or
change the call sites (including the analogous spots around
wpiAdjustForUpdateNonField at the other location) to pass the actual
TypeUseLocation and guard inside wpiAdjustInitializationAnnotations so it only
modifies rhsATM when the location is PARAMETER, leaving field/receiver updates
unchanged.
---
Outside diff comments:
In
`@dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java`:
- Around line 584-590: The TODO in AbstractAnalysis around the
worklist.contains(b) check is outdated because Worklist already provides an O(1
contains via its internal queueSet); update the code by removing the misleading
TODO comment (or rewrite it to note that Worklist.contains() is O(1 due to
Worklist.queueSet) and explain any remaining performance considerations),
referencing the worklist variable and the Worklist class methods (especially
Worklist.contains and queueSet) so future readers know the optimization is
implemented.
---
Duplicate comments:
In
`@checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java`:
- Around line 1004-1008: Iterating rhsATM.getPrimaryAnnotations() and calling
rhsATM.replaceAnnotation(...) can mutate the annotation set; instead, first
detect whether any annotation matches
"org.checkerframework.checker.initialization.qual.UnknownInitialization" by
scanning rhsATM.getPrimaryAnnotations() (store a boolean or the matching
AnnotationMirror), then after the loop call
rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION) only if a match was found;
reference rhsATM, getPrimaryAnnotations(), replaceAnnotation, and
UNKNOWN_INITIALIZATION when making the change.
In
`@checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java`:
- Line 68: The visitor class OptionalImplVisitor currently extends
BaseTypeVisitor<BaseAnnotatedTypeFactory>, weakening the type contract; change
its generic to the concrete OptionalImplAnnotatedTypeFactory so the class
signature uses OptionalImplAnnotatedTypeFactory as the visitor factory type
(replace BaseAnnotatedTypeFactory with OptionalImplAnnotatedTypeFactory in the
extends clause of OptionalImplVisitor) to restore the intended binding and
enable access to factory-specific APIs.
🪄 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: bcdb7dcf-4bff-47d9-9afc-9791974ed012
📒 Files selected for processing (4)
checker/build.gradlechecker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.javachecker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.javadataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java
💤 Files with no reviewable changes (1)
- checker/build.gradle
| // Adjust initialization annotations first | ||
| wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.FIELD); |
There was a problem hiding this comment.
Limit the WPI initialization rewrite to parameter updates.
These call sites rewrite @UnknownInitialization for field updates and all non-field updates. That is broader than the stated WPI fix: wpiAdjustForUpdateNonField also covers non-parameter locations such as receivers, so this can unnecessarily weaken inferred initialization annotations outside the looping case.
Please move this adjustment to the point that has the actual TypeUseLocation.PARAMETER, or otherwise pass through the real location and guard on it.
Also applies to: 977-978
🤖 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/nullness/NullnessAnnotatedTypeFactory.java`
around lines 957 - 958, The call to wpiAdjustInitializationAnnotations(rhsATM,
TypeUseLocation.FIELD) is too broad and rewrites `@UnknownInitialization` for
non-parameter updates; move this WPI initialization rewrite so it only runs for
parameter updates (i.e., at the site that has TypeUseLocation.PARAMETER) or
change the call sites (including the analogous spots around
wpiAdjustForUpdateNonField at the other location) to pass the actual
TypeUseLocation and guard inside wpiAdjustInitializationAnnotations so it only
modifies rhsATM when the location is PARAMETER, leaving field/receiver updates
unchanged.
In some NJR benchmarks (Zenodo Record), when multiple constructors are present, WPI does not account for the absence of initializations. This oversight can lead to non-termination issues, particularly with
@UnknownInitializationannotations when visiting object creation.This repository (wpi-njr-debug) recreates the problem. The
dataset/SimplifiedTestCodedirectory contains sample code that reproduces the issue.Changes Made
I have modified the
updateAnnotationSetmethod as follows:For parameters, if
rhsmATMisNullableorMonotonicNonNulland has the@UnknownInitializationannotation, and if the annotation is not@UnknownInitialization(java.lang.Object.class), replace it with@UnknownInitialization(java.lang.Object.class). This is because there is likely a constructor where it hasn't been initialized, and we haven't considered its effect. Otherwise, WPI might get stuck in a loop.Potential Trade-offs
This approach might result in losing some information regarding cases where the lhs is a parameter and the rhs is
Nullableand has the@UnknownInitializationannotation for any class other thanjava.lang.Object.We could narrow the domain of this change by analyzing the constructors and fields along with their initialization status or by delving deeper into the initialization checker and attempting to use it. However, based on my tests and pre-implementations, those approaches require significantly more effort and time to implement correctly.
Testing and Results
Based on my experiments, this change resolves the non-termination issue when combined with disabling contract annotations in most benchmarks.
@kelloggm, I would appreciate it if you could review the changes and provide your feedback.