From b3bb71f2e2952267c12c3b3d87bed9522c9cc5af Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 11 Jun 2025 15:38:29 +0200 Subject: [PATCH 1/4] Java: Update the CFG for assert statements to make them proper guards. --- .../lib/semmle/code/java/ControlFlowGraph.qll | 49 ++++++++++++++----- 1 file changed, 38 insertions(+), 11 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll index e3c7ed6e5d9e..476c72bc0e0d 100644 --- a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll +++ b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll @@ -327,12 +327,18 @@ private module ControlFlowGraphImpl { ) } + private ThrowableType assertionError() { result.hasQualifiedName("java.lang", "AssertionError") } + /** * Gets an exception type that may be thrown during execution of the * body or the resources (if any) of `try`. */ private ThrowableType thrownInBody(TryStmt try) { - exists(AstNode n | mayThrow(n, result) | + exists(AstNode n | + mayThrow(n, result) + or + n instanceof AssertStmt and result = assertionError() + | n.getEnclosingStmt().getEnclosingStmt+() = try.getBlock() or n.(Expr).getParent*() = try.getAResource() ) @@ -394,10 +400,7 @@ private module ControlFlowGraphImpl { exists(LogicExpr logexpr | logexpr.(BinaryExpr).getLeftOperand() = b or - // Cannot use LogicExpr.getAnOperand or BinaryExpr.getAnOperand as they remove parentheses. - logexpr.(BinaryExpr).getRightOperand() = b and inBooleanContext(logexpr) - or - logexpr.(UnaryExpr).getExpr() = b and inBooleanContext(logexpr) + logexpr.getAnOperand() = b and inBooleanContext(logexpr) ) or exists(ConditionalExpr condexpr | @@ -407,6 +410,8 @@ private module ControlFlowGraphImpl { inBooleanContext(condexpr) ) or + exists(AssertStmt assertstmt | assertstmt.getExpr() = b) + or exists(SwitchExpr switch | inBooleanContext(switch) and switch.getAResult() = b @@ -672,8 +677,6 @@ private module ControlFlowGraphImpl { this instanceof EmptyStmt or this instanceof LocalTypeDeclStmt - or - this instanceof AssertStmt } /** Gets child nodes in their order of execution. Indexing starts at either -1 or 0. */ @@ -744,8 +747,6 @@ private module ControlFlowGraphImpl { or index = 0 and result = this.(ThrowStmt).getExpr() or - index = 0 and result = this.(AssertStmt).getExpr() - or result = this.(RecordPatternExpr).getSubPattern(index) } @@ -807,9 +808,12 @@ private module ControlFlowGraphImpl { or result = first(n.(SynchronizedStmt).getExpr()) or + result = first(n.(AssertStmt).getExpr()) + or result.asStmt() = n and not n instanceof PostOrderNode and - not n instanceof SynchronizedStmt + not n instanceof SynchronizedStmt and + not n instanceof AssertStmt or result.asExpr() = n and n instanceof SwitchExpr } @@ -1112,7 +1116,19 @@ private module ControlFlowGraphImpl { // `return` statements give rise to a `Return` completion last.asStmt() = n.(ReturnStmt) and completion = ReturnCompletion() or - // `throw` statements or throwing calls give rise to ` Throw` completion + exists(AssertStmt assertstmt | assertstmt = n | + // `assert` statements may complete normally - we use the `AssertStmt` itself + // to represent this outcome + last.asStmt() = assertstmt and completion = NormalCompletion() + or + // `assert` statements may throw + completion = ThrowCompletion(assertionError()) and + if exists(assertstmt.getMessage()) + then last(assertstmt.getMessage(), last, NormalCompletion()) + else last(assertstmt.getExpr(), last, BooleanCompletion(false, _)) + ) + or + // `throw` statements or throwing calls give rise to `Throw` completion exists(ThrowableType tt | mayThrow(n, tt) | last = n.getCfgNode() and completion = ThrowCompletion(tt) ) @@ -1520,6 +1536,17 @@ private module ControlFlowGraphImpl { exists(int i | last(s.getVariable(i), n, completion) and result = first(s.getVariable(i + 1))) ) or + // Assert statements: + exists(AssertStmt assertstmt | + last(assertstmt.getExpr(), n, completion) and + completion = BooleanCompletion(true, _) and + result.asStmt() = assertstmt + or + last(assertstmt.getExpr(), n, completion) and + completion = BooleanCompletion(false, _) and + result = first(assertstmt.getMessage()) + ) + or // When expressions: exists(WhenExpr whenexpr | n.asExpr() = whenexpr and From f27e310ba3f4b58c17e904928f2a5ee7aaeb3eee Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 11 Jun 2025 15:53:02 +0200 Subject: [PATCH 2/4] Java: Adjust references. --- java/ql/lib/semmle/code/java/dataflow/Nullness.qll | 2 -- .../lib/semmle/code/java/frameworks/Assertions.qll | 14 ++++++++++---- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll index 786207d34865..36ad96c497f0 100644 --- a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll +++ b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll @@ -141,8 +141,6 @@ private ControlFlowNode varDereference(SsaVariable v, VarAccess va) { private ControlFlowNode ensureNotNull(SsaVariable v) { result = varDereference(v, _) or - result.asStmt().(AssertStmt).getExpr() = nullGuard(v, true, false) - or exists(AssertTrueMethod m | result.asCall() = m.getACheck(nullGuard(v, true, false))) or exists(AssertFalseMethod m | result.asCall() = m.getACheck(nullGuard(v, false, false))) diff --git a/java/ql/lib/semmle/code/java/frameworks/Assertions.qll b/java/ql/lib/semmle/code/java/frameworks/Assertions.qll index e7f86b9bfd81..e1601c854e4e 100644 --- a/java/ql/lib/semmle/code/java/frameworks/Assertions.qll +++ b/java/ql/lib/semmle/code/java/frameworks/Assertions.qll @@ -110,11 +110,17 @@ predicate assertFail(BasicBlock bb, ControlFlowNode n) { ( exists(AssertTrueMethod m | n.asExpr() = m.getACheck(any(BooleanLiteral b | b.getBooleanValue() = false)) - ) or + ) + or exists(AssertFalseMethod m | n.asExpr() = m.getACheck(any(BooleanLiteral b | b.getBooleanValue() = true)) - ) or - exists(AssertFailMethod m | n.asExpr() = m.getACheck()) or - n.asStmt().(AssertStmt).getExpr().(BooleanLiteral).getBooleanValue() = false + ) + or + exists(AssertFailMethod m | n.asExpr() = m.getACheck()) + or + exists(AssertStmt a | + n.asExpr() = a.getExpr() and + a.getExpr().(BooleanLiteral).getBooleanValue() = false + ) ) } From d0d47808e94fc404f254be1030a5004492b45180 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 12 Jun 2025 11:03:49 +0200 Subject: [PATCH 3/4] Java: Add change note. --- java/ql/lib/change-notes/2025-06-12-assert-cfg.md | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 java/ql/lib/change-notes/2025-06-12-assert-cfg.md diff --git a/java/ql/lib/change-notes/2025-06-12-assert-cfg.md b/java/ql/lib/change-notes/2025-06-12-assert-cfg.md new file mode 100644 index 000000000000..69219633166e --- /dev/null +++ b/java/ql/lib/change-notes/2025-06-12-assert-cfg.md @@ -0,0 +1,4 @@ +--- +category: minorAnalysis +--- +* Java `assert` statements are now assumed to be executed for the purpose of analysing control flow. This improves precision for a number of queries. From 6131c680f622f7b91b939d0a47d2591c10698d3c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 13 Jun 2025 14:07:46 +0200 Subject: [PATCH 4/4] Update java/ql/lib/semmle/code/java/ControlFlowGraph.qll Co-authored-by: Tom Hvitved --- java/ql/lib/semmle/code/java/ControlFlowGraph.qll | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll index 476c72bc0e0d..0d9d685cc716 100644 --- a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll +++ b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll @@ -1123,9 +1123,12 @@ private module ControlFlowGraphImpl { or // `assert` statements may throw completion = ThrowCompletion(assertionError()) and - if exists(assertstmt.getMessage()) - then last(assertstmt.getMessage(), last, NormalCompletion()) - else last(assertstmt.getExpr(), last, BooleanCompletion(false, _)) + ( + last(assertstmt.getMessage(), last, NormalCompletion()) + or + not exists(assertstmt.getMessage()) and + last(assertstmt.getExpr(), last, BooleanCompletion(false, _)) + ) ) or // `throw` statements or throwing calls give rise to `Throw` completion