C#: Improve ConstantCondition.ql

This commit is contained in:
Anders Schack-Mulligen
2025-09-26 16:28:32 +02:00
parent 587901bc8a
commit 64810f6fb5
2 changed files with 172 additions and 3 deletions

View File

@@ -16,16 +16,90 @@
import csharp
import semmle.code.csharp.commons.Assertions
import semmle.code.csharp.commons.Constants
import semmle.code.csharp.controlflow.BasicBlocks
import semmle.code.csharp.controlflow.Guards as Guards
import codeql.controlflow.queries.ConstantCondition as ConstCond
module ConstCondInput implements ConstCond::InputSig<ControlFlow::BasicBlock> {
class SsaDefinition = Ssa::Definition;
class GuardValue = Guards::GuardValue;
class Guard = Guards::Guards::Guard;
predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v) {
Guards::Guards::ssaControlsBranchEdge(def, bb1, bb2, v)
}
import Guards::Guards::InternalUtil
}
module ConstCondImpl = ConstCond::Make<Location, Cfg, ConstCondInput>;
predicate nullCheck(Expr e, boolean direct) {
exists(QualifiableExpr qe | qe.isConditional() and qe.getQualifier() = e and direct = true)
or
exists(NullCoalescingExpr nce | nce.getLeftOperand() = e and direct = true)
or
exists(ConditionalExpr ce | ce.getThen() = e or ce.getElse() = e |
nullCheck(ce, _) and direct = false
)
}
predicate constantGuard(
Guards::Guards::Guard g, string msg, Guards::Guards::Guard reason, string reasonMsg
) {
ConstCondImpl::problems(g, msg, reason, reasonMsg) and
// conditional qualified expressions sit at an akward place in the CFG, which
// leads to FPs
not g.(QualifiableExpr).getQualifier() = reason and
// and if they're extension method calls, the syntactic qualifier is actually argument 0
not g.(ExtensionMethodCall).getArgument(0) = reason and
// if a logical connective is constant, one of its operands is constant, so
// we report that instead
not g instanceof LogicalNotExpr and
not g instanceof LogicalAndExpr and
not g instanceof LogicalOrExpr and
// if a logical connective is a reason for another condition to be constant,
// then one of its operands is a more precise reason
not reason instanceof LogicalNotExpr and
not reason instanceof LogicalAndExpr and
not reason instanceof LogicalOrExpr and
// don't report double-checked locking
not exists(LockStmt ls, BasicBlock bb |
bb = ls.getBasicBlock() and
reason.getBasicBlock().strictlyDominates(bb) and
bb.dominates(g.getBasicBlock())
) and
// exclude indirect null checks like `x` in `(b ? x : null)?.Foo()`
not nullCheck(g, false)
}
/** A constant condition. */
abstract class ConstantCondition extends Expr {
abstract class ConstantCondition extends Guards::Guards::Guard {
/** Gets the alert message for this constant condition. */
abstract string getMessage();
predicate hasReason(Guards::Guards::Guard reason, string reasonMsg) {
// dummy value, overridden when message has a placeholder
reason = this and reasonMsg = "dummy"
}
/** Holds if this constant condition is white-listed. */
predicate isWhiteListed() { none() }
}
/** A constant guard. */
class ConstantGuard extends ConstantCondition {
ConstantGuard() { constantGuard(this, _, _, _) }
override string getMessage() { constantGuard(this, result, _, _) }
override predicate hasReason(Guards::Guards::Guard reason, string reasonMsg) {
constantGuard(this, _, reason, reasonMsg)
}
}
/** A constant Boolean condition. */
class ConstantBooleanCondition extends ConstantCondition {
boolean b;
@@ -111,6 +185,7 @@ class ConstantMatchingCondition extends ConstantCondition {
boolean b;
ConstantMatchingCondition() {
this instanceof Expr and
forex(ControlFlow::Node cfn | cfn = this.getAControlFlowNode() |
exists(ControlFlow::MatchingSuccessor t | exists(cfn.getASuccessorByType(t)) |
b = t.getValue()
@@ -138,9 +213,10 @@ class ConstantMatchingCondition extends ConstantCondition {
}
}
from ConstantCondition c, string msg
from ConstantCondition c, string msg, Guards::Guards::Guard reason, string reasonMsg
where
msg = c.getMessage() and
c.hasReason(reason, reasonMsg) and
not c.isWhiteListed() and
not isExprInAssertion(c)
select c, msg
select c, msg, reason, reasonMsg

View File

@@ -0,0 +1,93 @@
/**
* Provides a query for detecting constant conditions.
*/
overlay[local?]
module;
private import codeql.controlflow.BasicBlock as BB
private import codeql.util.Location
private signature class TypSig;
signature module InputSig<TypSig BasicBlock> {
class SsaDefinition;
/** An abstract value that a `Guard` may evaluate to. */
class GuardValue {
/** Gets a textual representation of this value. */
string toString();
/**
* Gets the dual value. Examples of dual values include:
* - null vs. not null
* - true vs. false
* - evaluating to a specific value vs. evaluating to any other value
* - throwing an exception vs. not throwing an exception
*/
GuardValue getDualValue();
/** Holds if this value represents throwing an exception. */
predicate isThrowsException();
}
/**
* A guard. This may be any expression whose value determines subsequent
* 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.
*/
class Guard {
/** Gets a textual representation of this guard. */
string toString();
/**
* Holds if this guard evaluating to `v` corresponds to taking the edge
* from `bb1` to `bb2`. For ordinary conditional branching this guard is
* the last node in `bb1`, but for switch case matching it is the switch
* expression, which may either be in `bb1` or an earlier basic block.
*/
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v);
}
/**
* Holds if `def` evaluating to `v` controls the control-flow branch
* edge from `bb1` to `bb2`. That is, following the edge from `bb1` to
* `bb2` implies that `def` evaluated to `v`.
*/
predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v);
bindingset[gv1, gv2]
predicate disjointValues(GuardValue gv1, GuardValue gv2);
}
module Make<LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Cfg::BasicBlock> Input> {
private import Cfg
private import Input
private predicate ssaControlsGuardEdge(
SsaDefinition def, GuardValue v, Guard g, BasicBlock bb1, BasicBlock bb2, GuardValue gv
) {
g.hasValueBranchEdge(bb1, bb2, gv) and
ssaControlsBranchEdge(def, bb1, bb2, v)
}
query predicate problems(Guard g, string msg, Guard reason, string reasonMsg) {
exists(
BasicBlock bb, GuardValue gv, GuardValue dual, SsaDefinition def, GuardValue v1,
GuardValue v2, BasicBlock bb1, BasicBlock bb2
|
// If `g` in `bb` evaluates to `gv` then `def` has value `v1`,
ssaControlsGuardEdge(def, v1, g, bb, _, gv) and
dual = gv.getDualValue() and
not gv.isThrowsException() and
not dual.isThrowsException() and
// but `def` controls `bb` with value `v2` via the guard `reason` taking the branch `bb1` to `bb2`,
ssaControlsGuardEdge(def, v2, reason, bb1, bb2, _) and
dominatingEdge(bb1, bb2) and
bb2.dominates(bb) and
// and `v1` and `v2` are disjoint so `g` cannot be `gv`.
disjointValues(v1, v2) and
msg = "Condition is always " + dual + " because of $@." and
reasonMsg = reason.toString()
)
}
}