From 8fb484d6002a818c7b275cf7b4981a8c777219a9 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Tue, 3 Nov 2026 13:41:34 +0100
Subject: [PATCH 1/2] SSA: Cache main computation directly.

---
 .../code/cpp/ir/dataflow/internal/SsaImpl.qll | 40 ++++------
 go/ql/lib/semmle/go/dataflow/SsaImpl.qll      |  9 ---
 ruby/ql/lib/codeql/ruby/dataflow/SSA.qll      |  6 +-
 .../codeql/ruby/dataflow/internal/SsaImpl.qll | 10 ---
 rust/ql/lib/codeql/rust/dataflow/Ssa.qll      |  6 +-
 .../codeql/rust/dataflow/internal/SsaImpl.qll | 10 ---
 shared/ssa/codeql/ssa/Ssa.qll                 | 74 +++++++++----------
 7 files changed, 57 insertions(+), 98 deletions(-)

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 8f17c3c9a136..85b3e1fae7f2 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
@@ -1106,35 +1106,25 @@ private module SsaInput implements Ssa::InputSig<Location, IRCfg::BasicBlock> {
   }
 }
 
-/**
- * The final SSA predicates used for dataflow purposes.
- */
-cached
-module SsaCached {
-  cached
-  predicate ssaDefReachesRead(SourceVariable v, Definition def, IRBlock bb, int i) {
-    SsaImpl::ssaDefReachesRead(v, def, bb, i)
-  }
+predicate ssaDefReachesRead(SourceVariable v, Definition def, IRBlock bb, int i) {
+  SsaImpl::ssaDefReachesRead(v, def, bb, i)
+}
 
-  cached
-  predicate phiHasInputFromBlock(PhiNode phi, Definition inp, IRBlock bb) {
-    SsaImpl::phiHasInputFromBlock(phi, inp, bb)
-  }
+predicate phiHasInputFromBlock(PhiNode phi, Definition inp, IRBlock bb) {
+  SsaImpl::phiHasInputFromBlock(phi, inp, bb)
+}
 
-  cached
-  predicate uncertainWriteDefinitionInput(Definition uncertain, Definition inp) {
-    SsaImpl::uncertainWriteDefinitionInput(uncertain, inp)
-  }
+predicate uncertainWriteDefinitionInput(Definition uncertain, Definition inp) {
+  SsaImpl::uncertainWriteDefinitionInput(uncertain, inp)
+}
 
-  cached
-  predicate ssaDefReachesEndOfBlock(IRBlock bb, Definition def) {
-    SsaImpl::ssaDefReachesEndOfBlock(bb, def, _)
-  }
+predicate ssaDefReachesEndOfBlock(IRBlock bb, Definition def) {
+  SsaImpl::ssaDefReachesEndOfBlock(bb, def, _)
+}
 
-  predicate variableRead = SsaInput::variableRead/4;
+predicate variableRead = SsaInput::variableRead/4;
 
-  predicate variableWrite = SsaInput::variableWrite/4;
-}
+predicate variableWrite = SsaInput::variableWrite/4;
 
 /** Gets the `DefImpl` corresponding to `def`. */
 pragma[nomagic]
@@ -1654,5 +1644,3 @@ class IndirectExplicitDefinition extends ExplicitDefinition {
 class DirectExplicitDefinition extends ExplicitDefinition {
   DirectExplicitDefinition() { this.getIndirectionIndex() = 0 }
 }
-
-import SsaCached
diff --git a/go/ql/lib/semmle/go/dataflow/SsaImpl.qll b/go/ql/lib/semmle/go/dataflow/SsaImpl.qll
index c206dccbba38..51ca4aebb518 100644
--- a/go/ql/lib/semmle/go/dataflow/SsaImpl.qll
+++ b/go/ql/lib/semmle/go/dataflow/SsaImpl.qll
@@ -140,32 +140,23 @@ final class PhiNode = Impl::PhiNode;
 module Consistency = Impl::Consistency;
 
 /**
- * NB: This predicate should be cached.
- *
  * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
  * basic block `bb`.
  */
-cached
 predicate ssaDefReachesRead(SsaSourceVariable v, Definition def, BasicBlock bb, int i) {
   Impl::ssaDefReachesRead(v, def, bb, i)
 }
 
 /**
- * NB: This predicate should be cached.
- *
  * Holds if the SSA definition of `v` at `def` reaches the end of basic block `bb`.
  */
-cached
 predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SsaSourceVariable v) {
   Impl::ssaDefReachesEndOfBlock(bb, def, v)
 }
 
 /**
- * NB: This predicate should be cached.
- *
  * Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
  */
