diff --git a/go/ql/lib/change-notes/2026-03-23-use-shared-ssa.md b/go/ql/lib/change-notes/2026-03-23-use-shared-ssa.md
new file mode 100644
index 00000000000..52814b92278
--- /dev/null
+++ b/go/ql/lib/change-notes/2026-03-23-use-shared-ssa.md
@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The Go SSA library now uses the shared SSA library (`codeql.ssa.Ssa`), consistent with other CodeQL languages such as C#, Java, Ruby, Rust, and Swift. This may result in minor changes to SSA construction in some edge cases.
diff --git a/go/ql/lib/qlpack.yml b/go/ql/lib/qlpack.yml
index 2bcd5042425..a542c9a7e98 100644
--- a/go/ql/lib/qlpack.yml
+++ b/go/ql/lib/qlpack.yml
@@ -10,6 +10,7 @@ dependencies:
   codeql/controlflow: ${workspace}
   codeql/dataflow: ${workspace}
   codeql/mad: ${workspace}
+  codeql/ssa: ${workspace}
   codeql/threat-models: ${workspace}
   codeql/tutorial: ${workspace}
   codeql/util: ${workspace}
diff --git a/go/ql/lib/semmle/go/controlflow/BasicBlocks.qll b/go/ql/lib/semmle/go/controlflow/BasicBlocks.qll
index dc52abb25ab..d9908f260bb 100644
--- a/go/ql/lib/semmle/go/controlflow/BasicBlocks.qll
+++ b/go/ql/lib/semmle/go/controlflow/BasicBlocks.qll
@@ -48,6 +48,17 @@ class BasicBlock = BbImpl::BasicBlock;
 
 class EntryBasicBlock = BbImpl::EntryBasicBlock;
 
