Skip to content

Call extend only once #7234

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 35 commits into
base: master
Choose a base branch
from
Open

Call extend only once #7234

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
87359b2
Call `extend` only once
mernst Aug 31, 2025
9e4b90b
Merge ../checker-framework-branch-master into cfg-extend-once
mernst Aug 31, 2025
df55f80
Rename `*Playground` to `*Pdf`
mernst Aug 31, 2025
b68c5e5
Merge ../checker-framework-fork-mernst-branch-playground into cfg-ext…
mernst Aug 31, 2025
f949caa
Renamings
mernst Aug 31, 2025
c1b8a49
Merge ../checker-framework-fork-mernst-branch-rename-playground-to-pd…
mernst Aug 31, 2025
95eaa3c
Javadoc fix
mernst Aug 31, 2025
d021484
Add changelog
mernst Aug 31, 2025
daf0d3f
Produce PDF as well as string representation when testing
mernst Aug 31, 2025
4a19961
Merge ../checker-framework-fork-mernst-branch-renaming into rename-pl…
mernst Aug 31, 2025
9845c39
Merge ../checker-framework-fork-mernst-branch-playground into cfg-ext…
mernst Aug 31, 2025
f09e2d6
Undo duplication
mernst Aug 31, 2025
4c0104a
Separate creation of CFG from visualizing it
mernst Aug 31, 2025
9ea4ca0
Fix Javadoc
mernst Aug 31, 2025
8f2b457
Fix Javadoc
mernst Aug 31, 2025
842c823
Fix nullness specification
mernst Aug 31, 2025
2a5935a
Tweaks
mernst Aug 31, 2025
b1e57a3
Merge ../checker-framework-fork-mernst-branch-playground into cfg-ext…
mernst Aug 31, 2025
d19a35f
Change order of arguments
mernst Aug 31, 2025
0dc71fe
Merge ../checker-framework-fork-mernst-branch-playground into cfg-ext…
mernst Aug 31, 2025
bee06df
Merge branch 'master' into playground
smillst Sep 4, 2025
b43f8b9
Merge ../checker-framework-branch-master into playground
mernst Sep 5, 2025
bedba2e
Merge ../checker-framework-fork-mernst-branch-playground into cfg-ext…
mernst Sep 5, 2025
89a03dc
Merge ../checker-framework-branch-master into cfg-extend-once-tests
mernst Sep 5, 2025
972d398
Merge ../checker-framework-fork-mernst-branch-cfg-extend-once-tests i…
mernst Sep 5, 2025
afe3aad
Merge branch 'master' into cfg-extend-once
mernst Sep 8, 2025
a9748ea
Merge ../checker-framework-branch-master into cfg-extend-once-tests
mernst Sep 9, 2025
eba9d48
Merge ../checker-framework-fork-mernst-branch-cfg-extend-once-tests i…
mernst Sep 9, 2025
bf2a052
Merge ../checker-framework-branch-master into cfg-extend-once-tests
mernst Sep 9, 2025
8352eb6
Merge ../checker-framework-branch-master into cfg-extend-once-tests
mernst Sep 9, 2025
9c8b23f
Merge ../checker-framework-fork-mernst-branch-cfg-extend-once-tests i…
mernst Sep 9, 2025
f2f456a
Merge branch 'cfg-extend-once-tests' of github.com:mernst/checker-fra…
mernst Sep 9, 2025
1629777
Merge ../checker-framework-fork-mernst-branch-cfg-extend-once-tests i…
mernst Sep 9, 2025
3c73cd7
Merge ../checker-framework-branch-master into cfg-extend-once-tests
mernst Sep 11, 2025
1a0a25e
Merge ../checker-framework-fork-mernst-branch-cfg-extend-once-tests i…
mernst Sep 11, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,6 +170,9 @@ dataflow/tests/busy-expression/Out.txt
dataflow/tests/busy-expression/*.class
dataflow/tests/busyexpr/Out.txt
dataflow/tests/busyexpr/*.class
dataflow/tests/busyexpr/Test-test-int.dot
dataflow/tests/busyexpr/Test-test-int.dot.pdf
dataflow/tests/busyexpr/methods.txt
Comment on lines +173 to +175
Copy link
Contributor

Choose a reason for hiding this comment

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

🧹 Nitpick (assertive)

Also ignore busy-expression DOT/PDF/methods artifacts

BusyExpression runs from a “busyexpr/busy-expression” pair of dirs; you added ignores for busyexpr but not busy-expression. Add symmetric patterns to avoid accidental git noise when run from the hyphenated dir.

 dataflow/tests/busyexpr/Test-test-int.dot
 dataflow/tests/busyexpr/Test-test-int.dot.pdf
 dataflow/tests/busyexpr/methods.txt
+dataflow/tests/busy-expression/Test-test-int.dot
+dataflow/tests/busy-expression/Test-test-int.dot.pdf
+dataflow/tests/busy-expression/methods.txt
📝 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
dataflow/tests/busyexpr/Test-test-int.dot
dataflow/tests/busyexpr/Test-test-int.dot.pdf
dataflow/tests/busyexpr/methods.txt
dataflow/tests/busyexpr/Test-test-int.dot
dataflow/tests/busyexpr/Test-test-int.dot.pdf
dataflow/tests/busyexpr/methods.txt
dataflow/tests/busy-expression/Test-test-int.dot
dataflow/tests/busy-expression/Test-test-int.dot.pdf
dataflow/tests/busy-expression/methods.txt
🤖 Prompt for AI Agents 
In .gitignore around lines 173-175: the file currently ignores artifacts under
dataflow/tests/busyexpr/* but not the hyphenated sibling directory
busy-expression; add symmetric ignore patterns for
dataflow/tests/busy-expression/Test-test-int.dot,
dataflow/tests/busy-expression/Test-test-int.dot.pdf and
dataflow/tests/busy-expression/methods.txt (or equivalent wildcard patterns) so
artifacts produced when running from the hyphenated dir are also ignored.

dataflow/tests/cfgconstruction/*.class
dataflow/tests/constant-propagation/Out.txt
dataflow/tests/constant-propagation/*.class
Expand Down
9 changes: 6 additions & 3 deletions dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1954,12 +1954,14 @@ public Node visitCompoundAssignment(CompoundAssignmentTree tree, Void p) {
Node operNode;
if (kind == Tree.Kind.MULTIPLY_ASSIGNMENT) {
operNode = new NumericalMultiplicationNode(operTree, targetRHS, value);
extendWithNode(operNode);
} else if (kind == Tree.Kind.DIVIDE_ASSIGNMENT) {
if (TypesUtils.isIntegralPrimitive(exprType)) {
operNode = new IntegerDivisionNode(operTree, targetRHS, value);
extendWithNodeWithException(operNode, arithmeticExceptionType);
} else {
operNode = new FloatingDivisionNode(operTree, targetRHS, value);
extendWithNode(operNode);
}
} else {
assert kind == Tree.Kind.REMAINDER_ASSIGNMENT;
Expand All @@ -1968,9 +1970,9 @@ public Node visitCompoundAssignment(CompoundAssignmentTree tree, Void p) {
extendWithNodeWithException(operNode, arithmeticExceptionType);
} else {
operNode = new FloatingRemainderNode(operTree, targetRHS, value);
extendWithNode(operNode);
}
}
extendWithNode(operNode);

TypeMirror castType = TypeAnnotationUtils.unannotatedType(leftType);
TypeCastTree castTree = treeBuilder.buildTypeCast(castType, operTree);
Expand Down Expand Up @@ -2167,6 +2169,7 @@ public Node visitBinary(BinaryTree tree, Void p) {
if (TypesUtils.isIntegralPrimitive(exprType)) {
r = new IntegerDivisionNode(tree, left, right);
extendWithNodeWithException(r, arithmeticExceptionType);
return r;
} else {
r = new FloatingDivisionNode(tree, left, right);
}
Expand All @@ -2175,6 +2178,7 @@ public Node visitBinary(BinaryTree tree, Void p) {
if (TypesUtils.isIntegralPrimitive(exprType)) {
r = new IntegerRemainderNode(tree, left, right);
extendWithNodeWithException(r, arithmeticExceptionType);
return r;
} else {
r = new FloatingRemainderNode(tree, left, right);
}
Expand Down Expand Up @@ -3119,7 +3123,7 @@ public Node visitEnhancedForLoop(EnhancedForLoopTree tree, Void p) {
handleArtificialTree(lengthSelect);
FieldAccessNode lengthAccessNode = new FieldAccessNode(lengthSelect, arrayNode1);
lengthAccessNode.setInSource(false);
extendWithNode(lengthAccessNode);
extendWithNodeWithException(lengthAccessNode, nullPointerExceptionType);

Comment on lines 3123 to 3127
Copy link
Contributor

Choose a reason for hiding this comment

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

🧹 Nitpick (assertive)

Shift NPE accounting to length access: OK; add rationale comment and confirm no AIOOBE risk.

Attaching NPE to array.length is sound here since you bounds-check before element access and the synthetic array temp isn’t reassigned. Consider a short comment to document this invariant.

Proposed comment:

       FieldAccessNode lengthAccessNode = new FieldAccessNode(lengthSelect, arrayNode1);
       lengthAccessNode.setInSource(false);
-      extendWithNodeWithException(lengthAccessNode, nullPointerExceptionType);
+      // Attach NPE to length access; element access is safe due to prior bounds check and the
+      // synthetic array temp not being reassigned.
+      extendWithNodeWithException(lengthAccessNode, nullPointerExceptionType);
📝 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
handleArtificialTree(lengthSelect);
FieldAccessNode lengthAccessNode = new FieldAccessNode(lengthSelect, arrayNode1);
lengthAccessNode.setInSource(false);
extendWithNode(lengthAccessNode);
extendWithNodeWithException(lengthAccessNode, nullPointerExceptionType);
handleArtificialTree(lengthSelect);
FieldAccessNode lengthAccessNode = new FieldAccessNode(lengthSelect, arrayNode1);
lengthAccessNode.setInSource(false);
// Attach NPE to length access; element access is safe due to prior bounds check and the
// synthetic array temp not being reassigned.
extendWithNodeWithException(lengthAccessNode, nullPointerExceptionType);
🤖 Prompt for AI Agents 
In
dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
around lines 3123-3127, add a short rationale comment immediately above the
length access handling that explains why the NPE is attached to array.length
(i.e., the code performs a bounds-check before any element access and the
synthetic array temp is never reassigned), and explicitly state that this
invariant rules out an ArrayIndexOutOfBoundsException at this site; keep the
comment concise and factual so future readers understand the safety assumption.

BinaryTree lessThan = treeBuilder.buildLessThan(indexUse1, lengthSelect);
handleArtificialTree(lessThan);
Expand Down Expand Up @@ -3154,7 +3158,6 @@ public Node visitEnhancedForLoop(EnhancedForLoopTree tree, Void p) {
extendWithNode(arrayAccessNode);
AssignmentNode arrayAccessAssignNode =
translateAssignment(variable, new LocalVariableNode(variable), arrayAccessNode);
extendWithNodeWithException(arrayAccessNode, nullPointerExceptionType);
// translateAssignment() scans variable and creates new nodes, so set the expression
// there, too.
Node arrayAccessAssignNodeExpr = arrayAccessAssignNode.getExpression();
Expand Down
19 changes: 14 additions & 5 deletions dataflow/src/test/java/busyexpr/BusyExpression.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,25 +5,34 @@
import org.checkerframework.dataflow.analysis.UnusedAbstractValue;
import org.checkerframework.dataflow.busyexpr.BusyExprStore;
import org.checkerframework.dataflow.busyexpr.BusyExprTransfer;
import org.checkerframework.dataflow.cfg.ControlFlowGraph;
import org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher;

/** Used in busyExpressionTest Gradle task to test the BusyExpression analysis. */
/**
* Run busy expression analysis create a text file of the CFG.
*
* <p>Used in busyExpressionTest Gradle task to test the BusyExpression analysis.
*/
Comment on lines +11 to +15
Copy link
Contributor

