From 1d4c8197ec0f082645ec42f3dfc8a9777086958a Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 17 Jun 2025 14:43:45 +0200 Subject: [PATCH 1/3] Java: Fix assert CFG by properly tagging the false successor. --- .../lib/semmle/code/java/ControlFlowGraph.qll | 39 +++++++++++++++---- java/ql/test/query-tests/Nullness/C.java | 2 +- .../query-tests/Nullness/NullMaybe.expected | 3 -- 3 files changed, 32 insertions(+), 12 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll index 0d9d685cc716..9ef33fe83c26 100644 --- a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll +++ b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll @@ -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; @@ -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 @@ -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: diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index eccf6382c156..d195eea6acb3 100644 --- a/java/ql/test/query-tests/Nullness/C.java +++ b/java/ql/test/query-tests/Nullness/C.java @@ -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 } } } diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected index a65d1f643c11..a19fae57e74e 100644 --- a/java/ql/test/query-tests/Nullness/NullMaybe.expected +++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected @@ -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 | From 326f2b049873ff5cd6062eae168fc2eea24edb97 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 26 Jun 2025 11:03:39 +0200 Subject: [PATCH 2/3] Java: Accept qltest change showing FP removal. --- java/ql/test/query-tests/RangeAnalysis/A.java | 2 +- .../query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/java/ql/test/query-tests/RangeAnalysis/A.java b/java/ql/test/query-tests/RangeAnalysis/A.java index 4fd1b87bb708..b68de9beaa7c 100644 --- a/java/ql/test/query-tests/RangeAnalysis/A.java +++ b/java/ql/test/query-tests/RangeAnalysis/A.java @@ -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) diff --git a/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected index dc0b87d68b25..92099db01cbd 100644 --- a/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected +++ b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected @@ -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. | From c091fc585bc18b47d980b515c14039813809dcaa Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 26 Jun 2025 11:03:59 +0200 Subject: [PATCH 3/3] Java: Account for AssertionError possibly not being extracted. --- java/ql/lib/semmle/code/java/ControlFlowGraph.qll | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll index 9ef33fe83c26..5ffb37b585f8 100644 --- a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll +++ b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll @@ -347,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