Merge pull request #19883 from aschackmull/java/fix-assert-cfg

Java: Fix assert CFG by properly tagging the false successor.
This commit is contained in:
Anders Schack-Mulligen
2025-06-26 11:43:27 +02:00
committed by GitHub
5 changed files with 44 additions and 15 deletions

View File

@@ -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 {
@@ -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;
@@ -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
@@ -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
)
or
// `throw` statements or throwing calls give rise to `Throw` completion
@@ -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
)
or
// When expressions:

View File

@@ -251,7 +251,7 @@ public class C {
(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
}
}
}

View File

@@ -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 |

View File

@@ -64,7 +64,7 @@ public class A {
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)

View File

@@ -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. |