C#: Instantiate ControlFlowReachability and implement new nullness.

Author: aschackmull

csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll

@@ -0,0 +1,57 @@
+/**
+ * Provides an implementation of local (intraprocedural) control flow reachability.
+ */
+
+import csharp
+private import codeql.controlflow.ControlFlow
+private import semmle.code.csharp.controlflow.BasicBlocks
+private import semmle.code.csharp.controlflow.Guards as Guards
+private import semmle.code.csharp.ExprOrStmtParent
+
+private module ControlFlowInput implements
+  InputSig<Location, ControlFlow::Node, ControlFlow::BasicBlock>
+{
+  private import csharp as CS
+
+  AstNode getEnclosingAstNode(ControlFlow::Node node) {
+    node.getAstNode() = result
+    or
+    not exists(node.getAstNode()) and result = node.getEnclosingCallable()
+  }
+
+  class AstNode = ExprOrStmtParent;
+
+  AstNode getParent(AstNode node) { result = node.getParent() }
+
+  class FinallyBlock extends AstNode {
+    FinallyBlock() { any(TryStmt try).getFinally() = this }
+  }
+
+  class Expr = CS::Expr;
+
+  class SourceVariable = Ssa::SourceVariable;
+
+  class SsaDefinition = Ssa::Definition;
+
+  class SsaWriteDefinition extends SsaDefinition instanceof Ssa::ExplicitDefinition {
+    Expr getDefinition() { result = super.getADefinition().getSource() }
+  }
+
+  class SsaPhiNode = Ssa::PhiNode;
+
+  class SsaUncertainDefinition = Ssa::UncertainDefinition;
+
+  class GuardValue = Guards::GuardValue;
+
+  predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v) {
+    Guards::Guards::ssaControlsBranchEdge(def, bb1, bb2, v)
+  }
+
+  predicate ssaControls(SsaDefinition def, BasicBlock bb, GuardValue v) {
+    Guards::Guards::ssaControls(def, bb, v)
+  }
+
+  import Guards::Guards::InternalUtil
+}
+
+module ControlFlowReachability = Make<Location, Cfg, ControlFlowInput>;

csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll

@@ -26,27 +26,30 @@ private import semmle.code.csharp.controlflow.Guards::AbstractValues
 private import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
 private import semmle.code.csharp.frameworks.System
 private import semmle.code.csharp.frameworks.Test
+private import semmle.code.csharp.controlflow.ControlFlowReachability as Cf
+
+private Expr maybeNullExpr(Expr reason) {
+  G::Internal::nullValue(result) and reason = result
+  or
+  result instanceof AsExpr and reason = result
+  or
+  result.(AssignExpr).getRValue() = maybeNullExpr(reason)
+  or
+  result.(Cast).getExpr() = maybeNullExpr(reason)
+  or
+  result =
+    any(ConditionalExpr ce |
+      ce.getThen() = maybeNullExpr(reason)
+      or
+      ce.getElse() = maybeNullExpr(reason)
+    )
+  or
+  result.(NullCoalescingExpr).getRightOperand() = maybeNullExpr(reason)
+}
 
 /** An expression that may be `null`. */
 class MaybeNullExpr extends Expr {
-  MaybeNullExpr() {
-    G::Internal::nullValue(this)
-    or
-    this instanceof AsExpr
-    or
-    this.(AssignExpr).getRValue() instanceof MaybeNullExpr
-    or
-    this.(Cast).getExpr() instanceof MaybeNullExpr
-    or
-    this =
-      any(ConditionalExpr ce |
-        ce.getThen() instanceof MaybeNullExpr
-        or
-        ce.getElse() instanceof MaybeNullExpr
-      )
-    or
-    this.(NullCoalescingExpr).getRightOperand() instanceof MaybeNullExpr
-  }
+  MaybeNullExpr() { this = maybeNullExpr(_) }
 }
 
 /** An expression that is always `null`. */
@@ -123,6 +126,10 @@ private predicate dereferenceAt(BasicBlock bb, int i, Ssa::Definition def, Deref
   d = def.getAReadAtNode(bb.getNode(i))
 }
 
+private predicate dereferenceAt(ControlFlow::Node node, Ssa::Definition def, Dereference d) {
+  d = def.getAReadAtNode(node)
+}
+
 /**
  * Holds if `e` having abstract value `vExpr` implies that SSA definition `def`
  * has abstract value `vDef`.
@@ -217,13 +224,16 @@ private predicate isNullDefaultArgument(Ssa::ImplicitParameterDefinition def, Al
 }
 
 /** Holds if `def` is an SSA definition that may be `null`. */