-cached
 predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
   Impl::phiHasInputFromBlock(phi, inp, bb)
 }
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/SSA.qll b/ruby/ql/lib/codeql/ruby/dataflow/SSA.qll
index d95740a8c867..5ded34644bd9 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/SSA.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/SSA.qll
@@ -333,7 +333,9 @@ module Ssa {
      * Gets the immediately preceding definition. Since this update is uncertain,
      * the value from the preceding definition might still be valid.
      */
-    final Definition getPriorDefinition() { result = SsaImpl::uncertainWriteDefinitionInput(this) }
+    final Definition getPriorDefinition() {
+      SsaImpl::Impl::uncertainWriteDefinitionInput(this, result)
+    }
 
     override string toString() { result = "<captured exit> " + this.getSourceVariable() }
   }
@@ -381,7 +383,7 @@ module Ssa {
 
     /** Holds if `inp` is an input to this phi node along the edge originating in `bb`. */
     predicate hasInputFromBlock(Definition inp, BasicBlock bb) {
-      inp = SsaImpl::phiHasInputFromBlock(this, bb)
+      SsaImpl::Impl::phiHasInputFromBlock(this, inp, bb)
     }
 
     override string toString() { result = "phi" }
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
index 9f5dfd9dcc25..2ed2e5940ae8 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
@@ -279,11 +279,6 @@ private module Cached {
 
   private import codeql.ruby.dataflow.SSA
 
-  cached
-  Definition phiHasInputFromBlock(PhiNode phi, Cfg::BasicBlock bb) {
-    Impl::phiHasInputFromBlock(phi, result, bb)
-  }
-
   /**
    * Holds if the value defined at SSA definition `def` can reach a read at `read`,
    * without passing through any other non-pseudo read.
@@ -310,11 +305,6 @@ private module Cached {
     )
   }
 
-  cached
-  Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
-    Impl::uncertainWriteDefinitionInput(def, result)
-  }
-
   cached
   module DataFlowIntegration {
     import DataFlowIntegrationImpl
diff --git a/rust/ql/lib/codeql/rust/dataflow/Ssa.qll b/rust/ql/lib/codeql/rust/dataflow/Ssa.qll
index 52e7d35e3b48..9c4ad45718b8 100644
--- a/rust/ql/lib/codeql/rust/dataflow/Ssa.qll
+++ b/rust/ql/lib/codeql/rust/dataflow/Ssa.qll
@@ -266,7 +266,7 @@ module Ssa {
 
     /** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */
     predicate hasInputFromBlock(Definition inp, BasicBlock bb) {
-      inp = SsaImpl::phiHasInputFromBlock(this, bb)
+      SsaImpl::Impl::phiHasInputFromBlock(this, inp, bb)
     }
 
     private string getSplitString() {
@@ -354,7 +354,9 @@ module Ssa {
      * Gets the immediately preceding definition. Since this update is uncertain,
      * the value from the preceding definition might still be valid.
      */
-    final Definition getPriorDefinition() { result = SsaImpl::uncertainWriteDefinitionInput(this) }
+    final Definition getPriorDefinition() {
+      SsaImpl::Impl::uncertainWriteDefinitionInput(this, result)
+    }
 
     override string toString() { result = "<captured exit> " + this.getSourceVariable() }
   }
diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
index 874126f6a08c..aeffd8edd20a 100644
--- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
+++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
@@ -236,11 +236,6 @@ private module Cached {
     )
   }
 
-  cached
-  Definition phiHasInputFromBlock(PhiDefinition phi, BasicBlock bb) {
-    Impl::phiHasInputFromBlock(phi, result, bb)
-  }
-
   /**
    * Holds if the value defined at SSA definition `def` can reach a read at `read`,
    * without passing through any other non-pseudo read.
@@ -267,11 +262,6 @@ private module Cached {
     )
   }
 
-  cached
-  Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
-    Impl::uncertainWriteDefinitionInput(def, result)
-  }
-
   cached
   module DataFlowIntegration {
     import DataFlowIntegrationImpl
diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll
index 9680480b7472..0fd5cd4d1be3 100644
--- a/shared/ssa/codeql/ssa/Ssa.qll
+++ b/shared/ssa/codeql/ssa/Ssa.qll
@@ -269,12 +269,8 @@ signature module SsaSig<
  * block, the read is assumed to happen before the write.
  *
  * The result of invoking this parameterized module is not meant to be exposed directly;
- * instead, one should define a language-specific layer on top, and make sure to cache
- * all exposed predicates marked with
- *
- * ```
- * NB: If this predicate is exposed, it should be cached.
- * ```
+ * instead, one should invoke the nested `MakeSsa` module and expose the
+ * resulting class hierarchy.
  */
 module Make<
   LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
@@ -282,6 +278,24 @@ module Make<
   private import Cfg
   private import Input
 
+  /** The cached stage of the SSA construction. */
+  cached
+  private module SsaCachedStage {
+    /** Reference to the cached stage of the SSA construction. */
+    cached
+    predicate ref() { any() }
+
+    /** Reverse references to the predicates that reference `ref()`. */
+    cached
+    predicate revRef() {
+      (exists(TWriteDef(_, _, _)) implies any()) and
+      (ssaDefReachesEndOfBlock(_, _, _) implies any()) and
+      (phiHasInputFromBlock(_, _, _) implies any()) and
+      (ssaDefReachesRead(_, _, _, _) implies any()) and
+      (uncertainWriteDefinitionInput(_, _) implies any())
+    }
+  }
+
   private BasicBlock getABasicBlockPredecessor(BasicBlock bb) { result.getASuccessor() = bb }
 
   /**
@@ -486,6 +500,7 @@ module Make<
   cached
   private newtype TDefinitionExt =
     TWriteDef(SourceVariable v, BasicBlock bb, int i) {
+      SsaCachedStage::ref() and
       variableWrite(bb, i, v, _) and
       liveAfterWrite(bb, i, v)
     } or
@@ -550,9 +565,10 @@ module Make<
      * block `bb`, at which point it is still live, without crossing another
      * SSA definition of `v`.
      */
-    pragma[nomagic]
+    cached
     predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
       exists(int last |
+        SsaCachedStage::ref() and
         last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
         ssaDefReachesRank(bb, def, last, v) and
         liveAtExit(bb, v)
@@ -594,8 +610,10 @@ module Make<
       not ssaDefReachesReadWithinBlock(v, _, bb, i)
     }
 
+    cached
     predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
       exists(SourceVariable v, BasicBlock bb, int i |
+        SsaCachedStage::ref() and
         def.definesAt(v, bb, i) and
         ssaDefReachesRead(v, inp, bb, i)
       )
@@ -761,7 +779,7 @@ module Make<
         if any(Definition def).definesAt(v, bb0, i0)
         then samevar = false
         else (
-          samevar = samevar0 and synthPhiRead(bb0, v) and i0 = -1
+          samevar = samevar0 and exists(TPhiReadNode(v, bb0)) and i0 = -1
         )
       )
     }
