diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
index d929f9d447b..a51eb2678a9 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
@@ -198,75 +198,15 @@ module SemanticExprConfig {
     result = v.asOperand().getUse().getBlock()
   }
 
-  private newtype TReadPosition =
-    TReadPositionBlock(IR::IRBlock block) or
-    TReadPositionPhiInputEdge(IR::IRBlock pred, IR::IRBlock succ) {
-      exists(IR::PhiInputOperand input |
-        pred = input.getPredecessorBlock() and
-        succ = input.getUse().getBlock()
-      )
-    }
-
-  class SsaReadPosition extends TReadPosition {
-    string toString() { none() }
-
-    Location getLocation() { none() }
-
-    predicate hasRead(SsaVariable v) { none() }
-  }
-
-  private class SsaReadPositionBlock extends SsaReadPosition, TReadPositionBlock {
-    IR::IRBlock block;
-
-    SsaReadPositionBlock() { this = TReadPositionBlock(block) }
-
-    final override string toString() { result = block.toString() }
-
-    final override Location getLocation() { result = block.getLocation() }
-
-    final override predicate hasRead(SsaVariable v) {
-      exists(IR::Operand operand | operand.getDef() = v.asInstruction() |
-        not operand instanceof IR::PhiInputOperand and
-        operand.getUse().getBlock() = block
-      )
-    }
-  }
-
-  private class SsaReadPositionPhiInputEdge extends SsaReadPosition, TReadPositionPhiInputEdge {
-    IR::IRBlock pred;
-    IR::IRBlock succ;
-
-    SsaReadPositionPhiInputEdge() { this = TReadPositionPhiInputEdge(pred, succ) }
-
-    final override string toString() { result = pred.toString() + "->" + succ.toString() }
-
-    final override Location getLocation() { result = succ.getLocation() }
-
-    final override predicate hasRead(SsaVariable v) {
-      exists(IR::PhiInputOperand operand | operand.getDef() = v.asInstruction() |
-        operand.getPredecessorBlock() = pred and
-        operand.getUse().getBlock() = succ
-      )
-    }
-  }
-
-  predicate hasReadOfSsaVariable(SsaReadPosition pos, SsaVariable v) { pos.hasRead(v) }
-
-  predicate readBlock(SsaReadPosition pos, BasicBlock block) { pos = TReadPositionBlock(block) }
-
-  predicate phiInputEdge(SsaReadPosition pos, BasicBlock origBlock, BasicBlock phiBlock) {
-    pos = TReadPositionPhiInputEdge(origBlock, phiBlock)
-  }
-
-  predicate phiInput(SsaReadPosition pos, SsaVariable phi, SsaVariable input) {
+  /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
+  predicate phiInputFromBlock(SsaVariable phi, SsaVariable inp, BasicBlock bb) {
     exists(IR::PhiInputOperand operand |
-      pos = TReadPositionPhiInputEdge(operand.getPredecessorBlock(), operand.getUse().getBlock())
-    |
+      bb = operand.getPredecessorBlock() and
       phi.asInstruction() = operand.getUse() and
       (
-        input.asInstruction() = operand.getDef()
+        inp.asInstruction() = operand.getDef()
         or
-        input.asOperand() = operand
+        inp.asOperand() = operand
       )
     )
   }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
index 0bbfc2998af..8e7f3c7cfb3 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
@@ -31,35 +31,8 @@ class SemSsaPhiNode extends SemSsaVariable {
   SemSsaPhiNode() { Specific::phi(this) }
 
   final SemSsaVariable getAPhiInput() { result = Specific::getAPhiInput(this) }
-}
-
-class SemSsaReadPosition instanceof Specific::SsaReadPosition {
-  final string toString() { result = super.toString() }
-
-  final Specific::Location getLocation() { result = super.getLocation() }
-
-  final predicate hasReadOfVar(SemSsaVariable var) { Specific::hasReadOfSsaVariable(this, var) }
-}
-
-class SemSsaReadPositionPhiInputEdge extends SemSsaReadPosition {
-  SemBasicBlock origBlock;
-  SemBasicBlock phiBlock;
-
-  SemSsaReadPositionPhiInputEdge() { Specific::phiInputEdge(this, origBlock, phiBlock) }
-
-  predicate phiInput(SemSsaPhiNode phi, SemSsaVariable inp) { Specific::phiInput(this, phi, inp) }
-
-  SemBasicBlock getOrigBlock() { result = origBlock }
-
-  SemBasicBlock getPhiBlock() { result = phiBlock }
-}
-
-class SemSsaReadPositionBlock extends SemSsaReadPosition {
-  SemBasicBlock block;
-
-  SemSsaReadPositionBlock() { Specific::readBlock(this, block) }
-
-  SemBasicBlock getBlock() { result = block }
-
-  SemExpr getAnExpr() { result = this.getBlock().getAnExpr() }
+
+  final predicate hasInputFromBlock(SemSsaVariable inp, SemBasicBlock bb) {
+    Specific::phiInputFromBlock(this, inp, bb)
+  }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
index e8b8bde758a..4957f700ac6 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
@@ -74,6 +74,8 @@ module Sem implements Semantic {
 
   BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
 
+  int getBlockId1(BasicBlock bb) { result = bb.getUniqueId() }
+
   class Guard = SemGuard;
 
   predicate implies_v2 = semImplies_v2/4;
@@ -92,12 +94,6 @@ module Sem implements Semantic {
 
   class SsaExplicitUpdate = SemSsaExplicitUpdate;
 
-  class SsaReadPosition = SemSsaReadPosition;
-
-  class SsaReadPositionPhiInputEdge = SemSsaReadPositionPhiInputEdge;
-
-  class SsaReadPositionBlock = SemSsaReadPositionBlock;
-
   predicate conversionCannotOverflow(Type fromType, Type toType) {
     SemanticType::conversionCannotOverflow(fromType, toType)
   }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
index c61bf4817c2..7276f066220 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
@@ -133,33 +133,4 @@ module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
     or
     not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
   }
-
-  import Ranking
-}
-
-import Ranking
-
-module Ranking {
-  /**
-   * Holds if `rix` is the number of input edges to `phi`.
-   */
-  predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
-    rix = max(int r | rankedPhiInput(phi, _, _, r))
-  }
-
-  /**
-   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
-   * in an arbitrary 1-based numbering of the input edges to `phi`.
-   */
-  predicate rankedPhiInput(
-    SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
-  ) {
-    edge.phiInput(phi, inp) and
-    edge =
-      rank[r](SemSsaReadPositionPhiInputEdge e |
-        e.phiInput(phi, _)
-      |
-        e order by e.getOrigBlock().getUniqueId()
-      )
-  }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
index c79172d74d0..f6f0d6302b7 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
@@ -45,7 +45,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   /** An SSA Phi definition, whose sign is the union of the signs of its inputs. */
   private class PhiSignDef extends FlowSignDef instanceof SemSsaPhiNode {
     final override Sign getSign() {
-      exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
+      exists(SemSsaVariable inp, SsaReadPositionPhiInputEdge edge |
         edge.phiInput(this, inp) and
         result = semSsaSign(inp, edge)
       )
@@ -170,11 +170,11 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
     override Sign getSignRestriction() {
       // Propagate via SSA
       // Propagate the sign from the def of `v`, incorporating any inference from guards.
-      result = semSsaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = this))
+      result = semSsaSign(v, any(SsaReadPositionBlock bb | bb.getBlock().getAnExpr() = this))
       or
       // No block for this read. Just use the sign of the def.
       // REVIEW: How can this happen?
-      not exists(SemSsaReadPositionBlock bb | bb.getAnExpr() = this) and
+      not exists(SsaReadPositionBlock bb | bb.getBlock().getAnExpr() = this) and
       result = semSsaDefSign(v)
     }
   }
@@ -290,7 +290,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * to only include bounds for which we might determine a sign.
    */
   private predicate lowerBound(
-    SemExpr lowerbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
+    SemExpr lowerbound, SemSsaVariable v, SsaReadPosition pos, boolean isStrict
   ) {
     exists(boolean testIsTrue, SemRelationalExpr comp |
       pos.hasReadOfVar(v) and
@@ -314,7 +314,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * to only include bounds for which we might determine a sign.
    */
   private predicate upperBound(
-    SemExpr upperbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
+    SemExpr upperbound, SemSsaVariable v, SsaReadPosition pos, boolean isStrict
   ) {
     exists(boolean testIsTrue, SemRelationalExpr comp |
       pos.hasReadOfVar(v) and
@@ -340,7 +340,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    *  - `isEq = true` : `v = eqbound`
    *  - `isEq = false` : `v != eqbound`
    */
-  private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
+  private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SsaReadPosition pos, boolean isEq) {
     exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
       pos.hasReadOfVar(pragma[only_bind_into](v)) and
       guardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
@@ -355,7 +355,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
    * order for `v` to be positive.
    */
-  private predicate posBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
+  private predicate posBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
     upperBound(bound, v, pos, _) or
     eqBound(bound, v, pos, true)
   }
@@ -364,7 +364,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
    * order for `v` to be negative.
    */
-  private predicate negBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
+  private predicate negBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
     lowerBound(bound, v, pos, _) or
     eqBound(bound, v, pos, true)
   }
@@ -373,24 +373,24 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
    * can be zero.
    */
-  private predicate zeroBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
+  private predicate zeroBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
     lowerBound(bound, v, pos, _) or
     upperBound(bound, v, pos, _) or
     eqBound(bound, v, pos, _)
   }
 
   /** Holds if `bound` allows `v` to be positive at `pos`. */
-  private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
+  private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
     posBound(bound, v, pos) and TPos() = semExprSign(bound)
   }
 
   /** Holds if `bound` allows `v` to be negative at `pos`. */
-  private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
+  private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
     negBound(bound, v, pos) and TNeg() = semExprSign(bound)
   }
 
   /** Holds if `bound` allows `v` to be zero at `pos`. */