Choose a reason for hiding this comment

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

⚠️ Potential issue

Fix Javadoc grammar

Small wording improvement.

-/**
- * Run busy expression analysis create a text file of the CFG.
+/**
+ * Run the busy-expression analysis and create a text file of the CFG.
🤖 Prompt for AI Agents 
In dataflow/src/test/java/busyexpr/BusyExpression.java around lines 11 to 15,
the Javadoc sentence "Run busy expression analysis create a text file of the
CFG." is grammatically incorrect; replace it with a clear, grammatical
description such as "Run the busy expression analysis and create a text file of
the control-flow graph (CFG)." and ensure the rest of the Javadoc remains
accurate and properly punctuated.

public class BusyExpression {
/**
* The main method expects to be run in dataflow/tests/busy-expression directory.
* The main method expects to be run in the {@code dataflow/tests/busy-expression/} directory.
*
* @param args not used
* @param args command-line arguments, not used
*/
Comment on lines +18 to 21
Copy link
Contributor

Choose a reason for hiding this comment

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

🧹 Nitpick (assertive)

Directory name mismatch: busyexpr vs busy-expression

The class is under package/dir “busyexpr”, but the Javadoc says to run from “dataflow/tests/busy-expression/”. Align to avoid confusion.

Would you like me to update the Javadoc to “dataflow/tests/busyexpr/” and grep the repo for other occurrences?