@@ -805,21 +823,15 @@ module Make<
     )
   }
 
-  /**
-   * NB: If this predicate is exposed, it should be cached.
-   *
-   * Same as `ssaDefReachesEndOfBlockExt`, but ignores phi-reads.
-   */
   predicate ssaDefReachesEndOfBlock = SsaDefReaches::ssaDefReachesEndOfBlock/3;
 
   /**
-   * NB: If this predicate is exposed, it should be cached.
-   *
    * Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
    */
-  pragma[nomagic]
+  cached
   predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
     exists(SourceVariable v, BasicBlock bbDef |
+      SsaCachedStage::ref() and
       phi.definesAt(v, bbDef, _) and
       getABasicBlockPredecessor(bbDef) = bb and
       ssaDefReachesEndOfBlock(bb, inp, v)
@@ -827,18 +839,17 @@ module Make<
   }
 
   /**
-   * NB: If this predicate is exposed, it should be cached.
-   *
-   * Same as `ssaDefReachesReadExt`, but ignores phi-reads.
+   * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
+   * basic block `bb`, without crossing another SSA definition of `v`.
    */
+  cached
   predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
+    SsaCachedStage::ref() and
     SsaDefReaches::ssaDefReachesRead(v, def, bb, i) and
     variableRead(bb, i, v, _)
   }
 
   /**
-   * NB: If this predicate is exposed, it should be cached.
-   *
    * Holds if `inp` is an immediately preceding definition of uncertain definition
    * `def`. Since `def` is uncertain, the value from the preceding definition might
    * still be valid.
@@ -1091,21 +1102,6 @@ module Make<
         variableRead(bb, i, v, false)
       }
 
-      cached
-      predicate isLiveAtEndOfBlock(Definition def, BasicBlock bb) {
-        ssaDefReachesEndOfBlock(bb, def, _)
-      }
-
-      cached
-      predicate phiHasInputFromBlockCached(PhiNode phi, Definition inp, BasicBlock bb) {
-        phiHasInputFromBlock(phi, inp, bb)
-      }
-
-      cached
-      predicate uncertainWriteDefinitionInputCached(UncertainWriteDefinition def, Definition inp) {
-        uncertainWriteDefinitionInput(def, inp)
-      }
-
       cached
       predicate explicitWrite(WriteDefinition def, VariableWrite write) {
         exists(BasicBlock bb, int i, SourceVariable v |
@@ -1148,7 +1144,7 @@ module Make<
        * point it is still live, without crossing another SSA definition of the
        * same source variable.
        */