-  private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
+  private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
     lowerBound(bound, v, pos, _) and TNeg() = semExprSign(bound)
     or
     lowerBound(bound, v, pos, false) and TZero() = semExprSign(bound)
@@ -408,7 +408,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * Holds if there is a bound that might restrict whether `v` has the sign `s`
    * at `pos`.
    */
-  private predicate hasGuard(SemSsaVariable v, SemSsaReadPosition pos, Sign s) {
+  private predicate hasGuard(SemSsaVariable v, SsaReadPosition pos, Sign s) {
     s = TPos() and posBound(_, v, pos)
     or
     s = TNeg() and negBound(_, v, pos)
@@ -421,7 +421,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * might be ruled out by a guard.
    */
   pragma[noinline]
-  private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
+  private Sign guardedSsaSign(SemSsaVariable v, SsaReadPosition pos) {
     result = semSsaDefSign(v) and
     pos.hasReadOfVar(v) and
     hasGuard(v, pos, result)
@@ -432,7 +432,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * can rule it out.
    */
   pragma[noinline]
-  private Sign unguardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
+  private Sign unguardedSsaSign(SemSsaVariable v, SsaReadPosition pos) {
     result = semSsaDefSign(v) and
     pos.hasReadOfVar(v) and
     not hasGuard(v, pos, result)
@@ -443,7 +443,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
    * ruled out the sign but does not.
    * This does not check that the definition of `v` also allows the sign.
    */
-  private Sign guardedSsaSignOk(SemSsaVariable v, SemSsaReadPosition pos) {
+  private Sign guardedSsaSignOk(SemSsaVariable v, SsaReadPosition pos) {
     result = TPos() and
     forex(SemExpr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
     or
@@ -455,7 +455,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   }
 
   /** Gets a possible sign for `v` at `pos`. */
-  private Sign semSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
+  private Sign semSsaSign(SemSsaVariable v, SsaReadPosition pos) {
     result = unguardedSsaSign(v, pos)
     or
     result = guardedSsaSign(v, pos) and
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
index 0fd07fe0258..64d17202d67 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -66,7 +66,6 @@
 import java
 private import SSA
 private import RangeUtils
-private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
 private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.security.RandomDataSource
 private import SignAnalysis
@@ -80,7 +79,6 @@ module Sem implements Semantic {
   private import java as J
   private import SSA as SSA
   private import RangeUtils as RU
-  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
   private import semmle.code.java.controlflow.internal.GuardsLogic as GL
 
   class Expr = J::Expr;
@@ -213,6 +211,12 @@ module Sem implements Semantic {
 
   BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getABBSuccessor() }
 
+  private predicate id(BasicBlock x, BasicBlock y) { x = y }
+
+  private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
+
+  int getBlockId1(BasicBlock bb) { idOf(bb, result) }
+
   final private class FinalGuard = GL::Guard;
 
   class Guard extends FinalGuard {
@@ -243,31 +247,14 @@ module Sem implements Semantic {
     Expr getAUse() { result = super.getAUse() }
   }
 
-  class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode { }
+  class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode {
+    predicate hasInputFromBlock(SsaVariable inp, BasicBlock bb) { super.hasInputFromBlock(inp, bb) }
+  }
 
   class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate {
     Expr getDefiningExpr() { result = super.getDefiningExpr() }
   }
 
-  final private class FinalSsaReadPosition = SsaReadPos::SsaReadPosition;
-
-  class SsaReadPosition extends FinalSsaReadPosition {
-    predicate hasReadOfVar(SsaVariable v) { super.hasReadOfVar(v) }
-  }
-
-  class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionPhiInputEdge
-  {
-    BasicBlock getOrigBlock() { result = super.getOrigBlock() }
-
-    BasicBlock getPhiBlock() { result = super.getPhiBlock() }
-
-    predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
-  }
-
-  class SsaReadPositionBlock extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionBlock {
-    BasicBlock getBlock() { result = super.getBlock() }
-  }
-
   predicate conversionCannotOverflow = safeCast/2;
 }
 
@@ -384,7 +371,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
 
 module Utils implements UtilSig<Sem, IntDelta> {
   private import RangeUtils as RU
-  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
 
   Sem::Guard semEqFlowCond(
     Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
@@ -403,14 +389,6 @@ module Utils implements UtilSig<Sem, IntDelta> {
   }
 
   Sem::Type getTrackedType(Sem::Expr e) { result = e.getType() }
-
-  predicate rankedPhiInput(
-    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
-  ) {
-    SsaReadPos::rankedPhiInput(phi, inp, edge, r)
-  }
-
-  predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix) { SsaReadPos::maxPhiInputRank(phi, rix) }
 }
 
 module Bounds implements BoundSig<Location, Sem, IntDelta> {
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
index 718c7c2175e..f01d5cc8d54 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
@@ -5,7 +5,6 @@
 import java
 private import SSA
 private import semmle.code.java.controlflow.internal.GuardsLogic
-private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
 private import semmle.code.java.Constants
 private import semmle.code.java.dataflow.RangeAnalysis
 private import codeql.rangeanalysis.internal.RangeUtils
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
index 253506347f3..bcc11e26518 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
@@ -6,6 +6,8 @@ module Private {
   import semmle.code.java.dataflow.RangeUtils as RU
   private import semmle.code.java.dataflow.SSA as Ssa
   private import semmle.code.java.controlflow.Guards as G
+  private import SsaReadPositionCommon
+  private import semmle.code.java.controlflow.internal.GuardsLogic as GL
   private import Sign
   import Impl
 
@@ -168,7 +170,33 @@ module Private {
 
   predicate ssaRead = RU::ssaRead/2;
 
-  predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
+  /**
+   * Holds if `guard` directly controls the position `controlled` with the
+   * value `testIsTrue`.
+   */
+  pragma[nomagic]
+  private predicate guardDirectlyControlsSsaRead(
+    Guard guard, SsaReadPosition controlled, boolean testIsTrue
+  ) {
+    guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
+    or
+    exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
+      guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
+      guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
+    )
+  }
+
+  /**
+   * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
+   */
+  predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
+    guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
+    or
+    exists(Guard guard0, boolean testIsTrue0 |
+      GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
+      guardControlsSsaRead(guard0, controlled, testIsTrue0)
+    )
+  }
 }
 
 private module Impl {
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
index ea2f2fb63c7..16d63b8ca00 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
@@ -21,7 +21,7 @@ module ModulusAnalysis<
 
   bindingset[pos, v]
   pragma[inline_late]
-  private predicate hasReadOfVarInlineLate(Sem::SsaReadPosition pos, Sem::SsaVariable v) {
+  private predicate hasReadOfVarInlineLate(SsaReadPosition pos, Sem::SsaVariable v) {
     pos.hasReadOfVar(v)
   }
 
@@ -29,9 +29,7 @@ module ModulusAnalysis<
    * Holds if `e + delta` equals `v` at `pos`.
    */
   pragma[nomagic]
-  private predicate valueFlowStepSsa(
-    Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, int delta
-  ) {
+  private predicate valueFlowStepSsa(Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, int delta) {
     U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
     or
     exists(Sem::Guard guard, boolean testIsTrue |
@@ -105,7 +103,7 @@ module ModulusAnalysis<
   /**
    * Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
    */
-  private predicate moduloGuardedRead(Sem::SsaVariable v, Sem::SsaReadPosition pos, int val, int mod) {
+  private predicate moduloGuardedRead(Sem::SsaVariable v, SsaReadPosition pos, int val, int mod) {
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = moduloCheck(v, val, mod, testIsTrue) and
@@ -148,7 +146,7 @@ module ModulusAnalysis<
    * Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
    */
   private predicate phiSelfModulus(
-    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int mod
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, int mod
   ) {
     exists(Bounds::SemSsaBound phibound, int v, int m |
       edge.phiInput(phi, inp) and
@@ -163,7 +161,7 @@ module ModulusAnalysis<
    * Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
    */
   private predicate phiModulusInit(Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
-    exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge |
+    exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge |
       edge.phiInput(phi, inp) and
       ssaModulus(inp, edge, b, val, mod)
     )
@@ -181,7 +179,7 @@ module ModulusAnalysis<
     rix = 0 and
     phiModulusInit(phi, b, val, mod)
     or
-    exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int v1, int m1 |
+    exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, int v1, int m1 |
       mod != 1 and
       val = remainder(v1, mod)
     |
@@ -192,7 +190,7 @@ module ModulusAnalysis<
       // equals `v2` modulo `mod`. The largest value of `mod` that satisfies
       // this is the greatest common divisor of `m1`, `m2`, and `v1 - v2`.
       exists(int v2, int m2 |
-        U::rankedPhiInput(phi, inp, edge, rix) and
+        rankedPhiInput(phi, inp, edge, rix) and
         phiModulusRankStep(phi, b, v1, m1, rix - 1) and
         ssaModulus(inp, edge, b, v2, m2) and
         mod = m1.gcd(m2).gcd(v1 - v2)
@@ -202,7 +200,7 @@ module ModulusAnalysis<
       // preceding potential congruence class `b + v1` mod `m1`. The result will be
       // the congruence class modulo the greatest common divisor of `m1` and `m2`.
       exists(int m2 |
-        U::rankedPhiInput(phi, inp, edge, rix) and
+        rankedPhiInput(phi, inp, edge, rix) and
         phiModulusRankStep(phi, b, v1, m1, rix - 1) and
         phiSelfModulus(phi, inp, edge, m2) and
         mod = m1.gcd(m2)
@@ -215,7 +213,7 @@ module ModulusAnalysis<
    */
   private predicate phiModulus(Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
     exists(int r |
-      U::maxPhiInputRank(phi, r) and
+      maxPhiInputRank(phi, r) and
       phiModulusRankStep(phi, b, val, mod, r)
     )
   }
@@ -224,7 +222,7 @@ module ModulusAnalysis<
    * Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
    */
   private predicate ssaModulus(
-    Sem::SsaVariable v, Sem::SsaReadPosition pos, Bounds::SemBound b, int val, int mod
+    Sem::SsaVariable v, SsaReadPosition pos, Bounds::SemBound b, int val, int mod
   ) {
     phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
     or
@@ -254,7 +252,7 @@ module ModulusAnalysis<
     val = 0 and
     b instanceof Bounds::SemZeroBound
     or
-    exists(Sem::SsaVariable v, Sem::SsaReadPositionBlock bb |
+    exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
       ssaModulus(v, bb, b, val, mod) and
       e = v.getAUse() and
       bb.getBlock() = e.getBasicBlock()
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index 93758dedca7..3bb399dcebc 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -150,6 +150,16 @@ signature module Semantic {
   /** Gets an immediate successor of basic block `bb`, if any. */
   BasicBlock getABasicBlockSuccessor(BasicBlock bb);
 
+  /**
+   * Gets an ideally unique integer for `bb`. If it is undesirable to make this
+   * unique, then `getBlock2` must provide a tiebreaker, such that the pair
+   * `(getBlockId1(bb),getBlockId2(bb))` becomes unique.
+   */
+  int getBlockId1(BasicBlock bb);
+
+  /** Gets a tiebreaker id in case `getBlockId1` is not unique. */
+  default string getBlockId2(BasicBlock bb) { result = "" }
+
   class Guard {
     string toString();
 
@@ -184,28 +194,15 @@ signature module Semantic {
     BasicBlock getBasicBlock();
   }
 
-  class SsaPhiNode extends SsaVariable;
+  class SsaPhiNode extends SsaVariable {
+    /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
+    predicate hasInputFromBlock(SsaVariable inp, BasicBlock bb);
+  }
 
   class SsaExplicitUpdate extends SsaVariable {
     Expr getDefiningExpr();
   }
 
-  class SsaReadPosition {
-    predicate hasReadOfVar(SsaVariable v);
-  }
-
-  class SsaReadPositionPhiInputEdge extends SsaReadPosition {
-    BasicBlock getOrigBlock();
-
-    BasicBlock getPhiBlock();
-
-    predicate phiInput(SsaPhiNode phi, SsaVariable inp);
-  }
-
-  class SsaReadPositionBlock extends SsaReadPosition {
-    BasicBlock getBlock();
-  }
-
   predicate conversionCannotOverflow(Type fromType, Type toType);
 }
 
@@ -330,19 +327,6 @@ signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
    * primitive types as the underlying primitive type.
    */
   Sem::Type getTrackedType(Sem::Expr e);
-
-  /**
-   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
-   * in an arbitrary 1-based numbering of the input edges to `phi`.
-   */
-  predicate rankedPhiInput(
-    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
-  );
-
-  /**
-   * Holds if `rix` is the number of input edges to `phi`.
-   */
-  predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix);
 }
 
 signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
@@ -688,7 +672,7 @@ module RangeStage<
    * - `upper = false` : `v >= e + delta`
    */
   private predicate boundFlowStepSsa(
-    Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, D::Delta delta, boolean upper,
+    Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, boolean upper,
     SemReason reason
   ) {
     semSsaUpdateStep(v, e, delta) and
@@ -706,7 +690,7 @@ module RangeStage<
 
   /** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
   private predicate unequalFlowStepIntegralSsa(
-    Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason
+    Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason
   ) {
     getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
     exists(Sem::Guard guard, boolean testIsTrue |
@@ -836,7 +820,7 @@ module RangeStage<
    * - `upper = false` : `v >= b + delta`
    */
   private predicate boundedSsa(
-    Sem::SsaVariable v, SemBound b, D::Delta delta, Sem::SsaReadPosition pos, boolean upper,
+    Sem::SsaVariable v, SemBound b, D::Delta delta, SsaReadPosition pos, boolean upper,
     boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
     exists(Sem::Expr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
@@ -873,7 +857,7 @@ module RangeStage<
    * Holds if `v != b + delta` at `pos` and `v` is of integral type.
    */
   private predicate unequalIntegralSsa(
-    Sem::SsaVariable v, SemBound b, D::Delta delta, Sem::SsaReadPosition pos, SemReason reason
+    Sem::SsaVariable v, SemBound b, D::Delta delta, SsaReadPosition pos, SemReason reason
   ) {
     exists(Sem::Expr e, D::Delta d1, D::Delta d2 |
       unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
@@ -920,7 +904,7 @@ module RangeStage<
    * - `upper = false` : `inp >= b + delta`
    */
   private predicate boundedPhiInp(
-    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, SemBound b,
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, SemBound b,
     D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
     edge.phiInput(phi, inp) and
@@ -964,7 +948,7 @@ module RangeStage<
   pragma[noinline]
   private predicate boundedPhiInp1(
     Sem::SsaPhiNode phi, SemBound b, boolean upper, Sem::SsaVariable inp,
-    Sem::SsaReadPositionPhiInputEdge edge, D::Delta delta
+    SsaReadPositionPhiInputEdge edge, D::Delta delta
   ) {
     boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
   }
@@ -976,7 +960,7 @@ module RangeStage<
    * - `upper = false` : `inp >= phi`
    */
   private predicate selfBoundedPhiInp(
-    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, boolean upper
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, boolean upper
   ) {
     exists(D::Delta d, SemSsaBound phibound |
       phibound.getVariable() = phi and
@@ -1009,8 +993,7 @@ module RangeStage<
    */
   private predicate boundedPhiCandValidForEdge(
     Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
-    D::Delta origdelta, SemReason reason, Sem::SsaVariable inp,
-    Sem::SsaReadPositionPhiInputEdge edge
+    D::Delta origdelta, SemReason reason, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge
   ) {
     boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
     (
@@ -1036,7 +1019,7 @@ module RangeStage<
     Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
     D::Delta origdelta, SemReason reason, int rix
   ) {
-    exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge |
+    exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge |
       rankedPhiInput(phi, inp, edge, rix) and
       boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
     |
@@ -1208,7 +1191,7 @@ module RangeStage<
       origdelta = delta and
       reason = TSemNoReason()
       or
-      exists(Sem::SsaVariable v, Sem::SsaReadPositionBlock bb |
+      exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
         boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
         e = v.getAUse() and
         bb.getBlock() = e.getBasicBlock()
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll
index 9c9046734b3..27205896014 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll
@@ -1,38 +1,99 @@
 private import codeql.rangeanalysis.RangeAnalysis
 
 module MakeUtils<Semantic Lang, DeltaSig D> {
+  private import Lang
+
   /**
    * Gets an expression that equals `v - d`.
    */
-  Lang::Expr ssaRead(Lang::SsaVariable v, D::Delta delta) {
+  Expr ssaRead(SsaVariable v, D::Delta delta) {
     result = v.getAUse() and delta = D::fromInt(0)
     or
-    exists(D::Delta d1, Lang::ConstantIntegerExpr c |
-      result.(Lang::AddExpr).hasOperands(ssaRead(v, d1), c) and
+    exists(D::Delta d1, ConstantIntegerExpr c |
+      result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
       delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and
       // In the scope of `x += ..`, which is SSA translated as `x2 = x1 + ..`,
       // the variable `x1` is shadowed by `x2`, so there's no need to view this
       // as a read of `x1`.
-      not Lang::isAssignOp(result)
+      not isAssignOp(result)
     )
     or
-    exists(Lang::SubExpr sub, D::Delta d1, Lang::ConstantIntegerExpr c |
+    exists(SubExpr sub, D::Delta d1, ConstantIntegerExpr c |
       result = sub and
       sub.getLeftOperand() = ssaRead(v, d1) and
       sub.getRightOperand() = c and
       delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and
-      not Lang::isAssignOp(result)
+      not isAssignOp(result)
     )
     or
-    result = v.(Lang::SsaExplicitUpdate).getDefiningExpr() and
-    if result instanceof Lang::PostIncExpr
+    result = v.(SsaExplicitUpdate).getDefiningExpr() and
+    if result instanceof PostIncExpr
     then delta = D::fromFloat(1) // x++ === ++x - 1
     else
-      if result instanceof Lang::PostDecExpr
+      if result instanceof PostDecExpr
       then delta = D::fromFloat(-1) // x-- === --x + 1
       else delta = D::fromFloat(0)
     or
-    result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
+    result.(CopyValueExpr).getOperand() = ssaRead(v, delta)
+  }
+
+  private newtype TSsaReadPosition =
+    TSsaReadPositionBlock(BasicBlock bb) {
+      exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)
+    } or
+    TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) {
+      exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock())
+    }
+
+  /**
+   * A position at which an SSA variable is read. This includes both ordinary
+   * reads occurring in basic blocks and input to phi nodes occurring along an
+   * edge between two basic blocks.
+   */
+  class SsaReadPosition extends TSsaReadPosition {
+    /** Holds if `v` is read at this position. */
+    abstract predicate hasReadOfVar(SsaVariable v);
+
+    /** Gets a textual representation of this SSA read position. */
+    abstract string toString();
+  }
+
+  /** A basic block in which an SSA variable is read. */
+  class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock {
+    /** Gets the basic block corresponding to this position. */
+    BasicBlock getBlock() { this = TSsaReadPositionBlock(result) }
+
+    override predicate hasReadOfVar(SsaVariable v) { exists(this.getAnSsaRead(v)) }
+
+    pragma[nomagic]
+    Expr getAnSsaRead(SsaVariable v) {
+      v.getAUse() = result and result.getBasicBlock() = this.getBlock()
+    }
+
+    override string toString() { result = "block" }
+  }
+
+  /**
+   * An edge between two basic blocks where the latter block has an SSA phi
+   * definition. The edge therefore has a read of an SSA variable serving as the
+   * input to the phi node.
+   */
+  class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge {
+    /** Gets the source of the edge. */
+    BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) }
+
+    /** Gets the target of the edge. */
+    BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) }
+
+    override predicate hasReadOfVar(SsaVariable v) { this.phiInput(_, v) }
+
+    /** Holds if `inp` is an input to `phi` along this edge. */
+    predicate phiInput(SsaPhiNode phi, SsaVariable inp) {
+      phi.hasInputFromBlock(inp, this.getOrigBlock()) and
+      this.getPhiBlock() = phi.getBasicBlock()
+    }
+
+    override string toString() { result = "edge" }
   }
 
   /**
@@ -40,10 +101,10 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
    * value `testIsTrue`.
    */
   pragma[nomagic]
-  predicate guardDirectlyControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
-    guard.directlyControls(controlled.(Lang::SsaReadPositionBlock).getBlock(), testIsTrue)
+  predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
+    guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
     or
-    exists(Lang::SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
+    exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
       guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
       guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
     )
@@ -52,11 +113,11 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
   /**
    * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
    */
-  predicate guardControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
+  predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
     guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
     or
-    exists(Lang::Guard guard0, boolean testIsTrue0 |
-      Lang::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
+    exists(Guard guard0, boolean testIsTrue0 |
+      implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
       guardControlsSsaRead(guard0, controlled, testIsTrue0)
     )
   }
@@ -64,9 +125,7 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
   /**
    * Holds if `inp` is an input to `phi` along a back edge.
    */
-  predicate backEdge(
-    Lang::SsaPhiNode phi, Lang::SsaVariable inp, Lang::SsaReadPositionPhiInputEdge edge
-  ) {
+  predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
     edge.phiInput(phi, inp) and
     (
       phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
@@ -85,12 +144,33 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
    * dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
    * edges.
    */
-  private predicate irreducibleSccEdge(Lang::BasicBlock b1, Lang::BasicBlock b2) {
+  private predicate irreducibleSccEdge(BasicBlock b1, BasicBlock b2) {
     trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
   }
 
-  private predicate trimmedEdge(Lang::BasicBlock pred, Lang::BasicBlock succ) {
-    Lang::getABasicBlockSuccessor(pred) = succ and
+  private predicate trimmedEdge(BasicBlock pred, BasicBlock succ) {
+    getABasicBlockSuccessor(pred) = succ and
     not succ.bbDominates(pred)
   }
+
+  /**
+   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
+   * in an arbitrary 1-based numbering of the input edges to `phi`.
+   */
+  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
+    edge.phiInput(phi, inp) and
+    edge =
+      rank[r](SsaReadPositionPhiInputEdge e |
+        e.phiInput(phi, _)
+      |
+        e order by getBlockId1(e.getOrigBlock()), getBlockId2(e.getOrigBlock())
+      )
+  }
+
+  /**
+   * Holds if `rix` is the number of input edges to `phi`.
+   */
+  predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
+    rix = max(int r | rankedPhiInput(phi, _, _, r))
+  }
 }