Skip to content

Guards: Support disjunctive implications. #20826

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Nov 14, 2025
Merged

Guards: Support disjunctive implications. #20826

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2192d75
Java: Add test for a known FP.
aschackmull Nov 12, 2025
d680039
Guards: Support disjunctive implications.
aschackmull Nov 12, 2025
dc029e8
C#: Accept qltest weirdness.
aschackmull Nov 14, 2025
4867306
C#: Add change note.
aschackmull Nov 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions csharp/ql/src/change-notes/2025-11-14-guards-disjunctive.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
---
category: minorAnalysis
---
* An improvement to the Guards library for recognizing disjunctions means improved precision for `cs/constant-condition`, `cs/inefficient-containskey`, and `cs/dereferenced-value-may-be-null`. The two former can have additional findings, and the latter will have fewer false positives.
4 changes: 4 additions & 0 deletions csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,12 @@
| Guards.cs:36:32:36:32 | access to parameter x | Guards.cs:35:13:35:21 | ... == ... | Guards.cs:35:13:35:13 | access to parameter x | false |
| Guards.cs:36:36:36:36 | access to parameter y | Guards.cs:35:26:35:34 | ... == ... | Guards.cs:35:26:35:26 | access to parameter y | false |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:23 | ... == ... | Guards.cs:38:15:38:15 | access to parameter x | false |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:23 | ... == ... | Guards.cs:38:15:38:15 | access to parameter x | true |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:36 | ... == ... | Guards.cs:38:28:38:28 | access to parameter y | false |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:36 | ... == ... | Guards.cs:38:28:38:28 | access to parameter y | true |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:25 | ... != ... | Guards.cs:41:17:41:17 | access to parameter x | false |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:25 | ... != ... | Guards.cs:41:17:41:17 | access to parameter x | true |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:38 | ... != ... | Guards.cs:41:30:41:30 | access to parameter y | false |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:38 | ... != ... | Guards.cs:41:30:41:30 | access to parameter y | true |
| Guards.cs:48:31:48:40 | access to field Field | Guards.cs:47:13:47:25 | ... != ... | Guards.cs:47:13:47:17 | access to field Field | true |
| Guards.cs:55:27:55:27 | access to parameter g | Guards.cs:53:13:53:27 | ... == ... | Guards.cs:53:13:53:13 | access to parameter g | false |
Expand Down
8 changes: 8 additions & 0 deletions csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,20 @@
| Guards.cs:36:36:36:36 | access to parameter y | Guards.cs:35:26:35:26 | access to parameter y | Guards.cs:35:26:35:26 | access to parameter y | not null |
| Guards.cs:36:36:36:36 | access to parameter y | Guards.cs:35:26:35:34 | ... == ... | Guards.cs:35:26:35:26 | access to parameter y | false |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | not null |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | null |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:23 | ... == ... | Guards.cs:38:15:38:15 | access to parameter x | false |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:23 | ... == ... | Guards.cs:38:15:38:15 | access to parameter x | true |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | not null |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | null |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:36 | ... == ... | Guards.cs:38:28:38:28 | access to parameter y | false |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:36 | ... == ... | Guards.cs:38:28:38:28 | access to parameter y | true |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | not null |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | null |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:25 | ... != ... | Guards.cs:41:17:41:17 | access to parameter x | false |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:25 | ... != ... | Guards.cs:41:17:41:17 | access to parameter x | true |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | not null |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | null |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:38 | ... != ... | Guards.cs:41:30:41:30 | access to parameter y | false |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:38 | ... != ... | Guards.cs:41:30:41:30 | access to parameter y | true |
| Guards.cs:48:31:48:40 | access to field Field | Guards.cs:47:13:47:17 | access to field Field | Guards.cs:47:13:47:17 | access to field Field | not null |
| Guards.cs:48:31:48:40 | access to field Field | Guards.cs:47:13:47:25 | ... != ... | Guards.cs:47:13:47:17 | access to field Field | true |
Expand Down
8 changes: 8 additions & 0 deletions csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,20 @@
| Guards.cs:36:36:36:36 | access to parameter y | Guards.cs:35:26:35:26 | access to parameter y | Guards.cs:35:26:35:26 | access to parameter y | not null |
| Guards.cs:36:36:36:36 | access to parameter y | Guards.cs:35:26:35:34 | ... == ... | Guards.cs:35:26:35:26 | access to parameter y | false |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | not null |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | Guards.cs:38:15:38:15 | access to parameter x | null |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:23 | ... == ... | Guards.cs:38:15:38:15 | access to parameter x | false |
| Guards.cs:39:31:39:31 | access to parameter x | Guards.cs:38:15:38:23 | ... == ... | Guards.cs:38:15:38:15 | access to parameter x | true |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | not null |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | Guards.cs:38:28:38:28 | access to parameter y | null |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:36 | ... == ... | Guards.cs:38:28:38:28 | access to parameter y | false |
| Guards.cs:39:35:39:35 | access to parameter y | Guards.cs:38:28:38:36 | ... == ... | Guards.cs:38:28:38:28 | access to parameter y | true |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | not null |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | Guards.cs:41:17:41:17 | access to parameter x | null |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:25 | ... != ... | Guards.cs:41:17:41:17 | access to parameter x | false |
| Guards.cs:42:32:42:32 | access to parameter x | Guards.cs:41:17:41:25 | ... != ... | Guards.cs:41:17:41:17 | access to parameter x | true |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | not null |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | Guards.cs:41:30:41:30 | access to parameter y | null |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:38 | ... != ... | Guards.cs:41:30:41:30 | access to parameter y | false |
| Guards.cs:42:36:42:36 | access to parameter y | Guards.cs:41:30:41:38 | ... != ... | Guards.cs:41:30:41:30 | access to parameter y | true |
| Guards.cs:48:31:48:40 | access to field Field | Guards.cs:47:13:47:17 | access to field Field | Guards.cs:47:13:47:17 | access to field Field | not null |
| Guards.cs:48:31:48:40 | access to field Field | Guards.cs:47:13:47:25 | ... != ... | Guards.cs:47:13:47:17 | access to field Field | true |
Expand Down
4 changes: 2 additions & 2 deletions csharp/ql/test/library-tests/controlflow/guards/Guards.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,10 @@ void M3(string? x, string? y)
if (x == null || y == null) { }
else Console.WriteLine(x + y); // null guarded

