diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
index 602732ea22a8..764bb823d66e 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
@@ -2182,17 +2182,6 @@ module IteratorFlow {
   private module DataFlowIntegrationInput implements IteratorSsa::DataFlowIntegrationInputSig {
     private import codeql.util.Void
 
-    class Expr extends Instruction {
-      Expr() {
-        exists(IRBlock bb, int i |
-          SsaInput::variableRead(bb, i, _, true) and
-          this = bb.getInstruction(i)
-        )
-      }
-
-      predicate hasCfgNode(IRCfg::BasicBlock bb, int i) { bb.getInstruction(i) = this }
-    }
-
     predicate ssaDefHasSource(IteratorSsa::WriteDefinition def) { none() }
 
     predicate allowFlowIntoUncertainDef(IteratorSsa::UncertainWriteDefinition def) { any() }
@@ -2280,7 +2269,7 @@ module IteratorFlow {
     result = n.(SsaIteratorNode).getIteratorFlowNode()
     or
     exists(Ssa::UseImpl use, IRBlock bb, int i |
-      result.(DataFlowIntegrationImpl::ExprNode).getExpr().hasCfgNode(bb, i) and
+      result.(DataFlowIntegrationImpl::ReadNode).readsAt(bb, i, v) and
       use.hasIndexInBlock(bb, i, v) and
       use.getNode() = n
     )
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll
index 70dfbd753723..5febe0ead3a8 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll
@@ -1154,17 +1154,6 @@ private module SsaImpl = Ssa::Make<Location, IRCfg, SsaInput>;
 private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationInputSig {
   private import codeql.util.Boolean
 
-  class Expr extends Instruction {
-    Expr() {
-      exists(IRBlock bb, int i |
-        variableRead(bb, i, _, true) and
-        this = bb.getInstruction(i)
-      )
-    }
-
-    predicate hasCfgNode(IRCfg::BasicBlock bb, int i) { bb.getInstruction(i) = this }
-  }
-
   predicate ssaDefHasSource(SsaImpl::WriteDefinition def) { none() }
 
   predicate allowFlowIntoUncertainDef(SsaImpl::UncertainWriteDefinition def) { any() }
diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
index df0bef74f0ca..658c59606188 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
@@ -494,9 +494,9 @@ module SsaFlow {
   Impl::Node asNode(Node n) {
     n = TSsaNode(result)
     or
-    result.(Impl::ExprNode).getExpr() = n.(ExprNode).getControlFlowNode()
+    result.(Impl::ReadNode).getControlFlowNode() = n.(ExprNode).getControlFlowNode()
     or
-    result.(Impl::ExprPostUpdateNode).getExpr() =
+    result.(Impl::PostUpdateReadNode).getControlFlowNode() =
       n.(PostUpdateNode).getPreUpdateNode().(ExprNode).getControlFlowNode()
     or
     result.(Impl::WriteDefSourceNode).getDefinition() = n.(ExplicitParameterNode).getSsaDefinition()
diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
index ce14d388e453..ed9a30f42260 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
@@ -1012,10 +1012,6 @@ deprecated Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def
 private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
   private import codeql.util.Boolean
 
-  class Expr extends ControlFlowNode {
-    predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
-  }
-
   predicate ssaDefHasSource(Impl::WriteDefinition def) {
     // exclude flow directly from RHS to SSA definition, as we instead want to
     // go from RHS to matching assignable definition, and from there to SSA definition
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
index 5a0df6a222c6..59f932164c80 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
@@ -40,9 +40,10 @@ module SsaFlow {
   Impl::Node asNode(Node n) {
     n = TSsaNode(result)
     or
-    result.(Impl::ExprNode).getExpr() = n.asExpr()
+    result.(Impl::ReadNode).getControlFlowNode() = n.asExpr().getControlFlowNode()
     or
-    result.(Impl::ExprPostUpdateNode).getExpr() = n.(PostUpdateNode).getPreUpdateNode().asExpr()
+    result.(Impl::PostUpdateReadNode).getControlFlowNode() =
+      n.(PostUpdateNode).getPreUpdateNode().asExpr().getControlFlowNode()
     or
     exists(Parameter p |
       n = TExplicitParameterNode(p) and
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
index c69d6ed5f812..4997a832a05e 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
@@ -636,16 +636,6 @@ private class TrackedSsaDef extends Definition {
 private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
   private import java as J
 
-  class Expr instanceof J::Expr {
-    string toString() { result = super.toString() }
-
-    Location getLocation() { result = super.getLocation() }
-
-    predicate hasCfgNode(BasicBlock bb, int i) {
-      super.getControlFlowNode() = bb.(J::BasicBlock).getNode(i)
-    }
-  }
-
   predicate ssaDefHasSource(WriteDefinition def) { def instanceof SsaExplicitWrite }
 
   predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) {
diff --git a/javascript/ql/lib/semmle/javascript/dataflow/internal/DataFlowPrivate.qll b/javascript/ql/lib/semmle/javascript/dataflow/internal/DataFlowPrivate.qll
index 1c3eb1dc9e31..dd821dda29d8 100644
--- a/javascript/ql/lib/semmle/javascript/dataflow/internal/DataFlowPrivate.qll
+++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/DataFlowPrivate.qll
@@ -1230,12 +1230,12 @@ private predicate samePhi(SsaPhiNode legacyPhi, Ssa2::PhiNode newPhi) {
 
 cached
 Node getNodeFromSsa2(Ssa2::Node node) {
-  result = TSsaUseNode(node.(Ssa2::ExprNode).getExpr())
+  result = TSsaUseNode(node.(Ssa2::ReadNode).getControlFlowNode())
   or
-  result = TExprPostUpdateNode(node.(Ssa2::ExprPostUpdateNode).getExpr())
+  result = TExprPostUpdateNode(node.(Ssa2::PostUpdateReadNode).getControlFlowNode())
   or
   exists(ImplicitThisUse use |
-    node.(Ssa2::ExprPostUpdateNode).getExpr() = use and
+    node.(Ssa2::PostUpdateReadNode).getControlFlowNode() = use and
     result = TImplicitThisUse(use, true)
   )
   or
diff --git a/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll b/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
index ebeec96673ab..b4b307e63349 100644
--- a/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
+++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
@@ -56,12 +56,6 @@ js::ControlFlowNode getARead(Definition def) {
 module SsaDataflowInput implements DataFlowIntegrationInputSig {
   private import codeql.util.Boolean
 
-  class Expr extends js::ControlFlowNode {
-    Expr() { this = any(SsaConfig::SourceVariable v).getAUse() }
-
-    predicate hasCfgNode(js::Cfg::BasicBlock bb, int i) { this = bb.getNode(i) }
-  }
-
   predicate ssaDefHasSource(WriteDefinition def) {
     // This library only handles use-use flow after a post-update, there are no definitions, only uses.
     none()
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
index 10dab22ca193..d220268a9007 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
@@ -123,9 +123,10 @@ module SsaFlow {
   Impl::Node asNode(Node n) {
     n = TSsaNode(result)
     or
-    result.(Impl::ExprNode).getExpr() = n.asExpr()
+    result.(Impl::ReadNode).getControlFlowNode() = n.asExpr()
     or
-    result.(Impl::ExprPostUpdateNode).getExpr() = n.(PostUpdateNode).getPreUpdateNode().asExpr()
+    result.(Impl::PostUpdateReadNode).getControlFlowNode() =
+      n.(PostUpdateNode).getPreUpdateNode().asExpr()
     or
     exists(SsaImpl::ParameterExt p |
       n = toParameterNode(p) and
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
index e866d5b70b23..0a2aad3bcef7 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
@@ -434,10 +434,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
   private import codeql.ruby.controlflow.internal.Guards as Guards
   private import codeql.util.Boolean
 
-  class Expr extends Cfg::CfgNodes::ExprCfgNode {
-    predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
-  }
-
   predicate ssaDefHasSource(WriteDefinition def) {
     any(ParameterExt p).isInitializedBy(def) or def.(Ssa::WriteDefinition).assigns(_)
   }
diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll
index befe95178930..02f14ed9bde1 100644
--- a/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll
+++ b/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll
@@ -123,9 +123,10 @@ module SsaFlow {
   SsaFlow::Node asNode(Node n) {
     n = TSsaNode(result)
     or
-    result.(SsaFlow::ExprNode).getExpr() = n.asExpr()
+    result.(SsaFlow::ReadNode).getControlFlowNode() = n.asExpr().getACfgNode()
     or
-    result.(SsaFlow::ExprPostUpdateNode).getExpr() = n.(PostUpdateNode).getPreUpdateNode().asExpr()
+    result.(SsaFlow::PostUpdateReadNode).getControlFlowNode() =
+      n.(PostUpdateNode).getPreUpdateNode().asExpr().getACfgNode()
   }
 
   predicate localFlowStep(
diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
index 1845e87b26c9..df358e2a1cb9 100644
--- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
+++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
@@ -328,16 +328,10 @@ private module Cached {
 import Cached
 private import codeql.rust.dataflow.Ssa
 
-private class ExprAlias = Expr;
-
 private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
   private import codeql.rust.dataflow.internal.DataFlowImpl as DataFlowImpl
   private import codeql.util.Boolean
 
-  class Expr extends ExprAlias {
-    predicate hasCfgNode(BasicBlock bb, int i) { this.getACfgNode() = bb.getNode(i) }
-  }
-
   predicate ssaDefHasSource(WriteDefinition def) { none() } // handled in `DataFlowImpl.qll` instead
 
   private predicate isArg(Call call, Expr e) {
diff --git a/shared/dataflow/codeql/dataflow/VariableCapture.qll b/shared/dataflow/codeql/dataflow/VariableCapture.qll
index b865fa2ef923..b4230b648306 100644
--- a/shared/dataflow/codeql/dataflow/VariableCapture.qll
+++ b/shared/dataflow/codeql/dataflow/VariableCapture.qll
@@ -748,12 +748,6 @@ module Flow<
   private module DataFlowIntegrationInput implements CaptureSsa::DataFlowIntegrationInputSig {
     private import codeql.util.Void
 
-    class Expr instanceof Cfg::ControlFlowNode {
-      string toString() { result = super.toString() }
-
-      predicate hasCfgNode(Cfg::BasicBlock bb, int i) { bb.getNode(i) = this }
-    }
-
     class GuardValue = Void;
 
     class Guard extends Void {
@@ -982,12 +976,12 @@ module Flow<
     n = TSynthSsa(result)
     or
     exists(BasicBlock bb, int i |
-      result.(SsaFlow::ExprNode).getExpr().hasCfgNode(bb, i) and
+      result.(SsaFlow::ReadNode).readsAt(bb, i, cc) and
       ssaReadAt(n, cc, false, bb, i)
     )
     or
     exists(BasicBlock bb, int i |
-      result.(SsaFlow::ExprPostUpdateNode).getExpr().hasCfgNode(bb, i) and
+      result.(SsaFlow::PostUpdateReadNode).readsAt(bb, i, cc) and
       ssaReadAt(n, cc, true, bb, i)
     )
     or
diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll
index 9670655856d3..7e0d344f0cc2 100644
--- a/shared/ssa/codeql/ssa/Ssa.qll
+++ b/shared/ssa/codeql/ssa/Ssa.qll
@@ -45,21 +45,13 @@ signature module InputSig<LocationSig Location, TypSig BasicBlock> {
   predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain);
 
   /**
-   * Holds if the `i1`th node of basic block `bb1` reads source variable `v`
-   * and this read has an associated post-update that occurs at the `i2`th node
-   * of basic block `bb2`.
+   * Holds if the `i`th node of basic block `bb` is a post-update read of
+   * source variable `v`.
    *
    * If left empty, post-updates are considered to occur at the same control
-   * flow node as the read.
-   *
-   * If specified for only some reads, the remaining reads are assumed to not
-   * have post-updates.
+   * flow node as certain reads.
    */
-  default predicate variableReadWithPostUpdate(
-    BasicBlock bb1, int i1, SourceVariable v, BasicBlock bb2, int i2
-  ) {
-    none()
-  }
+  default predicate postUpdateRead(BasicBlock bb, int i, SourceVariable v) { none() }
 
   /**
    * Reverse references to predicates that should be cached in the cached stage
@@ -377,10 +369,6 @@ module Make<
     }
   }
 
-  private predicate postUpdate(BasicBlock bb, int i, SourceVariable v) {
-    variableReadWithPostUpdate(_, _, v, bb, i)
-  }
-
   /**
    * Liveness analysis (based on source variables) to restrict the size of the
    * SSA representation.
@@ -485,7 +473,7 @@ module Make<
   pragma[nomagic]
   private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
     exists(BasicBlock readbb | readbb.inDominanceFrontier(bb) |
-      (variableRead(readbb, _, v, true) or postUpdate(readbb, _, v)) and
+      (variableRead(readbb, _, v, true) or postUpdateRead(readbb, _, v)) and
       not variableWrite(readbb, _, v, _)
       or
       synthPhiRead(readbb, v) and
@@ -646,7 +634,7 @@ module Make<
       variableRead(bb, i, v, true) and
       k = Read()
       or
-      postUpdate(bb, i, v) and
+      postUpdateRead(bb, i, v) and
       k = Read()
       or
       variableWrite(bb, i, v, false) and
@@ -684,7 +672,7 @@ module Make<
     }
 
     private predicate justPostUpdate(BasicBlock bb, int i, SourceVariable v) {
-      postUpdate(bb, i, v) and
+      postUpdateRead(bb, i, v) and
       not variableRead(bb, i, v, true) and
       not variableWrite(bb, i, v, _)
     }
@@ -1405,15 +1393,6 @@ module Make<
       inputRefs < 2
     }
 
-    /**
-     * Holds if the supposed read at `bb` and `i` has a post-update, but no
-     * actual certain read.
-     */
-    query predicate postUpdateWithoutRead(SourceVariable v, BasicBlock bb, int i) {
-      variableReadWithPostUpdate(bb, i, v, _, _) and
-      not variableRead(bb, i, v, true)
-    }
-
     /**
      * Gets counts of inconsistencies of each type.
      */
@@ -1466,26 +1445,11 @@ module Make<
         strictcount(BasicBlock bbPhi, SourceVariable v, int inputRefs |
           phiReadWithoutTwoPriorRefs(bbPhi, v, inputRefs)
         )
-      or
-      type = "Post-update without read" and
-      result = strictcount(SourceVariable v, BasicBlock bb, int i | postUpdateWithoutRead(v, bb, i))
     }
   }
 
   /** Provides the input to `DataFlowIntegration`. */
   signature module DataFlowIntegrationInputSig {
-    /**
-     * An expression with a value. That is, we expect these expressions to be
-     * represented in the data flow graph.
-     */
-    class Expr {
-      /** Gets a textual representation of this expression. */
-      string toString();
-
-      /** Holds if the `i`th node of basic block `bb` evaluates this expression. */
-      predicate hasCfgNode(BasicBlock bb, int i);
-    }
-
     /**
      * Holds if `def` has some form of input flow. For example, the right-hand
      * side of an assignment or a parameter of an SSA entry definition.
@@ -1600,11 +1564,10 @@ module Make<
     }
 
     pragma[nomagic]
-    private DfInput::Expr getARead(Definition def) {
+    private predicate hasRead(Definition def) {
       exists(SourceVariable v, BasicBlock bb, int i |
         ssaDefReachesRead(v, def, bb, i) and
-        variableRead(bb, i, v, true) and
-        result.hasCfgNode(bb, i)
+        variableRead(bb, i, v, true)
       )
     }
 
@@ -1623,7 +1586,7 @@ module Make<
 
     pragma[nomagic]
     private predicate phiInputHasRead(SsaPhiExt phi, BasicBlock input) {
-      exists(getARead(getAPhiInputDef(phi, input)))
+      hasRead(getAPhiInputDef(phi, input))
     }
 
     /** Holds if `bb` is the target end of a branch edge of a guard and the guard controls `bb`. */
@@ -1762,21 +1725,16 @@ module Make<
     cached
     private newtype TNode =
       TWriteDefSource(WriteDefinition def) { DfInput::ssaDefHasSource(def) } or
-      TExprNode(DfInput::Expr e, SourceVariable v, boolean isPost) {
-        exists(BasicBlock bb, int i | e.hasCfgNode(bb, i) |
+      TReadNode(ControlFlowNode n, SourceVariable v, boolean isPost) {
+        exists(BasicBlock bb, int i | bb.getNode(i) = n |
           variableRead(bb, i, v, true) and
-          isPost = false and
-          // Only materialise if 'expr' has a reaching definition.
-          // Note that the read may correspond to a different variable than 'v', but the C++
-          // instantiation currently expects this particular behaviour.
-          getARead(_) = e
+          isPost = false
           or
-          not postUpdate(_, _, _) and
+          not postUpdateRead(_, _, _) and
           variableRead(bb, i, v, true) and
-          isPost = true and
-          getARead(_) = e
+          isPost = true
           or
-          postUpdate(bb, i, v) and
+          postUpdateRead(bb, i, v) and
           isPost = true
         )
       } or
@@ -1825,84 +1783,48 @@ module Make<
 
     final class WriteDefSourceNode = WriteDefSourceNodeImpl;
 
-    /** A (post-update) expression node. */
-    abstract private class ExprNodePreOrPostImpl extends NodeImpl, TExprNode {
-      DfInput::Expr e;
+    /** A read node or post-update read node. */
+    abstract private class ReadNodePreOrPostImpl extends NodeImpl, TReadNode {
+      ControlFlowNode n_;
       boolean isPost;
       SourceVariable v_;
 
-      ExprNodePreOrPostImpl() { this = TExprNode(e, v_, isPost) }
-
-      /** Gets the underlying expression. */
-      DfInput::Expr getExpr() { result = e }
-
-      /** Holds if this represents the access to `var` performed at `expr`. */
-      predicate isExprAndVariable(DfInput::Expr expr, SourceVariable var) { expr = e and var = v_ }
+      ReadNodePreOrPostImpl() { this = TReadNode(n_, v_, isPost) }
 
-      override Location getLocation() {
-        exists(BasicBlock bb, int i |
-          e.hasCfgNode(bb, i) and
-          result = bb.getNode(i).getLocation()
-        )
-      }
+      /** Gets the control flow node of this read or post-update. */
+      ControlFlowNode getControlFlowNode() { result = n_ }
 
-      /** Gets the variable accessed at this expression. */
-      SourceVariable getSourceVariable() { result = v_ }
-    }
+      /** Holds if this node reads `v` at `n`. */
+      pragma[nomagic]
+      predicate readsAt(ControlFlowNode n, SourceVariable v) { n = n_ and v = v_ }
 
-    final class ExprNodePreOrPost = ExprNodePreOrPostImpl;
+      /** Holds if this node reads `v` at `bb,i`. */
+      pragma[nomagic]
+      predicate readsAt(BasicBlock bb, int i, SourceVariable v) { bb.getNode(i) = n_ and v = v_ }
 
-    /** An expression node. */
-    private class ExprNodeImpl extends ExprNodePreOrPostImpl {
-      ExprNodeImpl() { isPost = false }
+      override Location getLocation() { result = n_.getLocation() }
 
-      override string toString() { result = e.toString() }
+      /** Gets the variable accessed at this read. */
+      SourceVariable getSourceVariable() { result = v_ }
     }
 
-    final class ExprNode = ExprNodeImpl;
-
-    /** A post-update expression node. */
-    private class ExprPostUpdateNodeImpl extends ExprNodePreOrPostImpl {
-      ExprPostUpdateNodeImpl() { isPost = true }
-
-      /** Gets the pre-update expression node. */
-      ExprNode getPreUpdateNode() {
-        not postUpdate(_, _, _) and
-        result = TExprNode(e, v_, false)
-        or
-        exists(DfInput::Expr e1, BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
-          result = TExprNode(e1, v_, false) and
-          e1.hasCfgNode(bb1, i1) and
-          variableReadWithPostUpdate(bb1, i1, v_, bb2, i2) and
-          e.hasCfgNode(bb2, i2)
-        )
-      }
+    /** A node corresponding to a `(bb,i,v)` tuple from `variableRead(bb,i,v,true)` */
+    private class ReadNodeImpl extends ReadNodePreOrPostImpl {
+      ReadNodeImpl() { isPost = false }
 
-      override string toString() { result = e.toString() + " [postupdate]" }
+      override string toString() { result = n_.toString() }
     }
 
-    final class ExprPostUpdateNode = ExprPostUpdateNodeImpl;
-
-    pragma[nomagic]
-    private predicate exprReadAt(
-      DfInput::Expr e, BasicBlock bb, int i, SourceVariable v, boolean isPost, TExprNode node
-    ) {
-      e.hasCfgNode(bb, i) and
-      node = TExprNode(e, v, isPost)
-    }
+    final class ReadNode = ReadNodeImpl;
 
-    private class ReadNodeImpl extends ExprNodeImpl {
-      ReadNodeImpl() { exprReadAt(e, _, _, _, false, this) }
+    /** A post-update read node. */
+    private class PostUpdateReadNodeImpl extends ReadNodePreOrPostImpl {
+      PostUpdateReadNodeImpl() { isPost = true }
 
-      /** Holds if this node reads `v` at `bb,i` */
-      pragma[nomagic]
-      predicate readsAt(BasicBlock bb, int i, SourceVariable v) {
-        exprReadAt(e, bb, i, v, false, this)
-      }
+      override string toString() { result = n_.toString() + " [postupdate]" }
     }
 
-    /** A node corresponding to a `(bb,i,v)` tuple from `variableRead(bb,i,v,true)` */
-    final class ReadNode = ReadNodeImpl;
+    final class PostUpdateReadNode = PostUpdateReadNodeImpl;
 
     /** A synthesized SSA data flow node. */
     abstract private class SsaNodeImpl extends NodeImpl {
@@ -2040,7 +1962,7 @@ module Make<
         isUseStep = false
       )
       or
-      exprReadAt(_, bb, i, v, _, nodeFrom) and
+      nodeFrom.(ReadNodePreOrPostImpl).readsAt(bb, i, v) and
       not variableWrite(bb, i, v, true) and
       isUseStep = true
     }
@@ -2065,7 +1987,7 @@ module Make<
       // Flow from definition/read via post-update node
       exists(BasicBlock bb2, int i2 |
         AdjacentSsaRefs::adjacentRefRead(bb1, i1, bb2, i2, v) and
-        postUpdate(bb2, i2, v) and
+        postUpdateRead(bb2, i2, v) and
         not any(ReadNode r).readsAt(bb2, i2, v) and
         not any(UncertainWriteDefinition def2).definesAt(v, bb2, i2) and
         flowFromRefToNode(v, bb2, i2, nodeTo)
@@ -2126,6 +2048,13 @@ module Make<
       )
     }
 
+    private predicate readsDef(ReadNode node, Definition def) {
+      exists(SourceVariable v, BasicBlock bb, int i |
+        ssaDefReachesRead(v, def, bb, i) and
+        node.readsAt(bb, i, v)
+      )
+    }
+
     /** Holds if the value of `nodeTo` is given by `nodeFrom`. */
     predicate localMustFlowStep(SourceVariable v, Node nodeFrom, Node nodeTo) {
       exists(Definition def |
@@ -2134,13 +2063,13 @@ module Make<
         v = def.getSourceVariable() and
         if DfInput::includeWriteDefsInFlowStep()
         then nodeTo.(SsaDefinitionNode).getDefinition() = def
-        else nodeTo.(ExprNode).isExprAndVariable(getARead(def), v)
+        else readsDef(nodeTo, def)
       )
       or
       // Flow from SSA definition to read
       exists(DefinitionExt def |
         nodeFrom.(SsaDefinitionExtNodeImpl).getDefExt() = def and
-        nodeTo.(ExprNode).isExprAndVariable(getARead(def), v) and
+        readsDef(nodeTo, def) and
         v = def.getSourceVariable()
       )
     }
@@ -2206,11 +2135,10 @@ module Make<
           guardChecks(g, def, val, state)
         |
           // guard controls a read
-          exists(DfInput::Expr e |
-            e = getARead(def) and
-            e.hasCfgNode(bb, _) and
+          exists(SourceVariable v, int i |
+            ssaDefReachesRead(v, def, bb, i) and
             DfInput::guardControlsBlock(g, bb, val) and
-            result.(ExprNode).isExprAndVariable(e, def.getSourceVariable())
+            result.(ReadNode).readsAt(bb, i, v)
           )
           or
           // guard controls input block to a phi node
@@ -2245,7 +2173,7 @@ module Make<
   module TestAdjacentRefs {
     private newtype TRef =
       TRefRead(BasicBlock bb, int i, SourceVariable v) { variableRead(bb, i, v, true) } or
-      TRefPostUpdate(BasicBlock bb, int i, SourceVariable v) { postUpdate(bb, i, v) } or
+      TRefPostUpdate(BasicBlock bb, int i, SourceVariable v) { postUpdateRead(bb, i, v) } or
       TRefDef(Definition def) or
       TRefPhiRead(BasicBlock bb, SourceVariable v) { synthPhiRead(bb, v) }
 
diff --git a/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll b/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll
index 532ff80a8a2c..b9c0f0a78ace 100644
--- a/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll
+++ b/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll
@@ -29,13 +29,8 @@ module LocalSsaInput implements InputSig<Location, BasicBlock> {
     performsVariableAccess(_, v, TRead(), bb.getNode(i))
   }
 
-  predicate variableReadWithPostUpdate(
-    BasicBlock bb1, int i1, SourceVariable v, BasicBlock bb2, int i2
-  ) {
-    exists(U::AstNode repr |
-      performsVariableAccess(repr, v, TRead(), bb1.getNode(i1)) and
-      performsVariableAccess(repr, v, TPostUpdate(), bb2.getNode(i2))
-    )
+  predicate postUpdateRead(BasicBlock bb, int i, SourceVariable v) {
+    performsVariableAccess(_, v, TPostUpdate(), bb.getNode(i))
   }
 
   predicate ssaCachedStageRevRef() { LocalSsaDataFlowOutput::ssaCachedStageRevRef2() }
@@ -46,10 +41,6 @@ module LocalSsaOutput = Make<Location, Cfg, LocalSsaInput>;
 private import LocalSsaOutput
 
 module LocalSsaDataFlowInput implements DataFlowIntegrationInputSig {
-  class Expr extends ControlFlowNode {
-    predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
-  }
-
   class GuardValue = Void;
 
   class Guard extends Void {
@@ -71,13 +62,13 @@ Stage2Node getNodeFromLocalSsaNode(Ssa::Node n) {
   result = TLocalSsaNode(n)
   or
   exists(ControlFlowNode cfgnode, LocalVariable v, AstNode repr |
-    n.(Ssa::ExprNode).isExprAndVariable(cfgnode, v) and
+    n.(Ssa::ReadNode).readsAt(cfgnode, v) and
     performsVariableAccess(repr, v, TRead(), cfgnode) and
     result.(BuilderNode).isLocalVariableRead(repr, v)
   )
   or
   exists(ControlFlowNode cfgnode, LocalVariable v, AstNode repr |
-    n.(Ssa::ExprPostUpdateNode).isExprAndVariable(cfgnode, v) and
+    n.(Ssa::PostUpdateReadNode).readsAt(cfgnode, v) and
     performsVariableAccess(repr, v, TPostUpdate(), cfgnode) and
     result.(BuilderNode).isLocalVariablePostUpdate(repr, v)
   )