-private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason) {
+private predicate defMaybeNull(
+  Ssa::Definition def, ControlFlow::Node node, string msg, Element reason
+) {
   not nonNullDef(def) and
   (
     // A variable compared to `null` might be `null`
     exists(G::DereferenceableExpr de | de = def.getARead() |
       reason = de.getANullCheck(_, true) and
       msg = "as suggested by $@ null check" and
+      node = def.getControlFlowNode() and
       not de = any(Ssa::PhiNode phi).getARead() and
       strictcount(Element e | e = any(Ssa::Definition def0 | de = def0.getARead()).getElement()) = 1 and
       // Don't use a check as reason if there is a `null` assignment
@@ -234,23 +244,27 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
     or
     // A parameter might be `null` if there is a `null` argument somewhere
     isMaybeNullArgument(def, reason) and
+    node = def.getControlFlowNode() and
     (
       if reason instanceof AlwaysNullExpr
       then msg = "because of $@ null argument"
       else msg = "because of $@ potential null argument"
     )
     or
-    isNullDefaultArgument(def, reason) and msg = "because the parameter has a null default value"
+    isNullDefaultArgument(def, reason) and
+    node = def.getControlFlowNode() and
+    msg = "because the parameter has a null default value"
     or
     // If the source of a variable is `null` then the variable may be `null`
     exists(AssignableDefinition adef | adef = def.(Ssa::ExplicitDefinition).getADefinition() |
-      adef.getSource() instanceof MaybeNullExpr and
+      adef.getSource() = maybeNullExpr(node.getAstNode()) and
       reason = adef.getExpr() and
       msg = "because of $@ assignment"
     )
     or
     // A variable of nullable type may be null
     exists(Dereference d | dereferenceAt(_, _, def, d) |
+      node = def.getControlFlowNode() and
       d.hasNullableType() and
       not def instanceof Ssa::PhiNode and
       reason = def.getSourceVariable().getAssignable() and
@@ -261,7 +275,7 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
 
 pragma[noinline]
 private predicate sourceVariableMaybeNull(Ssa::SourceVariable v) {
-  defMaybeNull(v.getAnSsaDefinition(), _, _)
+  defMaybeNull(v.getAnSsaDefinition(), _, _, _)
 }
 
 pragma[noinline]
@@ -305,7 +319,7 @@ private predicate defNullImpliesStep(
  * That is, those basic blocks for which the SSA definition is suspected of being `null`.
  */
 private predicate defMaybeNullInBlock(Ssa::Definition def, BasicBlock bb) {
-  defMaybeNull(def, _, _) and
+  defMaybeNull(def, _, _, _) and
   bb = def.getBasicBlock()
   or
   exists(BasicBlock mid, Ssa::Definition midDef | defMaybeNullInBlock(midDef, mid) |
@@ -341,7 +355,7 @@ private predicate succSourceSink(SourcePathNode source, Ssa::Definition def, Bas
 private newtype TPathNode =
   TSourcePathNode(Ssa::Definition def, string msg, Element reason, boolean isNullArgument) {
     nullDerefCandidateVariable(def.getSourceVariable()) and
-    defMaybeNull(def, msg, reason) and
+    defMaybeNull(def, _, msg, reason) and
     if isMaybeNullArgument(def, reason) then isNullArgument = true else isNullArgument = false
   } or
   TInternalPathNode(Ssa::Definition def, BasicBlock bb) {
@@ -503,6 +517,40 @@ private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn, boolean
   )
 }
 
+private module NullnessConfig implements Cf::ControlFlowReachability::ConfigSig {
+  predicate source(ControlFlow::Node node, Ssa::Definition def) { defMaybeNull(def, node, _, _) }
+
+  predicate sink(ControlFlow::Node node, Ssa::Definition def) {
+    exists(Dereference d |
+      dereferenceAt(node, def, d) and
+      not d instanceof NonNullExpr
+    )
+  }
+
+  predicate barrierValue(G::GuardValue gv) { gv.isNullness(false) }
+
+  predicate uncertainFlow() { none() }
+}
+
+private module NullnessFlow = Cf::ControlFlowReachability::Flow<NullnessConfig>;
+
+predicate debug_nullness_new(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
+  exists(
+    Ssa::Definition origin, Ssa::Definition ssa, ControlFlow::Node src, ControlFlow::Node sink
+  |
+    defMaybeNull(origin, src, msg, reason) and
+    NullnessFlow::flow(src, origin, sink, ssa) and
+    ssa.getSourceVariable() = v and
+    dereferenceAt(sink, ssa, d) and
+    not d.isAlwaysNull(v)
+  )
+}
+
+predicate debug_nullness_orig(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
+  d.isFirstMaybeNull(v.getAnSsaDefinition(), _, _, msg, reason) and
+  not d instanceof NonNullExpr
+}
+
 /**
  * An expression that dereferences a value. That is, an expression that may
  * result in a `NullReferenceException` if the value is `null`.

csharp/ql/lib/semmle/code/csharp/dataflow/SSA.qll

@@ -163,13 +163,11 @@ module Ssa {
    * (`ImplicitDefinition`), or a phi node (`PhiNode`).
    */
   class Definition extends SsaImpl::Definition {
-    /**
-     * Gets the control flow node of this SSA definition, if any. Phi nodes are
-     * examples of SSA definitions without a control flow node, as they are
-     * modeled at index `-1` in the relevant basic block.
-     */
+    /** Gets the control flow node of this SSA definition. */
     final ControlFlow::Node getControlFlowNode() {
-      exists(ControlFlow::BasicBlock bb, int i | this.definesAt(_, bb, i) | result = bb.getNode(i))
+      exists(ControlFlow::BasicBlock bb, int i | this.definesAt(_, bb, i) |
+        result = bb.getNode(0.maximum(i))
+      )
     }
 
     /**