C#: Improve ConstantCondition.ql

Author: aschackmull

csharp/ql/src/Bad Practices/Control-Flow/ConstantCondition.ql

@@ -16,16 +16,76 @@
 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 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
+  // 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())
+  )
+}
 
 /** 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;
@@ -138,9 +198,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

shared/controlflow/codeql/controlflow/queries/ConstantCondition.qll

@@ -0,0 +1,89 @@
+/**
+ * Provides a query for detecting constant conditions.
+ */
+
+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, 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
+      not gv.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 = "Guard " + g + " is always " + gv.getDualValue() + " because of $@." and
+      reasonMsg = reason.toString()
+    )
+  }
+}