+/** Provides a `CfgSig` view of Go's control-flow graph for use with the shared SSA library. */
+module Cfg implements BB::CfgSig<Location> {
+  class ControlFlowNode = BbImpl::ControlFlowNode;
+
+  class BasicBlock = BbImpl::BasicBlock;
+
+  class EntryBasicBlock = BbImpl::EntryBasicBlock;
+
+  predicate dominatingEdge = BbImpl::dominatingEdge/2;
+}
+
 cached
 private predicate reachableBB(BasicBlock bb) {
   bb instanceof EntryBasicBlock
diff --git a/go/ql/lib/semmle/go/dataflow/SSA.qll b/go/ql/lib/semmle/go/dataflow/SSA.qll
index 46ce4da3935..3cc6d4304fd 100644
--- a/go/ql/lib/semmle/go/dataflow/SSA.qll
+++ b/go/ql/lib/semmle/go/dataflow/SSA.qll
@@ -63,9 +63,9 @@ private predicate unresolvedIdentifier(Ident id, string name) {
 /**
  * An SSA variable.
  */
-class SsaVariable extends TSsaDefinition {
+class SsaVariable extends Definition {
   /** Gets the source variable corresponding to this SSA variable. */
-  SsaSourceVariable getSourceVariable() { result = this.(SsaDefinition).getSourceVariable() }
+  SsaSourceVariable getSourceVariable() { this.definesAt(result, _, _) }
 
   /** Gets the (unique) definition of this SSA variable. */
   SsaDefinition getDefinition() { result = this }
@@ -74,21 +74,31 @@ class SsaVariable extends TSsaDefinition {
   Type getType() { result = this.getSourceVariable().getType() }
 
   /** Gets a use in basic block `bb` that refers to this SSA variable. */
-  IR::Instruction getAUseIn(ReachableBasicBlock bb) {
+  IR::Instruction getAUseIn(BasicBlock bb) {
     exists(int i, SsaSourceVariable v | v = this.getSourceVariable() |
       result = bb.getNode(i) and
-      this = getDefinition(bb, i, v)
+      ssaDefReachesRead(v, this, bb, i) and
+      useAt(bb, i, v)
     )
   }
 
   /** Gets a use that refers to this SSA variable. */
   IR::Instruction getAUse() { result = this.getAUseIn(_) }
 
-  /** Gets a textual representation of this element. */
-  string toString() { result = this.getDefinition().prettyPrintRef() }
+  /**
+   * Gets a textual representation of this element.
+   *
+   * The format is `kind@LINE:COL`, where `kind` is one of `def`, `capture`, or `phi`.
+   */
+  override string toString() {
+    exists(Location loc | loc = this.(SsaDefinition).getLocation() |
+      result =
+        this.(SsaDefinition).getKind() + "@" + loc.getStartLine() + ":" + loc.getStartColumn()
+    )
+  }
 
   /** Gets the location of this SSA variable. */
-  Location getLocation() { result = this.getDefinition().getLocation() }
+  Location getLocation() { result = this.(SsaDefinition).getLocation() }
 
   /**
    * DEPRECATED: Use `getLocation()` instead.
@@ -109,50 +119,28 @@ class SsaVariable extends TSsaDefinition {
 /**
  * An SSA definition.
  */
-class SsaDefinition extends TSsaDefinition {
+class SsaDefinition extends Definition {
   /** Gets the SSA variable defined by this definition. */
   SsaVariable getVariable() { result = this }
 
   /** Gets the source variable defined by this definition. */
-  abstract SsaSourceVariable getSourceVariable();
+  SsaSourceVariable getSourceVariable() { this.definesAt(result, _, _) }
 
   /**
    * Gets the basic block to which this definition belongs.
    */
-  abstract ReachableBasicBlock getBasicBlock();
-
-  /**
-   * INTERNAL: Use `getBasicBlock()` and `getSourceVariable()` instead.
-   *
-   * Holds if this is a definition of source variable `v` at index `idx` in basic block `bb`.
-   *
-   * Phi nodes are considered to be at index `-1`, all other definitions at the index of
-   * the control flow node they correspond to.
-   */
-  abstract predicate definesAt(ReachableBasicBlock bb, int idx, SsaSourceVariable v);
-
-  /**
-   * INTERNAL: Use `toString()` instead.
-   *
-   * Gets a pretty-printed representation of this SSA definition.
-   */
-  abstract string prettyPrintDef();
-
-  /**
-   * INTERNAL: Do not use.
-   *
-   * Gets a pretty-printed representation of a reference to this SSA definition.
-   */
-  abstract string prettyPrintRef();
+  BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
 
   /** Gets the innermost function or file to which this SSA definition belongs. */
   ControlFlow::Root getRoot() { result = this.getBasicBlock().getScope() }
 
-  /** Gets a textual representation of this element. */
-  string toString() { result = this.prettyPrintDef() }
-
-  /** Gets the source location for this element. */
-  abstract Location getLocation();
+  /**
+   * INTERNAL: Do not use.
+   *
+   * Gets a short string identifying the kind of this SSA definition,
+   * used in reference formatting (e.g., `"def"`, `"capture"`, `"phi"`).
+   */
+  string getKind() { none() }
 
   /**
    * DEPRECATED: Use `getLocation()` instead.
@@ -180,32 +168,25 @@ class SsaDefinition extends TSsaDefinition {
 /**
  * An SSA definition that corresponds to an explicit assignment or other variable definition.
  */
-class SsaExplicitDefinition extends SsaDefinition, TExplicitDef {
+class SsaExplicitDefinition extends SsaDefinition, WriteDefinition {
+  SsaExplicitDefinition() {
+    exists(BasicBlock bb, int i, SsaSourceVariable v |
+      this.definesAt(v, bb, i) and
+      defAt(bb, i, v)
+    )
+  }
+
   /** Gets the instruction where the definition happens. */
   IR::Instruction getInstruction() {
-    exists(BasicBlock bb, int i | this = TExplicitDef(bb, i, _) | result = bb.getNode(i))
+    exists(BasicBlock bb, int i | this.definesAt(_, bb, i) | result = bb.getNode(i))
   }
 
   /** Gets the right-hand side of the definition. */
   IR::Instruction getRhs() { this.getInstruction().writes(_, result) }
 
-  override predicate definesAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    this = TExplicitDef(bb, i, v)
-  }
+  override string getKind() { result = "def" }
 
-  override ReachableBasicBlock getBasicBlock() { this.definesAt(result, _, _) }
-
-  override SsaSourceVariable getSourceVariable() { this = TExplicitDef(_, _, result) }
-
-  override string prettyPrintRef() {
-    exists(Location loc | loc = this.getLocation() |
-      result = "def@" + loc.getStartLine() + ":" + loc.getStartColumn()
-    )
-  }
-
-  override string prettyPrintDef() { result = "definition of " + this.getSourceVariable() }
-
-  override Location getLocation() { result = this.getInstruction().getLocation() }
+  override string toString() { result = "definition of " + this.getSourceVariable() }
 }
 
 /** Provides a helper predicate for working with explicit SSA definitions. */
@@ -220,19 +201,6 @@ module SsaExplicitDefinition {
  * An SSA definition that does not correspond to an explicit variable definition.
  */
 abstract class SsaImplicitDefinition extends SsaDefinition {
-  /**
-   * INTERNAL: Do not use.
-   *
-   * Gets the definition kind to include in `prettyPrintRef`.
-   */
-  abstract string getKind();
-
-  override string prettyPrintRef() {
-    exists(Location loc | loc = this.getLocation() |
-      result = this.getKind() + "@" + loc.getStartLine() + ":" + loc.getStartColumn()
-    )
-  }
-
   override Location getLocation() { result = this.getBasicBlock().getLocation() }
 }
 
@@ -243,24 +211,16 @@ abstract class SsaImplicitDefinition extends SsaDefinition {
  * Capturing definitions appear at the beginning of such functions, as well as
  * at any function call that may affect the value of the variable.
  */
-class SsaVariableCapture extends SsaImplicitDefinition, TCapture {
-  override predicate definesAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    this = TCapture(bb, i, v)
-  }
-
-  override ReachableBasicBlock getBasicBlock() { this.definesAt(result, _, _) }
-
-  override SsaSourceVariable getSourceVariable() { this.definesAt(_, _, result) }
-
-  override string getKind() { result = "capture" }
-
-  override string prettyPrintDef() { result = "capture variable " + this.getSourceVariable() }
-
+class SsaVariableCapture extends SsaImplicitDefinition, UncertainWriteDefinition {
   override Location getLocation() {
-    exists(ReachableBasicBlock bb, int i | this.definesAt(bb, i, _) |
+    exists(BasicBlock bb, int i | this.definesAt(_, bb, i) |
       result = bb.getNode(i).getLocation()
     )
   }
+
+  override string getKind() { result = "capture" }
+
+  override string toString() { result = "capture variable " + this.getSourceVariable() }
 }
 
 /**
@@ -277,7 +237,10 @@ abstract class SsaPseudoDefinition extends SsaImplicitDefinition {
    * Gets a textual representation of the inputs of this pseudo-definition
    * in lexicographical order.
    */
-  string ppInputs() { result = concat(this.getAnInput().getDefinition().prettyPrintRef(), ", ") }
+  string ppInputs() {
+    result =
+      concat(SsaVariable inp | inp = this.getAnInput() | inp.toString() order by inp.toString())
+  }
 }
 
 /**
@@ -285,26 +248,14 @@ abstract class SsaPseudoDefinition extends SsaImplicitDefinition {
  * in the flow graph where otherwise two or more definitions for the variable
  * would be visible.
  */
-class SsaPhiNode extends SsaPseudoDefinition, TPhi {
-  override SsaVariable getAnInput() {
-    result = getDefReachingEndOf(this.getBasicBlock().getAPredecessor(_), this.getSourceVariable())
-  }
-
-  override predicate definesAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    bb = this.getBasicBlock() and v = this.getSourceVariable() and i = -1
-  }
-
-  override ReachableBasicBlock getBasicBlock() { this = TPhi(result, _) }
-
-  override SsaSourceVariable getSourceVariable() { this = TPhi(_, result) }
+class SsaPhiNode extends SsaPseudoDefinition, PhiNode {
+  override SsaVariable getAnInput() { phiHasInputFromBlock(this, result, _) }
 
   override string getKind() { result = "phi" }
 
-  override string prettyPrintDef() {
+  override string toString() {
     result = this.getSourceVariable() + " = phi(" + this.ppInputs() + ")"
   }
-
-  override Location getLocation() { result = this.getBasicBlock().getLocation() }
 }
 
 /**
diff --git a/go/ql/lib/semmle/go/dataflow/SsaImpl.qll b/go/ql/lib/semmle/go/dataflow/SsaImpl.qll
index 9648335a6dd..f972174184a 100644
--- a/go/ql/lib/semmle/go/dataflow/SsaImpl.qll
+++ b/go/ql/lib/semmle/go/dataflow/SsaImpl.qll
@@ -7,76 +7,25 @@ overlay[local]
 module;
 
 import go
+private import codeql.ssa.Ssa as SsaImplCommon
+private import semmle.go.controlflow.BasicBlocks as BasicBlocks
+
+private class BasicBlock = BasicBlocks::BasicBlock;
 
 cached
 private module Internal {
   /** Holds if the `i`th node of `bb` defines `v`. */
   cached
-  predicate defAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
+  predicate defAt(BasicBlock bb, int i, SsaSourceVariable v) {
     bb.getNode(i).(IR::Instruction).writes(v, _)
   }
 
   /** Holds if the `i`th node of `bb` reads `v`. */
   cached
-  predicate useAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
+  predicate useAt(BasicBlock bb, int i, SsaSourceVariable v) {
     bb.getNode(i).(IR::Instruction).reads(v)
   }
 
-  /**
-   * A data type representing SSA definitions.
-   *
-   * We distinguish three kinds of SSA definitions:
-   *
-   *   1. Variable definitions, including declarations, assignments and increments/decrements.
-   *   2. Pseudo-definitions for captured variables at the beginning of the capturing function
-   *      as well as after calls.
-   *   3. Phi nodes.
-   *
-   * SSA definitions are only introduced where necessary. In particular,
-   * unreachable code has no SSA definitions associated with it, and neither
-   * have dead assignments (that is, assignments whose value is never read).
-   */
-  cached
-  newtype TSsaDefinition =
-    /**
-     * An SSA definition that corresponds to an explicit assignment or other variable definition.
-     */
-    TExplicitDef(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-      defAt(bb, i, v) and
-      (liveAfterDef(bb, i, v) or v.isCaptured())
-    } or
-    /**
-     * An SSA definition representing the capturing of an SSA-convertible variable
-     * in the closure of a nested function.
-     *
-     * Capturing definitions appear at the beginning of such functions, as well as
-     * at any function call that may affect the value of the variable.
-     */
-    TCapture(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-      mayCapture(bb, i, v) and
-      liveAfterDef(bb, i, v)
-    } or
-    /**
-     * An SSA phi node, that is, a pseudo-definition for a variable at a point
-     * in the flow graph where otherwise two or more definitions for the variable
-     * would be visible.
-     */
-    TPhi(ReachableJoinBlock bb, SsaSourceVariable v) {
-      liveAtEntry(bb, v) and
-      inDefDominanceFrontier(bb, v)
-    }
-
-  /**
-   * Holds if `bb` is in the dominance frontier of a block containing a definition of `v`.
-   */
-  pragma[noinline]
-  private predicate inDefDominanceFrontier(ReachableJoinBlock bb, SsaSourceVariable v) {
-    exists(ReachableBasicBlock defbb, SsaDefinition def |
-      def.definesAt(defbb, _, v) and
-      defbb.inDominanceFrontier(bb)
-    )
-  }
-
   /**
    * Holds if `v` is a captured variable which is declared in `declFun` and read in `useFun`.
    */
@@ -87,7 +36,7 @@ private module Internal {
   }
 
   /** Holds if the `i`th node of `bb` in function `f` is an entry node. */
-  private predicate entryNode(FuncDef f, ReachableBasicBlock bb, int i) {
+  private predicate entryNode(FuncDef f, BasicBlock bb, int i) {
     f = bb.getScope() and
     bb.getNode(i).isEntryNode()
   }
@@ -95,17 +44,17 @@ private module Internal {
   /**
    * Holds if the `i`th node of `bb` in function `f` is a function call.
    */
-  private predicate callNode(FuncDef f, ReachableBasicBlock bb, int i) {
+  private predicate callNode(FuncDef f, BasicBlock bb, int i) {
     f = bb.getScope() and
     bb.getNode(i).(IR::EvalInstruction).getExpr() instanceof CallExpr
   }
 
   /**
    * Holds if the `i`th node of basic block `bb` may induce a pseudo-definition for
-   * modeling updates to captured variable `v`. Whether the definition is actually
-   * introduced depends on whether `v` is live at this point in the program.
+   * modeling updates to captured variable `v`.
    */
-  private predicate mayCapture(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
+  cached
+  predicate mayCapture(BasicBlock bb, int i, SsaSourceVariable v) {
     exists(FuncDef capturingContainer, FuncDef declContainer |
       // capture initial value of variable declared in enclosing scope
       readsCapturedVar(capturingContainer, v, declContainer) and
@@ -119,347 +68,109 @@ private module Internal {
     )
   }
 
-  /** A classification of variable references into reads and writes. */
-  private newtype RefKind =
-    ReadRef() or
-    WriteRef()
-
-  /**
-   * Holds if the `i`th node of basic block `bb` is a reference to `v`, either a read
-   * (when `tp` is `ReadRef()`) or a direct or indirect write (when `tp` is `WriteRef()`).
-   */
-  private predicate ref(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind tp) {
-    useAt(bb, i, v) and tp = ReadRef()
-    or
-    (mayCapture(bb, i, v) or defAt(bb, i, v)) and
-    tp = WriteRef()
-  }
-
-  /**
-   * 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 `tp`.
-   */
-  private int refRank(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind tp) {
-    i = rank[result](int j | ref(bb, j, v, _)) and
-    ref(bb, i, v, tp)
-  }
-
-  /**
-   * Gets the maximum rank among all references to `v` in basic block `bb`.
-   */
-  private int maxRefRank(ReachableBasicBlock bb, SsaSourceVariable v) {
-    result = max(refRank(bb, _, v, _))
-  }
-
-  /**
-   * Holds if variable `v` is live after the `i`th node of basic block `bb`, where
-   * `i` is the index of a node that may assign or capture `v`.
-   *
-   * For the purposes of this predicate, function calls are considered as writes of captured variables.
-   */
-  private predicate liveAfterDef(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    exists(int r | r = refRank(bb, i, v, WriteRef()) |
-      // the next reference to `v` inside `bb` is a read
-      r + 1 = refRank(bb, _, v, ReadRef())
-      or
-      // this is the last reference to `v` inside `bb`, but `v` is live at entry
-      // to a successor basic block of `bb`
-      r = maxRefRank(bb, v) and
-      liveAtSuccEntry(bb, v)
-    )
-  }
-
-  /**
-   * Holds if variable `v` is live at the beginning of basic block `bb`.
-   *
-   * For the purposes of this predicate, function calls are considered as writes of captured variables.
-   */
-  private predicate liveAtEntry(ReachableBasicBlock bb, SsaSourceVariable v) {
-    // the first reference to `v` inside `bb` is a read
-    refRank(bb, _, v, ReadRef()) = 1
-    or
-    // there is no reference to `v` inside `bb`, but `v` is live at entry
-    // to a successor basic block of `bb`
-    not exists(refRank(bb, _, v, _)) and
-    liveAtSuccEntry(bb, v)
-  }
-
-  /**
-   * Holds if `v` is live at the beginning of any successor of basic block `bb`.
-   */
-  private predicate liveAtSuccEntry(ReachableBasicBlock bb, SsaSourceVariable v) {
-    liveAtEntry(bb.getASuccessor(_), v)
-  }
-
   /**
    * Holds if `v` is assigned outside its declaring function.
    */
-  private predicate assignedThroughClosure(SsaSourceVariable v) {
+  cached
+  predicate assignedThroughClosure(SsaSourceVariable v) {
     any(IR::Instruction def | def.writes(v, _)).getRoot() != v.getDeclaringFunction()
   }
 
-  /**
-   * Holds if the `i`th node of `bb` is a use or an SSA definition of variable `v`, with
-   * `k` indicating whether it is the former or the latter.
-   *
-   * Note this includes phi nodes, whereas `ref` above only includes explicit writes and captures.
-   */
-  private predicate ssaRef(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind k) {
-    useAt(bb, i, v) and k = ReadRef()
-    or
-    any(SsaDefinition def).definesAt(bb, i, v) and k = WriteRef()
-  }
-
-  /**
-   * Gets the (1-based) rank of the `i`th node of `bb` among all SSA definitions
-   * and uses of `v` in `bb`, with `k` indicating whether it is a definition or a use.
-   *
-   * For example, if `bb` is a basic block with a phi node for `v` (considered
-   * to be at index -1), uses `v` at node 2 and defines it at node 5, we have:
-   *
-   * ```
-   * ssaRefRank(bb, -1, v, WriteRef()) = 1    // phi node
-   * ssaRefRank(bb,  2, v, ReadRef())  = 2    // use at node 2
-   * ssaRefRank(bb,  5, v, WriteRef()) = 3    // definition at node 5
-   * ```
-   */
-  private int ssaRefRank(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind k) {
-    i = rank[result](int j | ssaRef(bb, j, v, _)) and
-    ssaRef(bb, i, v, k)
-  }
-
-  /**
-   * Gets the minimum rank of a read in `bb` such that all references to `v` between that
-   * read and the read at index `i` are reads (and not writes).
-   */
-  private int rewindReads(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    exists(int r | r = ssaRefRank(bb, i, v, ReadRef()) |
-      exists(int j, RefKind k | r - 1 = ssaRefRank(bb, j, v, k) |
-        k = ReadRef() and result = rewindReads(bb, j, v)
-        or
-        k = WriteRef() and result = r
-      )
-      or
-      r = 1 and result = r
-    )
-  }
-
-  /**
-   * Gets the SSA definition of `v` in `bb` that reaches the read of `v` at node `i`, if any.
-   */
-  private SsaDefinition getLocalDefinition(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    exists(int r | r = rewindReads(bb, i, v) |
-      exists(int j | result.definesAt(bb, j, v) and ssaRefRank(bb, j, v, _) = r - 1)
-    )
-  }
-
-  /**
-   * Gets an SSA definition of `v` that reaches the end of the immediate dominator of `bb`.
-   */
-  pragma[noinline]
-  private SsaDefinition getDefReachingEndOfImmediateDominator(
-    ReachableBasicBlock bb, SsaSourceVariable v
-  ) {
-    result = getDefReachingEndOf(bb.getImmediateDominator(), v)
-  }
-
-  /**
-   * Gets an SSA definition of `v` that reaches the end of basic block `bb`.
-   */
-  cached
-  SsaDefinition getDefReachingEndOf(ReachableBasicBlock bb, SsaSourceVariable v) {
-    exists(int lastRef | lastRef = max(int i | ssaRef(bb, i, v, _)) |
-      result = getLocalDefinition(bb, lastRef, v)
-      or
-      result.definesAt(bb, lastRef, v) and
-      liveAtSuccEntry(bb, v)
-    )
-    or
-    // In SSA form, the (unique) reaching definition of a use is the closest
-    // definition that dominates the use. If two definitions dominate a node
-    // then one must dominate the other, so we can find the reaching definition
-    // by following the idominance relation backwards.
-    result = getDefReachingEndOfImmediateDominator(bb, v) and
-    not exists(SsaDefinition ssa | ssa.definesAt(bb, _, v)) and
-    liveAtSuccEntry(bb, v)
-  }
-
-  /**
-   * Gets the unique SSA definition of `v` whose value reaches the `i`th node of `bb`,
-   * which is a use of `v`.
-   */
-  cached
-  SsaDefinition getDefinition(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
-    result = getLocalDefinition(bb, i, v)
-    or
-    rewindReads(bb, i, v) = 1 and result = getDefReachingEndOf(bb.getImmediateDominator(), v)
-  }
-
-  private module AdjacentUsesImpl {
-    /** Holds if `v` is defined or used in `b`. */
-    private predicate varOccursInBlock(SsaSourceVariable v, ReachableBasicBlock b) {
-      ssaRef(b, _, v, _)
-    }
-
-    /** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */
-    private predicate blockPrecedesVar(SsaSourceVariable v, ReachableBasicBlock b) {
-      varOccursInBlock(v, b)
-      or
-      exists(getDefReachingEndOf(b, v))
-    }
+  module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
+    class SourceVariable = SsaSourceVariable;
 
     /**
-     * Holds if `v` occurs in `b1` and `b2` is one of `b1`'s successors.
+     * Holds if the `i`th node of basic block `bb` is a (potential) write to source
+     * variable `v`. The Boolean `certain` indicates whether the write is certain.
      *
-     * Factored out of `varBlockReaches` to force join order compared to the larger
-     * set `blockPrecedesVar(v, b2)`.
+     * Certain writes are explicit definitions; uncertain writes are captures.
      */
-    pragma[noinline]
-    private predicate varBlockReachesBaseCand(
-      SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock b2
-    ) {
-      varOccursInBlock(v, b1) and
-      b2 = b1.getASuccessor(_)
-    }
-
-    /**
-     * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
-     * in `b2` or one of its transitive successors but not in any block on the path
-     * between `b1` and `b2`. Unlike `varBlockReaches` this may include blocks `b2`
-     * where `v` is dead.
-     *
-     * Factored out of `varBlockReaches` to force join order compared to the larger
-     * set `blockPrecedesVar(v, b2)`.
-     */
-    pragma[noinline]
-    private predicate varBlockReachesRecCand(
-      SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock mid, ReachableBasicBlock b2
-    ) {
-      varBlockReaches(v, b1, mid) and
-      not varOccursInBlock(v, mid) and
-      b2 = mid.getASuccessor(_)
-    }
-
-    /**
-     * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
-     * in `b2` or one of its transitive successors but not in any block on the path
-     * between `b1` and `b2`.
-     */
-    private predicate varBlockReaches(
-      SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock b2
-    ) {
-      varBlockReachesBaseCand(v, b1, b2) and
-      blockPrecedesVar(v, b2)
+    predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+      defAt(bb, i, v) and certain = true
       or
-      varBlockReachesRecCand(v, b1, _, b2) and
-      blockPrecedesVar(v, b2)
+      mayCapture(bb, i, v) and certain = false
     }
 
     /**
-     * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
-     * `b2` but not in any block on the path between `b1` and `b2`.
+     * Holds if the `i`th node of basic block `bb` reads source variable `v`.
      */
-    private predicate varBlockStep(
-      SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock b2
-    ) {
-      varBlockReaches(v, b1, b2) and
-      varOccursInBlock(v, b2)
+    predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+      useAt(bb, i, v) and certain = true
     }
-
-    /**
-     * Gets the maximum rank among all SSA references to `v` in basic block `bb`.
-     */
-    private int maxSsaRefRank(ReachableBasicBlock bb, SsaSourceVariable v) {
-      result = max(ssaRefRank(bb, _, v, _))
-    }
-
-    /**
-     * Holds if `v` occurs at index `i1` in `b1` and at index `i2` in `b2` and
-     * there is a path between them without any occurrence of `v`.
-     */
-    pragma[nomagic]
-    predicate adjacentVarRefs(
-      SsaSourceVariable v, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2, int i2
-    ) {
-      exists(int rankix |
-        b1 = b2 and
-        ssaRefRank(b1, i1, v, _) = rankix and
-        ssaRefRank(b2, i2, v, _) = rankix + 1
-      )
-      or
-      maxSsaRefRank(b1, v) = ssaRefRank(b1, i1, v, _) and
-      varBlockStep(v, b1, b2) and
-      ssaRefRank(b2, i2, v, _) = 1
-    }
-
-    predicate variableUse(SsaSourceVariable v, IR::Instruction use, ReachableBasicBlock bb, int i) {
-      bb.getNode(i) = use and
-      exists(SsaVariable sv |
-        sv.getSourceVariable() = v and
-        use = sv.getAUse()
-      )
-    }
-  }
-
-  private import AdjacentUsesImpl
-
-  /**
-   * Holds if the value defined at `def` can reach `use` without passing through
-   * any other uses, but possibly through phi nodes.
-   */
-  cached
-  predicate firstUse(SsaDefinition def, IR::Instruction use) {
-    exists(SsaSourceVariable v, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2, int i2 |
-      adjacentVarRefs(v, b1, i1, b2, i2) and
-      def.definesAt(b1, i1, v) and
-      variableUse(v, use, b2, i2)
-    )
-    or
-    exists(
-      SsaSourceVariable v, SsaPhiNode redef, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2,
-      int i2
-    |
-      adjacentVarRefs(v, b1, i1, b2, i2) and
-      def.definesAt(b1, i1, v) and
-      redef.definesAt(b2, i2, v) and
-      firstUse(redef, use)
-    )
-  }
-
-  /**
-   * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
-   * variable, that is, the value read in `use1` can reach `use2` without passing
-   * through any other use or any SSA definition of the variable.
-   */
-  cached
-  predicate adjacentUseUseSameVar(IR::Instruction use1, IR::Instruction use2) {
-    exists(SsaSourceVariable v, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2, int i2 |
-      adjacentVarRefs(v, b1, i1, b2, i2) and
-      variableUse(v, use1, b1, i1) and
-      variableUse(v, use2, b2, i2)
-    )
-  }
-
-  /**
-   * Holds if `use1` and `use2` form an adjacent use-use-pair of the same
-   * `SsaSourceVariable`, that is, the value read in `use1` can reach `use2`
-   * without passing through any other use or any SSA definition of the variable
-   * except for phi nodes and uncertain implicit updates.
-   */
-  cached
-  predicate adjacentUseUse(IR::Instruction use1, IR::Instruction use2) {
-    adjacentUseUseSameVar(use1, use2)
-    or
-    exists(
-      SsaSourceVariable v, SsaPhiNode def, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2,
-      int i2
-    |
-      adjacentVarRefs(v, b1, i1, b2, i2) and
-      variableUse(v, use1, b1, i1) and
-      def.definesAt(b2, i2, v) and
-      firstUse(def, use2)
-    )
   }
 }
 
 import Internal
+import SsaImplCommon::Make<Location, BasicBlocks::Cfg, SsaInput> as Impl
+
+final class Definition = Impl::Definition;
+
+final class WriteDefinition = Impl::WriteDefinition;
+
+final class UncertainWriteDefinition = Impl::UncertainWriteDefinition;
+
+final class PhiNode = Impl::PhiNode;
+
+module Consistency = Impl::Consistency;
+
+/**
+ * NB: This predicate should be cached.
+ *
+ * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
+ * basic block `bb`.
+ */
+cached
+predicate ssaDefReachesRead(SsaSourceVariable v, Definition def, BasicBlock bb, int i) {
+  Impl::ssaDefReachesRead(v, def, bb, i)
+}
+
+/**
+ * NB: This predicate should be cached.
+ *
+ * Holds if the SSA definition of `v` at `def` reaches the end of basic block `bb`.
+ */
+cached
+predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SsaSourceVariable v) {
+  Impl::ssaDefReachesEndOfBlock(bb, def, v)
+}
+
+/**
+ * NB: This predicate should be cached.
+ *
+ * Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
+ */
+cached
+predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
+  Impl::phiHasInputFromBlock(phi, inp, bb)
+}
+
+/**
+ * NB: This predicate should be cached.
+ *
+ * Holds if `def` reaches the first use `use` without going through any other use,
+ * but possibly through phi nodes.
+ */
+cached
+predicate firstUse(Definition def, IR::Instruction use) {
+  exists(BasicBlock bb, int i |
+    Impl::firstUse(def, bb, i, _) and
+    use = bb.getNode(i)
+  )
+}
+
+/**
+ * NB: This predicate should be cached.
+ *
+ * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
+ * variable, that is, the value read in `use1` can reach `use2` without passing
+ * through any other use or any SSA definition of the variable except for phi nodes
+ * and uncertain implicit updates.
+ */
+cached
+predicate adjacentUseUse(IR::Instruction use1, IR::Instruction use2) {
+  exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+    Impl::adjacentUseUse(bb1, i1, bb2, i2, _, _) and
+    use1 = bb1.getNode(i1) and
+    use2 = bb2.getNode(i2)
+  )
+}