@@ -550,11 +550,14 @@ class SsaPhiNode extends Node, TSsaPhiNode {
    * `fromBackEdge` is true if data flows along a back-edge,
    * and `false` otherwise.
    */
+  cached
   final Node getAnInput(boolean fromBackEdge) {
     localFlowStep(result, this) and
-    if phi.getBasicBlock().dominates(result.getBasicBlock())
-    then fromBackEdge = true
-    else fromBackEdge = false
+    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. */
 
@@ -87,6 +87,30 @@ module ProductFlow {
      * dataflow graph.
      */
     default predicate isBarrierIn2(DataFlow::Node node) { none() }
+
+    /**
+     * Gets the virtual dispatch branching limit when calculating field flow in the first
+     * projection of the product dataflow graph.
+     *
+     * This can be overridden to a smaller value to improve performance (a
+     * value of 0 disables field flow), or a larger value to get more results.
+     */
+    default int fieldFlowBranchLimit1() {
+      // NOTE: This should be synchronized with the default value in the shared dataflow library
+      result = 2
+    }
+
+    /**
+     * Gets the virtual dispatch branching limit when calculating field flow in the second
+     * projection of the product dataflow graph.
+     *
+     * This can be overridden to a smaller value to improve performance (a
+     * value of 0 disables field flow), or a larger value to get more results.
+     */
+    default int fieldFlowBranchLimit2() {
+      // NOTE: This should be synchronized with the default value in the shared dataflow library
+      result = 2
+    }
   }
 
   /**
@@ -272,6 +296,30 @@ module ProductFlow {
      * dataflow graph.
      */
     default predicate isBarrierIn2(DataFlow::Node node) { none() }
+
+    /**
+     * Gets the virtual dispatch branching limit when calculating field flow in the first
+     * projection of the product dataflow graph.
+     *
+     * This can be overridden to a smaller value to improve performance (a
+     * value of 0 disables field flow), or a larger value to get more results.
+     */
+    default int fieldFlowBranchLimit1() {
+      // NOTE: This should be synchronized with the default value in the shared dataflow library
+      result = 2
+    }
+
+    /**
+     * Gets the virtual dispatch branching limit when calculating field flow in the second
+     * projection of the product dataflow graph.
+     *
+     * This can be overridden to a smaller value to improve performance (a
+     * value of 0 disables field flow), or a larger value to get more results.
+     */
+    default int fieldFlowBranchLimit2() {
+      // NOTE: This should be synchronized with the default value in the shared dataflow library
+      result = 2
+    }
   }
 
   /**
@@ -335,6 +383,8 @@ module ProductFlow {
       }
 
       predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) }
+
+      int fieldFlowBranchLimit() { result = Config::fieldFlowBranchLimit1() }
     }
 
     private module Flow1 = DataFlow::GlobalWithState<Config1>;
@@ -367,6 +417,8 @@ module ProductFlow {
       }
 
       predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) }
+
+      int fieldFlowBranchLimit() { result = Config::fieldFlowBranchLimit2() }
     }
 
     private module Flow2 = DataFlow::GlobalWithState<Config2>;
 
@@ -1,6 +1,6 @@
 /**
- * This file contains the range-analysis specific parts of the `cpp/invalid-pointer-deref` query
- * that is used by both `AllocationToInvalidPointer.qll` and `InvalidPointerToDereference.qll`.
+ * This file contains the range-analysis specific parts of the `cpp/invalid-pointer-deref`
+ * and `cpp/overrun-write` query.
  */
 
 private import cpp
 
@@ -39,6 +39,7 @@ predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
  * Holds if `guard` directly controls the position `controlled` with the
  * value `testIsTrue`.
  */
+pragma[nomagic]
 predicate semGuardDirectlyControlsSsaRead(
   SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue
 ) {
 
@@ -17,17 +17,25 @@ private import RangeUtils
 private import RangeAnalysisStage
 
 module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
+  pragma[nomagic]
+  private predicate valueFlowStepSsaEqFlowCond(
+    SemSsaReadPosition pos, SemSsaVariable v, SemExpr e, int delta
+  ) {
+    exists(SemGuard guard, boolean testIsTrue |
+      guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
+      semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue)
+    )
+  }
+
   /**
    * Holds if `e + delta` equals `v` at `pos`.
    */
+  pragma[nomagic]
   private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta) {
     U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
     or
-    exists(SemGuard guard, boolean testIsTrue |
-      pos.hasReadOfVar(v) and
-      guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
-      semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue)
-    )
+    pos.hasReadOfVar(v) and
+    valueFlowStepSsaEqFlowCond(pos, v, e, delta)
   }
 
   /**
 
@@ -660,7 +660,7 @@ module RangeStage<
    * - `upper = false` : `v >= b + delta`
    */
   private predicate boundedSsa(
-    SemSsaVariable v, SemSsaReadPosition pos, SemBound b, D::Delta delta, boolean upper,
+    SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, boolean upper,
     boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
     exists(SemExpr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
@@ -673,10 +673,13 @@ module RangeStage<
     )
     or
     exists(D::Delta d, SemReason r1, SemReason r2 |
-      boundedSsa(v, pos, b, d, upper, fromBackEdge, origdelta, r2) or
-      boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
+      boundedSsa(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
+        pragma[only_bind_into](pos), upper, fromBackEdge, origdelta, r2)
+      or
+      boundedPhi(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
+        upper, fromBackEdge, origdelta, r2)
     |
-      unequalIntegralSsa(v, pos, b, d, r1) and
+      unequalIntegralSsa(v, b, d, pos, r1) and
       (
         upper = true and delta = D::fromFloat(D::toFloat(d) - 1)
         or
@@ -694,7 +697,7 @@ module RangeStage<
    * Holds if `v != b + delta` at `pos` and `v` is of integral type.
    */
   private predicate unequalIntegralSsa(
-    SemSsaVariable v, SemSsaReadPosition pos, SemBound b, D::Delta delta, SemReason reason
+    SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, SemReason reason
   ) {
     exists(SemExpr e, D::Delta d1, D::Delta d2 |
       unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
@@ -746,7 +749,7 @@ module RangeStage<
   ) {
     edge.phiInput(phi, inp) and
     exists(D::Delta d, boolean fromBackEdge0 |
-      boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
+      boundedSsa(inp, b, d, edge, upper, fromBackEdge0, origdelta, reason)
       or
       boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
       or
@@ -1022,7 +1025,7 @@ module RangeStage<
       reason = TSemNoReason()
       or
       exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
-        boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
+        boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
         e = v.getAUse() and
         bb.getBlock() = e.getBasicBlock()
       )
 
@@ -49,6 +49,7 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
    * - `isEq = true`  : `v == e + delta`
    * - `isEq = false` : `v != e + delta`
    */
+  pragma[nomagic]
   SemGuard semEqFlowCond(
     SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
   ) {
 
@@ -56,7 +56,7 @@ private import semmle.code.cpp.ir.dataflow.internal.ProductFlow
 private import semmle.code.cpp.ir.ValueNumbering
 private import semmle.code.cpp.controlflow.IRGuards
 private import codeql.util.Unit
-private import RangeAnalysisUtil
+private import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
 
 private VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
 
@@ -77,6 +77,15 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
   )
 }
 
+/**
+ * Gets the virtual dispatch branching limit when calculating field flow while searching
+ * for flow from an allocation to the construction of an out-of-bounds pointer.
+ *
+ * This can be overridden to a smaller value to improve performance (a
+ * value of 0 disables field flow), or a larger value to get more results.
+ */
+int allocationToInvalidPointerFieldFlowBranchLimit() { result = 0 }
+
 /**
  * A module that encapsulates a barrier guard to remove false positives from flow like:
  * ```cpp
@@ -101,9 +110,12 @@ private module SizeBarrier {
     predicate isSource(DataFlow::Node source) {
       // The sources is the same as in the sources for the second
       // projection in the `AllocToInvalidPointerConfig` module.
-      hasSize(_, source, _)
+      hasSize(_, source, _) and
+      InterestingPointerAddInstruction::isInterestingSize(source)
     }
 
+    int fieldFlowBranchLimit() { result = allocationToInvalidPointerFieldFlowBranchLimit() }
+
     /**
      * Holds if `small <= large + k` holds if `g` evaluates to `testIsTrue`.
      */
@@ -201,6 +213,8 @@ private module InterestingPointerAddInstruction {
       hasSize(source.asConvertedExpr(), _, _)
     }
 
+    int fieldFlowBranchLimit() { result = allocationToInvalidPointerFieldFlowBranchLimit() }
+
     predicate isSink(DataFlow::Node sink) {
       sink.asInstruction() = any(PointerAddInstruction pai).getLeft()
     }
@@ -220,6 +234,19 @@ private module InterestingPointerAddInstruction {
       flowTo(n)
     )
   }
+
+  /**
+   * Holds if `n` is a size of an allocation whose result flows to the left operand
+   * of a pointer-arithmetic instruction.
+   *
+   * This predicate is used to reduce the set of tuples in `SizeBarrierConfig::isSource`.
+   */
+  predicate isInterestingSize(DataFlow::Node n) {
+    exists(DataFlow::Node alloc |
+      hasSize(alloc.asConvertedExpr(), n, _) and
+      flow(alloc, _)
+    )
+  }
 }
 
 /**
@@ -244,6 +271,10 @@ private module Config implements ProductFlow::StateConfigSig {
     hasSize(allocSource.asConvertedExpr(), sizeSource, sizeAddend)
   }
 
+  int fieldFlowBranchLimit1() { result = allocationToInvalidPointerFieldFlowBranchLimit() }
+
+  int fieldFlowBranchLimit2() { result = allocationToInvalidPointerFieldFlowBranchLimit() }
+
   predicate isSinkPair(
     DataFlow::Node allocSink, FlowState1 unit, DataFlow::Node sizeSink, FlowState2 sizeAddend
   ) {
 
@@ -81,7 +81,17 @@ private import semmle.code.cpp.dataflow.new.DataFlow
 private import semmle.code.cpp.ir.ValueNumbering
 private import semmle.code.cpp.controlflow.IRGuards
 private import AllocationToInvalidPointer as AllocToInvalidPointer
-private import RangeAnalysisUtil
+private import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
+
+/**
+ * Gets the virtual dispatch branching limit when calculating field flow while
+ * searching for flow from an out-of-bounds pointer to a dereference of the
+ * pointer.
+ *
+ * This can be overridden to a smaller value to improve performance (a
+ * value of 0 disables field flow), or a larger value to get more results.
+ */
+int invalidPointerToDereferenceFieldFlowBranchLimit() { result = 0 }
 
 private module InvalidPointerToDerefBarrier {
   private module BarrierConfig implements DataFlow::ConfigSig {
@@ -101,6 +111,8 @@ private module InvalidPointerToDerefBarrier {
     }
 
     predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
+
+    int fieldFlowBranchLimit() { result = invalidPointerToDereferenceFieldFlowBranchLimit() }
   }
 
   private module BarrierFlow = DataFlow::Global<BarrierConfig>;
@@ -178,6 +190,8 @@ private module InvalidPointerToDerefConfig implements DataFlow::StateConfigSig {
     // Note that this is the only place where the `FlowState` is used in this configuration.
     node = InvalidPointerToDerefBarrier::getABarrierNode(pai)
   }
+
+  int fieldFlowBranchLimit() { result = invalidPointerToDereferenceFieldFlowBranchLimit() }
 }
 
 private import DataFlow::GlobalWithState<InvalidPointerToDerefConfig>
 
@@ -20,28 +20,10 @@ import semmle.code.cpp.models.interfaces.Allocation
 import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
+import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
 import StringSizeFlow::PathGraph1
 import codeql.util.Unit
 
-pragma[nomagic]
-Instruction getABoundIn(SemBound b, IRFunction func) {
-  getSemanticExpr(result) = b.getExpr(0) and
-  result.getEnclosingIRFunction() = func
-}
-
-/**
- * Holds if `i <= b + delta`.
- */
-bindingset[i]
-pragma[inline_late]
-predicate bounded(Instruction i, Instruction b, int delta) {
-  exists(SemBound bound, IRFunction func |
-    semBounded(getSemanticExpr(i), bound, delta, true, _) and
-    b = getABoundIn(bound, func) and
-    i.getEnclosingIRFunction() = func
-  )
-}
-
 VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
 
 /**