🤖 Prompt for AI Agents 
In dataflow/src/test/java/busyexpr/BusyExpression.java around lines 18 to 21,
the Javadoc references the directory "dataflow/tests/busy-expression/" which
doesn't match the package/dir name "busyexpr"; update the Javadoc to
"dataflow/tests/busyexpr/" to match the package, and then run a repository-wide
search (e.g., grep) for "busy-expression" to find and update any other
mismatched references so documentation and paths are consistent.

public static void main(String[] args) {

String inputFile = "Test.java"; // input file name;
String inputFile = "Test.java";
String method = "test";
String clazz = "Test";
String outputFile = "Out.txt";

BusyExprTransfer transfer = new BusyExprTransfer();
BackwardAnalysis<UnusedAbstractValue, BusyExprStore, BusyExprTransfer> backwardAnalysis =
new BackwardAnalysisImpl<>(transfer);
CFGVisualizeLauncher.writeStringOfCFG(inputFile, method, clazz, outputFile, backwardAnalysis);
ControlFlowGraph cfg =
CFGVisualizeLauncher.generateMethodCFG(inputFile, method, clazz, backwardAnalysis);
CFGVisualizeLauncher.writeStringOfCFG(cfg, outputFile, backwardAnalysis);
// The .dot and .pdf files are not tested, only created for debugging convenience.
CFGVisualizeLauncher.generateDOTofCFG(cfg, ".", true, true, backwardAnalysis);
}
Comment on lines +32 to 37
Copy link
Contributor

