Fix WPI Non-Termination Issue with @UnknownInitialization Annotations #6657
+442
−4
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -1065,4 +1065,3 @@ publishing { | |
| signing { | ||
| sign(publishing.publications.checker) | ||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| @@ -0,0 +1,101 @@ | ||||||||||||||||||
| package org.checkerframework.checker.optional; | ||||||||||||||||||
|
|
||||||||||||||||||
| import com.sun.source.tree.ExpressionTree; | ||||||||||||||||||
| import com.sun.source.tree.LambdaExpressionTree; | ||||||||||||||||||
| import com.sun.source.tree.MemberSelectTree; | ||||||||||||||||||
| import com.sun.source.tree.MethodInvocationTree; | ||||||||||||||||||
| import com.sun.source.tree.Tree; | ||||||||||||||||||
| import com.sun.source.tree.VariableTree; | ||||||||||||||||||
| import com.sun.source.util.TreePath; | ||||||||||||||||||
| import java.util.List; | ||||||||||||||||||
| import javax.annotation.processing.ProcessingEnvironment; | ||||||||||||||||||
| import javax.lang.model.element.AnnotationMirror; | ||||||||||||||||||
| import javax.lang.model.element.ExecutableElement; | ||||||||||||||||||
| import javax.lang.model.util.Elements; | ||||||||||||||||||
| import org.checkerframework.checker.nullness.qual.Nullable; | ||||||||||||||||||
| import org.checkerframework.checker.optional.qual.Present; | ||||||||||||||||||
| import org.checkerframework.dataflow.cfg.UnderlyingAST; | ||||||||||||||||||
| import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda; | ||||||||||||||||||
| import org.checkerframework.dataflow.cfg.node.LocalVariableNode; | ||||||||||||||||||
| import org.checkerframework.dataflow.expression.JavaExpression; | ||||||||||||||||||
| import org.checkerframework.framework.flow.CFAbstractAnalysis; | ||||||||||||||||||
| import org.checkerframework.framework.flow.CFStore; | ||||||||||||||||||
| import org.checkerframework.framework.flow.CFTransfer; | ||||||||||||||||||
| import org.checkerframework.framework.flow.CFValue; | ||||||||||||||||||
| import org.checkerframework.javacutil.AnnotationBuilder; | ||||||||||||||||||
| import org.checkerframework.javacutil.TreeUtils; | ||||||||||||||||||
|
|
||||||||||||||||||
| /** The transfer function for the Optional Checker. */ | ||||||||||||||||||
| public class OptionalTransfer extends CFTransfer { | ||||||||||||||||||
|
|
||||||||||||||||||
| /** The {@link OptionalImplAnnotatedTypeFactory} instance for this transfer class. */ | ||||||||||||||||||
| private final OptionalImplAnnotatedTypeFactory optionalTypeFactory; | ||||||||||||||||||
|
|
||||||||||||||||||
| /** The @{@link Present} annotation. */ | ||||||||||||||||||
| private final AnnotationMirror PRESENT; | ||||||||||||||||||
|
|
||||||||||||||||||
| /** The element for java.util.Optional.ifPresent(). */ | ||||||||||||||||||
| private final ExecutableElement optionalIfPresent; | ||||||||||||||||||
|
|
||||||||||||||||||
| /** The element for java.util.Optional.ifPresentOrElse(), or null. */ | ||||||||||||||||||
| private final @Nullable ExecutableElement optionalIfPresentOrElse; | ||||||||||||||||||
|
|
||||||||||||||||||
| /** | ||||||||||||||||||
| * Create an OptionalTransfer. | ||||||||||||||||||
| * | ||||||||||||||||||
| * @param analysis the Optional Checker instance | ||||||||||||||||||
| */ | ||||||||||||||||||
| public OptionalTransfer(CFAbstractAnalysis<CFValue, CFStore, CFTransfer> analysis) { | ||||||||||||||||||
| super(analysis); | ||||||||||||||||||
| optionalTypeFactory = (OptionalImplAnnotatedTypeFactory) analysis.getTypeFactory(); | ||||||||||||||||||
|
Contributor
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.
🤖 Prompt for AI Agents |
||||||||||||||||||
| Elements elements = optionalTypeFactory.getElementUtils(); | ||||||||||||||||||
| PRESENT = AnnotationBuilder.fromClass(elements, Present.class); | ||||||||||||||||||
| ProcessingEnvironment env = optionalTypeFactory.getProcessingEnv(); | ||||||||||||||||||
| optionalIfPresent = TreeUtils.getMethod("java.util.Optional", "ifPresent", 1, env); | ||||||||||||||||||
| optionalIfPresentOrElse = | ||||||||||||||||||
| TreeUtils.getMethodOrNull("java.util.Optional", "ifPresentOrElse", 2, env); | ||||||||||||||||||
| } | ||||||||||||||||||
|
|
||||||||||||||||||
| @Override | ||||||||||||||||||
| public CFStore initialStore(UnderlyingAST underlyingAST, List<LocalVariableNode> parameters) { | ||||||||||||||||||
|
|
||||||||||||||||||
| CFStore result = super.initialStore(underlyingAST, parameters); | ||||||||||||||||||
|
|
||||||||||||||||||
| if (underlyingAST.getKind() == UnderlyingAST.Kind.LAMBDA) { | ||||||||||||||||||
| // Check whether this lambda is an argument to `Optional.ifPresent()` or | ||||||||||||||||||
| // `Optional.ifPresentOrElse()`. If so, then within the lambda, the receiver of the | ||||||||||||||||||
| // `ifPresent*` method is @Present. | ||||||||||||||||||
| CFGLambda cfgLambda = (CFGLambda) underlyingAST; | ||||||||||||||||||
| LambdaExpressionTree lambdaTree = cfgLambda.getLambdaTree(); | ||||||||||||||||||
| List<? extends VariableTree> lambdaParams = lambdaTree.getParameters(); | ||||||||||||||||||
| if (lambdaParams.size() == 1) { | ||||||||||||||||||
| TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); | ||||||||||||||||||
| Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); | ||||||||||||||||||
|
Comment on lines
+72
to
+73
Contributor
There was a problem hiding this comment. Potential NPE if While unlikely in practice (a lambda should always have a parent), 🛡️ 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
Suggested change
🤖 Prompt for AI Agents |
||||||||||||||||||
| if (lambdaParent instanceof MethodInvocationTree) { | ||||||||||||||||||
| MethodInvocationTree invok = (MethodInvocationTree) lambdaParent; | ||||||||||||||||||
| ExecutableElement methodElt = TreeUtils.elementFromUse(invok); | ||||||||||||||||||
| if (methodElt.equals(optionalIfPresent) || methodElt.equals(optionalIfPresentOrElse)) { | ||||||||||||||||||
| // `underlyingAST` is an invocation of `Optional.ifPresent()` or | ||||||||||||||||||
| // `Optional.ifPresentOrElse()`. In the lambda, the receiver is @Present. | ||||||||||||||||||
| ExpressionTree methodSelectTree = TreeUtils.withoutParens(invok.getMethodSelect()); | ||||||||||||||||||
| ExpressionTree receiverTree = ((MemberSelectTree) methodSelectTree).getExpression(); | ||||||||||||||||||
| JavaExpression receiverJe = JavaExpression.fromTree(receiverTree); | ||||||||||||||||||
| result.insertValue(receiverJe, PRESENT); | ||||||||||||||||||
| } | ||||||||||||||||||
| } | ||||||||||||||||||
| } | ||||||||||||||||||
| } | ||||||||||||||||||
|
|
||||||||||||||||||
| // TODO: Similar logic to the above can be applied in the Nullness Checker. | ||||||||||||||||||
| // Some methods take a function as an argument, guaranteeing that, if the function is | ||||||||||||||||||
| // called: | ||||||||||||||||||
| // * the value passed to the function is non-null | ||||||||||||||||||
| // * some other argument to the method is non-null | ||||||||||||||||||
| // Examples: | ||||||||||||||||||
| // * Jodd's `StringUtil.ifNotNull()` | ||||||||||||||||||
| // * `Opt.ifPresent()` | ||||||||||||||||||
| // * `Opt.map()` | ||||||||||||||||||
|
|
||||||||||||||||||
| return result; | ||||||||||||||||||
| } | ||||||||||||||||||
| } | ||||||||||||||||||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,91 @@ | ||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") | ||
| interface Game { | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| void newGame(); | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") | ||
| class // package-private | ||
| GameImpl implements // package-private | ||
| Game { | ||
|
|
||
| private MoveValidator moveValidator; | ||
|
|
||
| @org.checkerframework.dataflow.qual.Impure | ||
| public GameImpl(MoveValidator mValidator) { | ||
| mValidator.setGame(this); | ||
| moveValidator = mValidator; | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public GameImpl() { | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public void newGame( // package-private | ||
| GameImpl this) { | ||
| // Implementation of starting a new game | ||
| } | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") | ||
| interface MoveValidator { | ||
|
|
||
| @org.checkerframework.dataflow.qual.Impure | ||
| void setGame( MoveValidator this, Game game); | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") | ||
| class // package-private | ||
| PlayerDependentMoveValidator implements // package-private | ||
| MoveValidator { | ||
|
|
||
| private Game game; | ||
|
|
||
| private MoveValidator blackMoveValidator = new SimpleMoveValidator(); | ||
|
|
||
| @org.checkerframework.dataflow.qual.Impure | ||
| public void setGame( // package-private | ||
| PlayerDependentMoveValidator this, Game game) { | ||
| this.game = game; | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public PlayerDependentMoveValidator() { | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.Impure | ||
| public PlayerDependentMoveValidator( Game game) { | ||
| this.setGame(game); | ||
| blackMoveValidator.setGame(game); | ||
| } | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") | ||
| class // package-private | ||
| SimpleMoveValidator implements // package-private | ||
| MoveValidator { | ||
|
|
||
| private Game game; | ||
|
|
||
| @org.checkerframework.dataflow.qual.Impure | ||
| public void setGame( // package-private | ||
| SimpleMoveValidator this, Game game) { | ||
| this.game = game; | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public SimpleMoveValidator() { | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.Pure | ||
| public MoveValidator createMoveValidator() { | ||
| return new PlayerDependentMoveValidator(game); | ||
| } | ||
| public void test(){ | ||
| PlayerDependentMoveValidator g1 = | ||
| new PlayerDependentMoveValidator(game); | ||
| this.game = g1.game; | ||
| } | ||
|
Comment on lines
+86
to
+90
Contributor
There was a problem hiding this comment. Same visibility issue as the NullnessChecker variant. The Additionally, the 🤖 Prompt for AI Agents |
||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,98 @@ | ||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") | ||
| interface Game { | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| void newGame(); | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") | ||
| class // package-private | ||
| GameImpl implements // package-private | ||
| Game { | ||
|
|
||
| private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.MonotonicNonNull MoveValidator moveValidator; | ||
|
|
||
| @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.moveValidator" }) | ||
| @org.checkerframework.dataflow.qual.Impure | ||
| public GameImpl(MoveValidator mValidator) { | ||
| mValidator.setGame(this); | ||
| moveValidator = mValidator; | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public GameImpl() { | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.moveValidator" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) | ||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public void newGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private | ||
| GameImpl this) { | ||
| // Implementation of starting a new game | ||
| } | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") | ||
| interface MoveValidator { | ||
|
|
||
| @org.checkerframework.dataflow.qual.Impure | ||
| void setGame(@org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game); | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") | ||
| class // package-private | ||
| PlayerDependentMoveValidator implements // package-private | ||
| MoveValidator { | ||
|
|
||
| private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game; | ||
|
|
||
| private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull MoveValidator blackMoveValidator = new SimpleMoveValidator(); | ||
|
|
||
| @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.game" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) | ||
| @org.checkerframework.dataflow.qual.Impure | ||
| public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private | ||
| PlayerDependentMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) { | ||
| this.game = game; | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public PlayerDependentMoveValidator() { | ||
| } | ||
|
|
||
| @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "#1" }) | ||
| @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) | ||
| @org.checkerframework.dataflow.qual.Impure | ||
| public PlayerDependentMoveValidator(@org.checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) { | ||
| this.setGame(game); | ||
| blackMoveValidator.setGame(game); | ||
| } | ||
| } | ||
|
|
||
| @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") | ||
| class // package-private | ||
| SimpleMoveValidator implements // package-private | ||
| MoveValidator { | ||
|
|
||
| private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.MonotonicNonNull Game game; | ||
|
|
||
| @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) | ||
| @org.checkerframework.dataflow.qual.Impure | ||
| public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private | ||
| SimpleMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.NonNull Game game) { | ||
| this.game = game; | ||
| } | ||
|
|
||
| @org.checkerframework.dataflow.qual.SideEffectFree | ||
| public SimpleMoveValidator() { | ||
| } | ||
|
|
||
| @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) | ||
| @org.checkerframework.dataflow.qual.Pure | ||
| public @org.checkerframework.checker.initialization.qual.UnderInitialization(PlayerDependentMoveValidator.class) @org.checkerframework.checker.nullness.qual.NonNull MoveValidator createMoveValidator() { | ||
| return new PlayerDependentMoveValidator(game); | ||
| } | ||
| public void test(){ | ||
| PlayerDependentMoveValidator g1 = | ||
| new PlayerDependentMoveValidator(game); | ||
| this.game = g1.game; | ||
| } | ||
| } |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Limit the WPI initialization rewrite to parameter updates.
These call sites rewrite
@UnknownInitializationfor field updates and all non-field updates. That is broader than the stated WPI fix:wpiAdjustForUpdateNonFieldalso 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