Merge pull request #18942 from aschackmull/cpp/refactor-ssa

C++: Refactor SSA usage in data flow.
2026-04-21 15:05:56 +02:00 · 2025-03-14 13:31:32 +01:00
parent 60f96eee7e c2309442d5
commit 474b8a5a31
15 changed files with 388 additions and 507 deletions
--- 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
--- 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;
+class SsaSynthNode extends Node, TSsaSynthNode {
+  Ssa::SynthNode node;

-  SsaPhiNode() { this = TSsaPhiNode(phi) }
+  SsaSynthNode() { this = TSsaSynthNode(node) }

-  /** Gets the phi node associated with this node. */
-  Ssa::PhiNode getPhiNode() { result = phi }
+  /** 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() {
-    exists(Ssa::SourceVariable sv |
-      this.getPhiNode().definesAt(sv, _, _, _) and
-      result = sv.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 = phi.getBasicBlock().getLocation() }
+  final override Location getLocationImpl() { result = node.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 }
-
-  /** Gets the basic block in which this input originates. */
-  IRBlock getBlock() { result = block }
-
-  override DataFlowCallable getEnclosingCallable() {
-    result.asSourceCallable() = this.getFunction()
-  }
-
-  override Declaration getFunction() { result = phi.getBasicBlock().getEnclosingFunction() }
-
-  override DataFlowType getType() { result = this.getSourceVariable().getType() }
-
-  override predicate isGLValue() { phi.getSourceVariable().isGLValue() }
-
-  final override Location getLocationImpl() { result = block.getLastInstruction().getLocation() }
-
-  override string toStringImpl() { result = "Phi input" }
-
-  /** 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)
  }
 }

--- 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
-  // Node -> Use
-  useToNode(bb, i, sv, node) and
-  uncertain = false
+  nodeHasInstruction(node, def.getValue().asInstruction(), def.getIndirectionIndex())
+  or
+  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>;

+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 }
+  }
+
+  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)
+    )
+  }
+
+  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.
- *
- * 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
-  }
-
-  /**
-   * 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 }
-
-  /**
-   * 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)
-  }
-
+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
--- 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>;
--- 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.
--- a/Management/AllocaInLoop.ql
+++ b/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))
    )
--- 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
--- 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 |
--- 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 |
--- 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
--- 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 |
--- 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 |
--- 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 |
--- 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 |
--- 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) {