C++: Use SSA data flow integration module.

2025-12-16 16:53:25 +01:00 · 2025-02-28 14:30:15 +01:00
parent c7ff2f55b5
commit 9375e571b1
8 changed files with 220 additions and 336 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
--- 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
@@ -686,117 +686,45 @@ 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() }
+  override string toStringImpl() { result = node.toString() }
 }

 /**
- * 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`.
+ * Holds if `n` has a local flow step that goes through a back-edge.
 */
-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() }
+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
+  )
 }

 /**
@@ -1374,7 +1302,7 @@ class UninitializedNode extends Node {
    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()
    )
  }
@@ -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
@@ -295,6 +296,11 @@ abstract class UseImpl extends TUseImpl {
    )
  }

+  final predicate hasNodeAndSourceVariable(Node n, SourceVariable sv) {
+    sv = this.getSourceVariable() and
+    n = this.getNode()
+  }
+
  /**
   * Holds if this use is guaranteed to read the
   * associated variable.
@@ -669,21 +675,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 +688,17 @@ predicate outNodeHasAddressAndIndex(
 *
 * Holds if `node` is the node that corresponds to the definition of `def`.
 */
-predicate defToNode(
-  Node node, Definition 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 +706,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 +715,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 +761,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 +817,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 +857,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 +872,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
 ) {
@@ -1036,18 +926,6 @@ 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`,
@@ -1069,6 +947,11 @@ module SsaCached {
    SsaImpl::ssaDefReachesReadExt(v, def, bb, i)
  }

+  cached
+  predicate ssaDefReachesRead(SourceVariable v, Definition def, IRBlock bb, int i) {
+    SsaImpl::ssaDefReachesRead(v, def, bb, i)
+  }
+
  predicate variableRead = SsaInput::variableRead/4;

  predicate variableWrite = SsaInput::variableWrite/4;
@@ -1096,6 +979,127 @@ class GlobalDef extends Definition {

 private module SsaImpl = SsaImplCommon::Make<Location, SsaInput>;

+private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationInputSig {
+  private import codeql.util.Void
+
+  final private class UseImplFinal = UseImpl;
+
+  class Expr extends UseImplFinal {
+    predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this.hasIndexInBlock(bb, i) }
+  }
+
+  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.hasIndexInBlock(bb, i, v)
+    )
+  }
+
+  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 guardChecks(
+    DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch,
+    int indirectionIndex
+  ) {
+    guardChecksNode(g, e.getNode(), branch, indirectionIndex)
+  }
+
+  Node getABarrierNode(int indirectionIndex) {
+    exists(DataFlowIntegrationImpl::Node n |
+      n =
+        DataFlowIntegrationImpl::BarrierGuardWithState<int, guardChecks/4>::getABarrierNode(indirectionIndex)
+    |
+      n = result.(SsaSynthNode).getSynthNode()
+      or
+      n.(DataFlowIntegrationImpl::ExprNode).getExpr().getNode() = result
+    )
+  }
+}
+
+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
+  result.(DataFlowIntegrationImpl::ExprNode).getExpr().hasNodeAndSourceVariable(n, v)
+  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.
 *
@@ -1209,16 +1213,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