diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
index 70b2f3cf0d84..f6371e5b696c 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
@@ -1318,7 +1318,7 @@ predicate nodeIsHidden(Node n) {
   or
   n instanceof InitialGlobalValue
   or
-  n instanceof SsaPhiInputNode
+  n instanceof SsaSynthNode
 }
 
 predicate neverSkipInPathGraph(Node n) {
@@ -1632,9 +1632,7 @@ private Instruction getAnInstruction(Node n) {
   not n instanceof InstructionNode and
   result = n.asOperand().getUse()
   or
-  result = n.(SsaPhiNode).getPhiNode().getBasicBlock().getFirstInstruction()
-  or
-  result = n.(SsaPhiInputNode).getBasicBlock().getFirstInstruction()
+  result = n.(SsaSynthNode).getBasicBlock().getFirstInstruction()
   or
   n.(IndirectInstruction).hasInstructionAndIndirectionIndex(result, _)
   or
@@ -1766,14 +1764,14 @@ module IteratorFlow {
      * Note: Unlike `def.getAnUltimateDefinition()` this predicate also
      * traverses back through iterator increment and decrement operations.
      */
-    private Ssa::DefinitionExt getAnUltimateDefinition(Ssa::DefinitionExt def) {
+    private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
       result = def.getAnUltimateDefinition()
       or
       exists(IRBlock bb, int i, IteratorCrementCall crementCall, Ssa::SourceVariable sv |
         crementCall = def.getValue().asInstruction().(StoreInstruction).getSourceValue() and
         sv = def.getSourceVariable() and
         bb.getInstruction(i) = crementCall and
-        Ssa::ssaDefReachesReadExt(sv, result, bb, i)
+        Ssa::ssaDefReachesRead(sv, result, bb, i)
       )
     }
 
@@ -1801,13 +1799,13 @@ module IteratorFlow {
       GetsIteratorCall beginCall, Instruction writeToDeref
     ) {
       exists(
-        StoreInstruction beginStore, IRBlock bbStar, int iStar, Ssa::DefinitionExt def,
-        IteratorPointerDereferenceCall starCall, Ssa::DefinitionExt ultimate, Operand address
+        StoreInstruction beginStore, IRBlock bbStar, int iStar, Ssa::Definition def,
+        IteratorPointerDereferenceCall starCall, Ssa::Definition ultimate, Operand address
       |
         isIteratorWrite(writeToDeref, address) and
         operandForFullyConvertedCall(address, starCall) and
         bbStar.getInstruction(iStar) = starCall and
-        Ssa::ssaDefReachesReadExt(_, def, bbStar, iStar) and
+        Ssa::ssaDefReachesRead(_, def, bbStar, iStar) and
         ultimate = getAnUltimateDefinition*(def) and
         beginStore = ultimate.getValue().asInstruction() and
         operandForFullyConvertedCall(beginStore.getSourceValueOperand(), beginCall)
@@ -1836,45 +1834,15 @@ module IteratorFlow {
 
   private module IteratorSsa = SsaImpl::Make<Location, SsaInput>;
 
-  cached
-  private newtype TSsaDef =
-    TDef(IteratorSsa::DefinitionExt def) or
-    TPhi(PhiNode phi)
-
-  abstract private class SsaDef extends TSsaDef {
-    /** Gets a textual representation of this element. */
-    string toString() { none() }
-
-    /** Gets the underlying non-phi definition or use. */
-    IteratorSsa::DefinitionExt asDef() { none() }
-
-    /** Gets the underlying phi node. */
-    PhiNode asPhi() { none() }
-
-    /** Gets the location of this element. */
-    abstract Location getLocation();
-  }
-
-  private class Def extends TDef, SsaDef {
-    IteratorSsa::DefinitionExt def;
-
-    Def() { this = TDef(def) }
-
-    final override IteratorSsa::DefinitionExt asDef() { result = def }
-
+  private class Def extends IteratorSsa::DefinitionExt {
     final override Location getLocation() { result = this.getImpl().getLocation() }
 
-    /** Gets the variable written to by this definition. */
-    final SourceVariable getSourceVariable() { result = def.getSourceVariable() }
-
-    override string toString() { result = def.toString() }
-
     /**
      * Holds if this definition (or use) has index `index` in block `block`,
      * and is a definition (or use) of the variable `sv`.
      */
     predicate hasIndexInBlock(IRBlock block, int index, SourceVariable sv) {
-      def.definesAt(sv, block, index, _)
+      super.definesAt(sv, block, index, _)
     }
 
     private Ssa::DefImpl getImpl() {
@@ -1891,20 +1859,6 @@ module IteratorFlow {
     int getIndirectionIndex() { result = this.getImpl().getIndirectionIndex() }
   }
 
-  private class Phi extends TPhi, SsaDef {
-    PhiNode phi;
-
-    Phi() { this = TPhi(phi) }
-
-    final override PhiNode asPhi() { result = phi }
-
-    final override Location getLocation() { result = phi.getBasicBlock().getLocation() }
-
-    override string toString() { result = phi.toString() }
-
-    SsaIteratorNode getNode() { result.getIteratorFlowNode() = phi }
-  }
-
   private class PhiNode extends IteratorSsa::DefinitionExt {
     PhiNode() {
       this instanceof IteratorSsa::PhiNode or
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
index a6018535824a..3b6e190cc981 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
@@ -27,7 +27,7 @@ import ExprNodes
  * - `VariableNode`, which is used to model flow through global variables.
  * - `PostUpdateNodeImpl`, which is used to model the state of an object after
  *    an update after a number of loads.
- * - `SsaPhiNode`, which represents phi nodes as computed by the shared SSA
+ * - `SsaSynthNode`, which represents synthesized nodes as computed by the shared SSA
  *    library.
  * - `RawIndirectOperand`, which represents the value of `operand` after
  *    loading the address a number of times.
@@ -47,8 +47,7 @@ private newtype TIRDataFlowNode =
     or
     Ssa::isModifiableByCall(operand, indirectionIndex)
   } or
-  TSsaPhiInputNode(Ssa::PhiNode phi, IRBlock input) { phi.hasInputFromBlock(_, _, _, _, input) } or
-  TSsaPhiNode(Ssa::PhiNode phi) or
+  TSsaSynthNode(Ssa::SynthNode n) or
   TSsaIteratorNode(IteratorFlow::IteratorFlowNode n) or
   TRawIndirectOperand0(Node0Impl node, int indirectionIndex) {
     Ssa::hasRawIndirectOperand(node.asOperand(), indirectionIndex)
@@ -184,10 +183,11 @@ class Node extends TIRDataFlowNode {
     or
     this.asOperand().getUse() = block.getInstruction(i)
     or
-    this.(SsaPhiNode).getPhiNode().getBasicBlock() = block and i = -1
-    or
-    this.(SsaPhiInputNode).getBlock() = block and
-    i = block.getInstructionCount()
+    exists(Ssa::SynthNode ssaNode |
+      this.(SsaSynthNode).getSynthNode() = ssaNode and
+      ssaNode.getBasicBlock() = block and
+      ssaNode.getIndex() = i
+    )
     or
     this.(RawIndirectOperand).getOperand().getUse() = block.getInstruction(i)
     or
@@ -364,10 +364,10 @@ class Node extends TIRDataFlowNode {
    * pointed to by `p`.
    */
   Expr asDefinition(boolean uncertain) {
-    exists(StoreInstruction store, Ssa::DefinitionExt def |
+    exists(StoreInstruction store, Ssa::Definition def |
       store = this.asInstruction() and
       result = asDefinitionImpl(store) and
-      Ssa::defToNode(this, def, _, _, _, _) and
+      Ssa::defToNode(this, def, _) and
       if def.isCertain() then uncertain = false else uncertain = true
     )
   }
@@ -686,117 +686,30 @@ class PostFieldUpdateNode extends PostUpdateNodeImpl {
 /**
  * INTERNAL: do not use.
  *
- * A phi node produced by the shared SSA library, viewed as a node in a data flow graph.
+ * A synthesized SSA node produced by the shared SSA library, viewed as a node
+ * in a data flow graph.
  */
-class SsaPhiNode extends Node, TSsaPhiNode {
-  Ssa::PhiNode phi;
-
-  SsaPhiNode() { this = TSsaPhiNode(phi) }
-
-  /** Gets the phi node associated with this node. */
-  Ssa::PhiNode getPhiNode() { result = phi }
-
-  override DataFlowCallable getEnclosingCallable() {
-    result.asSourceCallable() = this.getFunction()
-  }
+class SsaSynthNode extends Node, TSsaSynthNode {
+  Ssa::SynthNode node;
 
-  override Declaration getFunction() { result = phi.getBasicBlock().getEnclosingFunction() }
-
-  override DataFlowType getType() {
-    exists(Ssa::SourceVariable sv |
-      this.getPhiNode().definesAt(sv, _, _, _) and
-      result = sv.getType()
-    )
-  }
-
-  override predicate isGLValue() { phi.getSourceVariable().isGLValue() }
-
-  final override Location getLocationImpl() { result = phi.getBasicBlock().getLocation() }
-
-  override string toStringImpl() { result = phi.toString() }
-
-  /**
-   * Gets a node that is used as input to this phi node.
-   * `fromBackEdge` is true if data flows along a back-edge,
-   * and `false` otherwise.
-   */
-  cached
-  final Node getAnInput(boolean fromBackEdge) {
-    result.(SsaPhiInputNode).getPhiNode() = phi and
-    exists(IRBlock bPhi, IRBlock bResult |
-      bPhi = phi.getBasicBlock() and bResult = result.getBasicBlock()
-    |
-      if bPhi.dominates(bResult) then fromBackEdge = true else fromBackEdge = false
-    )
-  }
-
-  /** Gets a node that is used as input to this phi node. */
-  final Node getAnInput() { result = this.getAnInput(_) }
-
-  /** Gets the source variable underlying this phi node. */
-  Ssa::SourceVariable getSourceVariable() { result = phi.getSourceVariable() }
-
-  /**
-   * Holds if this phi node is a phi-read node.
-   *
-   * Phi-read nodes are like normal phi nodes, but they are inserted based
-   * on reads instead of writes.
-   */
-  predicate isPhiRead() { phi.isPhiRead() }
-}
-
-/**
- * INTERNAL: Do not use.
- *
- * A node that is used as an input to a phi node.
- *
- * This class exists to allow more powerful barrier guards. Consider this
- * example:
- *
- * ```cpp
- * int x = source();
- * if(!safe(x)) {
- *   x = clear();
- * }
- * // phi node for x here
- * sink(x);
- * ```
- *
- * At the phi node for `x` it is neither the case that `x` is dominated by
- * `safe(x)`, or is the case that the phi is dominated by a clearing of `x`.
- *
- * By inserting a "phi input" node as the last entry in the basic block that
- * defines the inputs to the phi we can conclude that each of those inputs are
- * safe to pass to `sink`.
- */
-class SsaPhiInputNode extends Node, TSsaPhiInputNode {
-  Ssa::PhiNode phi;
-  IRBlock block;
-
-  SsaPhiInputNode() { this = TSsaPhiInputNode(phi, block) }
-
-  /** Gets the phi node associated with this node. */
-  Ssa::PhiNode getPhiNode() { result = phi }
+  SsaSynthNode() { this = TSsaSynthNode(node) }
 
-  /** Gets the basic block in which this input originates. */
-  IRBlock getBlock() { result = block }
+  /** Gets the synthesized SSA node associated with this node. */
+  Ssa::SynthNode getSynthNode() { result = node }
 
   override DataFlowCallable getEnclosingCallable() {
     result.asSourceCallable() = this.getFunction()
   }
 
-  override Declaration getFunction() { result = phi.getBasicBlock().getEnclosingFunction() }
+  override Declaration getFunction() { result = node.getBasicBlock().getEnclosingFunction() }
 
-  override DataFlowType getType() { result = this.getSourceVariable().getType() }
+  override DataFlowType getType() { result = node.getSourceVariable().getType() }
 
-  override predicate isGLValue() { phi.getSourceVariable().isGLValue() }
+  override predicate isGLValue() { node.getSourceVariable().isGLValue() }
 
-  final override Location getLocationImpl() { result = block.getLastInstruction().getLocation() }
-
-  override string toStringImpl() { result = "Phi input" }
+  final override Location getLocationImpl() { result = node.getLocation() }
 
-  /** Gets the source variable underlying this phi node. */
-  Ssa::SourceVariable getSourceVariable() { result = phi.getSourceVariable() }
+  override string toStringImpl() { result = node.toString() }
 }
 
 /**
@@ -1371,10 +1284,10 @@ class UninitializedNode extends Node {
   LocalVariable v;
 
   UninitializedNode() {
-    exists(Ssa::DefinitionExt def, Ssa::SourceVariable sv |
+    exists(Ssa::Definition def, Ssa::SourceVariable sv |
       def.getIndirectionIndex() = 0 and
       def.getValue().asInstruction() instanceof UninitializedInstruction and
-      Ssa::defToNode(this, def, sv, _, _, _) and
+      Ssa::defToNode(this, def, sv) and
       v = sv.getBaseVariable().(Ssa::BaseIRVariable).getIRVariable().getAst()
     )
   }
@@ -1799,6 +1712,21 @@ predicate hasInstructionAndIndex(
 
 cached
 private module Cached {
+  /**
+   * Holds if `n` has a local flow step that goes through a back-edge.
+   */
+  cached
+  predicate flowsToBackEdge(Node n) {
+    exists(Node succ, IRBlock bb1, IRBlock bb2 |
+      Ssa::ssaFlow(n, succ) and
+      bb1 = n.getBasicBlock() and
+      bb2 = succ.getBasicBlock() and
+      bb1 != bb2 and
+      bb2.dominates(bb1) and
+      bb1.getASuccessor+() = bb2
+    )
+  }
+
   /**
    * Holds if data flows from `nodeFrom` to `nodeTo` in exactly one local
    * (intra-procedural) step. This relation is only used for local dataflow
@@ -1887,15 +1815,9 @@ private module Cached {
   cached
   predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
     (
-      // Post update node -> Node flow
-      Ssa::postUpdateFlow(nodeFrom, nodeTo)
-      or
       // Def-use/Use-use flow
       Ssa::ssaFlow(nodeFrom, nodeTo)
       or
-      // Phi input -> Phi
-      nodeFrom.(SsaPhiInputNode).getPhiNode() = nodeTo.(SsaPhiNode).getPhiNode()
-      or
       IteratorFlow::localFlowStep(nodeFrom, nodeTo)
       or
       // Operand -> Instruction flow
@@ -1910,9 +1832,6 @@ private module Cached {
         not iFrom = Ssa::getIRRepresentationOfOperand(opTo)
       )
       or
-      // Phi node -> Node flow
-      Ssa::fromPhiNode(nodeFrom, nodeTo)
-      or
       // Indirect operand -> (indirect) instruction flow
       indirectionOperandFlow(nodeFrom, nodeTo)
       or
@@ -2356,22 +2275,6 @@ class ContentSet instanceof Content {
   }
 }
 
-pragma[nomagic]
-private predicate guardControlsPhiInput(
-  IRGuardCondition g, boolean branch, Ssa::DefinitionExt def, IRBlock input, Ssa::PhiNode phi
-) {
-  phi.hasInputFromBlock(def, _, _, _, input) and
-  (
-    g.controls(input, branch)
-    or
-    exists(EdgeKind kind |
-      g.getBlock() = input and
-      kind = getConditionalEdge(branch) and
-      input.getSuccessor(kind) = phi.getBasicBlock()
-    )
-  )
-}
-
 /**
  * Holds if the guard `g` validates the expression `e` upon evaluating to `branch`.
  *
@@ -2403,6 +2306,10 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
     )
   }
 
+  private predicate guardChecksNode(IRGuardCondition g, Node n, boolean branch) {
+    guardChecks(g, n.asOperand().getDef().getConvertedResultExpression(), branch)
+  }
+
   /**
    * Gets an expression node that is safely guarded by the given guard check.
    *
@@ -2443,14 +2350,7 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
       controls(g, result, edge)
     )
     or
-    exists(
-      IRGuardCondition g, boolean branch, Ssa::DefinitionExt def, IRBlock input, Ssa::PhiNode phi
-    |
-      guardChecks(g, def.getARead().asOperand().getDef().getConvertedResultExpression(), branch) and
-      guardControlsPhiInput(g, branch, def, pragma[only_bind_into](input),
-        pragma[only_bind_into](phi)) and
-      result = TSsaPhiInputNode(phi, input)
-    )
+    result = Ssa::BarrierGuard<guardChecksNode/3>::getABarrierNode()
   }
 
   /**
@@ -2499,6 +2399,13 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
     )
   }
 
+  private predicate guardChecksIndirectNode(
+    IRGuardCondition g, Node n, boolean branch, int indirectionIndex
+  ) {
+    guardChecks(g, n.asIndirectOperand(indirectionIndex).getDef().getConvertedResultExpression(),
+      branch)
+  }
+
   /**
    * Gets an indirect expression node with indirection index `indirectionIndex` that is
    * safely guarded by the given guard check.
@@ -2541,16 +2448,8 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
       controls(g, result, edge)
     )
     or
-    exists(
-      IRGuardCondition g, boolean branch, Ssa::DefinitionExt def, IRBlock input, Ssa::PhiNode phi
-    |
-      guardChecks(g,
-        def.getARead().asIndirectOperand(indirectionIndex).getDef().getConvertedResultExpression(),
-        branch) and
-      guardControlsPhiInput(g, branch, def, pragma[only_bind_into](input),
-        pragma[only_bind_into](phi)) and
-      result = TSsaPhiInputNode(phi, input)
-    )
+    result =
+      Ssa::BarrierGuardWithIntParam<guardChecksIndirectNode/4>::getABarrierNode(indirectionIndex)
   }
 }
 
@@ -2559,14 +2458,6 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
  */
 signature predicate instructionGuardChecksSig(IRGuardCondition g, Instruction instr, boolean branch);
 
-private EdgeKind getConditionalEdge(boolean branch) {
-  branch = true and
-  result instanceof TrueEdge
-  or
-  branch = false and
-  result instanceof FalseEdge
-}
-
 /**
  * Provides a set of barrier nodes for a guard that validates an instruction.
  *
@@ -2583,6 +2474,10 @@ module InstructionBarrierGuard<instructionGuardChecksSig/3 instructionGuardCheck
     )
   }
 
+  private predicate guardChecksNode(IRGuardCondition g, Node n, boolean branch) {
+    instructionGuardChecks(g, n.asOperand().getDef(), branch)
+  }
+
   /** Gets a node that is safely guarded by the given guard check. */
   Node getABarrierNode() {
     exists(IRGuardCondition g, ValueNumber value, boolean edge |
@@ -2591,14 +2486,7 @@ module InstructionBarrierGuard<instructionGuardChecksSig/3 instructionGuardCheck
       controls(g, result, edge)
     )
     or
-    exists(
-      IRGuardCondition g, boolean branch, Ssa::DefinitionExt def, IRBlock input, Ssa::PhiNode phi
-    |
-      instructionGuardChecks(g, def.getARead().asOperand().getDef(), branch) and
-      guardControlsPhiInput(g, branch, def, pragma[only_bind_into](input),
-        pragma[only_bind_into](phi)) and
-      result = TSsaPhiInputNode(phi, input)
-    )
+    result = Ssa::BarrierGuard<guardChecksNode/3>::getABarrierNode()
   }
 
   bindingset[value, n]
@@ -2610,6 +2498,12 @@ module InstructionBarrierGuard<instructionGuardChecksSig/3 instructionGuardCheck
     )
   }
 
+  private predicate guardChecksIndirectNode(
+    IRGuardCondition g, Node n, boolean branch, int indirectionIndex
+  ) {
+    instructionGuardChecks(g, n.asIndirectOperand(indirectionIndex).getDef(), branch)
+  }
+
   /**
    * Gets an indirect node with indirection index `indirectionIndex` that is
    * safely guarded by the given guard check.
@@ -2621,14 +2515,8 @@ module InstructionBarrierGuard<instructionGuardChecksSig/3 instructionGuardCheck
       controls(g, result, edge)
     )
     or
-    exists(
-      IRGuardCondition g, boolean branch, Ssa::DefinitionExt def, IRBlock input, Ssa::PhiNode phi
-    |
-      instructionGuardChecks(g, def.getARead().asIndirectOperand(indirectionIndex).getDef(), branch) and
-      guardControlsPhiInput(g, branch, def, pragma[only_bind_into](input),
-        pragma[only_bind_into](phi)) and
-      result = TSsaPhiInputNode(phi, input)
-    )
+    result =
+      Ssa::BarrierGuardWithIntParam<guardChecksIndirectNode/4>::getABarrierNode(indirectionIndex)
   }
 }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
index 77e6e8590cef..df919b42c9d3 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
@@ -2,6 +2,7 @@ private import codeql.ssa.Ssa as SsaImplCommon
 private import semmle.code.cpp.ir.IR
 private import DataFlowUtil
 private import DataFlowImplCommon as DataFlowImplCommon
+private import semmle.code.cpp.controlflow.IRGuards as IRGuards
 private import semmle.code.cpp.models.interfaces.Allocation as Alloc
 private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
 private import semmle.code.cpp.models.interfaces.Taint as Taint
@@ -464,6 +465,17 @@ private predicate finalParameterNodeHasParameterAndIndex(
   n.getIndirectionIndex() = indirectionIndex
 }
 
+pragma[nomagic]
+private predicate hasReturnPosition(IRFunction f, IRBlock block, int index) {
+  exists(Instruction return |
+    return instanceof ReturnInstruction or
+    return instanceof UnreachedInstruction
+  |
+    block.getInstruction(index) = return and
+    return.getEnclosingIRFunction() = f
+  )
+}
+
 class FinalParameterUse extends UseImpl, TFinalParameterUse {
   Parameter p;
 
@@ -492,12 +504,9 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
     // `UnreachedInstruction`. If that's the case this predicate will
     // return multiple results. I don't think this is detrimental to
     // performance, however.
-    exists(Instruction return |
-      return instanceof ReturnInstruction or
-      return instanceof UnreachedInstruction
-    |
-      block.getInstruction(index) = return and
-      return.getEnclosingFunction() = p.getFunction()
+    exists(IRFunction f |
+      hasReturnPosition(f, block, index) and
+      f.getFunction() = p.getFunction()
     )
   }
 
@@ -587,13 +596,7 @@ class GlobalUse extends UseImpl, TGlobalUse {
     // globals at any exit so that we can flow out of non-returning functions.
     // Obviously this isn't correct as we can't actually flow but the global flow
     // requires this if we want to flow into children.
-    exists(Instruction return |
-      return instanceof ReturnInstruction or
-      return instanceof UnreachedInstruction
-    |
-      block.getInstruction(index) = return and
-      return.getEnclosingIRFunction() = f
-    )
+    hasReturnPosition(f, block, index)
   }
 
   override BaseSourceVariable getBaseSourceVariable() {
@@ -669,21 +672,6 @@ class GlobalDefImpl extends DefImpl, TGlobalDefImpl {
   override Location getLocation() { result = f.getLocation() }
 }
 
-/**
- * Holds if there is a definition or access at index `i1` in basic block `bb1`
- * and the next subsequent read is at index `i2` in basic block `bb2`.
- */
-predicate adjacentDefRead(IRBlock bb1, int i1, SourceVariable sv, IRBlock bb2, int i2) {
-  adjacentDefReadExt(_, sv, bb1, i1, bb2, i2)
-}
-
-predicate useToNode(IRBlock bb, int i, SourceVariable sv, Node nodeTo) {
-  exists(UseImpl use |
-    use.hasIndexInBlock(bb, i, sv) and
-    nodeTo = use.getNode()
-  )
-}
-
 pragma[noinline]
 predicate outNodeHasAddressAndIndex(
   IndirectArgumentOutNode out, Operand address, int indirectionIndex
@@ -697,34 +685,17 @@ predicate outNodeHasAddressAndIndex(
  *
  * Holds if `node` is the node that corresponds to the definition of `def`.
  */
-predicate defToNode(
-  Node node, DefinitionExt def, SourceVariable sv, IRBlock bb, int i, boolean uncertain
-) {
-  def.definesAt(sv, bb, i, _) and
-  (
-    nodeHasOperand(node, def.getValue().asOperand(), def.getIndirectionIndex())
-    or
-    nodeHasInstruction(node, def.getValue().asInstruction(), def.getIndirectionIndex())
-    or
-    node.(InitialGlobalValue).getGlobalDef() = def
-  ) and
-  if def.isCertain() then uncertain = false else uncertain = true
+predicate defToNode(Node node, Definition def, SourceVariable sv) {
+  def.getSourceVariable() = sv and
+  defToNode(node, def)
 }
 
-/**
- * INTERNAL: Do not use.
- *
- * Holds if `node` is the node that corresponds to the definition or use at
- * index `i` in block `bb` of `sv`.
- *
- * `uncertain` is `true` if this is an uncertain definition.
- */
-predicate nodeToDefOrUse(Node node, SourceVariable sv, IRBlock bb, int i, boolean uncertain) {
-  defToNode(node, _, sv, bb, i, uncertain)
+private predicate defToNode(Node node, Definition def) {
+  nodeHasOperand(node, def.getValue().asOperand(), def.getIndirectionIndex())
+  or
+  nodeHasInstruction(node, def.getValue().asInstruction(), def.getIndirectionIndex())
   or
-  // Node -> Use
-  useToNode(bb, i, sv, node) and
-  uncertain = false
+  node.(InitialGlobalValue).getGlobalDef() = def
 }
 
 /**
@@ -732,10 +703,7 @@ predicate nodeToDefOrUse(Node node, SourceVariable sv, IRBlock bb, int i, boolea
  * only holds when there is no use-use relation out of `nTo`.
  */
 private predicate indirectConversionFlowStep(Node nFrom, Node nTo) {
-  not exists(SourceVariable sv, IRBlock bb2, int i2 |
-    useToNode(bb2, i2, sv, nTo) and
-    adjacentDefRead(bb2, i2, sv, _, _)
-  ) and
+  not ssaFlowImpl(nTo, _) and
   exists(Operand op1, Operand op2, int indirectionIndex, Instruction instr |
     hasOperandAndIndex(nFrom, op1, pragma[only_bind_into](indirectionIndex)) and
     hasOperandAndIndex(nTo, op2, pragma[only_bind_into](indirectionIndex)) and
@@ -744,50 +712,6 @@ private predicate indirectConversionFlowStep(Node nFrom, Node nTo) {
   )
 }
 
-/**
- * Holds if `node` is a phi input node that should receive flow from the
- * definition to (or use of) `sv` at `(bb1, i1)`.
- */
-private predicate phiToNode(SsaPhiInputNode node, SourceVariable sv, IRBlock bb1, int i1) {
-  exists(PhiNode phi, IRBlock input |
-    phi.hasInputFromBlock(_, sv, bb1, i1, input) and
-    node.getPhiNode() = phi and
-    node.getBlock() = input
-  )
-}
-
-/**
- * Holds if there should be flow from `nodeFrom` to `nodeTo` because
- * `nodeFrom` is a definition or use of `sv` at index `i1` at basic
- * block `bb1`.
- *
- * `uncertain` is `true` if `(bb1, i1)` is a definition, and that definition
- * is _not_ guaranteed to overwrite the entire allocation.
- */
-private predicate ssaFlowImpl(
-  IRBlock bb1, int i1, SourceVariable sv, Node nodeFrom, Node nodeTo, boolean uncertain
-) {
-  nodeToDefOrUse(nodeFrom, sv, bb1, i1, uncertain) and
-  (
-    exists(IRBlock bb2, int i2 |
-      adjacentDefRead(bb1, i1, sv, bb2, i2) and
-      useToNode(bb2, i2, sv, nodeTo)
-    )
-    or
-    phiToNode(nodeTo, sv, bb1, i1)
-  ) and
-  nodeFrom != nodeTo
-}
-
-/** Gets a node that represents the prior definition of `node`. */
-private Node getAPriorDefinition(DefinitionExt next) {
-  exists(IRBlock bb, int i, SourceVariable sv |
-    lastRefRedefExt(_, pragma[only_bind_into](sv), pragma[only_bind_into](bb),
-      pragma[only_bind_into](i), _, next) and
-    nodeToDefOrUse(result, sv, bb, i, _)
-  )
-}
-
 private predicate inOut(FIO::FunctionInput input, FIO::FunctionOutput output) {
   exists(int indirectionIndex |
     input.isQualifierObject(indirectionIndex) and
@@ -834,21 +758,6 @@ private predicate modeledFlowBarrier(Node n) {
   )
 }
 
-/** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
-predicate ssaFlow(Node nodeFrom, Node nodeTo) {
-  exists(Node nFrom, boolean uncertain, IRBlock bb, int i, SourceVariable sv |
-    ssaFlowImpl(bb, i, sv, nFrom, nodeTo, uncertain) and
-    not modeledFlowBarrier(nFrom) and
-    nodeFrom != nodeTo
-  |
-    if uncertain = true
-    then
-      nodeFrom =
-        [nFrom, getAPriorDefinition(any(DefinitionExt next | next.definesAt(sv, bb, i, _)))]
-    else nodeFrom = nFrom
-  )
-}
-
 private predicate isArgumentOfCallableInstruction(DataFlowCall call, Instruction instr) {
   isArgumentOfCallableOperand(call, unique( | | getAUse(instr)))
 }
@@ -905,22 +814,15 @@ private predicate postUpdateNodeToFirstUse(PostUpdateNode pun, Node n) {
   // So this predicate recurses back along conversions and `PointerArithmetic`
   // instructions to find the first use that has provides use-use flow, and
   // uses that target as the target of the `nodeFrom`.
-  exists(Node adjusted, IRBlock bb1, int i1, SourceVariable sv |
+  exists(Node adjusted |
     indirectConversionFlowStep*(adjusted, pun.getPreUpdateNode()) and
-    useToNode(bb1, i1, sv, adjusted)
-  |
-    exists(IRBlock bb2, int i2 |
-      adjacentDefRead(bb1, i1, sv, bb2, i2) and
-      useToNode(bb2, i2, sv, n)
-    )
-    or
-    phiToNode(n, sv, bb1, i1)
+    ssaFlowImpl(adjusted, n)
   )
 }
 
 private predicate stepUntilNotInCall(DataFlowCall call, Node n1, Node n2) {
   isArgumentOfCallable(call, n1) and
-  exists(Node mid | ssaFlowImpl(_, _, _, n1, mid, _) |
+  exists(Node mid | ssaFlowImpl(n1, mid) |
     isArgumentOfCallable(call, mid) and
     stepUntilNotInCall(call, mid, n2)
     or
@@ -952,7 +854,7 @@ private predicate isArgumentOfSameCall(DataFlowCall call, Node n1, Node n2) {
  * similarly we want flow from the second argument of `write_first_argument` to `x`
  * on the next line.
  */
-predicate postUpdateFlow(PostUpdateNode pun, Node nodeTo) {
+private predicate postUpdateFlow(PostUpdateNode pun, Node nodeTo) {
   exists(Node preUpdate, Node mid |
     preUpdate = pun.getPreUpdateNode() and
     postUpdateNodeToFirstUse(pun, mid)
@@ -967,21 +869,6 @@ predicate postUpdateFlow(PostUpdateNode pun, Node nodeTo) {
   )
 }
 
-/** Holds if `nodeTo` receives flow from the phi node `nodeFrom`. */
-predicate fromPhiNode(SsaPhiNode nodeFrom, Node nodeTo) {
-  exists(PhiNode phi, SourceVariable sv, IRBlock bb1, int i1 |
-    phi = nodeFrom.getPhiNode() and
-    phi.definesAt(sv, bb1, i1, _)
-  |
-    exists(IRBlock bb2, int i2 |
-      adjacentDefRead(bb1, i1, sv, bb2, i2) and
-      useToNode(bb2, i2, sv, nodeTo)
-    )
-    or
-    phiToNode(nodeTo, sv, bb1, i1)
-  )
-}
-
 private predicate baseSourceVariableIsGlobal(
   BaseIRVariable base, GlobalLikeVariable global, IRFunction func
 ) {
@@ -1023,11 +910,6 @@ private module SsaInput implements SsaImplCommon::InputSig<Location> {
     exists(UseImpl use | use.hasIndexInBlock(bb, i, v) |
       if use.isCertain() then certain = true else certain = false
     )
-    or
-    exists(GlobalUse global |
-      global.hasIndexInBlock(bb, i, v) and
-      certain = true
-    )
   }
 }
 
@@ -1036,42 +918,14 @@ private module SsaInput implements SsaImplCommon::InputSig<Location> {
  */
 cached
 module SsaCached {
-  /**
-   * Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
-   * or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
-   * path between them without any read of `def`.
-   */
-  cached
-  predicate adjacentDefReadExt(
-    DefinitionExt def, SourceVariable sv, IRBlock bb1, int i1, IRBlock bb2, int i2
-  ) {
-    SsaImpl::adjacentDefReadExt(def, sv, bb1, i1, bb2, i2)
-  }
-
-  /**
-   * Holds if the node at index `i` in `bb` is a last reference to SSA definition
-   * `def`. The reference is last because it can reach another write `next`,
-   * without passing through another read or write.
-   *
-   * 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`.
-   */
   cached
-  predicate lastRefRedefExt(
-    DefinitionExt def, SourceVariable sv, IRBlock bb, int i, IRBlock input, DefinitionExt next
-  ) {
-    SsaImpl::lastRefRedefExt(def, sv, bb, i, input, next)
+  predicate ssaDefReachesRead(SourceVariable v, Definition def, IRBlock bb, int i) {
+    SsaImpl::ssaDefReachesRead(v, def, bb, i)
   }
 
   cached
-  DefinitionExt phiHasInputFromBlockExt(PhiNode phi, IRBlock bb) {
-    SsaImpl::phiHasInputFromBlockExt(phi, result, bb)
-  }
-
-  cached
-  predicate ssaDefReachesReadExt(SourceVariable v, DefinitionExt def, IRBlock bb, int i) {
-    SsaImpl::ssaDefReachesReadExt(v, def, bb, i)
+  predicate phiHasInputFromBlock(PhiNode phi, Definition inp, IRBlock bb) {
+    SsaImpl::phiHasInputFromBlock(phi, inp, bb)
   }
 
   predicate variableRead = SsaInput::variableRead/4;
@@ -1080,14 +934,14 @@ module SsaCached {
 }
 
 /** Gets the `DefImpl` corresponding to `def`. */
-private DefImpl getDefImpl(SsaImpl::DefinitionExt def) {
+private DefImpl getDefImpl(SsaImpl::Definition def) {
   exists(SourceVariable sv, IRBlock bb, int i |
-    def.definesAt(sv, bb, i, _) and
+    def.definesAt(sv, bb, i) and
     result.hasIndexInBlock(bb, i, sv)
   )
 }
 
-class GlobalDef extends DefinitionExt {
+class GlobalDef extends Definition {
   GlobalDefImpl impl;
 
   GlobalDef() { impl = getDefImpl(this) }
@@ -1101,51 +955,173 @@ class GlobalDef extends DefinitionExt {
 
 private module SsaImpl = SsaImplCommon::Make<Location, SsaInput>;
 
-/**
- * An static single assignment (SSA) phi node.
- *
- * This is either a normal phi node or a phi-read node.
- */
-class PhiNode extends SsaImpl::DefinitionExt {
-  PhiNode() {
-    this instanceof SsaImpl::PhiNode or
-    this instanceof SsaImpl::PhiReadNode
+private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationInputSig {
+  private import codeql.util.Void
+
+  class Expr extends Instruction {
+    Expr() {
+      exists(IRBlock bb, int i |
+        variableRead(bb, i, _, true) and
+        this = bb.getInstruction(i)
+      )
+    }
+
+    predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { bb.getInstruction(i) = this }
   }
 
-  /**
-   * Holds if this phi node is a phi-read node.
-   *
-   * Phi-read nodes are like normal phi nodes, but they are inserted based
-   * on reads instead of writes.
-   */
-  predicate isPhiRead() { this instanceof SsaImpl::PhiReadNode }
+  Expr getARead(SsaImpl::Definition def) {
+    exists(SourceVariable v, IRBlock bb, int i |
+      ssaDefReachesRead(v, def, bb, i) and
+      variableRead(bb, i, v, true) and
+      result.hasCfgNode(bb, i)
+    )
+  }
 
-  /**
-   * Holds if the node at index `i` in `bb` is a last reference to SSA
-   * definition `def` of `sv`. The reference is last because it can reach
-   * this phi node, without passing through another read or write.
-   *
-   * The path from node `i` in `bb` to this phi node goes via basic block
-   * `input`, which is either a predecessor of the basic block of this phi
-   * node, or `input` = `bb` in case this phi node occurs in basic block `bb`.
-   */
-  predicate hasInputFromBlock(DefinitionExt def, SourceVariable sv, IRBlock bb, int i, IRBlock input) {
-    SsaCached::lastRefRedefExt(def, sv, bb, i, input, this)
+  predicate ssaDefAssigns(SsaImpl::WriteDefinition def, Expr value) { none() }
+
+  class Parameter extends Void {
+    Location getLocation() { none() }
   }
 
+  predicate ssaDefInitializesParam(SsaImpl::WriteDefinition def, Parameter p) { none() }
+
+  predicate allowFlowIntoUncertainDef(SsaImpl::UncertainWriteDefinition def) { any() }
+
+  private EdgeKind getConditionalEdge(boolean branch) {
+    branch = true and
+    result instanceof TrueEdge
+    or
+    branch = false and
+    result instanceof FalseEdge
+  }
+
+  class Guard instanceof IRGuards::IRGuardCondition {
+    string toString() { result = super.toString() }
+
+    predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+      exists(EdgeKind kind |
+        super.getBlock() = bb1 and
+        kind = getConditionalEdge(branch) and
+        bb1.getSuccessor(kind) = bb2
+      )
+    }
+  }
+
+  predicate guardControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
+    guard.(IRGuards::IRGuardCondition).controls(bb, branch)
+  }
+}
+
+private module DataFlowIntegrationImpl = SsaImpl::DataFlowIntegration<DataFlowIntegrationInput>;
+
+class SynthNode extends DataFlowIntegrationImpl::SsaNode {
+  SynthNode() { not this.asDefinition() instanceof SsaImpl::WriteDefinition }
+}
+
+signature predicate guardChecksNodeSig(IRGuards::IRGuardCondition g, Node e, boolean branch);
+
+signature predicate guardChecksNodeSig(
+  IRGuards::IRGuardCondition g, Node e, boolean branch, int indirectionIndex
+);
+
+module BarrierGuardWithIntParam<guardChecksNodeSig/4 guardChecksNode> {
+  private predicate ssaDefReachesCertainUse(Definition def, UseImpl use) {
+    exists(SourceVariable v, IRBlock bb, int i |
+      use.hasIndexInBlock(bb, i, v) and
+      variableRead(bb, i, v, true) and
+      ssaDefReachesRead(v, def, bb, i)
+    )
+  }
+
+  private predicate guardChecks(
+    DataFlowIntegrationInput::Guard g, SsaImpl::Definition def, boolean branch, int indirectionIndex
+  ) {
+    exists(UseImpl use |
+      guardChecksNode(g, use.getNode(), branch, indirectionIndex) and
+      ssaDefReachesCertainUse(def, use)
+    )
+  }
+
+  Node getABarrierNode(int indirectionIndex) {
+    // Only get the SynthNodes from the shared implementation, as the ExprNodes cannot
+    // be matched on SourceVariable.
+    result.(SsaSynthNode).getSynthNode() =
+      DataFlowIntegrationImpl::BarrierGuardDefWithState<int, guardChecks/4>::getABarrierNode(indirectionIndex)
+    or
+    // Calculate the guarded UseImpls corresponding to ExprNodes directly.
+    exists(DataFlowIntegrationInput::Guard g, boolean branch, Definition def, IRBlock bb |
+      guardChecks(g, def, branch, indirectionIndex) and
+      exists(UseImpl use |
+        ssaDefReachesCertainUse(def, use) and
+        use.getBlock() = bb and
+        DataFlowIntegrationInput::guardControlsBlock(g, bb, branch) and
+        result = use.getNode()
+      )
+    )
+  }
+}
+
+module BarrierGuard<guardChecksNodeSig/3 guardChecksNode> {
+  private predicate guardChecksNode(
+    IRGuards::IRGuardCondition g, Node e, boolean branch, int indirectionIndex
+  ) {
+    guardChecksNode(g, e, branch) and indirectionIndex = 0
+  }
+
+  Node getABarrierNode() {
+    result = BarrierGuardWithIntParam<guardChecksNode/4>::getABarrierNode(0)
+  }
+}
+
+bindingset[result, v]
+pragma[inline_late]
+DataFlowIntegrationImpl::Node fromDfNode(Node n, SourceVariable v) {
+  result = n.(SsaSynthNode).getSynthNode()
+  or
+  exists(UseImpl use, IRBlock bb, int i |
+    result.(DataFlowIntegrationImpl::ExprNode).getExpr().hasCfgNode(bb, i) and
+    use.hasIndexInBlock(bb, i, v) and
+    use.isCertain() and
+    use.getNode() = n
+  )
+  or
+  defToNode(n, result.(DataFlowIntegrationImpl::SsaDefinitionNode).getDefinition())
+}
+
+private predicate ssaFlowImpl(Node nodeFrom, Node nodeTo) {
+  exists(SourceVariable v |
+    nodeFrom != nodeTo and
+    DataFlowIntegrationImpl::localFlowStep(v, fromDfNode(nodeFrom, v), fromDfNode(nodeTo, v), _)
+  )
+}
+
+/** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
+predicate ssaFlow(Node nodeFrom, Node nodeTo) {
+  postUpdateFlow(nodeFrom, nodeTo)
+  or
+  ssaFlowImpl(nodeFrom, nodeTo) and
+  not modeledFlowBarrier(nodeFrom)
+}
+
+/**
+ * An static single assignment (SSA) phi node.
+ */
+class PhiNode extends Definition instanceof SsaImpl::PhiNode {
   /** Gets a definition that is an input to this phi node. */
-  final DefinitionExt getAnInput() { this.hasInputFromBlock(result, _, _, _, _) }
+  final Definition getAnInput() { phiHasInputFromBlock(this, result, _) }
 }
 
 /** An static single assignment (SSA) definition. */
-class DefinitionExt extends SsaImpl::DefinitionExt {
-  private DefinitionExt getAPhiInputOrPriorDefinition() { result = this.(PhiNode).getAnInput() }
+class Definition extends SsaImpl::Definition {
+  // TODO: Include prior definitions of uncertain writes or rename predicate
+  // i.e. the disjunct `SsaImpl::uncertainWriteDefinitionInput(this, result)`
+  private Definition getAPhiInputOrPriorDefinition() { result = this.(PhiNode).getAnInput() }
 
   /**
    * Gets a definition that ultimately defines this SSA definition and is
    * not itself a phi node.
    */
-  final DefinitionExt getAnUltimateDefinition() {
+  final Definition getAnUltimateDefinition() {
     result = this.getAPhiInputOrPriorDefinition*() and
     not result instanceof PhiNode
   }
@@ -1180,16 +1156,6 @@ class DefinitionExt extends SsaImpl::DefinitionExt {
 
   /** Gets the unspecified type of the variable being defined by this definition. */
   Type getUnspecifiedType() { result = this.getUnderlyingType().getUnspecifiedType() }
-
-  /** Gets a node that represents a read of this SSA definition. */
-  pragma[nomagic]
-  Node getARead() {
-    exists(SourceVariable sv, IRBlock bb, int i | SsaCached::ssaDefReachesReadExt(sv, this, bb, i) |
-      useToNode(bb, i, sv, result)
-      or
-      phiToNode(result, sv, bb, i)
-    )
-  }
 }
 
 import SsaCached
diff --git a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll
index 83017aec3537..223d0abf1d4e 100644
--- a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll
+++ b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll
@@ -327,9 +327,7 @@ private module Config implements ProductFlow::StateConfigSig {
 
   predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
 
-  predicate isBarrierOut2(DataFlow::Node node) {
-    node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
-  }
+  predicate isBarrierOut2(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
 }
 
 private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<Config>;
diff --git a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll
index 03369aacade3..f10c6457f795 100644
--- a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll
+++ b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll
@@ -203,9 +203,7 @@ private module InvalidPointerToDerefConfig implements DataFlow::StateConfigSig {
 
   predicate isSink(DataFlow::Node sink, FlowState pai) { none() }
 
-  predicate isBarrier(DataFlow::Node node) {
-    node = any(DataFlow::SsaPhiNode phi | not phi.isPhiRead()).getAnInput(true)
-  }
+  predicate isBarrier(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
 
   predicate isBarrier(DataFlow::Node node, FlowState pai) {
     // `node = getABarrierNode(pai)` ensures that node < pai, so this node is safe to dereference.
diff --git a/cpp/ql/src/Likely Bugs/Memory Management/AllocaInLoop.ql b/cpp/ql/src/Likely Bugs/Memory Management/AllocaInLoop.ql
index 587a2ecc6ffb..b4e517b3bab9 100644
--- a/cpp/ql/src/Likely Bugs/Memory Management/AllocaInLoop.ql	
+++ b/cpp/ql/src/Likely Bugs/Memory Management/AllocaInLoop.ql	
@@ -208,8 +208,7 @@ class LoopWithAlloca extends Stmt {
       this.conditionRequiresInequality(va, _, _) and
       DataFlow::localFlow(result, DataFlow::exprNode(va)) and
       // Phi nodes will be preceded by nodes that represent actual definitions
-      not result instanceof DataFlow::SsaPhiNode and
-      not result instanceof DataFlow::SsaPhiInputNode and
+      not result instanceof DataFlow::SsaSynthNode and
       // A source is outside the loop if it's not inside the loop
       not exists(Expr e | e = getExpr(result) | this = getAnEnclosingLoopOfExpr(e))
     )
diff --git a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
index 1872234ead20..b193b846b5a8 100644
--- a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
+++ b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
@@ -212,9 +212,7 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
     )
   }
 
-  predicate isBarrierOut2(DataFlow::Node node) {
-    node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
-  }
+  predicate isBarrierOut2(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
 
   predicate isAdditionalFlowStep2(
     DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
index eb0212153e8e..a9927b510930 100644
--- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
+++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
@@ -44,6 +44,7 @@ edges
 | test.cpp:143:18:143:21 | asdf | test.cpp:134:25:134:27 | arr | provenance |  |
 | test.cpp:143:18:143:21 | asdf | test.cpp:143:18:143:21 | asdf | provenance |  |
 | test.cpp:146:26:146:26 | *p | test.cpp:147:4:147:9 | -- ... | provenance |  |
+| test.cpp:146:26:146:26 | *p | test.cpp:147:4:147:9 | -- ... | provenance |  |
 | test.cpp:154:7:154:9 | definition of buf | test.cpp:156:12:156:18 | ... + ... | provenance | Config |
 | test.cpp:156:12:156:14 | buf | test.cpp:156:12:156:18 | ... + ... | provenance | Config |
 | test.cpp:156:12:156:18 | ... + ... | test.cpp:156:12:156:18 | ... + ... | provenance |  |
@@ -154,6 +155,7 @@ nodes
 | test.cpp:143:18:143:21 | asdf | semmle.label | asdf |
 | test.cpp:146:26:146:26 | *p | semmle.label | *p |
 | test.cpp:147:4:147:9 | -- ... | semmle.label | -- ... |
+| test.cpp:147:4:147:9 | -- ... | semmle.label | -- ... |
 | test.cpp:154:7:154:9 | definition of buf | semmle.label | definition of buf |
 | test.cpp:156:12:156:14 | buf | semmle.label | buf |
 | test.cpp:156:12:156:18 | ... + ... | semmle.label | ... + ... |
@@ -224,6 +226,8 @@ subpaths
 | test.cpp:136:9:136:16 | PointerAdd: ... += ... | test.cpp:142:10:142:13 | definition of asdf | test.cpp:138:13:138:15 | arr | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:142:10:142:13 | asdf | asdf | test.cpp:138:12:138:15 | Load: * ... | read |
 | test.cpp:136:9:136:16 | PointerAdd: ... += ... | test.cpp:143:18:143:21 | asdf | test.cpp:138:13:138:15 | arr | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:142:10:142:13 | asdf | asdf | test.cpp:138:12:138:15 | Load: * ... | read |
 | test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:154:7:154:9 | definition of buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
+| test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:154:7:154:9 | definition of buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
+| test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:156:12:156:14 | buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
 | test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:156:12:156:14 | buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
 | test.cpp:221:5:221:11 | PointerAdd: access to array | test.cpp:217:19:217:24 | definition of buffer | test.cpp:221:5:221:11 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:217:19:217:24 | buffer | buffer | test.cpp:221:5:221:15 | Store: ... = ... | write |
 | test.cpp:221:5:221:11 | PointerAdd: access to array | test.cpp:218:23:218:28 | buffer | test.cpp:221:5:221:11 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:217:19:217:24 | buffer | buffer | test.cpp:221:5:221:15 | Store: ... = ... | write |
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected
index d9bc9b3425e8..85ef90b127d4 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected
@@ -31,8 +31,6 @@
 | example.c:17:21:17:21 | 0 | example.c:17:21:17:21 | 0 |
 | example.c:19:6:19:6 | *b | example.c:15:37:15:37 | *b |
 | example.c:19:6:19:6 | *b [post update] | example.c:15:37:15:37 | *b |
-| example.c:19:6:19:6 | *b [post update] | example.c:19:6:19:6 | *b |
-| example.c:19:6:19:6 | b [post update] | example.c:19:6:19:6 | b |
 | example.c:24:2:24:7 | *coords | example.c:26:18:26:24 | *& ... |
 | example.c:24:2:24:7 | *coords [post update] | example.c:26:18:26:24 | *& ... |
 | example.c:24:2:24:7 | coords | example.c:26:18:26:24 | & ... |
@@ -67,34 +65,34 @@
 | test.cpp:8:8:8:9 | t1 | test.cpp:9:8:9:9 | t1 |
 | test.cpp:9:8:9:9 | t1 | test.cpp:11:7:11:8 | t1 |
 | test.cpp:9:8:9:9 | t1 | test.cpp:11:7:11:8 | t1 |
-| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | Phi input |
-| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | Phi input |
+| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | [input] SSA phi read(t2) |
+| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | [input] SSA phi(*t2) |
 | test.cpp:10:8:10:9 | t2 | test.cpp:13:10:13:11 | t2 |
-| test.cpp:11:7:11:8 | Phi input | test.cpp:15:3:15:6 | SSA phi read(t2) |
-| test.cpp:11:7:11:8 | Phi input | test.cpp:15:3:15:6 | SSA phi(*t2) |
+| test.cpp:11:7:11:8 | [input] SSA phi read(t2) | test.cpp:15:3:15:6 | SSA phi read(t2) |
+| test.cpp:11:7:11:8 | [input] SSA phi(*t2) | test.cpp:15:3:15:6 | SSA phi(*t2) |
 | test.cpp:11:7:11:8 | t1 | test.cpp:21:8:21:9 | t1 |
 | test.cpp:12:5:12:10 | ... = ... | test.cpp:13:10:13:11 | t2 |
 | test.cpp:12:10:12:10 | 0 | test.cpp:12:5:12:10 | ... = ... |
-| test.cpp:13:5:13:8 | Phi input | test.cpp:15:3:15:6 | SSA phi read(t2) |
-| test.cpp:13:5:13:8 | Phi input | test.cpp:15:3:15:6 | SSA phi(*t2) |
-| test.cpp:13:10:13:11 | t2 | test.cpp:13:5:13:8 | Phi input |
-| test.cpp:13:10:13:11 | t2 | test.cpp:13:5:13:8 | Phi input |
+| test.cpp:13:5:13:8 | [input] SSA phi read(t2) | test.cpp:15:3:15:6 | SSA phi read(t2) |
+| test.cpp:13:5:13:8 | [input] SSA phi(*t2) | test.cpp:15:3:15:6 | SSA phi(*t2) |
+| test.cpp:13:10:13:11 | t2 | test.cpp:13:5:13:8 | [input] SSA phi read(t2) |
+| test.cpp:13:10:13:11 | t2 | test.cpp:13:5:13:8 | [input] SSA phi(*t2) |
 | test.cpp:15:3:15:6 | SSA phi read(t2) | test.cpp:15:8:15:9 | t2 |
 | test.cpp:15:3:15:6 | SSA phi(*t2) | test.cpp:15:8:15:9 | t2 |
-| test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | Phi input |
-| test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | Phi input |
+| test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | [input] SSA phi read(*t2) |
+| test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | [input] SSA phi read(t2) |
 | test.cpp:17:3:17:8 | ... = ... | test.cpp:21:8:21:9 | t1 |
 | test.cpp:17:8:17:8 | 0 | test.cpp:17:3:17:8 | ... = ... |
-| test.cpp:21:8:21:9 | t1 | test.cpp:23:15:23:16 | Phi input |
-| test.cpp:21:8:21:9 | t1 | test.cpp:23:15:23:16 | Phi input |
+| test.cpp:21:8:21:9 | t1 | test.cpp:23:15:23:16 | [input] SSA phi read(t1) |
+| test.cpp:21:8:21:9 | t1 | test.cpp:23:15:23:16 | [input] SSA phi(*t1) |
 | test.cpp:23:15:23:16 | 0 | test.cpp:23:15:23:16 | 0 |
-| test.cpp:23:15:23:16 | 0 | test.cpp:23:15:23:16 | Phi input |
-| test.cpp:23:15:23:16 | Phi input | test.cpp:23:19:23:19 | SSA phi read(*t2) |
-| test.cpp:23:15:23:16 | Phi input | test.cpp:23:19:23:19 | SSA phi read(i) |
-| test.cpp:23:15:23:16 | Phi input | test.cpp:23:19:23:19 | SSA phi read(t1) |
-| test.cpp:23:15:23:16 | Phi input | test.cpp:23:19:23:19 | SSA phi read(t2) |
-| test.cpp:23:15:23:16 | Phi input | test.cpp:23:19:23:19 | SSA phi(*i) |
-| test.cpp:23:15:23:16 | Phi input | test.cpp:23:19:23:19 | SSA phi(*t1) |
+| test.cpp:23:15:23:16 | 0 | test.cpp:23:15:23:16 | [input] SSA phi(*i) |
+| test.cpp:23:15:23:16 | [input] SSA phi read(*t2) | test.cpp:23:19:23:19 | SSA phi read(*t2) |
+| test.cpp:23:15:23:16 | [input] SSA phi read(i) | test.cpp:23:19:23:19 | SSA phi read(i) |
+| test.cpp:23:15:23:16 | [input] SSA phi read(t1) | test.cpp:23:19:23:19 | SSA phi read(t1) |
+| test.cpp:23:15:23:16 | [input] SSA phi read(t2) | test.cpp:23:19:23:19 | SSA phi read(t2) |
+| test.cpp:23:15:23:16 | [input] SSA phi(*i) | test.cpp:23:19:23:19 | SSA phi(*i) |
+| test.cpp:23:15:23:16 | [input] SSA phi(*t1) | test.cpp:23:19:23:19 | SSA phi(*t1) |
 | test.cpp:23:19:23:19 | SSA phi read(*t2) | test.cpp:24:10:24:11 | t2 |
 | test.cpp:23:19:23:19 | SSA phi read(i) | test.cpp:23:19:23:19 | i |
 | test.cpp:23:19:23:19 | SSA phi read(t1) | test.cpp:23:23:23:24 | t1 |
@@ -103,25 +101,25 @@
 | test.cpp:23:19:23:19 | SSA phi(*t1) | test.cpp:23:23:23:24 | t1 |
 | test.cpp:23:19:23:19 | i | test.cpp:23:27:23:27 | i |
 | test.cpp:23:19:23:19 | i | test.cpp:23:27:23:27 | i |
-| test.cpp:23:23:23:24 | t1 | test.cpp:23:27:23:29 | Phi input |
+| test.cpp:23:23:23:24 | t1 | test.cpp:23:27:23:29 | [input] SSA phi read(t1) |
 | test.cpp:23:23:23:24 | t1 | test.cpp:26:8:26:9 | t1 |
 | test.cpp:23:23:23:24 | t1 | test.cpp:26:8:26:9 | t1 |
 | test.cpp:23:27:23:27 | *i | test.cpp:23:27:23:27 | *i |
 | test.cpp:23:27:23:27 | *i | test.cpp:23:27:23:27 | i |
 | test.cpp:23:27:23:27 | i | test.cpp:23:27:23:27 | i |
 | test.cpp:23:27:23:27 | i | test.cpp:23:27:23:27 | i |
-| test.cpp:23:27:23:27 | i | test.cpp:23:27:23:29 | Phi input |
+| test.cpp:23:27:23:27 | i | test.cpp:23:27:23:29 | [input] SSA phi read(i) |
 | test.cpp:23:27:23:29 | ... ++ | test.cpp:23:27:23:29 | ... ++ |
-| test.cpp:23:27:23:29 | ... ++ | test.cpp:23:27:23:29 | Phi input |
-| test.cpp:23:27:23:29 | Phi input | test.cpp:23:19:23:19 | SSA phi read(*t2) |
-| test.cpp:23:27:23:29 | Phi input | test.cpp:23:19:23:19 | SSA phi read(i) |
-| test.cpp:23:27:23:29 | Phi input | test.cpp:23:19:23:19 | SSA phi read(t1) |
-| test.cpp:23:27:23:29 | Phi input | test.cpp:23:19:23:19 | SSA phi read(t2) |
-| test.cpp:23:27:23:29 | Phi input | test.cpp:23:19:23:19 | SSA phi(*i) |
-| test.cpp:23:27:23:29 | Phi input | test.cpp:23:19:23:19 | SSA phi(*t1) |
-| test.cpp:24:5:24:11 | ... = ... | test.cpp:23:27:23:29 | Phi input |
-| test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | Phi input |
-| test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | Phi input |
+| test.cpp:23:27:23:29 | ... ++ | test.cpp:23:27:23:29 | [input] SSA phi(*i) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(*t2) | test.cpp:23:19:23:19 | SSA phi read(*t2) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(i) | test.cpp:23:19:23:19 | SSA phi read(i) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(t1) | test.cpp:23:19:23:19 | SSA phi read(t1) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(t2) | test.cpp:23:19:23:19 | SSA phi read(t2) |
+| test.cpp:23:27:23:29 | [input] SSA phi(*i) | test.cpp:23:19:23:19 | SSA phi(*i) |
+| test.cpp:23:27:23:29 | [input] SSA phi(*t1) | test.cpp:23:19:23:19 | SSA phi(*t1) |
+| test.cpp:24:5:24:11 | ... = ... | test.cpp:23:27:23:29 | [input] SSA phi(*t1) |
+| test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | [input] SSA phi read(*t2) |
+| test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | [input] SSA phi read(t2) |
 | test.cpp:24:10:24:11 | t2 | test.cpp:24:5:24:11 | ... = ... |
 | test.cpp:382:48:382:54 | source1 | test.cpp:384:16:384:23 | *& ... |
 | test.cpp:383:12:383:13 | 0 | test.cpp:383:12:383:13 | 0 |
@@ -189,8 +187,6 @@
 | test.cpp:488:24:488:30 | content | test.cpp:488:21:488:30 | content |
 | test.cpp:489:20:489:20 | *s | test.cpp:487:67:487:67 | *s |
 | test.cpp:489:20:489:20 | *s [post update] | test.cpp:487:67:487:67 | *s |
-| test.cpp:489:20:489:20 | *s [post update] | test.cpp:489:20:489:20 | *s |
-| test.cpp:489:20:489:20 | s [post update] | test.cpp:489:20:489:20 | s |
 | test.cpp:489:23:489:29 | *content | test.cpp:489:23:489:29 | *content |
 | test.cpp:489:23:489:29 | *content | test.cpp:490:8:490:17 | * ... |
 | test.cpp:489:23:489:29 | content | test.cpp:489:23:489:29 | content |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-022/SAMATE/TaintedPath/TaintedPath.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-022/SAMATE/TaintedPath/TaintedPath.expected
index dc8bb31748a8..031804b92251 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-022/SAMATE/TaintedPath/TaintedPath.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-022/SAMATE/TaintedPath/TaintedPath.expected
@@ -1,7 +1,13 @@
 edges
+| CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:55:27:55:38 | fgets output argument | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:62:25:62:46 | ... = ... | provenance |  |
+| CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:55:27:55:38 | fgets output argument | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:69:21:69:40 | ... = ... | provenance |  |
 | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:55:27:55:38 | fgets output argument | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:77:23:77:26 | *data | provenance |  |
+| CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:62:25:62:46 | ... = ... | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:77:23:77:26 | *data | provenance |  |
+| CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:69:21:69:40 | ... = ... | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:77:23:77:26 | *data | provenance |  |
 nodes
 | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:55:27:55:38 | fgets output argument | semmle.label | fgets output argument |
+| CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:62:25:62:46 | ... = ... | semmle.label | ... = ... |
+| CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:69:21:69:40 | ... = ... | semmle.label | ... = ... |
 | CWE23_Relative_Path_Traversal__char_console_fopen_11.cpp:77:23:77:26 | *data | semmle.label | *data |
 subpaths
 #select
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-134/SAMATE/UncontrolledFormatString.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-134/SAMATE/UncontrolledFormatString.expected
index 835bff109bf3..560ecc8bd775 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-134/SAMATE/UncontrolledFormatString.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-134/SAMATE/UncontrolledFormatString.expected
@@ -1,12 +1,21 @@
 edges
+| char_connect_socket_w32_vsnprintf_01_bad.c:94:46:94:69 | recv output argument | char_connect_socket_w32_vsnprintf_01_bad.c:100:13:100:60 | ... = ... | provenance |  |
 | char_connect_socket_w32_vsnprintf_01_bad.c:94:46:94:69 | recv output argument | char_connect_socket_w32_vsnprintf_01_bad.c:125:15:125:18 | *data | provenance |  |
+| char_connect_socket_w32_vsnprintf_01_bad.c:100:13:100:60 | ... = ... | char_connect_socket_w32_vsnprintf_01_bad.c:125:15:125:18 | *data | provenance |  |
+| char_console_fprintf_01_bad.c:30:23:30:35 | fgets output argument | char_console_fprintf_01_bad.c:37:21:37:43 | ... = ... | provenance |  |
+| char_console_fprintf_01_bad.c:30:23:30:35 | fgets output argument | char_console_fprintf_01_bad.c:44:17:44:37 | ... = ... | provenance |  |
 | char_console_fprintf_01_bad.c:30:23:30:35 | fgets output argument | char_console_fprintf_01_bad.c:49:21:49:24 | *data | provenance |  |
+| char_console_fprintf_01_bad.c:37:21:37:43 | ... = ... | char_console_fprintf_01_bad.c:49:21:49:24 | *data | provenance |  |
+| char_console_fprintf_01_bad.c:44:17:44:37 | ... = ... | char_console_fprintf_01_bad.c:49:21:49:24 | *data | provenance |  |
 | char_environment_fprintf_01_bad.c:27:30:27:35 | *call to getenv | char_environment_fprintf_01_bad.c:27:30:27:35 | *call to getenv | provenance |  |
 | char_environment_fprintf_01_bad.c:27:30:27:35 | *call to getenv | char_environment_fprintf_01_bad.c:36:21:36:24 | *data | provenance | TaintFunction |
 nodes
 | char_connect_socket_w32_vsnprintf_01_bad.c:94:46:94:69 | recv output argument | semmle.label | recv output argument |
+| char_connect_socket_w32_vsnprintf_01_bad.c:100:13:100:60 | ... = ... | semmle.label | ... = ... |
 | char_connect_socket_w32_vsnprintf_01_bad.c:125:15:125:18 | *data | semmle.label | *data |
 | char_console_fprintf_01_bad.c:30:23:30:35 | fgets output argument | semmle.label | fgets output argument |
+| char_console_fprintf_01_bad.c:37:21:37:43 | ... = ... | semmle.label | ... = ... |
+| char_console_fprintf_01_bad.c:44:17:44:37 | ... = ... | semmle.label | ... = ... |
 | char_console_fprintf_01_bad.c:49:21:49:24 | *data | semmle.label | *data |
 | char_environment_fprintf_01_bad.c:27:30:27:35 | *call to getenv | semmle.label | *call to getenv |
 | char_environment_fprintf_01_bad.c:27:30:27:35 | *call to getenv | semmle.label | *call to getenv |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/consts/NonConstantFormat.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/consts/NonConstantFormat.expected
index e59c3e893a4f..421d12dabd31 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/consts/NonConstantFormat.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/consts/NonConstantFormat.expected
@@ -1,6 +1,9 @@
 edges
-| consts.cpp:24:7:24:9 | **gv1 | consts.cpp:24:7:24:9 | **gv1 | provenance |  |
+| consts.cpp:24:7:24:9 | **gv1 | consts.cpp:25:2:25:4 | *a | provenance |  |
 | consts.cpp:24:7:24:9 | **gv1 | consts.cpp:30:9:30:14 | *access to array | provenance |  |
+| consts.cpp:24:7:24:9 | **gv1 | consts.cpp:123:2:123:12 | *... = ... | provenance |  |
+| consts.cpp:25:2:25:4 | *a | consts.cpp:26:2:26:4 | *b | provenance |  |
+| consts.cpp:26:2:26:4 | *b | consts.cpp:24:7:24:9 | **gv1 | provenance |  |
 | consts.cpp:29:7:29:25 | **nonConstFuncToArray | consts.cpp:126:9:126:30 | *call to nonConstFuncToArray | provenance |  |
 | consts.cpp:30:9:30:14 | *access to array | consts.cpp:29:7:29:25 | **nonConstFuncToArray | provenance |  |
 | consts.cpp:85:7:85:8 | gets output argument | consts.cpp:86:9:86:10 | *v1 | provenance |  |
@@ -25,8 +28,7 @@ edges
 | consts.cpp:106:13:106:19 | *call to varFunc | consts.cpp:107:9:107:10 | *v5 | provenance |  |
 | consts.cpp:111:2:111:15 | *... = ... | consts.cpp:112:9:112:10 | *v6 | provenance |  |
 | consts.cpp:111:7:111:13 | *call to varFunc | consts.cpp:111:2:111:15 | *... = ... | provenance |  |
-| consts.cpp:115:17:115:18 | *v1 | consts.cpp:116:9:116:13 | *access to array | provenance |  |
-| consts.cpp:115:17:115:18 | *v1 | consts.cpp:120:2:120:11 | *... = ... | provenance |  |
+| consts.cpp:115:17:115:18 | *v1 | consts.cpp:115:21:115:22 | *v2 | provenance |  |
 | consts.cpp:115:21:115:22 | *v2 | consts.cpp:116:9:116:13 | *access to array | provenance |  |
 | consts.cpp:115:21:115:22 | *v2 | consts.cpp:120:2:120:11 | *... = ... | provenance |  |
 | consts.cpp:120:2:120:11 | *... = ... | consts.cpp:121:9:121:10 | *v8 | provenance |  |
@@ -36,6 +38,8 @@ edges
 | consts.cpp:144:16:144:18 | readStringRef output argument | consts.cpp:145:9:145:11 | *v12 | provenance |  |
 nodes
 | consts.cpp:24:7:24:9 | **gv1 | semmle.label | **gv1 |
+| consts.cpp:25:2:25:4 | *a | semmle.label | *a |
+| consts.cpp:26:2:26:4 | *b | semmle.label | *b |
 | consts.cpp:29:7:29:25 | **nonConstFuncToArray | semmle.label | **nonConstFuncToArray |
 | consts.cpp:30:9:30:14 | *access to array | semmle.label | *access to array |
 | consts.cpp:85:7:85:8 | gets output argument | semmle.label | gets output argument |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected
index e55caaa63728..0cfd3b0413ee 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected
@@ -27,6 +27,10 @@ edges
 | test.cpp:53:5:53:23 | ... = ... | test.cpp:51:33:51:35 | *end | provenance |  |
 | test.cpp:53:12:53:23 | ... + ... | test.cpp:53:5:53:23 | ... = ... | provenance |  |
 | test.cpp:60:34:60:37 | mk_array output argument | test.cpp:67:9:67:14 | ... = ... | provenance | Config |
+| test.cpp:60:34:60:37 | mk_array output argument | test.cpp:67:9:67:14 | ... = ... | provenance | Config |
+| test.cpp:66:37:66:39 | *++ ... | test.cpp:67:9:67:14 | ... = ... | provenance |  |
+| test.cpp:66:37:66:39 | *++ ... | test.cpp:67:9:67:14 | ... = ... | provenance |  |
+| test.cpp:67:9:67:14 | ... = ... | test.cpp:66:37:66:39 | *++ ... | provenance |  |
 | test.cpp:205:15:205:33 | call to malloc | test.cpp:205:15:205:33 | call to malloc | provenance |  |
 | test.cpp:205:15:205:33 | call to malloc | test.cpp:206:17:206:23 | ... + ... | provenance | Config |
 | test.cpp:206:17:206:23 | ... + ... | test.cpp:206:17:206:23 | ... + ... | provenance |  |
@@ -47,6 +51,11 @@ edges
 | test.cpp:271:14:271:21 | ... + ... | test.cpp:271:14:271:21 | ... + ... | provenance |  |
 | test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... | provenance | Config |
 | test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... | provenance | Config |
+| test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... | provenance | Config |
+| test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... | provenance | Config |
+| test.cpp:272:31:272:33 | *... ++ | test.cpp:274:5:274:10 | ... = ... | provenance |  |
+| test.cpp:272:31:272:33 | *... ++ | test.cpp:274:5:274:10 | ... = ... | provenance |  |
+| test.cpp:274:5:274:10 | ... = ... | test.cpp:272:31:272:33 | *... ++ | provenance |  |
 | test.cpp:355:14:355:27 | new[] | test.cpp:355:14:355:27 | new[] | provenance |  |
 | test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... | provenance | Config |
 | test.cpp:356:15:356:23 | ... + ... | test.cpp:356:15:356:23 | ... + ... | provenance |  |
@@ -114,9 +123,18 @@ edges
 | test.cpp:794:5:794:24 | ... = ... | test.cpp:792:60:792:62 | *end | provenance |  |
 | test.cpp:794:12:794:24 | ... + ... | test.cpp:794:5:794:24 | ... = ... | provenance |  |
 | test.cpp:800:40:800:43 | mk_array_no_field_flow output argument | test.cpp:807:7:807:12 | ... = ... | provenance | Config |
+| test.cpp:800:40:800:43 | mk_array_no_field_flow output argument | test.cpp:807:7:807:12 | ... = ... | provenance | Config |
+| test.cpp:806:35:806:37 | *++ ... | test.cpp:807:7:807:12 | ... = ... | provenance |  |
+| test.cpp:806:35:806:37 | *++ ... | test.cpp:807:7:807:12 | ... = ... | provenance |  |
+| test.cpp:807:7:807:12 | ... = ... | test.cpp:806:35:806:37 | *++ ... | provenance |  |
 | test.cpp:815:52:815:54 | end | test.cpp:815:52:815:54 | end | provenance |  |
 | test.cpp:815:52:815:54 | end | test.cpp:821:7:821:12 | ... = ... | provenance | Config |
 | test.cpp:815:52:815:54 | end | test.cpp:821:7:821:12 | ... = ... | provenance | Config |
+| test.cpp:815:52:815:54 | end | test.cpp:821:7:821:12 | ... = ... | provenance | Config |
+| test.cpp:815:52:815:54 | end | test.cpp:821:7:821:12 | ... = ... | provenance | Config |
+| test.cpp:820:35:820:37 | *++ ... | test.cpp:821:7:821:12 | ... = ... | provenance |  |
+| test.cpp:820:35:820:37 | *++ ... | test.cpp:821:7:821:12 | ... = ... | provenance |  |
+| test.cpp:821:7:821:12 | ... = ... | test.cpp:820:35:820:37 | *++ ... | provenance |  |
 | test.cpp:832:40:832:43 | mk_array_no_field_flow output argument | test.cpp:833:37:833:39 | end | provenance |  |
 | test.cpp:833:37:833:39 | end | test.cpp:815:52:815:54 | end | provenance |  |
 | test.cpp:841:18:841:35 | call to malloc | test.cpp:841:18:841:35 | call to malloc | provenance |  |
@@ -157,6 +175,8 @@ nodes
 | test.cpp:53:5:53:23 | ... = ... | semmle.label | ... = ... |
 | test.cpp:53:12:53:23 | ... + ... | semmle.label | ... + ... |
 | test.cpp:60:34:60:37 | mk_array output argument | semmle.label | mk_array output argument |
+| test.cpp:66:37:66:39 | *++ ... | semmle.label | *++ ... |
+| test.cpp:67:9:67:14 | ... = ... | semmle.label | ... = ... |
 | test.cpp:67:9:67:14 | ... = ... | semmle.label | ... = ... |
 | test.cpp:205:15:205:33 | call to malloc | semmle.label | call to malloc |
 | test.cpp:205:15:205:33 | call to malloc | semmle.label | call to malloc |
@@ -174,6 +194,8 @@ nodes
 | test.cpp:270:13:270:24 | new[] | semmle.label | new[] |
 | test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... |
 | test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... |
+| test.cpp:272:31:272:33 | *... ++ | semmle.label | *... ++ |
+| test.cpp:274:5:274:10 | ... = ... | semmle.label | ... = ... |
 | test.cpp:274:5:274:10 | ... = ... | semmle.label | ... = ... |
 | test.cpp:355:14:355:27 | new[] | semmle.label | new[] |
 | test.cpp:355:14:355:27 | new[] | semmle.label | new[] |
@@ -240,9 +262,13 @@ nodes
 | test.cpp:794:5:794:24 | ... = ... | semmle.label | ... = ... |
 | test.cpp:794:12:794:24 | ... + ... | semmle.label | ... + ... |
 | test.cpp:800:40:800:43 | mk_array_no_field_flow output argument | semmle.label | mk_array_no_field_flow output argument |
+| test.cpp:806:35:806:37 | *++ ... | semmle.label | *++ ... |
+| test.cpp:807:7:807:12 | ... = ... | semmle.label | ... = ... |
 | test.cpp:807:7:807:12 | ... = ... | semmle.label | ... = ... |
 | test.cpp:815:52:815:54 | end | semmle.label | end |
 | test.cpp:815:52:815:54 | end | semmle.label | end |
+| test.cpp:820:35:820:37 | *++ ... | semmle.label | *++ ... |
+| test.cpp:821:7:821:12 | ... = ... | semmle.label | ... = ... |
 | test.cpp:821:7:821:12 | ... = ... | semmle.label | ... = ... |
 | test.cpp:832:40:832:43 | mk_array_no_field_flow output argument | semmle.label | mk_array_no_field_flow output argument |
 | test.cpp:833:37:833:39 | end | semmle.label | end |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-311/semmle/tests/CleartextTransmission.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-311/semmle/tests/CleartextTransmission.expected
index 42718aa4a388..fae3d76599a8 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-311/semmle/tests/CleartextTransmission.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-311/semmle/tests/CleartextTransmission.expected
@@ -16,7 +16,8 @@ edges
 | test3.cpp:138:24:138:32 | password1 | test3.cpp:138:21:138:22 | call to id | provenance |  |
 | test3.cpp:144:16:144:29 | call to get_global_str | test3.cpp:144:16:144:29 | call to get_global_str | provenance |  |
 | test3.cpp:144:16:144:29 | call to get_global_str | test3.cpp:146:15:146:18 | data | provenance |  |
-| test3.cpp:157:19:157:26 | password | test3.cpp:159:15:159:20 | *buffer | provenance | TaintFunction |
+| test3.cpp:157:19:157:26 | password | test3.cpp:158:3:158:16 | ... = ... | provenance | TaintFunction |
+| test3.cpp:158:3:158:16 | ... = ... | test3.cpp:159:15:159:20 | *buffer | provenance |  |
 | test3.cpp:270:16:270:23 | password | test3.cpp:272:15:272:18 | *data | provenance | DataFlowFunction |
 | test3.cpp:278:20:278:23 | data | test3.cpp:280:14:280:17 | data | provenance |  |
 | test3.cpp:283:20:283:23 | data | test3.cpp:285:14:285:17 | data | provenance |  |
@@ -70,6 +71,7 @@ nodes
 | test3.cpp:144:16:144:29 | call to get_global_str | semmle.label | call to get_global_str |
 | test3.cpp:146:15:146:18 | data | semmle.label | data |
 | test3.cpp:157:19:157:26 | password | semmle.label | password |
+| test3.cpp:158:3:158:16 | ... = ... | semmle.label | ... = ... |
 | test3.cpp:159:15:159:20 | *buffer | semmle.label | *buffer |
 | test3.cpp:173:15:173:22 | password | semmle.label | password |
 | test3.cpp:181:15:181:22 | password | semmle.label | password |
diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll
index 275b8963ea5d..b893c75eb8e7 100644
--- a/shared/ssa/codeql/ssa/Ssa.qll
+++ b/shared/ssa/codeql/ssa/Ssa.qll
@@ -1650,6 +1650,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       /** Gets the basic block to which this node belongs. */
       abstract BasicBlock getBasicBlock();
 
+      /**
+       * INTERNAL: Do not use.
+       *
+       * Gets the basic block index of this node.
+       */
+      abstract int getIndex();
+
       /** Gets the underlying source variable that this node tracks flow for. */
       abstract SourceVariable getSourceVariable();
     }
@@ -1669,6 +1676,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
 
       override BasicBlock getBasicBlock() { result = def.getBasicBlock() }
 
+      override int getIndex() { def.definesAt(_, _, result, _) }
+
       override SourceVariable getSourceVariable() { result = def.getSourceVariable() }
 
       override Location getLocation() { result = def.getLocation() }
@@ -1751,6 +1760,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
 
       override BasicBlock getBasicBlock() { result = input_ }
 
+      override int getIndex() { result = input_.length() }
+
       override SourceVariable getSourceVariable() { result = def_.getSourceVariable() }
 
       override Location getLocation() { result = input_.getNode(input_.length() - 1).getLocation() }
@@ -1886,6 +1897,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       signature predicate guardChecksSig(
         DfInput::Guard g, DfInput::Expr e, boolean branch, State state
       );
+
+      /**
+       * Holds if the guard `g` validates the SSA definition `def` upon
+       * evaluating to `branch`, blocking flow in the given `state`.
+       */
+      signature predicate guardChecksDefSig(
+        DfInput::Guard g, Definition def, boolean branch, State state
+      );
     }
 
     /**
@@ -1922,6 +1941,20 @@ module Make<LocationSig Location, InputSig<Location> Input> {
         guardChecks(g, DfInput::getARead(def), branch, state)
       }
 
+      private module Barrier = BarrierGuardDefWithState<State, guardChecksSsaDef/4>;
+
+      predicate getABarrierNode = Barrier::getABarrierNode/1;
+    }
+
+    /**
+     * Provides a set of barrier nodes for a guard that validates an expression.
+     *
+     * This is expected to be used in `isBarrier`/`isSanitizer` definitions
+     * in data flow and taint tracking.
+     */
+    module BarrierGuardDefWithState<
+      StateSig State, WithState<State>::guardChecksDefSig/4 guardChecksSsaDef>
+    {
       /** Gets a node that is safely guarded by the given guard check. */
       pragma[nomagic]
       Node getABarrierNode(State state) {