C#: Add CIL SSA library

csharp/ql/src/semmle/code/cil/BasicBlock.qll

@@ -240,6 +240,9 @@ class BasicBlock extends Cached::TBasicBlockStart {
 
   /** Gets a textual representation of this basic block. */
   string toString() { result = getFirstNode().toString() }
+
+  /** Gets the location of this basic block. */
+  Location getLocation() { result = this.getFirstNode().getLocation() }
 }
 
 /**
@@ -305,7 +308,7 @@ class EntryBasicBlock extends BasicBlock {
 }
 
 /** Holds if `bb` is an entry basic block. */
-private predicate entryBB(BasicBlock bb) { bb.getFirstNode() instanceof EntryPoint }
+private predicate entryBB(BasicBlock bb) { bb.getFirstNode() instanceof MethodImplementation }
 
 /**
  * An exit basic block, that is, a basic block whose last node is

csharp/ql/src/semmle/code/cil/CIL.qll

@@ -20,3 +20,4 @@ import Attribute
 import Stubs
 import CustomModifierReceiver
 import Parameterizable
+import semmle.code.cil.Ssa

csharp/ql/src/semmle/code/cil/CallableReturns.qll

@@ -42,7 +42,11 @@ private predicate alwaysNullExpr(Expr expr) {
   or
   alwaysNullMethod(expr.(StaticCall).getTarget())
   or
-  forex(VariableUpdate vu | DefUse::variableUpdateUse(_, vu, expr) | alwaysNullVariableUpdate(vu))
+  forex(Ssa::Definition def |
+    expr = any(Ssa::Definition def0 | def = def0.getAnUltimateDefinition()).getARead()
+  |
+    alwaysNullVariableUpdate(def.getVariableUpdate())
+  )
 }
 
 pragma[noinline]
@@ -58,7 +62,9 @@ private predicate alwaysNotNullExpr(Expr expr) {
   or
   alwaysNotNullMethod(expr.(StaticCall).getTarget())
   or
-  forex(VariableUpdate vu | DefUse::variableUpdateUse(_, vu, expr) |
-    alwaysNotNullVariableUpdate(vu)
+  forex(Ssa::Definition def |
+    expr = any(Ssa::Definition def0 | def = def0.getAnUltimateDefinition()).getARead()
+  |
+    alwaysNotNullVariableUpdate(def.getVariableUpdate())
   )
 }

csharp/ql/src/semmle/code/cil/ControlFlow.qll

@@ -9,6 +9,9 @@ class ControlFlowNode extends @cil_controlflow_node {
   /** Gets a textual representation of this control flow node. */
   string toString() { none() }
 
+  /** Gets the location of this control flow node. */
+  Location getLocation() { none() }
+
   /**
    * Gets the number of items this node pushes onto the stack.
    * This value is either 0 or 1, except for the instruction `dup`

csharp/ql/src/semmle/code/cil/DataFlow.qll

@@ -57,12 +57,40 @@ class Untainted extends TaintType, TExactValue { }
 /** A taint type where the data is tainted. */
 class Tainted extends TaintType, TTaintedValue { }
 