if (!(x == null || y == null))
if (!(x == null || y == null)) // MISHANDLED, likely due to splitting
Console.WriteLine(x + y); // null guarded

if (!!!(x != null && y != null)) { }
if (!!!(x != null && y != null)) { } // MISHANDLED, likely due to splitting
else Console.WriteLine(x + y); // null guarded

if (Field != null)
Expand Down
11 changes: 11 additions & 0 deletions java/ql/test/query-tests/Nullness/C.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,4 +254,15 @@ public void ex18(boolean b, int[] xs, Object related) {
xs[0] = 42; // OK
}
}

public void ex19(Object t, Object x) {
boolean b = t != null || x != null;
if (b) {
if (t != null) {
t.hashCode(); // OK
} else {
x.hashCode(); // OK
}
}
}
}
104 changes: 103 additions & 1 deletion shared/controlflow/codeql/controlflow/Guards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -926,6 +926,9 @@ module Make<
guardControls(g0, v0, tgtGuard, tgtVal) and
additionalImpliesStep(g0, v0, guard, v)
)
or
baseGuardValue(tgtGuard, tgtVal) and
disjunctiveGuardControls(guard, v, tgtGuard, tgtVal)
}

/**
Expand Down Expand Up @@ -1003,6 +1006,104 @@ module Make<
)
}

private import DisjunctiveGuard

private module DisjunctiveGuard {
/**
* Holds if `disjunction` evaluating to `val` means that either
* `disjunct1` or `disjunct2` is `val`.
*/
private predicate disjunction(
Guard disjunction, GuardValue val, Guard disjunct1, Guard disjunct2
) {
2 =
strictcount(Guard op |
disjunction.(OrExpr).getAnOperand() = op or disjunction.(AndExpr).getAnOperand() = op
) and
disjunct1 != disjunct2 and
(
exists(OrExpr d | d = disjunction |
d.getAnOperand() = disjunct1 and
d.getAnOperand() = disjunct2 and
val.asBooleanValue() = true
)
or
exists(AndExpr d | d = disjunction |
d.getAnOperand() = disjunct1 and
d.getAnOperand() = disjunct2 and
val.asBooleanValue() = false
)
)
}

