Skip to content

Java: Fix assert CFG by properly tagging the false successor.#19883

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

Merged
aschackmull merged 3 commits into from
Jun 26, 2025
Merged

Java: Fix assert CFG by properly tagging the false successor. #19883

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1d4c819
Java: Fix assert CFG by properly tagging the false successor.
aschackmull Jun 17, 2025
326f2b0
Java: Accept qltest change showing FP removal.
aschackmull Jun 26, 2025
c091fc5
Java: Account for AssertionError possibly not being extracted.
aschackmull Jun 26, 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
51 changes: 42 additions & 9 deletions java/ql/lib/semmle/code/java/ControlFlowGraph.qll
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -100,7 +100,8 @@ module ControlFlow {
private newtype TNode =
TExprNode(Expr e) { hasControlFlow(e) } or
TStmtNode(Stmt s) or
TExitNode(Callable c) { exists(c.getBody()) }
TExitNode(Callable c) { exists(c.getBody()) } or
TAssertThrowNode(AssertStmt s)

/** A node in the expression-level control-flow graph. */
class Node extends TNode {
Expand DownExpand Up@@ -204,6 +205,25 @@ module ControlFlow {
/** Gets the source location for this element. */
override Location getLocation() { result = c.getLocation() }
}

/** A control flow node indicating a failing assertion. */
class AssertThrowNode extends Node, TAssertThrowNode {
AssertStmt s;

AssertThrowNode() { this = TAssertThrowNode(s) }

override Stmt getEnclosingStmt() { result = s }

override Callable getEnclosingCallable() { result = s.getEnclosingCallable() }

override ExprParent getAstNode() { result = s }

/** Gets a textual representation of this element. */
override string toString() { result = "Assert Throw" }

/** Gets the source location for this element. */
override Location getLocation() { result = s.getLocation() }
}
}

class ControlFlowNode = ControlFlow::Node;
Expand DownExpand Up@@ -327,7 +347,17 @@ private module ControlFlowGraphImpl {
)
}

private ThrowableType assertionError() { result.hasQualifiedName("java.lang", "AssertionError") }
private ThrowableType actualAssertionError() {
result.hasQualifiedName("java.lang", "AssertionError")
}

private ThrowableType assertionError() {
result = actualAssertionError()
or
// In case `AssertionError` is not extracted, we use `Error` as a fallback.
not exists(actualAssertionError()) and
result.hasQualifiedName("java.lang", "Error")
}

/**
* Gets an exception type that may be thrown during execution of the
Expand DownExpand Up@@ -1123,12 +1153,7 @@ private module ControlFlowGraphImpl {
or
// `assert` statements may throw
completion = ThrowCompletion(assertionError()) and
(
last(assertstmt.getMessage(), last, NormalCompletion())
or
not exists(assertstmt.getMessage()) and
last(assertstmt.getExpr(), last, BooleanCompletion(false, _))
)
last.(AssertThrowNode).getAstNode() = assertstmt
Comment thread
aschackmull marked this conversation as resolved.
)
or
// `throw` statements or throwing calls give rise to `Throw` completion
Expand DownExpand Up@@ -1547,7 +1572,15 @@ private module ControlFlowGraphImpl {
or
last(assertstmt.getExpr(), n, completion) and
completion = BooleanCompletion(false, _) and
result = first(assertstmt.getMessage())
(
result = first(assertstmt.getMessage())
or
not exists(assertstmt.getMessage()) and
result.(AssertThrowNode).getAstNode() = assertstmt
)
or
last(assertstmt.getMessage(), n, NormalCompletion()) and
result.(AssertThrowNode).getAstNode() = assertstmt
)
Comment thread
aschackmull marked this conversation as resolved.
or
// When expressions:
Expand Down
2 changes: 1 addition & 1 deletion java/ql/test/query-tests/Nullness/C.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -251,7 +251,7 @@ public void ex18(boolean b, int[] xs, Object related) {
(b && xs == null && related == null);
if (b) {
if (related == null) { return; }
xs[0] = 42; // FP - correlated conditions fails to recognize assert edges
xs[0] = 42; // OK
}
}
}
3 changes: 0 additions & 3 deletions java/ql/test/query-tests/Nullness/NullMaybe.expected
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -32,9 +32,6 @@
| C.java:207:9:207:11 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:201:5:201:22 | Object obj | obj | C.java:201:12:201:21 | obj | this |
| C.java:219:9:219:10 | o1 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:212:20:212:28 | o1 | o1 | C.java:213:9:213:18 | ... == ... | this |
| C.java:233:7:233:8 | xs | Variable $@ may be null at this access because of $@ assignment. | C.java:231:5:231:56 | int[] xs | xs | C.java:231:11:231:55 | xs | this |
| C.java:254:7:254:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:248:31:248:38 | xs | xs | C.java:249:19:249:28 | ... == ... | this |
| C.java:254:7:254:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:248:31:248:38 | xs | xs | C.java:250:18:250:27 | ... != ... | this |
| C.java:254:7:254:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:248:31:248:38 | xs | xs | C.java:251:18:251:27 | ... == ... | this |
| F.java:11:5:11:7 | obj | Variable $@ may be null at this access as suggested by $@ null guard. | F.java:8:18:8:27 | obj | obj | F.java:9:9:9:19 | ... == ... | this |
| F.java:17:5:17:7 | obj | Variable $@ may be null at this access as suggested by $@ null guard. | F.java:14:18:14:27 | obj | obj | F.java:15:9:15:19 | ... == ... | this |
| G.java:20:12:20:12 | s | Variable $@ may be null at this access as suggested by $@ null guard. | G.java:3:27:3:34 | s | s | G.java:5:9:5:17 | ... == ... | this |
2 changes: 1 addition & 1 deletion java/ql/test/query-tests/RangeAnalysis/A.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -64,7 +64,7 @@ void m4(int[] a, int[] b) {
int sum = 0;
for (int i = 0; i < a.length; ) {
sum += a[i++]; // OK
sum += a[i++]; // OK - FP
sum += a[i++]; // OK
}
int len = b.length;
if ((len & 1) != 0)
Expand Down
1 change: 0 additions & 1 deletion java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -3,7 +3,6 @@
| A.java:45:14:45:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:49:14:49:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:58:14:58:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:67:14:67:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:89:12:89:16 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:100:18:100:31 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 8. |
| A.java:113:14:113:21 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
Expand Down