Java: Update the CFG for assert statements to make them proper guards.

[aschackmull]

This upgrades the CFG for Java assert statements to be proper guards and includes the message part, which was previously a CFG orphan, in the CFG. That is, the false edge of the condition now leads to an exception edge rather than simply ignoring the value.
For things like nullness, this is definitely what we want, and in general it's probably fine to assume that asserts are evaluated (even though they technically can be disabled).

[Copilot]

Pull Request Overview

This PR refines how Java assert statements are represented in the control‐flow graph, treating them as true guards and incorporating the optional message expression into the flow.

• Expanded the assertion framework predicates to include AssertStmt nodes.
• Removed direct handling of AssertStmt in nullness flow in favor of the updated CFG.
• Enhanced ControlFlowGraph.qll to generate throw and normal edges for asserts, update boolean contexts, and record thrown types.

Reviewed Changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
java/ql/lib/semmle/code/java/frameworks/Assertions.qll	Added AssertStmt cases to the assert‐failure guard
java/ql/lib/semmle/code/java/dataflow/Nullness.qll	Removed direct AssertStmt null‐guard branch
java/ql/lib/semmle/code/java/ControlFlowGraph.qll	Integrated assert into CFG edges and completions
java/ql/lib/change-notes/2025-06-12-assert-cfg.md	Documented CFG change for assert analysis

Comments suppressed due to low confidence (2)

java/ql/lib/semmle/code/java/dataflow/Nullness.qll:143

• Removing the direct AssertStmt null‐guard branch may break nullness inference for plain assert statements. Ensure that the new CFG paths fully cover this case or reintroduce null‐guard logic for AssertStmt.

result.asStmt().(AssertStmt).getExpr() = nullGuard(v, true, false)

java/ql/lib/semmle/code/java/ControlFlowGraph.qll:1119

• It would be beneficial to add unit tests that verify both normal and exceptional CFG edges for assert statements (with and without messages), to ensure the new logic behaves as expected.

exists(AssertStmt assertstmt | assertstmt = n |

[aschackmull]

I've spot-checked a bunch of the changed results. The removed results were FPs, and the new results were typically redundant checks - e.g. both asserting a condition and then also checking it in an if statement.

[hvitved]

One suggestion, otherwise LGTM.

[intrigus-lgtm]

in general it's probably fine to assume that asserts are evaluated (even though they technically can be disabled).

Isn't it the other way around in Java?
Assertions can be enabled if needed, but are disabled by default?

[aschackmull]

in general it's probably fine to assume that asserts are evaluated (even though they technically can be disabled).

Isn't it the other way around in Java? Assertions can be enabled if needed, but are disabled by default?

Right, so my parenthesized remark ought to have been worded slightly different. Nevertheless, for the purpose of bug-finding, assuming that assertions succeed (which is what we get by unconditionally including them in the CFG) gives us good information about non-local invariants and helps us avoid reporting FPs.