-      predicate isLiveAtEndOfBlock(BasicBlock bb) { isLiveAtEndOfBlock(this, bb) }
+      predicate isLiveAtEndOfBlock(BasicBlock bb) { ssaDefReachesEndOfBlock(bb, this, _) }
 
       /**
        * Gets an SSA definition whose value can flow to this one in one step. This
@@ -1260,7 +1256,7 @@ module Make<
        * Gets the immediately preceding definition. Since this update is uncertain,
        * the value from the preceding definition might still be valid.
        */
-      SsaDefinition getPriorDefinition() { uncertainWriteDefinitionInputCached(this, result) }
+      SsaDefinition getPriorDefinition() { uncertainWriteDefinitionInput(this, result) }
     }
 
     /**
@@ -1284,7 +1280,7 @@ module Make<
 
       /** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */
       predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
-        phiHasInputFromBlockCached(this, inp, bb)
+        phiHasInputFromBlock(this, inp, bb)
       }
 
       /**

From 88c24eccab47960a6b344d13b6d64cc81cdce94a Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 4 Nov 2026 10:53:10 +0100
Subject: [PATCH 2/2] SSA: Tie caching of all 3 SSA modules together.

---
 .../ir/dataflow/internal/DataFlowPrivate.qll  |  2 +
 .../code/cpp/ir/dataflow/internal/SsaImpl.qll | 10 +---
 .../code/csharp/dataflow/internal/BaseSSA.qll |  2 +
 .../code/csharp/dataflow/internal/SsaImpl.qll |  6 +-
 .../code/java/dataflow/internal/BaseSSA.qll   |  2 +
 .../code/java/dataflow/internal/SsaImpl.qll   |  6 +-
 .../dataflow/internal/sharedlib/Ssa.qll       | 16 ++---
 .../codeql/ruby/dataflow/internal/SsaImpl.qll |  4 +-
 .../codeql/rust/dataflow/internal/SsaImpl.qll |  4 +-
 .../codeql/dataflow/VariableCapture.qll       |  2 +
 shared/ssa/codeql/ssa/Ssa.qll                 | 60 ++++++++++++-------
 .../unified/internal/dataflow/LocalSsa.qll    |  2 +
 12 files changed, 68 insertions(+), 48 deletions(-)

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 29f1a16bf58e..fe3941893734 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
@@ -2173,6 +2173,8 @@ module IteratorFlow {
     predicate variableRead(IRCfg::BasicBlock bb, int i, SourceVariable v, boolean certain) {
       Ssa::variableRead(bb, i, v, certain)
     }
+
+    predicate ssaCachedStageRevRef() { DataFlowIntegrationImpl::ssaCachedStageRevRef2() }
   }
 
   private module IteratorSsa = SsaImpl::Make<Location, IRCfg, SsaInput>;
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 85b3e1fae7f2..9626339b2900 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
@@ -1104,6 +1104,8 @@ private module SsaInput implements Ssa::InputSig<Location, IRCfg::BasicBlock> {
       if use.isCertain() then certain = true else certain = false
     )
   }
+
+  predicate ssaCachedStageRevRef() { DataFlowIntegrationImpl::ssaCachedStageRevRef2() }
 }
 
 predicate ssaDefReachesRead(SourceVariable v, Definition def, IRBlock bb, int i) {
@@ -1163,14 +1165,6 @@ private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationI
     predicate hasCfgNode(IRCfg::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 ssaDefHasSource(SsaImpl::WriteDefinition def) { none() }
 
   predicate allowFlowIntoUncertainDef(SsaImpl::UncertainWriteDefinition def) { any() }
diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
index 0e879ac94123..ccefca61186e 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
@@ -121,6 +121,8 @@ private module BaseSsaImpl {
         certain = true
       )
     }
+
+    predicate ssaCachedStageRevRef() { BaseSsa::ssaCachedStageRevRef1() }
   }
 
   module SsaImpl = SsaImplCommon::Make<Location, Cfg, SsaImplInput>;
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 b7257a2f5f2b..f7bb0f809057 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
@@ -39,6 +39,10 @@ private module SsaImplInput implements SsaImplCommon::InputSig<Location, BasicBl
     variableReadPseudo(bb, i, v) and
     certain = false
   }
+
+  predicate ssaCachedStageRevRef() {
+    Ssa_::ssaCachedStageRevRef1() and DataFlowIntegrationImpl::ssaCachedStageRevRef2()
+  }
 }
 
 import SsaImplCommon::Make<Location, Cfg, SsaImplInput> as Impl
@@ -1012,8 +1016,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
     predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
   }
 
-  Expr getARead(Definition def) { def.(SsaDefinition).getARead().getControlFlowNode() = result }
-
   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/BaseSSA.qll b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
index 07d871ab9bc8..ec480a6c0cc5 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
@@ -184,6 +184,8 @@ private module SsaImplInput implements SsaImplCommon::InputSig<Location, BasicBl
     variableCapture(v, _, bb, i) and
     certain = false
   }
+
+  predicate ssaCachedStageRevRef() { Ssa::ssaCachedStageRevRef1() }
 }
 
 private module Impl = SsaImplCommon::Make<Location, Cfg, SsaImplInput>;
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 94dda4b64e08..3f5aa4ad5e96 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
@@ -199,6 +199,10 @@ private module SsaImplInput implements SsaImplCommon::InputSig<Location, BasicBl
     variableCapture(v, _, bb, i) and
     certain = false
   }
+
+  predicate ssaCachedStageRevRef() {
+    Ssa::ssaCachedStageRevRef1() and DataFlowIntegrationImpl::ssaCachedStageRevRef2()
+  }
 }
 
 import SsaImplCommon::Make<Location, Cfg, SsaImplInput> as Impl
@@ -642,8 +646,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
     }
   }
 
-  Expr getARead(Definition def) { result = def.(SsaDefinition).getARead() }
-
   predicate ssaDefHasSource(WriteDefinition def) { def instanceof SsaExplicitWrite }
 
   predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) {
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 7b479ac475b6..efac37607f25 100644
--- a/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
+++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
@@ -38,6 +38,8 @@ module SsaConfig implements InputSig<js::Location, js::Cfg::BasicBlock> {
     certain = true and
     bb.getNode(i).(ThisUse).getBindingContainer() = v.asThisContainer()
   }
+
+  predicate ssaCachedStageRevRef() { DataFlowIntegrationImpl::ssaCachedStageRevRef2() }
 }
 
 import Make<js::Location, js::Cfg, SsaConfig>
@@ -56,16 +58,6 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
     none()
   }
 
-  cached
-  Expr getARead(Definition def) {
-    // Copied from implementation so we can cache it here
-    exists(SsaConfig::SourceVariable v, js::BasicBlock bb, int i |
-      ssaDefReachesRead(v, def, bb, i) and
-      SsaConfig::variableRead(bb, i, v, true) and
-      result.hasCfgNode(bb, i)
-    )
-  }
-
   class GuardValue = Boolean;
 
   class Guard extends js::ControlFlowNode {
@@ -107,4 +99,6 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
   }
 }
 
-import DataFlowIntegration<SsaDataflowInput>
+module DataFlowIntegrationImpl = DataFlowIntegration<SsaDataflowInput>;
+
+import DataFlowIntegrationImpl
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
index 2ed2e5940ae8..67763a2bf78c 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
@@ -56,6 +56,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
     namespaceSelfExitRead(bb, i, v) and
     certain = false
   }
+
+  predicate ssaCachedStageRevRef() { DataFlowIntegrationImpl::ssaCachedStageRevRef2() }
 }
 
 import SsaImplCommon::Make<Location, Cfg::Cfg, SsaInput> as Impl
@@ -436,8 +438,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
     predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
   }
 
-  Expr getARead(Definition def) { result = Cached::getARead(def) }
-
   predicate ssaDefHasSource(WriteDefinition def) {
     any(ParameterExt p).isInitializedBy(def) or def.(Ssa::WriteDefinition).assigns(_)
   }
diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
index aeffd8edd20a..ef2583ab9e9d 100644
--- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
+++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
@@ -79,6 +79,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
     or
     capturedExitRead(bb, i, v) and certain = false
   }
+
+  predicate ssaCachedStageRevRef() { DataFlowIntegrationImpl::ssaCachedStageRevRef2() }
 }
 
 import SsaImplCommon::Make<Location, BasicBlocks::Cfg, SsaInput> as Impl
@@ -336,8 +338,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
     predicate hasCfgNode(BasicBlock bb, int i) { this.getACfgNode() = bb.getNode(i) }
   }
 
-  Expr getARead(Definition def) { result = Cached::getARead(def) }
-
   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 b53db9159916..b865fa2ef923 100644
--- a/shared/dataflow/codeql/dataflow/VariableCapture.qll
+++ b/shared/dataflow/codeql/dataflow/VariableCapture.qll
@@ -739,6 +739,8 @@ module Flow<
       ) and
       certain = true
     }
+
+    predicate ssaCachedStageRevRef() { SsaFlow::ssaCachedStageRevRef2() }
   }
 
   private module CaptureSsa = Ssa::Make<Location, Cfg, CaptureSsaInput>;
diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll
index 0fd5cd4d1be3..8943cedf9d54 100644
--- a/shared/ssa/codeql/ssa/Ssa.qll
+++ b/shared/ssa/codeql/ssa/Ssa.qll
@@ -60,6 +60,16 @@ signature module InputSig<LocationSig Location, TypSig BasicBlock> {
   ) {
     none()
   }
+
+  /**
+   * Reverse references to predicates that should be cached in the cached stage
+   * of the SSA construction.
+   *
+   * If `MakeSsa` and/or `DataFlowIntegration` is used, then this predicate
+   * should be instantiated with (the union of) their respective
+   * `ssaCachedStageRevRef` predicates.
+   */
+  default predicate ssaCachedStageRevRef() { any() }
 }
 
 /**
@@ -292,7 +302,8 @@ module Make<
       (ssaDefReachesEndOfBlock(_, _, _) implies any()) and
       (phiHasInputFromBlock(_, _, _) implies any()) and
       (ssaDefReachesRead(_, _, _, _) implies any()) and
-      (uncertainWriteDefinitionInput(_, _) implies any())
+      (uncertainWriteDefinitionInput(_, _) implies any()) and
+      (Input::ssaCachedStageRevRef() implies any())
     }
   }
 
@@ -1114,10 +1125,15 @@ module Make<
       predicate parameterInit(WriteDefinition def, Parameter p) {
         exists(VariableWrite write | explicitWrite(def, write) and write.isParameterInit(p))
       }
+
+      cached
+      predicate revRef() { any() }
     }
 
     additional predicate ssaDefReachesUncertainRead = Cached::ssaDefReachesUncertainRead/4;
 
+    additional predicate ssaCachedStageRevRef1 = Cached::revRef/0;
+
     final private class FinalDefinition = Definition;
 
     /** A static single assignment (SSA) definition. */
