C#: Use shared SSA implementation for PreSsa

config/identical-files.json

@@ -425,5 +425,9 @@
     "java/ql/src/IDEContextual.qll",
     "javascript/ql/src/IDEContextual.qll",
     "python/ql/src/analysis/IDEContextual.qll"
+  ],
+  "SSA C#": [
+    "csharp/ql/src/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
+    "csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll"
   ]
-}
+}

csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll

@@ -995,7 +995,7 @@ module Internal {
   // pre-SSA predicates
   private module PreCFG {
     private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
-    private import semmle.code.csharp.controlflow.internal.PreSsa as PreSsa
+    private import semmle.code.csharp.controlflow.internal.PreSsa
 
     /**
      * Holds if pre-basic-block `bb` only is reached when guard `g` has abstract value `v`,
@@ -1081,25 +1081,25 @@ module Internal {
 
     pragma[noinline]
     private predicate conditionalAssign0(
-      Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
+      Guard guard, AbstractValue vGuard, PreSsa::PhiNode phi, Expr e, PreSsa::Definition upd,
       PreBasicBlocks::PreBasicBlock bbGuard
     ) {
       e = upd.getDefinition().getSource() and
-      upd = def.getAPhiInput() and
+      upd = phi.getAnInput() and
       preControlsDirect(guard, upd.getBasicBlock(), vGuard) and
       bbGuard.getAnElement() = guard and
-      bbGuard.strictlyDominates(def.getBasicBlock()) and
-      not preControlsDirect(guard, def.getBasicBlock(), vGuard)
+      bbGuard.strictlyDominates(phi.getBasicBlock()) and
+      not preControlsDirect(guard, phi.getBasicBlock(), vGuard)
     }
 
     pragma[noinline]
     private predicate conditionalAssign1(
-      Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
+      Guard guard, AbstractValue vGuard, PreSsa::PhiNode phi, Expr e, PreSsa::Definition upd,
       PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
     ) {
-      conditionalAssign0(guard, vGuard, def, e, upd, bbGuard) and
+      conditionalAssign0(guard, vGuard, phi, e, upd, bbGuard) and
       other != upd and
-      other = def.getAPhiInput()
+      other = phi.getAnInput()
     }
 
     pragma[noinline]
@@ -1127,7 +1127,7 @@ module Internal {
     ) {
       conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other) and
       other.getBasicBlock().dominates(bbGuard) and
-      not PreSsa::ssaDefReachesEndOfBlock(getConditionalSuccessor(guard, vGuard), other, _)
+      not other.isLiveAtEndOfBlock(getConditionalSuccessor(guard, vGuard))
     }
 
     /**
@@ -1315,14 +1315,14 @@ module Internal {
      */
     private PreSsa::Definition getADefinition(PreSsa::Definition def, boolean fromBackEdge) {
       result = def and
-      not exists(def.getAPhiInput()) and
+      not def instanceof PreSsa::PhiNode and
       fromBackEdge = false
       or
       exists(PreSsa::Definition input, PreBasicBlocks::PreBasicBlock pred, boolean fbe |
-        input = def.getAPhiInput()
+        input = def.(PreSsa::PhiNode).getAnInput()
       |
         pred = def.getBasicBlock().getAPredecessor() and
-        PreSsa::ssaDefReachesEndOfBlock(pred, input, _) and
+        input.isLiveAtEndOfBlock(pred) and
         result = getADefinition(input, fbe) and
         (if def.getBasicBlock().dominates(pred) then fromBackEdge = true else fromBackEdge = fbe)
       )
@@ -1446,7 +1446,7 @@ module Internal {
       private predicate firstReadSameVarUniquePredecesssor(
         PreSsa::Definition def, AssignableRead read
       ) {
-        PreSsa::firstReadSameVar(def, read) and
+        read = def.getAFirstRead() and
         not exists(AssignableRead other | PreSsa::adjacentReadPairSameVar(other, read) |
           other != read
         )

csharp/ql/src/semmle/code/csharp/controlflow/internal/PreBasicBlocks.qll

@@ -82,13 +82,6 @@ class PreBasicBlock extends ControlFlowElement {
     or
     this.strictlyDominates(bb)
   }
-
-  predicate inDominanceFrontier(PreBasicBlock df) {
-    this.dominatesPredecessor(df) and
-    not this.strictlyDominates(df)
-  }
-
-  private predicate dominatesPredecessor(PreBasicBlock df) { this.dominates(df.getAPredecessor()) }
 }
 
 private Completion getConditionalCompletion(ConditionalCompletion cc) {

csharp/ql/src/semmle/code/csharp/controlflow/internal/PreSsa.qll

@@ -1,370 +1,74 @@
+import csharp
+
 /**
- * INTERNAL: Do not use.
- *
  * Provides an SSA implementation based on "pre-basic-blocks", restricted
  * to local scope variables and fields/properties that behave like local
  * scope variables.
- *
- * The logic is duplicated from the implementation in `SSA.qll`, and
- * being an internal class, all predicate documentation has been removed.
  */
+module PreSsa {
+  import pressa.SsaImplSpecific
+  private import pressa.SsaImplCommon as SsaImpl
 
-import csharp
-private import AssignableDefinitions
-private import PreBasicBlocks
-private import ControlFlowGraphImpl
-private import semmle.code.csharp.controlflow.Guards as Guards
+  class Definition extends SsaImpl::Definition {
+    final AssignableRead getARead() {
+      exists(BasicBlock bb, int i |
+        SsaImpl::ssaDefReachesRead(_, this, bb, i) and
+        result = bb.getElement(i)
+      )
+    }
 
-pragma[noinline]
-private predicate assignableNoCapturing(Assignable a, Callable c) {
-  exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable()) and
-  forall(AssignableDefinition def | def.getTarget() = a |
-    c = def.getEnclosingCallable()
-    or
-    def.getEnclosingCallable() instanceof Constructor
-  )
-}
+    final AssignableDefinition getDefinition() {
+      exists(BasicBlock bb, int i, SourceVariable v |
+        this.definesAt(v, bb, i) and
+        definitionAt(result, bb, i, v)
+      )
+    }
 
-pragma[noinline]
-private predicate assignableNoComplexQualifiers(Assignable a) {
-  forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
-}
+    final AssignableRead getAFirstRead() {
+      exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+        this.definesAt(_, bb1, i1) and
+        SsaImpl::adjacentDefRead(this, bb1, i1, bb2, i2) and
+        result = bb2.getElement(i2)
+      )
+    }
 
-/**
- * A simple assignable. Either a local scope variable or a field/property
- * that behaves like a local scope variable.
- */
-class SimpleAssignable extends Assignable {
-  private Callable c;
+    private Definition getAPhiInputOrPriorDefinition() {
+      result = this.(PhiNode).getAnInput() or
+      SsaImpl::uncertainWriteDefinitionInput(this, result)
+    }
 
-  SimpleAssignable() {
-    (
-      this instanceof LocalScopeVariable
+    final Definition getAnUltimateDefinition() {
+      result = this.getAPhiInputOrPriorDefinition*() and
+      not result instanceof PhiNode
+    }
+
+    final predicate isLiveAtEndOfBlock(BasicBlock bb) {
+      SsaImpl::ssaDefReachesEndOfBlock(bb, this, _)
+    }
+
+    Location getLocation() {
+      result = this.getDefinition().getLocation()
       or
-      this instanceof Field
-      or
-      this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
-    ) and
-    assignableNoCapturing(this, c) and
-    assignableNoComplexQualifiers(this)
+      exists(Callable c, BasicBlock bb, SourceVariable v |
+        this.definesAt(v, bb, -1) and
+        implicitEntryDef(c, bb, v) and
+        result = c.getLocation()
+      )
+    }
   }
 
-  /** Gets a callable in which this simple assignable can be analyzed. */
-  Callable getACallable() { result = c }
-}
+  class PhiNode extends SsaImpl::PhiNode, Definition {
+    final override Location getLocation() { result = this.getBasicBlock().getLocation() }
 
-pragma[noinline]
-private predicate phiNodeMaybeLive(PreBasicBlock bb, SimpleAssignable a) {
-  exists(PreBasicBlock def | defAt(def, _, _, a) | def.inDominanceFrontier(bb))
-}
-
-private newtype TPreSsaDef =
-  TExplicitPreSsaDef(PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a) {
-    assignableDefAtLive(bb, i, def, a)
-  } or
-  TImplicitEntryPreSsaDef(Callable c, PreBasicBlock bb, Assignable a) {
-    implicitEntryDef(c, bb, a) and
-    liveAtEntry(bb, a)
-  } or
-  TPhiPreSsaDef(PreBasicBlock bb, SimpleAssignable a) {
-    phiNodeMaybeLive(bb, a) and
-    liveAtEntry(bb, a)
+    final Definition getAnInput() { SsaImpl::phiHasInputFromBlock(this, result, _) }
   }
 
-class Definition extends TPreSsaDef {
-  string toString() {
-    exists(AssignableDefinition def | this = TExplicitPreSsaDef(_, _, def, _) |
-      result = def.toString()
-    )
-    or
-    exists(SimpleAssignable a | this = TImplicitEntryPreSsaDef(_, _, a) |
-      result = "implicit(" + a + ")"
-    )
-    or
-    exists(SimpleAssignable a | this = TPhiPreSsaDef(_, a) | result = "phi(" + a.toString() + ")")
-  }
-
-  SimpleAssignable getAssignable() {
-    this = TExplicitPreSsaDef(_, _, _, result)
-    or
-    this = TImplicitEntryPreSsaDef(_, _, result)
-    or
-    this = TPhiPreSsaDef(_, result)
-  }
-
-  AssignableRead getARead() {
-    firstReadSameVar(this, result)
-    or
-    exists(AssignableRead read | firstReadSameVar(this, read) |
-      adjacentReadPairSameVar+(read, result)
+  predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
+    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+      read1 = bb1.getElement(i1) and
+      variableRead(bb1, i1, _, true) and
+      SsaImpl::adjacentDefRead(_, bb1, i1, bb2, i2) and
+      read2 = bb2.getElement(i2)
     )
   }
-
-  Location getLocation() {
-    exists(AssignableDefinition def | this = TExplicitPreSsaDef(_, _, def, _) |
-      result = def.getLocation()
-    )
-    or
-    exists(Callable c | this = TImplicitEntryPreSsaDef(c, _, _) | result = c.getLocation())
-    or
-    exists(PreBasicBlock bb | this = TPhiPreSsaDef(bb, _) | result = bb.getLocation())
-  }
-
-  PreBasicBlock getBasicBlock() {
-    this = TExplicitPreSsaDef(result, _, _, _)
-    or
-    this = TImplicitEntryPreSsaDef(_, result, _)
-    or
-    this = TPhiPreSsaDef(result, _)
-  }
-
-  Callable getCallable() { result = this.getBasicBlock().getEnclosingCallable() }
-
-  AssignableDefinition getDefinition() { this = TExplicitPreSsaDef(_, _, result, _) }
-
-  Definition getAPhiInput() {
-    exists(PreBasicBlock bb, PreBasicBlock phiPred, SimpleAssignable a |
-      this = TPhiPreSsaDef(bb, a)
-    |
-      bb.getAPredecessor() = phiPred and
-      ssaDefReachesEndOfBlock(phiPred, result, a)
-    )
-  }
-
-  Definition getAnUltimateDefinition() {
-    result = this.getAPhiInput*() and
-    not result = TPhiPreSsaDef(_, _)
-  }
-}
-
-predicate implicitEntryDef(Callable c, PreBasicBlock bb, SimpleAssignable a) {
-  not a instanceof LocalScopeVariable and
-  c = a.getACallable() and
-  scopeFirst(c, bb)
-}
-
-private predicate assignableDefAt(
-  PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a
-) {
-  bb.getElement(i) = def.getExpr() and
-  a = def.getTarget() and
-  // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
-  not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
-    second.getAssignment() = first.getAssignment() and
-    second.getEvaluationOrder() > first.getEvaluationOrder() and
-    second.getTarget() = a
-  )
-  or
-  def.(ImplicitParameterDefinition).getParameter() = a and
-  exists(Callable c | a = c.getAParameter() |
-    scopeFirst(c, bb) and
-    i = -1
-  )
-}
-
-private predicate readAt(PreBasicBlock bb, int i, AssignableRead read, SimpleAssignable a) {
-  read = bb.getElement(i) and
-  read.getTarget() = a
-}
-
-pragma[noinline]
-private predicate exitBlock(PreBasicBlock bb, Callable c) {
-  scopeLast(c, bb.getLastElement(), _) and
-  c = bb.getEnclosingCallable()
-}
-
-private predicate outRefExitRead(PreBasicBlock bb, int i, LocalScopeVariable v) {
-  exitBlock(bb, v.getCallable()) and
-  i = bb.length() + 1 and
-  (v.isRef() or v.(Parameter).isOut())
-}
-
-private newtype RefKind =
-  Read() or
-  Write(boolean certain) { certain = true or certain = false }
-
-private predicate ref(PreBasicBlock bb, int i, SimpleAssignable a, RefKind k) {
-  (readAt(bb, i, _, a) or outRefExitRead(bb, i, a)) and
-  k = Read()
-  or
-  exists(AssignableDefinition def, boolean certain | assignableDefAt(bb, i, def, a) |
-    (if def.getTargetAccess().isRefArgument() then certain = false else certain = true) and
-    k = Write(certain)
-  )
-}
-
-private int refRank(PreBasicBlock bb, int i, SimpleAssignable a, RefKind k) {
-  i = rank[result](int j | ref(bb, j, a, _)) and
-  ref(bb, i, a, k)
-}
-
-private int maxRefRank(PreBasicBlock bb, SimpleAssignable a) {
-  result = refRank(bb, _, a, _) and
-  not result + 1 = refRank(bb, _, a, _)
-}
-
-private int firstReadOrCertainWrite(PreBasicBlock bb, SimpleAssignable a) {
-  result =
-    min(int r, RefKind k |
-      r = refRank(bb, _, a, k) and
-      k != Write(false)
-    |
-      r
-    )
-}
-
-predicate liveAtEntry(PreBasicBlock bb, SimpleAssignable a) {
-  refRank(bb, _, a, Read()) = firstReadOrCertainWrite(bb, a)
-  or
-  not exists(firstReadOrCertainWrite(bb, a)) and
-  liveAtExit(bb, a)
-}
-
-private predicate liveAtExit(PreBasicBlock bb, SimpleAssignable a) {
-  liveAtEntry(bb.getASuccessor(), a)
-}
-
-predicate assignableDefAtLive(PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a) {
-  assignableDefAt(bb, i, def, a) and
-  exists(int rnk | rnk = refRank(bb, i, a, Write(_)) |
-    rnk + 1 = refRank(bb, _, a, Read())
-    or
-    rnk = maxRefRank(bb, a) and
-    liveAtExit(bb, a)
-  )
-}
-
-predicate defAt(PreBasicBlock bb, int i, Definition def, SimpleAssignable a) {
-  def = TExplicitPreSsaDef(bb, i, _, a)
-  or
-  def = TImplicitEntryPreSsaDef(_, bb, a) and i = -1
-  or
-  def = TPhiPreSsaDef(bb, a) and i = -1
-}
-
-private newtype SsaRefKind =
-  SsaRead() or
-  SsaDef()
-
-private predicate ssaRef(PreBasicBlock bb, int i, SimpleAssignable a, SsaRefKind k) {
-  readAt(bb, i, _, a) and
-  k = SsaRead()
-  or
-  defAt(bb, i, _, a) and
-  k = SsaDef()
-}
-
-private int ssaRefRank(PreBasicBlock bb, int i, SimpleAssignable a, SsaRefKind k) {
-  i = rank[result](int j | ssaRef(bb, j, a, _)) and
-  ssaRef(bb, i, a, k)
-}
-
-private predicate defReachesRank(PreBasicBlock bb, Definition def, SimpleAssignable a, int rnk) {
-  exists(int i |
-    rnk = ssaRefRank(bb, i, a, SsaDef()) and
-    defAt(bb, i, def, a)
-  )
-  or
-  defReachesRank(bb, def, a, rnk - 1) and
-  rnk = ssaRefRank(bb, _, a, SsaRead())
-}
-
-private int maxSsaRefRank(PreBasicBlock bb, SimpleAssignable a) {
-  result = ssaRefRank(bb, _, a, _) and
-  not result + 1 = ssaRefRank(bb, _, a, _)
-}
-
-pragma[noinline]
-private predicate ssaDefReachesEndOfBlockRec(PreBasicBlock bb, Definition def, SimpleAssignable a) {
-  exists(PreBasicBlock idom | ssaDefReachesEndOfBlock(idom, def, a) | idom.immediatelyDominates(bb))
-}
-
-predicate ssaDefReachesEndOfBlock(PreBasicBlock bb, Definition def, SimpleAssignable a) {
-  exists(int last | last = maxSsaRefRank(bb, a) |
-    defReachesRank(bb, def, a, last) and
-    liveAtExit(bb, a)
-  )
-  or
-  ssaDefReachesEndOfBlockRec(bb, def, a) and
-  liveAtExit(bb, a) and
-  not ssaRef(bb, _, a, SsaDef())
-}
-
-private predicate ssaDefReachesReadWithinBlock(
-  SimpleAssignable a, Definition def, PreBasicBlock bb, int i
-) {
-  defReachesRank(bb, def, a, ssaRefRank(bb, i, a, SsaRead()))
-}
-
-private predicate ssaDefReachesRead(SimpleAssignable a, Definition def, PreBasicBlock bb, int i) {
-  ssaDefReachesReadWithinBlock(a, def, bb, i)
-  or
-  ssaRef(bb, i, a, SsaRead()) and
-  ssaDefReachesEndOfBlock(bb.getAPredecessor(), def, a) and
-  not ssaDefReachesReadWithinBlock(a, _, bb, i)
-}
-
-private int ssaDefRank(Definition def, PreBasicBlock bb, int i) {
-  exists(SimpleAssignable a |
-    a = def.getAssignable() and
-    result = ssaRefRank(bb, i, a, _)
-  |
-    ssaDefReachesRead(a, def, bb, i)
-    or
-    defAt(bb, i, def, a)
-  )
-}
-
-private predicate varOccursInBlock(Definition def, PreBasicBlock bb, SimpleAssignable a) {
-  exists(ssaDefRank(def, bb, _)) and
-  a = def.getAssignable()
-}
-
-pragma[noinline]
-private PreBasicBlock getAMaybeLiveSuccessor(Definition def, PreBasicBlock bb) {
-  result = bb.getASuccessor() and
-  not varOccursInBlock(_, bb, def.getAssignable()) and
-  ssaDefReachesEndOfBlock(bb, def, _)
-}
-
-private predicate varBlockReaches(Definition def, PreBasicBlock bb1, PreBasicBlock bb2) {
-  varOccursInBlock(def, bb1, _) and
-  bb2 = bb1.getASuccessor()
-  or
-  exists(PreBasicBlock mid | varBlockReaches(def, bb1, mid) |
-    bb2 = getAMaybeLiveSuccessor(def, mid)
-  )
-}
-
-private predicate varBlockReachesRead(Definition def, PreBasicBlock bb1, AssignableRead read) {
-  exists(PreBasicBlock bb2, int i2 |
-    varBlockReaches(def, bb1, bb2) and
-    ssaRefRank(bb2, i2, def.getAssignable(), SsaRead()) = 1 and
-    readAt(bb2, i2, read, _)
-  )
-}
-
-private predicate adjacentVarRead(Definition def, PreBasicBlock bb1, int i1, AssignableRead read) {
-  exists(int rankix, int i2 |
-    rankix = ssaDefRank(def, bb1, i1) and
-    rankix + 1 = ssaDefRank(def, bb1, i2) and
-    readAt(bb1, i2, read, _)
-  )
-  or
-  ssaDefRank(def, bb1, i1) = maxSsaRefRank(bb1, def.getAssignable()) and
-  varBlockReachesRead(def, bb1, read)
-}
-
-predicate firstReadSameVar(Definition def, AssignableRead read) {
-  exists(PreBasicBlock bb1, int i1 |
-    defAt(bb1, i1, def, _) and
-    adjacentVarRead(def, bb1, i1, read)
-  )
-}
-
-predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
-  exists(Definition def, PreBasicBlock bb1, int i1 |
-    readAt(bb1, i1, read1, _) and
-    adjacentVarRead(def, bb1, i1, read2)
-  )
 }

csharp/ql/src/semmle/code/csharp/controlflow/internal/Splitting.qll

@@ -6,10 +6,10 @@
 
 import csharp
 private import Completion
-private import PreSsa as PreSsa
 private import ControlFlowGraphImpl
 private import SuccessorTypes
 private import semmle.code.csharp.controlflow.ControlFlowGraph::ControlFlow
+private import semmle.code.csharp.controlflow.internal.PreSsa
 
 /** The maximum number of splits allowed for a given node. */
 private int maxSplits() { result = 5 }
@@ -1143,9 +1143,7 @@ module BooleanSplitting {
      * another condition that reads the same SSA variable.
      */
     private predicate firstDefCondition(ConditionBlock cb) {
-      exists(AssignableRead read | this.defConditionReachableFromRead(cb, read) |
-        PreSsa::firstReadSameVar(def, read)
-      )
+      this.defConditionReachableFromRead(cb, def.getAFirstRead())
     }
 
     override predicate correlatesConditions(ConditionBlock cb1, ConditionBlock cb2, boolean inverted) {
@@ -1168,9 +1166,9 @@ module BooleanSplitting {
       )
     }
 
-    override Callable getEnclosingCallable() { result = def.getCallable() }
+    override Callable getEnclosingCallable() { result = def.getBasicBlock().getEnclosingCallable() }
 
-    override string toString() { result = def.getAssignable().toString() }
+    override string toString() { result = def.getSourceVariable().toString() }
 
     override Location getLocation() { result = def.getLocation() }
   }
@@ -1321,7 +1319,6 @@ module BooleanSplitting {
 module LoopSplitting {
   private import semmle.code.csharp.controlflow.Guards as Guards
   private import PreBasicBlocks
-  private import PreSsa
 
   /** Holds if `ce` is guarded by a (non-)empty check, as specified by `v`. */
   private predicate emptinessGuarded(

csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/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/csharp/controlflow/internal/pressa/SsaImplSpecific.qll

@@ -0,0 +1,106 @@
+/** Provides the C# specific parameters for `SsaImplCommon.qll`. */
+
+private import csharp
+private import AssignableDefinitions
+private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
+
+class BasicBlock = PreBasicBlocks::PreBasicBlock;
+
+BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
+
+BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
+class ExitBasicBlock extends BasicBlock {
+  ExitBasicBlock() { scopeLast(_, this.getLastElement(), _) }
+}
+
+pragma[noinline]
+private predicate assignableNoCapturing(Assignable a, Callable c) {
+  exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable()) and
+  forall(AssignableDefinition def | def.getTarget() = a |
+    c = def.getEnclosingCallable()
+    or
+    def.getEnclosingCallable() instanceof Constructor
+  )
+}
+
+pragma[noinline]
+private predicate assignableNoComplexQualifiers(Assignable a) {
+  forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
+}
+
+/**
+ * A simple assignable. Either a local scope variable or a field/property
+ * that behaves like a local scope variable.
+ */
+class SourceVariable extends Assignable {
+  private Callable c;
+
+  SourceVariable() {
+    (
+      this instanceof LocalScopeVariable
+      or
+      this instanceof Field
+      or
+      this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
+    ) and
+    assignableNoCapturing(this, c) and
+    assignableNoComplexQualifiers(this)
+  }
+
+  /** Gets a callable in which this simple assignable can be analyzed. */
+  Callable getACallable() { result = c }
+}
+
+predicate definitionAt(AssignableDefinition def, BasicBlock bb, int i, SourceVariable v) {
+  bb.getElement(i) = def.getExpr() and
+  v = def.getTarget() and
+  // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
+  not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
+    second.getAssignment() = first.getAssignment() and
+    second.getEvaluationOrder() > first.getEvaluationOrder() and
+    second.getTarget() = v
+  )
+  or
+  def.(ImplicitParameterDefinition).getParameter() = v and
+  exists(Callable c | v = c.getAParameter() |
+    scopeFirst(c, bb) and
+    i = -1
+  )
+}
+
+predicate implicitEntryDef(Callable c, BasicBlock bb, SourceVariable v) {
+  not v instanceof LocalScopeVariable and
+  c = v.getACallable() and
+  scopeFirst(c, bb)
+}
+
+predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+  exists(AssignableDefinition def |
+    definitionAt(def, bb, i, v) and
+    if def.getTargetAccess().isRefArgument() then certain = false else certain = true
+  )
+  or
+  exists(Callable c |
+    implicitEntryDef(c, bb, v) and
+    i = -1 and
+    certain = true
+  )
+}
+
+predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+  exists(AssignableRead read |
+    read = bb.getElement(i) and
+    read.getTarget() = v and
+    certain = true
+  )
+  or
+  v =
+    any(LocalScopeVariable lsv |
+      lsv.getCallable() = bb.(ExitBasicBlock).getEnclosingCallable() and
+      i = bb.length() and
+      (lsv.isRef() or v.(Parameter).isOut()) and
+      certain = false
+    )
+}

csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql

@@ -1,5 +1,5 @@
 import csharp
-import semmle.code.csharp.controlflow.internal.PreSsa as PreSsa
+import semmle.code.csharp.controlflow.internal.PreSsa
 import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
 import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
 
@@ -7,16 +7,14 @@ class CallableWithSplitting extends Callable {
   CallableWithSplitting() { this = any(SplitControlFlowElement e).getEnclosingCallable() }
 }
 
-query predicate defReadInconsistency(
-  AssignableRead ar, Expr e, PreSsa::SimpleAssignable a, boolean b
-) {
+query predicate defReadInconsistency(AssignableRead ar, Expr e, PreSsa::SourceVariable v, boolean b) {
   // Exclude definitions in callables with CFG splitting, as SSA definitions may be
   // very different from pre-SSA definitions
   not ar.getEnclosingCallable() instanceof CallableWithSplitting and
   exists(AssignableDefinition def | e = def.getExpr() |
     b = true and
-    exists(PreSsa::Definition ssaDef | ssaDef.getAssignable() = a |
-      PreSsa::firstReadSameVar(ssaDef, ar) and
+    exists(PreSsa::Definition ssaDef | ssaDef.getSourceVariable() = v |
+      ar = ssaDef.getAFirstRead() and
       ssaDef.getDefinition() = def and
       not exists(Ssa::ExplicitDefinition edef |
         edef.getADefinition() = def and
@@ -28,9 +26,9 @@ query predicate defReadInconsistency(
     exists(Ssa::ExplicitDefinition edef |
       edef.getADefinition() = def and
       edef.getAFirstRead() = ar and
-      def.getTarget() = a and
+      def.getTarget() = v and
       not exists(PreSsa::Definition ssaDef |
-        PreSsa::firstReadSameVar(ssaDef, ar) and
+        ar = ssaDef.getAFirstRead() and
         ssaDef.getDefinition() = def
       )
     )
@@ -38,21 +36,21 @@ query predicate defReadInconsistency(
 }
 
 query predicate readReadInconsistency(
-  LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SimpleAssignable a, boolean b
+  LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SourceVariable v, boolean b
 ) {
   // Exclude definitions in callables with CFG splitting, as SSA definitions may be
   // very different from pre-SSA definitions
   not read1.getEnclosingCallable() instanceof CallableWithSplitting and
   (
     b = true and
-    a = read1.getTarget() and
+    v = read1.getTarget() and
     PreSsa::adjacentReadPairSameVar(read1, read2) and
     not SsaImpl::adjacentReadPairSameVar(_, read1.getAControlFlowNode(), read2.getAControlFlowNode())
     or
     b = false and
-    a = read1.getTarget() and
+    v = read1.getTarget() and
     SsaImpl::adjacentReadPairSameVar(_, read1.getAControlFlowNode(), read2.getAControlFlowNode()) and
-    read1.getTarget() instanceof PreSsa::SimpleAssignable and
+    read1.getTarget() instanceof PreSsa::SourceVariable and
     not PreSsa::adjacentReadPairSameVar(read1, read2) and
     // Exclude split CFG elements because SSA may be more precise than pre-SSA
     // in those cases
@@ -61,17 +59,15 @@ query predicate readReadInconsistency(
   )
 }
 
-query predicate phiInconsistency(
-  ControlFlowElement cfe, Expr e, PreSsa::SimpleAssignable a, boolean b
-) {
+query predicate phiInconsistency(ControlFlowElement cfe, Expr e, PreSsa::SourceVariable v, boolean b) {
   // Exclude definitions in callables with CFG splitting, as SSA definitions may be
   // very different from pre-SSA definitions
   not cfe.getEnclosingCallable() instanceof CallableWithSplitting and
   exists(AssignableDefinition adef | e = adef.getExpr() |
     b = true and
-    exists(PreSsa::Definition def | a = def.getAssignable() |
-      adef = def.getAPhiInput+().getDefinition() and
-      cfe = def.getBasicBlock().getFirstElement() and
+    exists(PreSsa::PhiNode prePhi | v = prePhi.getSourceVariable() |
+      adef = prePhi.getAnInput+().getDefinition() and
+      cfe = prePhi.getBasicBlock().getFirstElement() and
       not exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
         edef = phi.getAnUltimateDefinition()
       |
@@ -83,15 +79,15 @@ query predicate phiInconsistency(
     or
     b = false and
     exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
-      a = phi.getSourceVariable().getAssignable()
+      v = phi.getSourceVariable().getAssignable()
     |
       edef = phi.getAnUltimateDefinition() and
       edef.getADefinition() = adef and
       phi.definesAt(_, bb, _) and
       cfe = bb.getFirstNode().getElement() and
-      not exists(PreSsa::Definition def |
-        adef = def.getAPhiInput+().getDefinition() and
-        cfe = def.getBasicBlock().getFirstElement()
+      not exists(PreSsa::PhiNode prePhi |
+        adef = prePhi.getAnInput+().getDefinition() and
+        cfe = prePhi.getBasicBlock().getFirstElement()
       )
     )
   )