private predicate disjunct(Guard guard, GuardValue val) { disjunction(_, val, guard, _) }

module DisjunctImplies = ImpliesTC<disjunct/2>;

/**
* Holds if one of the disjuncts in `disjunction` evaluating to `dv` implies that `def`
* evaluates to `v`. The other disjunct is `otherDisjunct`.
*/
pragma[nomagic]
private predicate ssaControlsDisjunct(
SsaDefinition def, GuardValue v, Guard disjunction, Guard otherDisjunct, GuardValue dv
) {
exists(Guard disjunct |
disjunction(disjunction, dv, disjunct, otherDisjunct) and
DisjunctImplies::ssaControls(def, v, disjunct, dv)
)
}

/**
* Holds if the disjunction of `def` evaluating to `v` and
* `otherDisjunct` evaluating to `dv` controls `bb`.
*/
pragma[nomagic]
private predicate ssaDisjunctionControls(
SsaDefinition def, GuardValue v, Guard otherDisjunct, GuardValue dv, BasicBlock bb
) {
exists(Guard disjunction |
ssaControlsDisjunct(def, v, disjunction, otherDisjunct, dv) and
disjunction.valueControls(bb, dv)
)
}

/**
* Holds if `tgtGuard` evaluating to `tgtVal` implies that `def`
* evaluates to `v`. The basic block of `tgtGuard` is `bb`.
*/
pragma[nomagic]
private predicate ssaControlsGuard(
SsaDefinition def, GuardValue v, Guard tgtGuard, GuardValue tgtVal, BasicBlock bb
) {
(
BranchImplies::ssaControls(def, v, tgtGuard, tgtVal) or
WrapperGuard::ReturnImplies::ssaControls(def, v, tgtGuard, tgtVal)
) and
tgtGuard.getBasicBlock() = bb
}

/**
* Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard`
* evaluates to `v`.
*/
pragma[nomagic]
predicate disjunctiveGuardControls(
Guard guard, GuardValue v, Guard tgtGuard, GuardValue tgtVal
) {
exists(SsaDefinition def, GuardValue v1, GuardValue v2, BasicBlock bb |
// If `def==v1 || guard==v` controls `bb`,
ssaDisjunctionControls(def, v1, guard, v, bb) and
// and `tgtGuard==tgtVal` in `bb` implies `def==v2`,
ssaControlsGuard(def, v2, tgtGuard, tgtVal, bb) and
// and `v1` and `v2` are disjoint,
disjointValues(v1, v2)
// then assuming `tgtGuard==tgtVal` it follows that `def` cannot be `v1`
// and therefore we must have `guard==v`.
)
}
}

/**
* Provides an implementation of guard implication logic for guard
* wrappers.
Expand All @@ -1021,7 +1122,8 @@ module Make<

private predicate relevantCallValue(NonOverridableMethodCall call, GuardValue val) {
BranchImplies::guardControls(call, val, _, _) or
ReturnImplies::guardControls(call, val, _, _)
ReturnImplies::guardControls(call, val, _, _) or
DisjunctImplies::guardControls(call, val, _, _)
}

predicate relevantReturnValue(NonOverridableMethod m, GuardValue val) {
Expand Down
Loading