@@ -1470,19 +1486,6 @@ module Make<
       predicate hasCfgNode(BasicBlock bb, int i);
     }
 
-    /**
-     * Gets a read of SSA definition `def`.
-     *
-     * Override this with a cached version when applicable.
-     */
-    default Expr getARead(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)
-      )
-    }
-
     /**
      * 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.
@@ -1581,6 +1584,12 @@ module Make<
       }
     }
 
+    /** Reverse references to the cached predicates in this module. */
+    predicate ssaCachedStageRevRef2() {
+      (exists(getAPhiInputDef(_, _)) implies any()) and
+      (exists(TWriteDefSource(_)) implies any())
+    }
+
     cached
     private Definition getAPhiInputDef(SsaPhiExt phi, BasicBlock bb) {
       exists(SourceVariable v, BasicBlock bbDef |
@@ -1590,6 +1599,15 @@ module Make<
       )
     }
 
+    pragma[nomagic]
+    private DfInput::Expr getARead(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)
+      )
+    }
+
     /**
      * Holds if the phi input edge from `input` to `phi` is a back edge and
      * must be kept.
@@ -1605,7 +1623,7 @@ module Make<
 
     pragma[nomagic]
     private predicate phiInputHasRead(SsaPhiExt phi, BasicBlock input) {
-      exists(DfInput::getARead(getAPhiInputDef(phi, input)))
+      exists(getARead(getAPhiInputDef(phi, input)))
     }
 
     /** Holds if `bb` is the target end of a branch edge of a guard and the guard controls `bb`. */
