-
Notifications
You must be signed in to change notification settings - Fork 439
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.
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
base: master
Are you sure you want to change the base?
Call extend only once
#7234
Changes from 26 commits
87359b2
9e4b90b
df55f80
b68c5e5
f949caa
c1b8a49
95eaa3c
d021484
daf0d3f
4a19961
9845c39
f09e2d6
4c0104a
9ea4ca0
8f2b457
842c823
2a5935a
b1e57a3
d19a35f
0dc71fe
bee06df
b43f8b9
bedba2e
89a03dc
972d398
afe3aad
a9748ea
eba9d48
bf2a052
8352eb6
9c8b23f
f2f456a
1629777
3c73cd7
1a0a25e
32d7463
94c7c4a
1252419
396a774
0dde2f2
6212920
c2a78c3
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -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; | ||||||||||||||||||||||||
|
|
@@ -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); | ||||||||||||||||||||||||
|
|
@@ -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); | ||||||||||||||||||||||||
| } | ||||||||||||||||||||||||
|
|
@@ -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); | ||||||||||||||||||||||||
| } | ||||||||||||||||||||||||
|
|
@@ -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); | ||||||||||||||||||||||||
|
|
||||||||||||||||||||||||
|
||||||||||||||||||||||||
| 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.
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -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
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 |
||||||||||||||||||||||||||||
| 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
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 |
||||||||||||||||||||||||||||
| 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
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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
Suggested change
🤖 Prompt for AI Agents |
||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||
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.
🧹 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.
📝 Committable suggestion
🤖 Prompt for AI Agents