From 1d4c8197ec0f082645ec42f3dfc8a9777086958a Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Tue, 17 Jun 2025 14:43:45 +0200
Subject: [PATCH] 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 0d9d685cc71..9ef33fe83c2 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 eccf6382c15..d195eea6acb 100644
--- a/java/ql/test/query-tests/Nullness/C.java
+++ b/java/ql/test/query-tests/Nullness/C.java
@@ -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
     }
   }
 }
diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected
index a65d1f643c1..a19fae57e74 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 |