diff --git a/codeql b/codeql
index 65ea01e1455..cf860f1dac4 160000
--- a/codeql
+++ b/codeql
@@ -1 +1 @@
-Subproject commit 65ea01e1455b5f8c0f12a804f0d4715d64681d8c
+Subproject commit cf860f1dac4ab74df67c147ec63bca4184ac5d86
diff --git a/ql/src/codeql_ruby/dataflow/SSA.qll b/ql/src/codeql_ruby/dataflow/SSA.qll
index de2604cb238..e83927e5de6 100644
--- a/ql/src/codeql_ruby/dataflow/SSA.qll
+++ b/ql/src/codeql_ruby/dataflow/SSA.qll
@@ -48,13 +48,7 @@ module Ssa {
      * end
      * ```
      */
-    final VariableReadAccessCfgNode getARead() {
-      exists(LocalVariable v, BasicBlock bb, int i |
-        SsaImplCommon::ssaDefReachesRead(v, this, bb, i) and
-        SsaImpl::variableReadActual(bb, i, v) and
-        result = bb.getNode(i)
-      )
-    }
+    final VariableReadAccessCfgNode getARead() { result = SsaImpl::getARead(this) }
 
     /**
      * Gets a first control-flow node that reads the value of this SSA definition.
@@ -143,6 +137,15 @@ module Ssa {
       SsaImpl::adjacentReadPair(this, read1, read2)
     }
 
+    /**
+     * Gets an SSA definition whose value can flow to this one in one step. This
+     * includes inputs to phi nodes and the prior definitions of uncertain writes.
+     */
+    private Definition getAPhiInputOrPriorDefinition() {
+      result = this.(PhiNode).getAnInput() or
+      result = this.(CapturedCallDefinition).getPriorDefinition()
+    }
+
     /**
      * Gets a definition that ultimately defines this SSA definition and is
      * not itself a phi node.
@@ -168,8 +171,9 @@ module Ssa {
      * end
      * ```
      */
-    final override Definition getAnUltimateDefinition() {
-      result = SsaImplCommon::Definition.super.getAnUltimateDefinition()
+    final Definition getAnUltimateDefinition() {
+      result = this.getAPhiInputOrPriorDefinition*() and
+      not result instanceof PhiNode
     }
 
     override string toString() { result = this.getControlFlowNode().toString() }
@@ -284,9 +288,11 @@ module Ssa {
       )
     }
 
-    final override Definition getPriorDefinition() {
-      result = SsaImplCommon::UncertainWriteDefinition.super.getPriorDefinition()
-    }
+    /**
+     * Gets the immediately preceding definition. Since this update is uncertain,
+     * the value from the preceding definition might still be valid.
+     */
+    final Definition getPriorDefinition() { result = SsaImpl::uncertainWriteDefinitionInput(this) }
 
     override string toString() { result = this.getControlFlowNode().toString() }
   }
