Shared/Java: Add shared Guards library and switch Java to use it. by aschackmull · Pull Request #19573 · github/codeql

aschackmull · 2025-05-23T13:45:53Z

This adds a new shared Guards library, which provides complex implication logic between guards. The implementation is heavily inspired by the corresponding Java and C# versions.
The Java Guards library is then switched to use this new library, which results in a number of precision improvements for the nullness and useless comparison test queries.

There's currently a known FP related to correlated conditions in assert statements that I've documented as a qltest. I plan to fix that in a follow-up PR.

Review of the shared implementation (the single file shared/controlflow/codeql/controlflow/Guards.qll) is likely best done by reading the final result, but the other changes can be reviewed commit-by-commit.

+}
+
+private module LogicInput_v2 implements GuardsImpl::LogicInputSig {
+ private import semmle.code.java.dataflow.SSA as SSA


hvitved

Looks really good, great to finally have a shared guards library 🎉

hvitved · 2025-06-24T08:25:52Z

+ * controls the basic block `A`, in this case because the true branch dominates
+ * `A`, but more elaborate controls-relationships may also hold.
+ * For example, in
+ * ```


nit: add java after bacticks

hvitved · 2025-06-24T08:30:20Z

+ predicate strictlyDominates(BasicBlock bb);
+ }
+
+ predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2);


Perhaps add QL doc describing how this differs from bb1.strictlyDominates(bb2)?

Copied qldoc from the shared BasicBlocks lib.

hvitved · 2025-06-24T11:11:55Z

+ /** Gets the integer that this value represents, if any. */
+ int asIntValue() { this = TValue(TValueInt(result), true) }
+
+ /** Gets the boolean that this value represents, if any. */


nit: Boolean

Why? We write e.g. "integer" with lowercase. It's not really referring to a specific class or anything, it's just the English language meaning of "boolean", right? And the ql type that's being returned is also the lowercased boolean.

I misread it as an adjective instead of a noun.

hvitved · 2025-06-24T11:30:49Z

+ v1.asBooleanValue() = true and
+ g2.(Case).getSwitchExpr() = switchExpr and
+ v2.asBooleanValue() = false and
+ g1 != g2


Would it make sense to generalize to say: if g1, v1 represents matching case i, then g2, v2 represents non-matching any case j < i?

On second thought, why is this implication even needed? I would have thought that dominance came for free from the CFG?

The implication is needed if the CFG uses a jump-table interpretation (which Java mostly does), because then non-matching a case isn't represented in a specific edge. And it's only the default case that tends to be relevant, since knowing e.g. not "foo" when you already know "bar" in case "foo": .. case "bar": .. tends to be pointless.

hvitved · 2025-06-24T11:36:58Z

+ }
+
+ class SsaWriteDefinition extends SsaDefinition {
+ Expr getDefinition();


Perhaps just move this into SsaDefinition and then get rid of SsaWriteDefinition?

I'm trying to reflect the shared SSA api as much as possible here. Hence this choice.

hvitved · 2025-06-24T12:19:35Z

+ * starting from a given set of base cases.
+ */
+ cached
+ module ImpliesTC<baseGuardValueSig/2 baseGuardValue> {


hvitved · 2025-06-25T07:25:00Z

+ * control flow. It may also be a switch case, which as a guard is considered
+ * to evaluate to either true or false depending on whether the case matches.
+ */
+ final class Guard extends PreGuard {


Should this class have a charpred to restrict it somehow?

That's a good question and indeed a subtle change from the language-specific guards libraries. I think we can do it with guardControlsBranchEdge(this, _, _, _) if we change a bunch of Guard references to PreGuard. Again, this is something that would merit a dca rerun, so I'd like to investigate this option as a follow-up.

OTOH, I'm not sure that it would actually achieve much, but I do agree that it would make more sense to have it.

hvitved · 2025-06-25T07:32:29Z

+ predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos);
+
+ /** A non-overridable method with a boolean return value. */
+ class BooleanMethod {


Could all of this logic be generalized to methods that return constant values? E.g. like a Compare method that typically returns -1, 0, or 1?

I want to generalise it to at least null/not-null and exception/no-exception. But something based around such integers might make sense as well. I'm already working on a follow-up branch that touches on this.

hvitved · 2025-06-25T07:51:09Z

+ * wrappers. This can be used to instantiate the `additionalImpliesStep`
+ * predicate.
+ */
+ module CustomGuard<CustomGuardInputSig CustomGuardInput> {


I think something like WrapperGuard would be a better name.
As we discussed offline, it might be better to remove the nesting of parameterized modules; I'll let you decide (perhaps follow-up).

Already looking at this in a follow-up branch.

hvitved · 2025-06-25T07:57:19Z

+
+ class BasicBlock = J::BasicBlock;
+
+ predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }


I'm surprised that dominatingEdge is exposed directly from the java.qll module.

Yeah, something to maybe fix in the glorious future. Historically the contents of Dominance.qll have been exposed by default for Java.

+ * with logical implications based on SSA.
+ */
+ module Logic<LogicInputSig LogicInput> {
+ private import LogicInput


…ons.

…pers.

…ranch points.

… on SSA.

github-actionsBot added C# C++ Java labels May 23, 2025

github-advanced-securityAI found potential problems May 23, 2025
View reviewed changes

aschackmull force-pushed the guardslib branch from cdd8231 to 3350c76Compare May 26, 2025 14:17

github-actionsBot removed C# C++ labels May 26, 2025

aschackmull force-pushed the guardslib branch 2 times, most recently from 969365f to 4abca27Compare May 27, 2025 06:50

aschackmull force-pushed the guardslib branch 3 times, most recently from f4e0076 to ed640abCompare June 17, 2025 11:49

github-actionsBot added the documentation label Jun 17, 2025

aschackmull marked this pull request as ready for review June 17, 2025 12:05

aschackmull requested a review from a team as a code owner June 17, 2025 12:05

aschackmull requested a review from hvitved June 17, 2025 12:06

hvitved reviewed Jun 25, 2025
View reviewed changes

github-advanced-securityAI found potential problems Jun 25, 2025
View reviewed changes

aschackmull force-pushed the guardslib branch from ad21050 to e5f66e3Compare June 25, 2025 14:33

hvitved approved these changes Jun 25, 2025
View reviewed changes

aschackmull added 10 commits June 26, 2025 07:17

Java: Add guards-logic qltest with inline expectation.
a0c8491

Java: Add hasInputFromBlock predicate in BaseSSA.
994c1f6

Shared: Add a shared Guards library inspired by the Java and C# versi…
1d75008
…ons.

Shared: Extend the shared Guards library with support for custom wrap…
14b87f9
…pers.

Shared: Extend the shared Guards library with support for exception b…
16c5b57
…ranch points.

Shared: Improve shared guards lib.
c212d0a

Shared: Many tweaks to Guards.
73ae613

Shared: Elaborate qldoc.
f772493

Shared: Switch case guards to be the case statements.
b19bff9

Shared: Simplify and improve joins.
378209a

aschackmull added 12 commits June 26, 2025 07:17

Shared: Bugfix for unique value implication.
22d5dc9

Java: Refactor clearlyNotNullExpr into a base case that does not rely…
a2778ee
… on SSA.

Java: Refactor integerGuard.
0607fef

Java: Replace some references to basicNullGuard.
cc13193

Java: Switch to the shared Guards library.
5c0dcd9

Java: Fix qltests
42b1b12

Java: Fix perf issue.
d4c897f

Shared: Try caching.
5a34a1a

Java: Fix perf issue.
73810a6

Java: document FP
4645856

Java: Add change note.
5ddddae

Shared: address review comments.
6f4adb8

aschackmull force-pushed the guardslib branch from e5f66e3 to 6f4adb8Compare June 26, 2025 05:17

aschackmull merged commit 4d2c678 into github:mainJun 26, 2025

aschackmull deleted the guardslib branch June 26, 2025 07:28

aschackmull mentioned this pull request Jun 26, 2025
Java: Fix assert CFG by properly tagging the false successor. #19883
Merged

This was referenced Sep 18, 2025
C++: Switch to the shared Guards library #20485
Merged
PS: Add ZipSlip query microsoft/codeql#287
Merged


		class BasicBlock = J::BasicBlock;

		predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }

Uh oh!

Conversation

aschackmull commented May 23, 2025• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Check warning

Uh oh!

Uh oh!

hvitved left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Check warning

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

aschackmull commented May 23, 2025•
edited
Loading