From 2192d752869be2ede306161d3d5cceb5736d3445 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 12 Nov 2025 14:08:18 +0100 Subject: [PATCH 1/4] Java: Add test for a known FP. --- java/ql/test/query-tests/Nullness/C.java | 11 +++++++++++ java/ql/test/query-tests/Nullness/NullMaybe.expected | 1 + 2 files changed, 12 insertions(+) diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index 881185abd237..42b6ed550a56 100644 --- a/java/ql/test/query-tests/Nullness/C.java +++ b/java/ql/test/query-tests/Nullness/C.java @@ -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(); // NPE - false positive + } + } + } } diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected index 89209bd3a710..f583c0f80b32 100644 --- a/java/ql/test/query-tests/Nullness/NullMaybe.expected +++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected @@ -35,6 +35,7 @@ | C.java:144:15:144:15 | a | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:141:20:141:26 | a | a | C.java:142:13:142:21 | ... == ... | 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:264:9:264:9 | x | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:258:30:258:37 | x | x | C.java:259:30:259:38 | ... != ... | 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 | From d6800394fa32b0df4b07546ea578caea7aad7459 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 12 Nov 2025 14:14:32 +0100 Subject: [PATCH 2/4] Guards: Support disjunctive implications. --- java/ql/test/query-tests/Nullness/C.java | 2 +- .../query-tests/Nullness/NullMaybe.expected | 1 - .../controlflow/codeql/controlflow/Guards.qll | 104 +++++++++++++++++- 3 files changed, 104 insertions(+), 3 deletions(-) diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index 42b6ed550a56..edd64cfa79b5 100644 --- a/java/ql/test/query-tests/Nullness/C.java +++ b/java/ql/test/query-tests/Nullness/C.java @@ -261,7 +261,7 @@ public void ex19(Object t, Object x) { if (t != null) { t.hashCode(); // OK } else { - x.hashCode(); // NPE - false positive + x.hashCode(); // OK } } } diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected index f583c0f80b32..89209bd3a710 100644 --- a/java/ql/test/query-tests/Nullness/NullMaybe.expected +++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected @@ -35,7 +35,6 @@ | C.java:144:15:144:15 | a | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:141:20:141:26 | a | a | C.java:142:13:142:21 | ... == ... | 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:264:9:264:9 | x | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:258:30:258:37 | x | x | C.java:259:30:259:38 | ... != ... | 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 | diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 17aee2a7caee..8490d0622a75 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -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) } /** @@ -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; + + /** + * 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. @@ -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) { From dc029e8da9e18502046952af6f39596b1161ce94 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 14 Nov 2025 11:38:13 +0100 Subject: [PATCH 3/4] C#: Accept qltest weirdness. --- .../controlflow/guards/BooleanGuardedExpr.expected | 4 ++++ .../controlflow/guards/GuardedControlFlowNode.expected | 8 ++++++++ .../library-tests/controlflow/guards/GuardedExpr.expected | 8 ++++++++ csharp/ql/test/library-tests/controlflow/guards/Guards.cs | 4 ++-- 4 files changed, 22 insertions(+), 2 deletions(-) diff --git a/csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected b/csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected index 649e83623705..ac260924d10a 100644 --- a/csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected +++ b/csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected @@ -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 | diff --git a/csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected b/csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected index b34cae88b800..d322431b1df8 100644 --- a/csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected +++ b/csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected @@ -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 | diff --git a/csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected b/csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected index b34cae88b800..d322431b1df8 100644 --- a/csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected +++ b/csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected @@ -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 | diff --git a/csharp/ql/test/library-tests/controlflow/guards/Guards.cs b/csharp/ql/test/library-tests/controlflow/guards/Guards.cs index 045967d6134f..8c4abb815e8b 100644 --- a/csharp/ql/test/library-tests/controlflow/guards/Guards.cs +++ b/csharp/ql/test/library-tests/controlflow/guards/Guards.cs @@ -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) From 4867306b5ea361065c50dbe39eeac6c82a1c4468 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 14 Nov 2025 11:44:27 +0100 Subject: [PATCH 4/4] C#: Add change note. --- csharp/ql/src/change-notes/2025-11-14-guards-disjunctive.md | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 csharp/ql/src/change-notes/2025-11-14-guards-disjunctive.md diff --git a/csharp/ql/src/change-notes/2025-11-14-guards-disjunctive.md b/csharp/ql/src/change-notes/2025-11-14-guards-disjunctive.md new file mode 100644 index 000000000000..015f16f8d091 --- /dev/null +++ b/csharp/ql/src/change-notes/2025-11-14-guards-disjunctive.md @@ -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.