@@ -330,7 +336,12 @@ module Ssa {
      * end
      * ```
      */
-    final override Definition getAnInput() { result = SsaImplCommon::PhiNode.super.getAnInput() }
+    final Definition getAnInput() { this.hasInputFromBlock(result, _) }
+
+    /** Holds if `inp` is an input to this phi node along the edge originating in `bb`. */
+    predicate hasInputFromBlock(Definition inp, BasicBlock bb) {
+      inp = SsaImpl::phiHasInputFromBlock(this, bb)
+    }
 
     private string getSplitString() {
       result = this.getBasicBlock().getFirstNode().(CfgNodes::AstCfgNode).getSplitsString()
diff --git a/ql/src/codeql_ruby/dataflow/internal/SsaImpl.qll b/ql/src/codeql_ruby/dataflow/internal/SsaImpl.qll
index 0478ac7b20f..3f7d066ad83 100644
--- a/ql/src/codeql_ruby/dataflow/internal/SsaImpl.qll
+++ b/ql/src/codeql_ruby/dataflow/internal/SsaImpl.qll
@@ -102,23 +102,22 @@ private predicate hasCapturedWrite(Variable v, CfgScope scope) {
 }
 
 /** Holds if `v` is read at index `i` in basic block `bb`. */
-predicate variableReadActual(BasicBlock bb, int i, LocalVariable v) {
+private predicate variableReadActual(BasicBlock bb, int i, LocalVariable v) {
   exists(VariableReadAccess read |
     read.getVariable() = v and
     read = bb.getNode(i).getNode()
   )
 }
 
-/**
- * Holds if a pseudo read of `v` is inserted at index `i` in basic block `bb`.
- *
- * Pseudo reads are used to make otherwise dead assignments live, as they will
- * otherwise not get an SSA definition.
- */
-predicate variableReadPseudo(BasicBlock bb, int i, LocalVariable v) {
-  capturedCallRead(bb, i, v)
+predicate variableRead(BasicBlock bb, int i, LocalVariable v, boolean certain) {
+  variableReadActual(bb, i, v) and
+  certain = true
   or
-  capturedExitRead(bb, i, v)
+  capturedCallRead(bb, i, v) and
+  certain = false
+  or
+  capturedExitRead(bb, i, v) and
+  certain = false
 }
 
 pragma[noinline]
@@ -131,49 +130,6 @@ private predicate hasVariableReadWithCapturedWrite(BasicBlock bb, LocalVariable
   )
 }
 
-private predicate adjacentDefReaches(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
-  adjacentDefRead(def, bb1, i1, bb2, i2)
-  or
-  exists(BasicBlock bb3, int i3 |
-    adjacentDefReaches(def, bb1, i1, bb3, i3) and
-    variableReadPseudo(bb3, i3, _) and
-    adjacentDefRead(def, bb3, i3, bb2, i2)
-  )
-}
-
-pragma[noinline]
-private predicate adjacentDefActualRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
-) {
-  adjacentDefReaches(def, bb1, i1, bb2, i2) and
-  variableReadActual(bb2, i2, _)
-}
-
-private predicate adjacentDefPseudoRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
-) {
-  adjacentDefReaches(def, bb1, i1, bb2, i2) and
-  variableReadPseudo(bb2, i2, _)
-}
-
-private predicate reachesLastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
-  lastRefRedef(def, bb, i, next)
-  or
-  exists(BasicBlock bb0, int i0 |
-    reachesLastRefRedef(def, bb0, i0, next) and
-    adjacentDefPseudoRead(def, bb, i, bb0, i0)
-  )
-}
-
-private predicate reachesLastRef(Definition def, BasicBlock bb, int i) {
-  lastRef(def, bb, i)
-  or
-  exists(BasicBlock bb0, int i0 |
-    reachesLastRef(def, bb0, i0) and
-    adjacentDefPseudoRead(def, bb, i, bb0, i0)
-  )
-}
-
 cached
 private module Cached {
   /**
@@ -211,6 +167,20 @@ private module Cached {
     )
   }
 
+  cached
+  VariableReadAccessCfgNode getARead(Definition def) {
+    exists(LocalVariable v, BasicBlock bb, int i |
+      ssaDefReachesRead(v, def, bb, i) and
+      variableReadActual(bb, i, v) and
+      result = bb.getNode(i)
+    )
+  }
+
+  cached
+  Definition phiHasInputFromBlock(PhiNode phi, BasicBlock bb) {
+    phiHasInputFromBlock(phi, result, bb)
+  }
+
   /**
    * Holds if the value defined at SSA definition `def` can reach a read at `read`,
    * without passing through any other non-pseudo read.
@@ -219,7 +189,7 @@ private module Cached {
   predicate firstRead(Definition def, VariableReadAccessCfgNode read) {
     exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
       def.definesAt(_, bb1, i1) and
-      adjacentDefActualRead(def, bb1, i1, bb2, i2) and
+      adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
       read = bb2.getNode(i2)
     )
   }
@@ -236,7 +206,7 @@ private module Cached {
     exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
       read1 = bb1.getNode(i1) and
       variableReadActual(bb1, i1, _) and
-      adjacentDefActualRead(def, bb1, i1, bb2, i2) and
+      adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
       read2 = bb2.getNode(i2)
     )
   }
@@ -249,7 +219,7 @@ private module Cached {
   cached
   predicate lastRead(Definition def, VariableReadAccessCfgNode read) {
     exists(BasicBlock bb, int i |
-      reachesLastRef(def, bb, i) and
+      lastRefNoUncertainReads(def, bb, i) and
       variableReadActual(bb, i, _) and
       read = bb.getNode(i)
     )
@@ -264,8 +234,12 @@ private module Cached {
    */
   cached
   predicate lastRefBeforeRedef(Definition def, BasicBlock bb, int i, Definition next) {
-    reachesLastRefRedef(def, bb, i, next) and
-    not variableReadPseudo(bb, i, def.getSourceVariable())
+    lastRefRedefNoUncertainReads(def, bb, i, next)
+  }
+
+  cached
+  Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
+    uncertainWriteDefinitionInput(def, result)
   }
 }
 
diff --git a/ql/src/codeql_ruby/dataflow/internal/SsaImplCommon.qll b/ql/src/codeql_ruby/dataflow/internal/SsaImplCommon.qll
index 8bfef0053ac..be01c05b8fa 100644
--- a/ql/src/codeql_ruby/dataflow/internal/SsaImplCommon.qll
+++ b/ql/src/codeql_ruby/dataflow/internal/SsaImplCommon.qll
@@ -7,501 +7,570 @@ 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
-private module 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()
+
   /**
-   * Liveness analysis (based on source variables) to restrict the size of the
-   * SSA representation.
+   * A classification of SSA variable references into reads and definitions.
    */
-  private module Liveness {
-    /**
-     * A classification of variable references into reads (of a given kind) and
-     * (certain or uncertain) writes.
-     */
-    private newtype TRefKind =
-      Read() or
-      Write(boolean certain) { certain = true or certain = false }
-
-    private class RefKind extends TRefKind {
-      string toString() {
-        this = Read() and result = "read"
-        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) {
-      variableRead(bb, i, v) and k = Read()
+  class SsaRefKind extends TSsaRefKind {
+    string toString() {
+      this = SsaRead() and
+      result = "SsaRead"
       or
-      exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
+      this = SsaDef() and
+      result = "SsaDef"
     }
 
-    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)
+    int getOrder() {
+      this = SsaRead() and
+      result = 0
       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)
+      this = SsaDef() and
+      result = 1
     }
-
-    /**
-     * 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`.
+   * 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.
    */
-  pragma[noinline]
-  private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) {
-    exists(BasicBlock defbb, Definition def |
-      def.definesAt(v, defbb, _) and
-      inDominanceFrontier(defbb, bb)
-    )
+  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()
   }
 