+private predicate localFlowPhiInput(DataFlowNode input, Ssa::PhiNode phi) {
+  exists(Ssa::Definition def, BasicBlock bb, int i | phi.hasLastInputRef(def, bb, i) |
+    def.definesAt(_, bb, i) and
+    input = def.getVariableUpdate().getSource()
+    or
+    input =
+      any(ReadAccess ra |
+        bb.getNode(i) = ra and
+        ra.getTarget() = def.getSourceVariable()
+      )
+  )
+  or
+  exists(Ssa::PhiNode mid, BasicBlock bb, int i |
+    localFlowPhiInput(input, mid) and
+    phi.hasLastInputRef(mid, bb, i) and
+    mid.definesAt(_, bb, i)
+  )
+}
+
 private predicate localExactStep(DataFlowNode src, DataFlowNode sink) {
   src = sink.(Opcodes::Dup).getAnOperand()
   or
-  defUse(_, src, sink)
+  exists(Ssa::Definition def, VariableUpdate vu |
+    vu = def.getVariableUpdate() and
+    src = vu.getSource() and
+    sink = def.getAFirstRead()
+  )
   or
-  src = sink.(ParameterReadAccess).getTarget()
+  any(Ssa::Definition def).hasAdjacentReads(src, sink)
+  or
+  exists(Ssa::PhiNode phi |
+    localFlowPhiInput(src, phi) and
+    sink = phi.getAFirstRead()
+  )
   or
   src = sink.(Conversion).getExpr()
   or
@@ -73,12 +101,6 @@ private predicate localExactStep(DataFlowNode src, DataFlowNode sink) {
   src = sink.(Return).getExpr()
   or
   src = sink.(ConditionalBranch).getAnOperand()
-  or
-  src = sink.(MethodParameter).getAWrite()
-  or
-  exists(VariableUpdate update |
-    update.getVariable().(Parameter) = sink and src = update.getSource()
-  )
 }
 
 private predicate localTaintStep(DataFlowNode src, DataFlowNode sink) {
@@ -87,8 +109,7 @@ private predicate localTaintStep(DataFlowNode src, DataFlowNode sink) {
   src = sink.(UnaryBitwiseOperation).getOperand()
 }
 
-cached
-module DefUse {
+deprecated module DefUse {
   /**
    * A classification of variable references into reads and writes.
    */
@@ -189,7 +210,7 @@ module DefUse {
 
   /** Holds if the variable update `vu` can be used at the read `use`. */
   cached
-  predicate variableUpdateUse(StackVariable target, VariableUpdate vu, ReadAccess use) {
+  deprecated predicate variableUpdateUse(StackVariable target, VariableUpdate vu, ReadAccess use) {
     defReachesReadWithinBlock(target, vu, use)
     or
     exists(BasicBlock bb, int i |
@@ -202,23 +223,40 @@ module DefUse {
 
   /** Holds if the update `def` can be used at the read `use`. */
   cached
-  predicate defUse(StackVariable target, Expr def, ReadAccess use) {
+  deprecated predicate defUse(StackVariable target, Expr def, ReadAccess use) {
     exists(VariableUpdate vu | def = vu.getSource() | variableUpdateUse(target, vu, use))
   }
 }
 
-private import DefUse
-
-abstract library class VariableUpdate extends Instruction {
-  abstract Expr getSource();
+/** A node that updates a variable. */
+abstract class VariableUpdate extends DataFlowNode {
+  /** Gets the value assigned, if any. */
+  abstract DataFlowNode getSource();
 
+  /** Gets the variable that is updated. */
   abstract Variable getVariable();
+
+  /** Holds if this variable update happens at index `i` in basic block `bb`. */
+  abstract predicate updatesAt(BasicBlock bb, int i);
+}
+
+private class MethodParameterDef extends VariableUpdate, MethodParameter {
+  override MethodParameter getSource() { result = this }
+
+  override MethodParameter getVariable() { result = this }
+
+  override predicate updatesAt(BasicBlock bb, int i) {
+    bb.(EntryBasicBlock).getANode().getImplementation().getMethod() = this.getMethod() and
+    i = -1
+  }
 }
 
 private class VariableWrite extends VariableUpdate, WriteAccess {
-  override Expr getSource() { result = getExpr() }
+  override Expr getSource() { result = this.getExpr() }
 
-  override Variable getVariable() { result = getTarget() }
+  override Variable getVariable() { result = this.getTarget() }
+
+  override predicate updatesAt(BasicBlock bb, int i) { this = bb.getNode(i) }
 }
 
 private class MethodOutOrRefTarget extends VariableUpdate, Call {
@@ -230,5 +268,7 @@ private class MethodOutOrRefTarget extends VariableUpdate, Call {
     result = this.getRawArgument(parameterIndex).(ReadAccess).getTarget()
   }
 
-  override Expr getSource() { result = this }
+  override Expr getSource() { none() }
+
+  override predicate updatesAt(BasicBlock bb, int i) { this = bb.getNode(i) }
 }

csharp/ql/src/semmle/code/cil/Method.qll

@@ -19,7 +19,7 @@ class MethodImplementation extends EntryPoint, @cil_method_implementation {
   override MethodImplementation getImplementation() { result = this }
 
   /** Gets the location of this implementation. */
-  Assembly getLocation() { cil_method_implementation(this, _, result) }
+  override Assembly getLocation() { cil_method_implementation(this, _, result) }
 
   /** Gets the instruction at index `index`. */
   Instruction getInstruction(int index) { cil_instruction(result, _, index, this) }

csharp/ql/src/semmle/code/cil/Ssa.qll

@@ -0,0 +1,66 @@
+/**
+ * Provides the module `Ssa` for working with static single assignment (SSA) form.
+ */
+
+private import CIL
+
+/**
+ * Provides classes for working with static single assignment (SSA) form.
+ */
+module Ssa {
+  private import internal.SsaImplCommon as SsaImpl
+  private import internal.SsaImpl
+
+  /** An SSA definition. */
+  class Definition extends SsaImpl::Definition {
+    /** Gets a read of this SSA definition. */
+    final ReadAccess getARead() { result = getARead(this) }
+
+    /** Gets the underlying variable update, if any. */
+    final VariableUpdate getVariableUpdate() {
+      exists(BasicBlock bb, int i |
+        result.updatesAt(bb, i) and
+        this.definesAt(result.getVariable(), bb, i)
+      )
+    }
+
+    /** Gets a first read of this SSA definition. */
+    final ReadAccess getAFirstRead() { result = getAFirstRead(this) }
+
+    /** Holds if `first` and `second` are adjacent reads of this SSA definition. */
+    final predicate hasAdjacentReads(ReadAccess first, ReadAccess second) {
+      hasAdjacentReads(this, first, second)
+    }
+
+    private Definition getAPhiInput() { result = this.(PhiNode).getAnInput() }
+
+    /**
+     * Gets a definition that ultimately defines this SSA definition and is
+     * not itself a phi node.
+     */
+    final Definition getAnUltimateDefinition() {
+      result = this.getAPhiInput*() and
+      not result instanceof PhiNode
+    }
+
+    /** Gets the location of this SSA definition. */
+    Location getLocation() { result = this.getVariableUpdate().getLocation() }
+  }
+
+  /** A phi node. */
+  class PhiNode extends SsaImpl::PhiNode, Definition {
+    final override Location getLocation() { result = this.getBasicBlock().getLocation() }
+
+    /** Gets an input to this phi node. */
+    final Definition getAnInput() { result = getAPhiInput(this) }
+
+    /**
+     * Holds if if `def` is an input to this phi node, and a reference to `def` at
+     * index `i` in basic block `bb` can reach this phi node without going through
+     * other references.
+     */
+    final predicate hasLastInputRef(Definition def, BasicBlock bb, int i) {
+      hasLastInputRef(this, def, bb, i)
+    }
+  }
+}

csharp/ql/src/semmle/code/cil/internal/SsaImpl.qll

@@ -0,0 +1,45 @@
+private import semmle.code.cil.CIL
+private import SsaImplCommon
+
+cached
+private module Cached {
+  cached
+  predicate forceCachingInSameStage() { any() }
+
+  cached
+  ReadAccess getARead(Definition def) {
+    exists(BasicBlock bb, int i |
+      ssaDefReachesRead(_, def, bb, i) and
+      result = bb.getNode(i)
+    )
+  }
+
+  cached
+  ReadAccess getAFirstRead(Definition def) {
+    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+      def.definesAt(_, bb1, i1) and
+      adjacentDefRead(def, bb1, i1, bb2, i2) and
+      result = bb2.getNode(i2)
+    )
+  }
+
+  cached
+  predicate hasAdjacentReads(Definition def, ReadAccess first, ReadAccess second) {
+    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+      first = bb1.getNode(i1) and
+      adjacentDefRead(def, bb1, i1, bb2, i2) and
+      second = bb2.getNode(i2)
+    )
+  }
+
+  cached
+  Definition getAPhiInput(PhiNode phi) { phiHasInputFromBlock(phi, result, _) }
+
+  cached
+  predicate hasLastInputRef(Definition phi, Definition def, BasicBlock bb, int i) {
+    lastRefRedef(def, bb, i, phi) and
+    def = getAPhiInput(phi)
+  }
+}
+
+import Cached

csharp/ql/src/semmle/code/cil/internal/SsaImplCommon.qll

@@ -0,0 +1,619 @@
+/**
+ * Provides a language-independant implementation of static single assignment
+ * (SSA) form.
+ */
+
+private import SsaImplSpecific
+
+private BasicBlock getABasicBlockPredecessor(BasicBlock bb) { getABasicBlockSuccessor(result) = bb }
+
+/**
+ * Liveness analysis (based on source variables) to restrict the size of the
+ * SSA representation.
+ */
+private module Liveness {
+  /**
+   * A classification of variable references into reads (of a given kind) and
+   * (certain or uncertain) writes.
+   */
+  private newtype TRefKind =
+    Read(boolean certain) { certain in [false, true] } or
+    Write(boolean certain) { certain in [false, true] }
+
+  private class RefKind extends TRefKind {
+    string toString() {
+      exists(boolean certain | this = Read(certain) and result = "read (" + certain + ")")
+      or
+      exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")
+    }
+
+    int getOrder() {
+      this = Read(_) and
+      result = 0
+      or
+      this = Write(_) and
+      result = 1
+    }
+  }
+
+  /**
+   * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
+   */
+  private predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) {
+    exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain))
+    or
+    exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
+  }
+
+  private newtype OrderedRefIndex =
+    MkOrderedRefIndex(int i, int tag) {
+      exists(RefKind rk | ref(_, i, _, rk) | tag = rk.getOrder())
+    }
+
+  private OrderedRefIndex refOrd(BasicBlock bb, int i, SourceVariable v, RefKind k, int ord) {
+    ref(bb, i, v, k) and
+    result = MkOrderedRefIndex(i, ord) and
+    ord = k.getOrder()
+  }
+
+  /**
+   * Gets the (1-based) rank of the reference to `v` at the `i`th node of
+   * basic block `bb`, which has the given reference kind `k`.
+   *
+   * Reads are considered before writes when they happen at the same index.
+   */
+  private int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) {
+    refOrd(bb, i, v, k, _) =
+      rank[result](int j, int ord, OrderedRefIndex res |
+        res = refOrd(bb, j, v, _, ord)
+      |
+        res order by j, ord
+      )
+  }
+
+  private int maxRefRank(BasicBlock bb, SourceVariable v) {
+    result = refRank(bb, _, v, _) and
+    not result + 1 = refRank(bb, _, v, _)
+  }
+
+  /**
+   * Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
+   * that is either a read or a certain write.
+   */
+  private int firstReadOrCertainWrite(BasicBlock bb, SourceVariable v) {
+    result =
+      min(int r, RefKind k |
+        r = refRank(bb, _, v, k) and
+        k != Write(false)
+      |
+        r
+      )
+  }
+
+  /**
+   * Holds if source variable `v` is live at the beginning of basic block `bb`.
+   */
+  predicate liveAtEntry(BasicBlock bb, SourceVariable v) {
+    // The first read or certain write to `v` inside `bb` is a read
+    refRank(bb, _, v, Read(_)) = firstReadOrCertainWrite(bb, v)
+    or
+    // There is no certain write to `v` inside `bb`, but `v` is live at entry
+    // to a successor basic block of `bb`
+    not exists(firstReadOrCertainWrite(bb, v)) and
+    liveAtExit(bb, v)
+  }
+
+  /**
+   * Holds if source variable `v` is live at the end of basic block `bb`.
+   */
+  predicate liveAtExit(BasicBlock bb, SourceVariable v) {
+    liveAtEntry(getABasicBlockSuccessor(bb), v)
+  }
+
+  /**
+   * Holds if variable `v` is live in basic block `bb` at index `i`.
+   * The rank of `i` is `rnk` as defined by `refRank()`.
+   */
+  private predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk) {
+    exists(RefKind kind | rnk = refRank(bb, i, v, kind) |
+      rnk = maxRefRank(bb, v) and
+      liveAtExit(bb, v)
+      or
+      ref(bb, i, v, kind) and
+      kind = Read(_)
+      or
+      exists(RefKind nextKind |
+        liveAtRank(bb, _, v, rnk + 1) and
+        rnk + 1 = refRank(bb, _, v, nextKind) and
+        nextKind != Write(true)
+      )
+    )
+  }
+
+  /**
+   * Holds if variable `v` is live after the (certain or uncertain) write at
+   * index `i` inside basic block `bb`.
+   */
+  predicate liveAfterWrite(BasicBlock bb, int i, SourceVariable v) {
+    exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, i, v, rnk))
+  }
+}
+
+private import Liveness
+
+/** Holds if `bb1` strictly dominates `bb2`. */
+private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
+  bb1 = getImmediateBasicBlockDominator+(bb2)
+}
+
+/** Holds if `bb1` dominates a predecessor of `bb2`. */
+private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
+  exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
+    bb1 = pred
+    or
+    strictlyDominates(bb1, pred)
+  )
+}
+
+/** Holds if `df` is in the dominance frontier of `bb`. */
+private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
+  dominatesPredecessor(bb, df) and
+  not strictlyDominates(bb, df)
+}
+
+/**
+ * Holds if `bb` is in the dominance frontier of a block containing a
+ * definition of `v`.
+ */
+pragma[noinline]
+private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) {
+  exists(BasicBlock defbb, Definition def |
+    def.definesAt(v, defbb, _) and
+    inDominanceFrontier(defbb, bb)
+  )
+}
+
+cached
+newtype TDefinition =
+  TWriteDef(SourceVariable v, BasicBlock bb, int i) {
+    variableWrite(bb, i, v, _) and
+    liveAfterWrite(bb, i, v)
+  } or
+  TPhiNode(SourceVariable v, BasicBlock bb) {
+    inDefDominanceFrontier(bb, v) and
+    liveAtEntry(bb, v)
+  }
+
+private module SsaDefReaches {
+  newtype TSsaRefKind =
+    SsaRead() or
+    SsaDef()
+
+  /**
+   * A classification of SSA variable references into reads and definitions.
+   */
+  class SsaRefKind extends TSsaRefKind {
+    string toString() {
+      this = SsaRead() and
+      result = "SsaRead"
+      or
+      this = SsaDef() and
+      result = "SsaDef"
+    }
+
+    int getOrder() {
+      this = SsaRead() and
+      result = 0
+      or
+      this = SsaDef() and
+      result = 1
+    }
+  }
+
+  /**
+   * Holds if the `i`th node of basic block `bb` is a reference to `v`,
+   * either a read (when `k` is `SsaRead()`) or an SSA definition (when `k`
+   * is `SsaDef()`).
+   *
+   * Unlike `Liveness::ref`, this includes `phi` nodes.
+   */
+  predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
+    variableRead(bb, i, v, _) and
+    k = SsaRead()
+    or
+    exists(Definition def | def.definesAt(v, bb, i)) and
+    k = SsaDef()
+  }
+
+  private newtype OrderedSsaRefIndex =
+    MkOrderedSsaRefIndex(int i, SsaRefKind k) { ssaRef(_, i, _, k) }
+
+  private OrderedSsaRefIndex ssaRefOrd(BasicBlock bb, int i, SourceVariable v, SsaRefKind k, int ord) {
+    ssaRef(bb, i, v, k) and
+    result = MkOrderedSsaRefIndex(i, k) and
+    ord = k.getOrder()
+  }
+
+  /**
+   * Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
+   * block `bb`, which has the given reference kind `k`.
+   *
+   * For example, if `bb` is a basic block with a phi node for `v` (considered
+   * to be at index -1), reads `v` at node 2, and defines it at node 5, we have:
+   *
+   * ```ql
+   * ssaRefRank(bb, -1, v, SsaDef()) = 1    // phi node
+   * ssaRefRank(bb,  2, v, Read())   = 2    // read at node 2
+   * ssaRefRank(bb,  5, v, SsaDef()) = 3    // definition at node 5
+   * ```
+   *
+   * Reads are considered before writes when they happen at the same index.
+   */
+  int ssaRefRank(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
+    ssaRefOrd(bb, i, v, k, _) =
+      rank[result](int j, int ord, OrderedSsaRefIndex res |
+        res = ssaRefOrd(bb, j, v, _, ord)
+      |
+        res order by j, ord
+      )
+  }
+
+  int maxSsaRefRank(BasicBlock bb, SourceVariable v) {
+    result = ssaRefRank(bb, _, v, _) and
+    not result + 1 = ssaRefRank(bb, _, v, _)
+  }
+
+  /**
+   * Holds if the SSA definition `def` reaches rank index `rnk` in its own
+   * basic block `bb`.
+   */
+  predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
+    exists(int i |
+      rnk = ssaRefRank(bb, i, v, SsaDef()) and
+      def.definesAt(v, bb, i)
+    )
+    or
+    ssaDefReachesRank(bb, def, rnk - 1, v) and
+    rnk = ssaRefRank(bb, _, v, SsaRead())
+  }
+
+  /**
+   * Holds if the SSA definition of `v` at `def` reaches index `i` in the same
+   * basic block `bb`, without crossing another SSA definition of `v`.
+   */
+  predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) {
+    exists(int rnk |
+      ssaDefReachesRank(bb, def, rnk, v) and
+      rnk = ssaRefRank(bb, i, v, SsaRead()) and
+      variableRead(bb, i, v, _)
+    )
+  }
+
+  /**
+   * Holds if the SSA definition of `v` at `def` reaches uncertain SSA definition
+   * `redef` in the same basic block, without crossing another SSA definition of `v`.
+   */
+  predicate ssaDefReachesUncertainDefWithinBlock(
+    SourceVariable v, Definition def, UncertainWriteDefinition redef
+  ) {
+    exists(BasicBlock bb, int rnk, int i |
+      ssaDefReachesRank(bb, def, rnk, v) and
+      rnk = ssaRefRank(bb, i, v, SsaDef()) - 1 and
+      redef.definesAt(v, bb, i)
+    )
+  }
+
+  /**
+   * Same as `ssaRefRank()`, but restricted to a particular SSA definition `def`.
+   */
+  int ssaDefRank(Definition def, SourceVariable v, BasicBlock bb, int i, SsaRefKind k) {
+    v = def.getSourceVariable() and
+    result = ssaRefRank(bb, i, v, k) and
+    (
+      ssaDefReachesRead(_, def, bb, i)
+      or
+      def.definesAt(_, bb, i)
+    )
+  }
+
+  predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
+    exists(ssaDefRank(def, v, bb, _, _))
+  }
+
+  pragma[noinline]
+  private BasicBlock getAMaybeLiveSuccessor(Definition def, BasicBlock bb) {
+    result = getABasicBlockSuccessor(bb) and
+    not defOccursInBlock(_, bb, def.getSourceVariable()) and
+    ssaDefReachesEndOfBlock(bb, def, _)
+  }
+
+  /**
+   * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
+   * `bb2` is a transitive successor of `bb1`, `def` is live at the end of `bb1`,
+   * and the underlying variable for `def` is neither read nor written in any block
+   * on the path between `bb1` and `bb2`.
+   */
+  predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
+    defOccursInBlock(def, bb1, _) and
+    bb2 = getABasicBlockSuccessor(bb1)
+    or
+    exists(BasicBlock mid | varBlockReaches(def, bb1, mid) | bb2 = getAMaybeLiveSuccessor(def, mid))
+  }
+
+  /**
+   * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
+   * `def` is read at index `i2` in basic block `bb2`, `bb2` is in a transitive
+   * successor block of `bb1`, and `def` is neither read nor written in any block
+   * on a path between `bb1` and `bb2`.
+   */
+  predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
+    varBlockReaches(def, bb1, bb2) and
+    ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
+    variableRead(bb2, i2, _, _)
+  }
+}
+
+private import SsaDefReaches
+
+pragma[noinline]
+private predicate ssaDefReachesEndOfBlockRec(BasicBlock bb, Definition def, SourceVariable v) {
+  exists(BasicBlock idom | ssaDefReachesEndOfBlock(idom, def, v) |
+    // The construction of SSA form ensures that each read of a variable is
+    // dominated by its definition. An SSA definition therefore reaches a
+    // control flow node if it is the _closest_ SSA definition that dominates
+    // the node. If two definitions dominate a node then one must dominate the
+    // other, so therefore the definition of _closest_ is given by the dominator
+    // tree. Thus, reaching definitions can be calculated in terms of dominance.
+    idom = getImmediateBasicBlockDominator(bb)
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if the SSA definition of `v` at `def` reaches the end of basic
+ * block `bb`, at which point it is still live, without crossing another
+ * SSA definition of `v`.
+ */
+pragma[nomagic]
+predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
+  exists(int last | last = maxSsaRefRank(bb, v) |
+    ssaDefReachesRank(bb, def, last, v) and
+    liveAtExit(bb, v)
+  )
+  or
+  ssaDefReachesEndOfBlockRec(bb, def, v) and
+  liveAtExit(bb, v) and
+  not ssaRef(bb, _, v, SsaDef())
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
+ */
+pragma[nomagic]
+predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
+  exists(SourceVariable v, BasicBlock bbDef |
+    phi.definesAt(v, bbDef, _) and
+    getABasicBlockPredecessor(bbDef) = bb and
+    ssaDefReachesEndOfBlock(bb, inp, v)
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
+ * basic block `bb`, without crossing another SSA definition of `v`. The read
+ * is of kind `rk`.
+ */
+pragma[nomagic]
+predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
+  ssaDefReachesReadWithinBlock(v, def, bb, i)
+  or
+  variableRead(bb, i, v, _) and
+  ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
+  not ssaDefReachesReadWithinBlock(v, _, bb, i)
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
+ * or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
+ * path between them without any read of `def`.
+ */
+pragma[nomagic]
+predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
+  exists(int rnk |
+    rnk = ssaDefRank(def, _, bb1, i1, _) and
+    rnk + 1 = ssaDefRank(def, _, bb1, i2, SsaRead()) and
+    variableRead(bb1, i2, _, _) and
+    bb2 = bb1
+  )
+  or
+  exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
+  defAdjacentRead(def, bb1, bb2, i2)
+}
+
+private predicate adjacentDefReachesRead(
+  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
+) {
+  adjacentDefRead(def, bb1, i1, bb2, i2) and
+  exists(SourceVariable v | v = def.getSourceVariable() |
+    ssaRef(bb1, i1, v, SsaDef())
+    or
+    variableRead(bb1, i1, v, true)
+  )
+  or
+  exists(BasicBlock bb3, int i3 |
+    adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
+    variableRead(bb3, i3, _, false) and
+    adjacentDefRead(def, bb3, i3, bb2, i2)
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Same as `adjacentDefRead`, but ignores uncertain reads.
+ */
+pragma[nomagic]
+predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
+  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
+  variableRead(bb2, i2, _, true)
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if the node at index `i` in `bb` is a last reference to SSA definition
+ * `def`. The reference is last because it can reach another write `next`,
+ * without passing through another read or write.
+ */
+pragma[nomagic]
+predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
+  exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
+    // Next reference to `v` inside `bb` is a write
+    next.definesAt(v, bb, j) and
+    rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
+    or
+    // Can reach a write using one or more steps
+    rnk = maxSsaRefRank(bb, v) and
+    exists(BasicBlock bb2 |
+      varBlockReaches(def, bb, bb2) and
+      next.definesAt(v, bb2, j) and
+      1 = ssaRefRank(bb2, j, v, SsaDef())
+    )
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if `inp` is an immediately preceding definition of uncertain definition
+ * `def`. Since `def` is uncertain, the value from the preceding definition might
+ * still be valid.
+ */
+pragma[nomagic]
+predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
+  lastRefRedef(inp, _, _, def)
+}
+
+private predicate adjacentDefReachesUncertainRead(
+  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
+) {
+  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
+  variableRead(bb2, i2, _, false)
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Same as `lastRefRedef`, but ignores uncertain reads.
+ */
+pragma[nomagic]
+predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Definition next) {
+  lastRefRedef(def, bb, i, next) and
+  not variableRead(bb, i, def.getSourceVariable(), false)
+  or
+  exists(BasicBlock bb0, int i0 |
+    lastRefRedef(def, bb0, i0, next) and
+    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if the node at index `i` in `bb` is a last reference to SSA
+ * definition `def`.
+ *
+ * That is, the node can reach the end of the enclosing callable, or another
+ * SSA definition for the underlying source variable, without passing through
+ * another read.
+ */
+pragma[nomagic]
+predicate lastRef(Definition def, BasicBlock bb, int i) {
+  lastRefRedef(def, bb, i, _)
+  or
+  exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
+    // Can reach exit directly
+    bb instanceof ExitBasicBlock
+    or
+    // Can reach a block using one or more steps, where `def` is no longer live
+    exists(BasicBlock bb2 | varBlockReaches(def, bb, bb2) |
+      not defOccursInBlock(def, bb2, _) and
+      not ssaDefReachesEndOfBlock(bb2, def, _)
+    )
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Same as `lastRefRedef`, but ignores uncertain reads.
+ */
+pragma[nomagic]
+predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
+  lastRef(def, bb, i) and
+  not variableRead(bb, i, def.getSourceVariable(), false)
+  or
+  exists(BasicBlock bb0, int i0 |
+    lastRef(def, bb0, i0) and
+    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+  )
+}
+
+/** A static single assignment (SSA) definition. */
+class Definition extends TDefinition {
+  /** Gets the source variable underlying this SSA definition. */
+  SourceVariable getSourceVariable() { this.definesAt(result, _, _) }
+
+  /**
+   * Holds if this SSA definition defines `v` at index `i` in basic block `bb`.
+   * Phi nodes are considered to be at index `-1`, while normal variable writes
+   * are at the index of the control flow node they wrap.
+   */
+  final predicate definesAt(SourceVariable v, BasicBlock bb, int i) {
+    this = TWriteDef(v, bb, i)
+    or
+    this = TPhiNode(v, bb) and i = -1
+  }
+
+  /** Gets the basic block to which this SSA definition belongs. */
+  final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
+
+  /** Gets a textual representation of this SSA definition. */
+  string toString() { none() }
+}
+
+/** An SSA definition that corresponds to a write. */
+class WriteDefinition extends Definition, TWriteDef {
+  private SourceVariable v;
+  private BasicBlock bb;
+  private int i;
+
+  WriteDefinition() { this = TWriteDef(v, bb, i) }
+
+  override string toString() { result = "WriteDef" }
+}
+
+/** A phi node. */
+class PhiNode extends Definition, TPhiNode {
+  override string toString() { result = "Phi" }
+}
+
+/**
+ * An SSA definition that represents an uncertain update of the underlying
+ * source variable.
+ */
+class UncertainWriteDefinition extends WriteDefinition {
+  UncertainWriteDefinition() {
+    exists(SourceVariable v, BasicBlock bb, int i |
+      this.definesAt(v, bb, i) and
+      variableWrite(bb, i, v, false)
+    )
+  }
+}

csharp/ql/src/semmle/code/cil/internal/SsaImplSpecific.qll

@@ -0,0 +1,30 @@
+/** Provides the CIL specific parameters for `SsaImplCommon.qll`. */
+
+private import cil
+private import SsaImpl
+
+class BasicBlock = CIL::BasicBlock;
+
+BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
+
+BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
+class ExitBasicBlock = CIL::ExitBasicBlock;
+
+class SourceVariable = CIL::StackVariable;
+
+predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+  forceCachingInSameStage() and
+  exists(CIL::VariableUpdate vu |
+    vu.updatesAt(bb, i) and
+    v = vu.getVariable() and
+    certain = true
+  )
+}
+
+predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+  exists(CIL::ReadAccess ra | bb.getNode(i) = ra |
+    ra.getTarget() = v and
+    certain = true
+  )
+}

csharp/ql/src/semmle/code/csharp/commons/Disposal.qll

@@ -11,14 +11,22 @@ private predicate isDisposeMethod(DotNet::Callable method) {
   method.getNumberOfParameters() = 0
 }
 
+private predicate cilVariableReadFlowsTo(CIL::Variable variable, CIL::DataFlowNode n) {
+  n = variable.getARead()
+  or
+  exists(CIL::DataFlowNode mid |
+    cilVariableReadFlowsTo(variable, mid) and
+    mid.getALocalFlowSucc(n, any(CIL::Untainted u))
+  )
+}
+
 private predicate disposedCilVariable(CIL::Variable variable) {
   // `variable` is the `this` parameter on a dispose method.
   isDisposeMethod(variable.(CIL::ThisParameter).getMethod())
   or
   // `variable` is passed to a method that disposes it.
-  exists(CIL::Call call, CIL::Parameter param, CIL::ReadAccess read |
-    read.getTarget() = variable and
-    read.flowsTo(call.getArgumentForParameter(param)) and
+  exists(CIL::Call call, CIL::Parameter param |
+    cilVariableReadFlowsTo(variable, call.getArgumentForParameter(param)) and
     disposedCilVariable(param)
   )
   or
@@ -27,9 +35,8 @@ private predicate disposedCilVariable(CIL::Variable variable) {
   or
   // A variable is disposed if it's assigned to another variable
   // that may be disposed.
-  exists(CIL::ReadAccess read, CIL::WriteAccess write |
-    read.flowsTo(write.getExpr()) and
-    read.getTarget() = variable and
+  exists(CIL::WriteAccess write |
+    cilVariableReadFlowsTo(variable, write.getExpr()) and
     disposedCilVariable(write.getTarget())
   )
 }