Merge pull request #15985 from hvitved/ruby/phi-barrier-guards

Ruby: Extend barrier guards to handle phi inputs
2025-12-17 01:03:14 +01:00 · 2024-04-03 15:22:39 +02:00
parent 9be2b9cbdb 90779f4413
commit 2d4cf55c87
11 changed files with 1676 additions and 454 deletions
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
@@ -72,47 +72,51 @@ CfgNodes::ExprCfgNode getAPostUpdateNodeForArg(Argument arg) {
  not exists(getALastEvalNode(result))
 }

-/** Provides predicates related to local data flow. */
-module LocalFlow {
-  private import codeql.ruby.dataflow.internal.SsaImpl
-
-  /** An SSA definition into which another SSA definition may flow. */
-  private class SsaInputDefinitionExtNode extends SsaDefinitionExtNode {
-    SsaInputDefinitionExtNode() {
-      def instanceof Ssa::PhiNode
-      or
-      def instanceof SsaImpl::PhiReadNode
-    }
+/** An SSA definition into which another SSA definition may flow. */
+class SsaInputDefinitionExt extends SsaImpl::DefinitionExt {
+  SsaInputDefinitionExt() {
+    this instanceof Ssa::PhiNode
+    or
+    this instanceof SsaImpl::PhiReadNode
  }

+  predicate hasInputFromBlock(SsaImpl::DefinitionExt def, BasicBlock bb, int i, BasicBlock input) {
+    SsaImpl::lastRefBeforeRedefExt(def, bb, i, input, this)
+  }
+}
+
+/** Provides predicates related to local data flow. */
+module LocalFlow {
  /**
   * Holds if `nodeFrom` is a node for SSA definition `def`, which can reach `next`.
   */
  pragma[nomagic]
  private predicate localFlowSsaInputFromDef(
-    SsaDefinitionExtNode nodeFrom, SsaImpl::DefinitionExt def, SsaInputDefinitionExtNode next
+    SsaDefinitionExtNode nodeFrom, SsaImpl::DefinitionExt def, SsaInputNode nodeTo
  ) {
-    exists(BasicBlock bb, int i |
-      lastRefBeforeRedefExt(def, bb, i, next.getDefinitionExt()) and
+    exists(BasicBlock bb, int i, BasicBlock input, SsaInputDefinitionExt next |
+      next.hasInputFromBlock(def, bb, i, input) and
      def = nodeFrom.getDefinitionExt() and
      def.definesAt(_, bb, i, _) and
-      nodeFrom != next
+      nodeTo = TSsaInputNode(next, input)
    )
  }

  /**
   * Holds if `nodeFrom` is a last read of SSA definition `def`, which
-   * can reach `next`.
+   * can reach `nodeTo`.
   */
  pragma[nomagic]
-  predicate localFlowSsaInputFromRead(
-    SsaImpl::DefinitionExt def, Node nodeFrom, SsaInputDefinitionExtNode next
-  ) {
-    exists(BasicBlock bb, int i, CfgNodes::ExprCfgNode exprFrom |
-      SsaImpl::lastRefBeforeRedefExt(def, bb, i, next.getDefinitionExt()) and
+  predicate localFlowSsaInputFromRead(SsaImpl::DefinitionExt def, Node nodeFrom, SsaInputNode nodeTo) {
+    exists(
+      BasicBlock bb, int i, CfgNodes::ExprCfgNode exprFrom, BasicBlock input,
+      SsaInputDefinitionExt next
+    |
+      next.hasInputFromBlock(def, bb, i, input) and
      exprFrom = bb.getNode(i) and
      exprFrom.getExpr() instanceof VariableReadAccess and
-      exprFrom = [nodeFrom.asExpr(), nodeFrom.(PostUpdateNodeImpl).getPreUpdateNode().asExpr()]
+      exprFrom = [nodeFrom.asExpr(), nodeFrom.(PostUpdateNodeImpl).getPreUpdateNode().asExpr()] and
+      nodeTo = TSsaInputNode(next, input)
    )
  }

@@ -181,7 +185,7 @@ module LocalFlow {
    or
    // Flow from SSA definition to first read
    def = nodeFrom.(SsaDefinitionExtNode).getDefinitionExt() and
-    firstReadExt(def, nodeTo.asExpr())
+    SsaImpl::firstReadExt(def, nodeTo.asExpr())
    or
    // Flow from post-update read to next read
    localSsaFlowStepUseUse(def, nodeFrom.(PostUpdateNodeImpl).getPreUpdateNode(), nodeTo)
@@ -189,6 +193,9 @@ module LocalFlow {
    // Flow into phi (read) SSA definition node from def
    localFlowSsaInputFromDef(nodeFrom, def, nodeTo)
    or
+    nodeTo.(SsaDefinitionExtNode).getDefinitionExt() = def and
+    def = nodeFrom.(SsaInputNode).getDefinitionExt()
+    or
    localFlowSsaParamInput(nodeFrom, nodeTo) and
    def = nodeTo.(SsaDefinitionExtNode).getDefinitionExt()
  }
@@ -530,6 +537,9 @@ private module Cached {
    TExprNode(CfgNodes::ExprCfgNode n) or
    TReturningNode(CfgNodes::ReturningCfgNode n) { exists(n.getReturnedValueNode()) } or
    TSsaDefinitionExtNode(SsaImpl::DefinitionExt def) or
+    TSsaInputNode(SsaInputDefinitionExt def, BasicBlock input) {
+      def.hasInputFromBlock(_, _, _, input)
+    } or
    TCapturedVariableNode(VariableCapture::CapturedVariable v) or
    TNormalParameterNode(Parameter p) {
      p instanceof SimpleParameter or
@@ -802,6 +812,8 @@ import Cached
 predicate nodeIsHidden(Node n) {
  n.(SsaDefinitionExtNode).isHidden()
  or
+  n instanceof SsaInputNode
+  or
  n = LocalFlow::getParameterDefNode(_)
  or
  exists(AstNode desug |
@@ -863,6 +875,57 @@ class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
  override string toStringImpl() { result = def.toString() }
 }

+/**
+ * A node that represents an input to an SSA phi (read) definition.
+ *
+ * This allows for barrier guards to filter input to phi nodes. For example, in
+ *
+ * ```rb
+ * x = taint
+ * if x != "safe" then
+ *     x = "safe"
+ * end
+ * sink x
+ * ```
+ *
+ * the `false` edge out of `x != "safe"` guards the input from `x = taint` into the
+ * `phi` node after the condition.
+ *
+ * It is also relevant to filter input into phi read nodes:
+ *
+ * ```rb
+ * x = taint
+ * if b then
+ *     if x != "safe1" then
+ *         return
+ *     end
+ * else
+ *     if x != "safe2" then
+ *         return
+ *     end
+ * end
+ *
+ * sink x
+ * ```
+ *
+ * both inputs into the phi read node after the outer condition are guarded.
+ */
+class SsaInputNode extends NodeImpl, TSsaInputNode {
+  SsaImpl::DefinitionExt def;
+  BasicBlock input;
+
+  SsaInputNode() { this = TSsaInputNode(def, input) }
+
+  /** Gets the underlying SSA definition. */
+  SsaImpl::DefinitionExt getDefinitionExt() { result = def }
+
+  override CfgScope getCfgScope() { result = input.getScope() }
+
+  override Location getLocationImpl() { result = input.getLastNode().getLocation() }
+
+  override string toStringImpl() { result = "[input] " + def }
+}
+
 /** An SSA definition for a `self` variable. */
 class SsaSelfDefinitionNode extends SsaDefinitionExtNode {
  private SelfVariable self;
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPublic.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPublic.qll
@@ -856,24 +856,52 @@ private predicate sameSourceVariable(Ssa::Definition def1, Ssa::Definition def2)
 * in data flow and taint tracking.
 */
 module BarrierGuard<guardChecksSig/3 guardChecks> {
+  private import SsaImpl as SsaImpl
+
  pragma[nomagic]
  private predicate guardChecksSsaDef(CfgNodes::AstCfgNode g, boolean branch, Ssa::Definition def) {
    guardChecks(g, def.getARead(), branch)
  }

  pragma[nomagic]
-  private predicate guardControlsSsaDef(
+  private predicate guardControlsSsaRead(
    CfgNodes::AstCfgNode g, boolean branch, Ssa::Definition def, Node n
  ) {
    def.getARead() = n.asExpr() and
    guardControlsBlock(g, n.asExpr().getBasicBlock(), branch)
  }

+  pragma[nomagic]
+  private predicate guardControlsPhiInput(
+    CfgNodes::AstCfgNode g, boolean branch, Ssa::Definition def, BasicBlock input,
+    SsaInputDefinitionExt phi
+  ) {
+    phi.hasInputFromBlock(def, _, _, input) and
+    (
+      guardControlsBlock(g, input, branch)
+      or
+      exists(SuccessorTypes::ConditionalSuccessor s |
+        g = input.getLastNode() and
+        s.getValue() = branch and
+        input.getASuccessor(s) = phi.getBasicBlock()
+      )
+    )
+  }
+
  /** Gets a node that is safely guarded by the given guard check. */
  Node getABarrierNode() {
    exists(CfgNodes::AstCfgNode g, boolean branch, Ssa::Definition def |
      guardChecksSsaDef(g, branch, def) and
-      guardControlsSsaDef(g, branch, def, result)
+      guardControlsSsaRead(g, branch, def, result)
+    )
+    or
+    exists(
+      CfgNodes::AstCfgNode g, boolean branch, Ssa::Definition def, BasicBlock input,
+      SsaInputDefinitionExt phi
+    |
+      guardChecksSsaDef(g, branch, def) and
+      guardControlsPhiInput(g, branch, def, input, phi) and
+      result = TSsaInputNode(phi, input)
    )
    or
    result.asExpr() = getAMaybeGuardedCapturedDef().getARead()
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
@@ -459,14 +459,16 @@ private module Cached {
   * The reference is either a read of `def` or `def` itself.
   */
  cached
-  predicate lastRefBeforeRedefExt(DefinitionExt def, Cfg::BasicBlock bb, int i, DefinitionExt next) {
+  predicate lastRefBeforeRedefExt(
+    DefinitionExt def, Cfg::BasicBlock bb, int i, Cfg::BasicBlock input, DefinitionExt next
+  ) {
    exists(LocalVariable v |
-      Impl::lastRefRedefExt(def, v, bb, i, next) and
+      Impl::lastRefRedefExt(def, v, bb, i, input, next) and
      not SsaInput::variableRead(bb, i, v, false)
    )
    or
    exists(SsaInput::BasicBlock bb0, int i0 |
-      Impl::lastRefRedefExt(def, _, bb0, i0, next) and
+      Impl::lastRefRedefExt(def, _, bb0, i0, input, next) and
      adjacentDefReachesUncertainReadExt(def, bb, i, bb0, i0)
    )
  }
--- a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-flow.expected
+++ b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-flow.expected
@@ -0,0 +1,23 @@
+testFailures
+edges
+| barrier_flow.rb:2:5:2:5 | x | barrier_flow.rb:4:10:4:10 | x | provenance |  |
+| barrier_flow.rb:2:9:2:17 | call to source | barrier_flow.rb:2:5:2:5 | x | provenance |  |
+| barrier_flow.rb:8:5:8:5 | x | barrier_flow.rb:11:14:11:14 | x | provenance |  |
+| barrier_flow.rb:8:9:8:17 | call to source | barrier_flow.rb:8:5:8:5 | x | provenance |  |
+| barrier_flow.rb:24:5:24:5 | x | barrier_flow.rb:26:10:26:10 | x | provenance |  |
+| barrier_flow.rb:24:9:24:17 | call to source | barrier_flow.rb:24:5:24:5 | x | provenance |  |
+nodes
+| barrier_flow.rb:2:5:2:5 | x | semmle.label | x |
+| barrier_flow.rb:2:9:2:17 | call to source | semmle.label | call to source |
+| barrier_flow.rb:4:10:4:10 | x | semmle.label | x |
+| barrier_flow.rb:8:5:8:5 | x | semmle.label | x |
+| barrier_flow.rb:8:9:8:17 | call to source | semmle.label | call to source |
+| barrier_flow.rb:11:14:11:14 | x | semmle.label | x |
+| barrier_flow.rb:24:5:24:5 | x | semmle.label | x |
+| barrier_flow.rb:24:9:24:17 | call to source | semmle.label | call to source |
+| barrier_flow.rb:26:10:26:10 | x | semmle.label | x |
+subpaths
+#select
+| barrier_flow.rb:4:10:4:10 | x | barrier_flow.rb:2:9:2:17 | call to source | barrier_flow.rb:4:10:4:10 | x | $@ | barrier_flow.rb:2:9:2:17 | call to source | call to source |
+| barrier_flow.rb:11:14:11:14 | x | barrier_flow.rb:8:9:8:17 | call to source | barrier_flow.rb:11:14:11:14 | x | $@ | barrier_flow.rb:8:9:8:17 | call to source | call to source |
+| barrier_flow.rb:26:10:26:10 | x | barrier_flow.rb:24:9:24:17 | call to source | barrier_flow.rb:26:10:26:10 | x | $@ | barrier_flow.rb:24:9:24:17 | call to source | call to source |
--- a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-flow.ql
+++ b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-flow.ql
@@ -0,0 +1,23 @@
+/**
+ * @kind path-problem
+ */
+
+import codeql.ruby.AST
+import codeql.ruby.CFG
+import TestUtilities.InlineFlowTest
+import codeql.ruby.dataflow.BarrierGuards
+import PathGraph
+
+module FlowConfig implements DataFlow::ConfigSig {
+  predicate isSource = DefaultFlowConfig::isSource/1;
+
+  predicate isSink = DefaultFlowConfig::isSink/1;
+
+  predicate isBarrier(DataFlow::Node n) { n instanceof StringConstCompareBarrier }
+}
+
+import ValueFlowTest<FlowConfig>
+
+from PathNode source, PathNode sink
+where flowPath(source, sink)
+select sink, source, sink, "$@", source, source.toString()
--- a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected
+++ b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected
@@ -1,6 +1,7 @@
 testFailures
 failures
 newStyleBarrierGuards
+| barrier-guards.rb:3:16:4:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:4:5:4:7 | foo |
 | barrier-guards.rb:10:5:10:7 | foo |
 | barrier-guards.rb:18:5:18:7 | foo |
@@ -8,6 +9,7 @@ newStyleBarrierGuards
 | barrier-guards.rb:28:5:28:7 | foo |
 | barrier-guards.rb:38:5:38:7 | foo |
 | barrier-guards.rb:45:9:45:11 | foo |
+| barrier-guards.rb:70:22:71:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:71:5:71:7 | foo |
 | barrier-guards.rb:83:5:83:7 | foo |
 | barrier-guards.rb:91:5:91:7 | foo |
@@ -36,6 +38,14 @@ newStyleBarrierGuards
 | barrier-guards.rb:276:5:276:7 | foo |
 | barrier-guards.rb:282:5:282:7 | foo |
 | barrier-guards.rb:292:5:292:7 | foo |
+| barrier_flow.rb:19:14:19:14 | x |
+| barrier_flow.rb:32:10:32:10 | x |
+| barrier_flow.rb:38:8:38:18 | [input] phi |
+| barrier_flow.rb:48:23:48:33 | [input] phi |
+| barrier_flow.rb:56:10:57:34 | [input] SSA phi read(x) |
+| barrier_flow.rb:58:5:59:34 | [input] SSA phi read(x) |
+| barrier_flow.rb:68:10:71:11 | [input] SSA phi read(x) |
+| barrier_flow.rb:72:5:75:11 | [input] SSA phi read(x) |
 controls
 | barrier-guards.rb:3:4:3:15 | ... == ... | barrier-guards.rb:4:5:4:7 | foo | true |
 | barrier-guards.rb:3:4:3:15 | ... == ... | barrier-guards.rb:6:5:6:7 | foo | false |
@@ -331,3 +341,29 @@ controls
 | barrier-guards.rb:291:6:291:6 | g | barrier-guards.rb:291:1:292:19 | [no-match] when ... | no-match |
 | barrier-guards.rb:291:6:291:6 | g | barrier-guards.rb:292:5:292:7 | foo | match |
 | barrier-guards.rb:291:6:291:6 | g | barrier-guards.rb:294:5:294:7 | foo | no-match |
+| barrier_flow.rb:10:8:10:18 | ... != ... | barrier_flow.rb:11:9:11:14 | self | true |
+| barrier_flow.rb:18:8:18:18 | ... == ... | barrier_flow.rb:19:9:19:14 | self | true |
+| barrier_flow.rb:26:19:26:29 | ... == ... | barrier_flow.rb:26:5:26:10 | self | false |
+| barrier_flow.rb:32:19:32:29 | ... != ... | barrier_flow.rb:32:5:32:10 | self | false |
+| barrier_flow.rb:38:8:38:18 | ... != ... | barrier_flow.rb:39:9:39:9 | x | true |
+| barrier_flow.rb:48:23:48:33 | ... == ... | barrier_flow.rb:48:5:48:5 | x | false |
+| barrier_flow.rb:56:8:56:8 | b | barrier_flow.rb:57:9:57:14 | return | true |
+| barrier_flow.rb:56:8:56:8 | b | barrier_flow.rb:57:9:57:34 | ... unless ... | true |
+| barrier_flow.rb:56:8:56:8 | b | barrier_flow.rb:57:23:57:23 | x | true |
+| barrier_flow.rb:56:8:56:8 | b | barrier_flow.rb:59:9:59:14 | return | false |
+| barrier_flow.rb:56:8:56:8 | b | barrier_flow.rb:59:9:59:34 | ... unless ... | false |
+| barrier_flow.rb:56:8:56:8 | b | barrier_flow.rb:59:23:59:23 | x | false |
+| barrier_flow.rb:57:23:57:34 | ... == ... | barrier_flow.rb:57:9:57:14 | return | false |
+| barrier_flow.rb:57:23:57:34 | ... == ... | barrier_flow.rb:57:9:57:34 | ... unless ... | true |
+| barrier_flow.rb:59:23:59:34 | ... == ... | barrier_flow.rb:59:9:59:14 | return | false |
+| barrier_flow.rb:59:23:59:34 | ... == ... | barrier_flow.rb:59:9:59:34 | ... unless ... | true |
+| barrier_flow.rb:68:8:68:8 | b | barrier_flow.rb:69:9:71:11 | if ... | true |
+| barrier_flow.rb:68:8:68:8 | b | barrier_flow.rb:69:12:69:12 | x | true |
+| barrier_flow.rb:68:8:68:8 | b | barrier_flow.rb:70:13:70:18 | return | true |
+| barrier_flow.rb:68:8:68:8 | b | barrier_flow.rb:73:9:75:11 | if ... | false |
+| barrier_flow.rb:68:8:68:8 | b | barrier_flow.rb:73:12:73:12 | x | false |
+| barrier_flow.rb:68:8:68:8 | b | barrier_flow.rb:74:13:74:18 | return | false |
+| barrier_flow.rb:69:12:69:23 | ... != ... | barrier_flow.rb:69:9:71:11 | if ... | false |
+| barrier_flow.rb:69:12:69:23 | ... != ... | barrier_flow.rb:70:13:70:18 | return | true |
+| barrier_flow.rb:73:12:73:23 | ... != ... | barrier_flow.rb:73:9:75:11 | if ... | false |
+| barrier_flow.rb:73:12:73:23 | ... != ... | barrier_flow.rb:74:13:74:18 | return | true |
--- a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.ql
+++ b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.ql
@@ -1,3 +1,4 @@
+import codeql.ruby.dataflow.internal.DataFlowPrivate
 import codeql.ruby.dataflow.internal.DataFlowPublic
 import codeql.ruby.dataflow.BarrierGuards
 import codeql.ruby.controlflow.CfgNodes
@@ -25,6 +26,7 @@ module BarrierGuardTest implements TestSig {
    tag = "guarded" and
    exists(DataFlow::Node n |
      newStyleBarrierGuards(n) and
+      not n instanceof SsaInputNode and
      location = n.getLocation() and
      element = n.toString() and
      value = ""
--- a/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier_flow.rb
+++ b/ruby/ql/test/library-tests/dataflow/barrier-guards/barrier_flow.rb
@@ -0,0 +1,79 @@
+def m1
+    x = source(1)
+
+    sink x # $ hasValueFlow=1
+end
+
+def m2
+    x = source(2)
+
+    if x != "safe" then
+        sink x # $ hasValueFlow=2
+    end
+end
+
+def m3
+    x = source(3)
+
+    if x == "safe" then
+        sink x # $ guarded
+    end
+end
+
+def m4
+    x = source(4)
+
+    sink x unless x == "safe" # $ hasValueFlow=4
+end
+
+def m5
+    x = source(5)
+
+    sink x unless x != "safe" # $ guarded
+end
+
+def m6
+    x = source(6)
+
+    if x != "safe" then
+        x = "safe"
+    end
+
+    sink x
+end
+
+def m7
+    x = source(7)
+
+    x = "safe" unless x == "safe"
+
+    sink x
+end
+
+def m8(b)
+    x = source(8)
+
+    if b then
+        return unless x == "safe1"
+    else
+        return unless x == "safe2"
+    end
+
+    sink x
+end
+
+def m9(b)
+    x = source(9)
+
+    if b then
+        if x != "safe1" then
+            return
+        end
+    else
+        if x != "safe2" then
+            return
+        end
+    end
+
+    sink x
+end
--- a/ruby/ql/test/library-tests/dataflow/local/DataflowStep.expected
+++ b/ruby/ql/test/library-tests/dataflow/local/DataflowStep.expected
--- a/ruby/ql/test/library-tests/dataflow/local/TaintStep.expected
+++ b/ruby/ql/test/library-tests/dataflow/local/TaintStep.expected
--- a/shared/ssa/codeql/ssa/Ssa.qll
+++ b/shared/ssa/codeql/ssa/Ssa.qll
@@ -473,7 +473,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    }

    pragma[noinline]
-    private predicate ssaDefReachesThroughBlock(DefinitionExt def, BasicBlock bb) {
+    predicate ssaDefReachesThroughBlock(DefinitionExt def, BasicBlock bb) {
      exists(SourceVariable v |
        ssaDefReachesEndOfBlockExt(bb, def, v) and
        not defOccursInBlock(_, bb, v, _)
@@ -741,6 +741,16 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    defAdjacentRead(def, bb1, bb2, i2)
  }

+  private predicate lastRefRedefExtSameBlock(
+    DefinitionExt def, SourceVariable v, BasicBlock bb, int i, DefinitionExt next
+  ) {
+    exists(int rnk, int j |
+      rnk = ssaDefRank(def, v, bb, i, _) and
+      next.definesAt(v, bb, j, _) and
+      rnk + 1 = ssaRefRank(bb, j, v, ssaDefExt())
+    )
+  }
+
  /**
   * NB: If this predicate is exposed, it should be cached.
   *
@@ -753,11 +763,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    DefinitionExt def, SourceVariable v, BasicBlock bb, int i, DefinitionExt next
  ) {
    // Next reference to `v` inside `bb` is a write
-    exists(int rnk, int j |
-      rnk = ssaDefRank(def, v, bb, i, _) and
-      next.definesAt(v, bb, j, _) and
-      rnk + 1 = ssaRefRank(bb, j, v, ssaDefExt())
-    )
+    lastRefRedefExtSameBlock(def, v, bb, i, next)
    or
    // Can reach a write using one or more steps
    lastSsaRefExt(def, v, bb, i) and
@@ -767,6 +773,38 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    )
  }

+  /**
+   * 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.
+   *
+   * The path from node `i` in `bb` to `next` goes via basic block `input`, which is
+   * either a predecessor of the basic block of `next`, or `input = bb` in case `next`
+   * occurs in basic block `bb`.
+   */
+  pragma[nomagic]
+  predicate lastRefRedefExt(
+    DefinitionExt def, SourceVariable v, BasicBlock bb, int i, BasicBlock input, DefinitionExt next
+  ) {
+    // Next reference to `v` inside `bb` is a write
+    lastRefRedefExtSameBlock(def, v, bb, i, next) and
+    input = bb
+    or
+    // Can reach a write using one or more steps
+    lastSsaRefExt(def, v, bb, i) and
+    exists(BasicBlock bb2 |
+      input = getABasicBlockPredecessor(bb2) and
+      1 = ssaDefRank(next, v, bb2, _, ssaDefExt())
+    |
+      input = bb
+      or
+      varBlockReachesExt(def, v, bb, input) and
+      ssaDefReachesThroughBlock(def, input)
+    )
+  }
+
  /**
   * NB: If this predicate is exposed, it should be cached.
   *