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. 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) diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index 881185abd237..edd64cfa79b5 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(); // OK + } + } + } } 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) {