@@ -1751,12 +1769,12 @@ module Make<
           // 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.
-          DfInput::getARead(_) = e
+          getARead(_) = e
           or
           not postUpdate(_, _, _) and
           variableRead(bb, i, v, true) and
           isPost = true and
-          DfInput::getARead(_) = e
+          getARead(_) = e
           or
           postUpdate(bb, i, v) and
           isPost = true
@@ -2116,13 +2134,13 @@ module Make<
         v = def.getSourceVariable() and
         if DfInput::includeWriteDefsInFlowStep()
         then nodeTo.(SsaDefinitionNode).getDefinition() = def
-        else nodeTo.(ExprNode).isExprAndVariable(DfInput::getARead(def), v)
+        else nodeTo.(ExprNode).isExprAndVariable(getARead(def), v)
       )
       or
       // Flow from SSA definition to read
       exists(DefinitionExt def |
         nodeFrom.(SsaDefinitionExtNodeImpl).getDefExt() = def and
-        nodeTo.(ExprNode).isExprAndVariable(DfInput::getARead(def), v) and
+        nodeTo.(ExprNode).isExprAndVariable(getARead(def), v) and
         v = def.getSourceVariable()
       )
     }
@@ -2200,7 +2218,7 @@ module Make<
       private predicate guardChecksSsaDef(
         DfInput::Guard g, Definition def, DfInput::GuardValue val, State state
       ) {
-        guardChecks(g, DfInput::getARead(def), val, state)
+        guardChecks(g, getARead(def), val, state)
       }
 
       private module Barrier = BarrierGuardDefWithState<State, guardChecksSsaDef/4>;
@@ -2225,7 +2243,7 @@ module Make<
         |
           // guard controls a read
           exists(DfInput::Expr e |
-            e = DfInput::getARead(def) and
+            e = getARead(def) and
             e.hasCfgNode(bb, _) and
             DfInput::guardControlsBlock(g, bb, val) and
             result.(ExprNode).isExprAndVariable(e, def.getSourceVariable())
diff --git a/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll b/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll
index 705ea43fdfdb..532ff80a8a2c 100644
--- a/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll
+++ b/unified/ql/lib/codeql/unified/internal/dataflow/LocalSsa.qll
@@ -37,6 +37,8 @@ module LocalSsaInput implements InputSig<Location, BasicBlock> {
       performsVariableAccess(repr, v, TPostUpdate(), bb2.getNode(i2))
     )
   }
+
+  predicate ssaCachedStageRevRef() { LocalSsaDataFlowOutput::ssaCachedStageRevRef2() }
 }
 
 module LocalSsaOutput = Make<Location, Cfg, LocalSsaInput>;