-  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 newtype OrderedSsaRefIndex =
+    MkOrderedSsaRefIndex(int i, SsaRefKind k) { ssaRef(_, i, _, k) }
 
-  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)
-    )
+  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()
   }
 
   /**
-   * 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`.
+   * 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.
    */
-  cached
-  predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
-    exists(int last | last = maxSsaRefRank(bb, v) |
-      ssaDefReachesRank(bb, def, last, v) and
-      liveAtExit(bb, v)
+  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
-    ssaDefReachesEndOfBlockRec(bb, def, v) and
-    liveAtExit(bb, v) and
-    not ssaRef(bb, _, v, SsaDef())
+    ssaDefReachesRank(bb, def, rnk - 1, v) and
+    rnk = ssaRefRank(bb, _, v, SsaRead())
   }
 
   /**
-   * 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`.
+   * 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`.
    */
-  cached
-  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)
+  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` without crossing another SSA definition of `v`.
+   * `redef` in the same basic block, without crossing another SSA definition of `v`.
    */
-  cached
-  predicate ssaDefReachesUncertainDef(
+  predicate ssaDefReachesUncertainDefWithinBlock(
     SourceVariable v, Definition def, UncertainWriteDefinition redef
   ) {
-    ssaDefReachesUncertainDefWithinBlock(v, def, redef)
-    or
-    exists(BasicBlock bb |
-      redef.definesAt(v, bb, _) and
-      ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
-      not ssaDefReachesUncertainDefWithinBlock(v, _, 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)
     )
   }
 
   /**
-   * 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`.
+   * Same as `ssaRefRank()`, but restricted to a particular SSA definition `def`.
    */
