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
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 1 commit
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
39 changes: 31 additions & 8 deletions java/ql/lib/semmle/code/java/ControlFlowGraph.qll
View file
Open in desktop
Original file line number Diff line number Diff 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 Down Expand 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 Down Expand Up @@ -1123,12 +1143,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
)
or
// `throw` statements or throwing calls give rise to `Throw` completion
Expand Down Expand Up @@ -1547,7 +1562,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
)
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 number Diff line number Diff 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 number Diff line number Diff 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 |