Choose a reason for hiding this comment

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

⚠️ Potential issue

Don’t require Graphviz in tests; avoid System.exit(1) on missing ‘dot’

generateDOTofCFG(..., pdf=true, ...) invokes ‘dot’ and System.exit(1) on failure, which can break CI. Generate DOT only (pdf=false) or guard behind an env flag.

-    CFGVisualizeLauncher.generateDOTofCFG(cfg, ".", true, true, backwardAnalysis);
+    // Generate DOT only to avoid external Graphviz dependency in tests.
+    CFGVisualizeLauncher.generateDOTofCFG(cfg, ".", false, true, backwardAnalysis);
📝 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
ControlFlowGraph cfg =
CFGVisualizeLauncher.generateMethodCFG(inputFile, method, clazz, backwardAnalysis);
CFGVisualizeLauncher.writeStringOfCFG(cfg, outputFile, backwardAnalysis);
// The .dot and .pdf files are not tested, only created for debugging convenience.
CFGVisualizeLauncher.generateDOTofCFG(cfg, ".", true, true, backwardAnalysis);
}
ControlFlowGraph cfg =
CFGVisualizeLauncher.generateMethodCFG(inputFile, method, clazz, backwardAnalysis);
CFGVisualizeLauncher.writeStringOfCFG(cfg, outputFile, backwardAnalysis);
// The .dot and .pdf files are not tested, only created for debugging convenience.
// Generate DOT only to avoid external Graphviz dependency in tests.
CFGVisualizeLauncher.generateDOTofCFG(cfg, ".", false, true, backwardAnalysis);
}
🤖 Prompt for AI Agents 
In dataflow/src/test/java/busyexpr/BusyExpression.java around lines 32 to 37,
the test invokes CFGVisualizeLauncher.generateDOTofCFG(cfg, ".", true, true,
backwardAnalysis) which asks Graphviz to produce a PDF and can call
System.exit(1) if ‘dot’ is missing; this can break CI. Change the test to only
generate the DOT by passing pdf=false (e.g. generateDOTofCFG(cfg, ".", true,
false, backwardAnalysis)) or wrap the call behind an environment flag (e.g. only
call when System.getenv("GENERATE_CFG_PDF") is set) so CI runs won’t invoke
Graphviz; do not modify library behavior here, just prevent the test from
forcing PDF generation or exiting the JVM.

}
Loading