-  cached
-  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)
-  }
-
-  /**
-   * 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.
-   */
-  cached
-  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())
+  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
-      // 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())
-      )
+      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 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.
+   * 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`.
    */
-  cached
-  predicate lastRef(Definition def, BasicBlock bb, int i) {
-    lastRefRedef(def, bb, i, _)
+  predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
+    defOccursInBlock(def, bb1, _) and
+    bb2 = getABasicBlockSuccessor(bb1)
     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, _)
-      )
-    )
+    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, _, _)
   }
 }
 
-import Cached
+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 is this SSA definition is live at the end of basic block `bb`.
-   * That is, this definition reaches the end of basic block `bb`, at which
-   * point it is still live, without crossing another SSA definition of the
-   * same source variable.
-   */
-  final predicate isLiveAtEndOfBlock(BasicBlock bb) { ssaDefReachesEndOfBlock(bb, this, _) }
-
   /**
    * 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
@@ -516,24 +585,6 @@ class Definition extends TDefinition {
   /** Gets the basic block to which this SSA definition belongs. */
   final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
 
-  /**
-   * Gets an SSA definition whose value can flow to this one in one step. This
-   * includes inputs to phi nodes and the prior definitions of uncertain writes.
-   */
-  private Definition getAPseudoInputOrPriorDefinition() {
-    result = this.(PhiNode).getAnInput() or
-    result = this.(UncertainWriteDefinition).getPriorDefinition()
-  }
-
-  /**
-   * Gets a definition that ultimately defines this SSA definition and is
-   * not itself a phi node.
-   */
-  Definition getAnUltimateDefinition() {
-    result = this.getAPseudoInputOrPriorDefinition*() and
-    not result instanceof PhiNode
-  }
-
   /** Gets a textual representation of this SSA definition. */
   string toString() { none() }
 }
@@ -551,22 +602,6 @@ class WriteDefinition extends Definition, TWriteDef {
 
 /** A phi node. */
 class PhiNode extends Definition, TPhiNode {
-  /** Gets an input of this phi node. */
-  Definition getAnInput() {
-    exists(BasicBlock bb, BasicBlock pred, SourceVariable v |
-      this.definesAt(v, bb, _) and
-      getABasicBlockPredecessor(bb) = pred and
-      ssaDefReachesEndOfBlock(pred, result, v)
-    )
-  }
-
-  /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
-  predicate hasInputFromBlock(Definition inp, BasicBlock bb) {
-    inp = this.getAnInput() and
-    getABasicBlockPredecessor(this.getBasicBlock()) = bb and
-    ssaDefReachesEndOfBlock(bb, inp, _)
-  }
-
   override string toString() { result = "Phi" }
 }
 
@@ -581,10 +616,4 @@ class UncertainWriteDefinition extends WriteDefinition {
       variableWrite(bb, i, v, false)
     )
   }
-
-  /**
-   * Gets the immediately preceding definition. Since this update is uncertain,
-   * the value from the preceding definition might still be valid.
-   */
-  Definition getPriorDefinition() { ssaDefReachesUncertainDef(_, result, this) }
 }
diff --git a/ql/src/codeql_ruby/dataflow/internal/SsaImplSpecific.qll b/ql/src/codeql_ruby/dataflow/internal/SsaImplSpecific.qll
index f5d7e8d34ca..89e47c8b5d9 100644
--- a/ql/src/codeql_ruby/dataflow/internal/SsaImplSpecific.qll
+++ b/ql/src/codeql_ruby/dataflow/internal/SsaImplSpecific.qll
@@ -31,8 +31,4 @@ predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain)
   certain = false
 }
 
-predicate variableRead(BasicBlock bb, int i, SourceVariable v) {
-  SsaImpl::variableReadActual(bb, i, v)
-  or
-  SsaImpl::variableReadPseudo(bb, i, v)
-}
+predicate variableRead = SsaImpl::variableRead/4;