Merge tag 'codeql-cli/latest'

Compatible with the latest released version of the CodeQL CLI
2025-12-23 12:16:33 +01:00 · 2023-07-13 18:33:38 +00:00
parent acda5fd88b 1af60aa9d4
commit d3e36cb49e
1713 changed files with 48043 additions and 21796 deletions
--- a/cpp/ql/lib/semmle/code/cpp/File.qll
+++ b/cpp/ql/lib/semmle/code/cpp/File.qll
@@ -34,14 +34,6 @@ class Container extends Locatable, @container {
   */
  string getAbsolutePath() { none() } // overridden by subclasses

-  /**
-   * DEPRECATED: Use `getLocation` instead.
-   * Gets a URL representing the location of this container.
-   *
-   * For more information see [Providing URLs](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/#providing-urls).
-   */
-  deprecated string getURL() { none() } // overridden by subclasses
-
  /**
   * Gets the relative path of this file or folder from the root folder of the
   * analyzed source location. The relative path of the root folder itself is
@@ -183,12 +175,6 @@ class Folder extends Container, @folder {
  }

  override string getAPrimaryQlClass() { result = "Folder" }
-
-  /**
-   * DEPRECATED: Use `getLocation` instead.
-   * Gets the URL of this folder.
-   */
-  deprecated override string getURL() { result = "file://" + this.getAbsolutePath() + ":0:0:0:0" }
 }

 /**
@@ -213,12 +199,6 @@ class File extends Container, @file {
    result.hasLocationInfo(_, 0, 0, 0, 0)
  }

-  /**
-   * DEPRECATED: Use `getLocation` instead.
-   * Gets the URL of this file.
-   */
-  deprecated override string getURL() { result = "file://" + this.getAbsolutePath() + ":0:0:0:0" }
-
  /** Holds if this file was compiled as C (at any point). */
  predicate compiledAsC() { fileannotations(underlyingElement(this), 1, "compiled as c", "1") }

--- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll
@@ -460,7 +460,6 @@ module Impl<FullStateConfigSig Config> {
     * The Boolean `cc` records whether the node is reached through an
     * argument in a call.
     */
-    pragma[assume_small_delta]
    private predicate fwdFlow(NodeEx node, Cc cc) {
      sourceNode(node, _) and
      if hasSourceCallCtx() then cc = true else cc = false
@@ -570,7 +569,6 @@ module Impl<FullStateConfigSig Config> {
    /**
     * Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
     */
-    pragma[assume_small_delta]
    pragma[nomagic]
    private predicate fwdFlowConsCand(Content c) {
      exists(NodeEx mid, NodeEx node |
@@ -1135,8 +1133,8 @@ module Impl<FullStateConfigSig Config> {
        DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow
      );

-      bindingset[node, state, t, ap]
-      predicate filter(NodeEx node, FlowState state, Typ t, Ap ap);
+      bindingset[node, state, t0, ap]
+      predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t);

      bindingset[typ, contentType]
      predicate typecheckStore(Typ typ, DataFlowType contentType);
@@ -1199,20 +1197,23 @@ module Impl<FullStateConfigSig Config> {
        NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
        ApOption argAp, Typ t, Ap ap, ApApprox apa
      ) {
-        fwdFlow0(node, state, cc, summaryCtx, argT, argAp, t, ap, apa) and
-        PrevStage::revFlow(node, state, apa) and
-        filter(node, state, t, ap)
+        fwdFlow1(node, state, cc, summaryCtx, argT, argAp, _, t, ap, apa)
      }

-      pragma[inline]
-      additional predicate fwdFlow(
+      private predicate fwdFlow1(
        NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
-        ApOption argAp, Typ t, Ap ap
+        ApOption argAp, Typ t0, Typ t, Ap ap, ApApprox apa
      ) {
-        fwdFlow(node, state, cc, summaryCtx, argT, argAp, t, ap, _)
+        fwdFlow0(node, state, cc, summaryCtx, argT, argAp, t0, ap, apa) and
+        PrevStage::revFlow(node, state, apa) and
+        filter(node, state, t0, ap, t)
+      }
+
+      pragma[nomagic]
+      private predicate typeStrengthen(Typ t0, Ap ap, Typ t) {
+        fwdFlow1(_, _, _, _, _, _, t0, t, ap, _) and t0 != t
      }

-      pragma[assume_small_delta]
      pragma[nomagic]
      private predicate fwdFlow0(
        NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
@@ -1339,6 +1340,11 @@ module Impl<FullStateConfigSig Config> {
      private predicate fwdFlowConsCand(Typ t2, Ap cons, Content c, Typ t1, Ap tail) {
        fwdFlowStore(_, t1, tail, c, t2, _, _, _, _, _, _) and
        cons = apCons(c, t1, tail)
+        or
+        exists(Typ t0 |
+          typeStrengthen(t0, cons, t2) and
+          fwdFlowConsCand(t0, cons, c, t1, tail)
+        )
      }

      pragma[nomagic]
@@ -1359,7 +1365,7 @@ module Impl<FullStateConfigSig Config> {
        ParamNodeOption summaryCtx, TypOption argT, ApOption argAp
      ) {
        exists(ApHeadContent apc |
-          fwdFlow(node1, state, cc, summaryCtx, argT, argAp, t, ap) and
+          fwdFlow(node1, state, cc, summaryCtx, argT, argAp, t, ap, _) and
          apc = getHeadContent(ap) and
          readStepCand0(node1, apc, c, node2)
        )
@@ -1520,14 +1526,14 @@ module Impl<FullStateConfigSig Config> {
        NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap
      ) {
        revFlow0(node, state, returnCtx, returnAp, ap) and
-        fwdFlow(node, state, _, _, _, _, _, ap)
+        fwdFlow(node, state, _, _, _, _, _, ap, _)
      }

      pragma[nomagic]
      private predicate revFlow0(
        NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap
      ) {
-        fwdFlow(node, state, _, _, _, _, _, ap) and
+        fwdFlow(node, state, _, _, _, _, _, ap, _) and
        sinkNode(node, state) and
        (
          if hasSinkCallCtx()
@@ -1780,13 +1786,13 @@ module Impl<FullStateConfigSig Config> {
        boolean fwd, int nodes, int fields, int conscand, int states, int tuples
      ) {
        fwd = true and
-        nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _, _)) and
+        nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _, _, _)) and
        fields = count(Content f0 | fwdConsCand(f0, _, _)) and
        conscand = count(Content f0, Typ t, Ap ap | fwdConsCand(f0, t, ap)) and
-        states = count(FlowState state | fwdFlow(_, state, _, _, _, _, _, _)) and
+        states = count(FlowState state | fwdFlow(_, state, _, _, _, _, _, _, _)) and
        tuples =
          count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
-            ApOption argAp, Typ t, Ap ap | fwdFlow(n, state, cc, summaryCtx, argT, argAp, t, ap))
+            ApOption argAp, Typ t, Ap ap | fwdFlow(n, state, cc, summaryCtx, argT, argAp, t, ap, _))
        or
        fwd = false and
        nodes = count(NodeEx node | revFlow(node, _, _, _, _)) and
@@ -1963,10 +1969,10 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
      PrevStage::revFlowState(state) and
-      exists(t) and
+      t0 = t and
      exists(ap) and
      not stateBarrier(node, state) and
      (
@@ -2012,7 +2018,8 @@ module Impl<FullStateConfigSig Config> {
      FlowCheckNode() {
        castNode(this.asNode()) or
        clearsContentCached(this.asNode(), _) or
-        expectsContentCached(this.asNode(), _)
+        expectsContentCached(this.asNode(), _) or
+        neverSkipInPathGraph(this.asNode())
      }
    }

@@ -2197,8 +2204,8 @@ module Impl<FullStateConfigSig Config> {
    import BooleanCallContext

    predicate localStep(
-      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-      DataFlowType t, LocalCc lcc
+      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, Typ t,
+      LocalCc lcc
    ) {
      localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _) and
      exists(lcc)
@@ -2218,10 +2225,16 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
      exists(state) and
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      // We can get away with not using type strengthening here, since we aren't
+      // going to use the tracked types in the construction of Stage 4 access
+      // paths. For Stage 4 and onwards, the tracked types must be consistent as
+      // the cons candidates including types are used to construct subsequent
+      // access path approximations.
+      t0 = t and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t0) else any()) and
      (
        notExpectsContent(node)
        or
@@ -2241,6 +2254,16 @@ module Impl<FullStateConfigSig Config> {
    import MkStage<Stage2>::Stage<Stage3Param>
  }

+  bindingset[node, t0]
+  private predicate strengthenType(NodeEx node, DataFlowType t0, DataFlowType t) {
+    if castingNodeEx(node)
+    then
+      exists(DataFlowType nt | nt = node.getDataFlowType() |
+        if typeStrongerThan(nt, t0) then t = nt else (compatibleTypes(nt, t0) and t = t0)
+      )
+    else t = t0
+  }
+
  private module Stage4Param implements MkStage<Stage3>::StageParam {
    private module PrevStage = Stage3;

@@ -2274,8 +2297,8 @@ module Impl<FullStateConfigSig Config> {

    pragma[nomagic]
    predicate localStep(
-      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-      DataFlowType t, LocalCc lcc
+      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, Typ t,
+      LocalCc lcc
    ) {
      localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _) and
      PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
@@ -2333,11 +2356,11 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
      exists(state) and
      not clear(node, ap) and
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      strengthenType(node, t0, t) and
      (
        notExpectsContent(node)
        or
@@ -2365,7 +2388,7 @@ module Impl<FullStateConfigSig Config> {
    exists(AccessPathFront apf |
      Stage4::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf) and
      Stage4::fwdFlow(node, state, any(Stage4::CcCall ccc), _, _, TAccessPathFrontSome(argApf), _,
-        apf)
+        apf, _)
    )
  }

@@ -2579,8 +2602,8 @@ module Impl<FullStateConfigSig Config> {
    import LocalCallContext

    predicate localStep(
-      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-      DataFlowType t, LocalCc lcc
+      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, Typ t,
+      LocalCc lcc
    ) {
      localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc) and
      PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
@@ -2609,9 +2632,9 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
+      strengthenType(node, t0, t) and
      exists(state) and
      exists(ap)
    }
@@ -2632,7 +2655,7 @@ module Impl<FullStateConfigSig Config> {
      Stage5::parameterMayFlowThrough(p, _) and
      Stage5::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0) and
      Stage5::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()), _,
-        TAccessPathApproxSome(apa), _, apa0)
+        TAccessPathApproxSome(apa), _, apa0, _)
    )
  }

@@ -2649,7 +2672,7 @@ module Impl<FullStateConfigSig Config> {
    TSummaryCtxSome(ParamNodeEx p, FlowState state, DataFlowType t, AccessPath ap) {
      exists(AccessPathApprox apa | ap.getApprox() = apa |
        Stage5::parameterMayFlowThrough(p, apa) and
-        Stage5::fwdFlow(p, state, _, _, _, _, t, apa) and
+        Stage5::fwdFlow(p, state, _, _, Option<DataFlowType>::some(t), _, _, apa, _) and
        Stage5::revFlow(p, state, _)
      )
    }
@@ -2751,7 +2774,6 @@ module Impl<FullStateConfigSig Config> {
  /**
   * Gets the number of `AccessPath`s that correspond to `apa`.
   */
-  pragma[assume_small_delta]
  private int countAps(AccessPathApprox apa) {
    evalUnfold(apa, false) and
    result = 1 and
@@ -2770,7 +2792,6 @@ module Impl<FullStateConfigSig Config> {
   * that it is expanded to a precise head-tail representation.
   */
  language[monotonicAggregates]
-  pragma[assume_small_delta]
  private int countPotentialAps(AccessPathApprox apa) {
    apa instanceof AccessPathApproxNil and result = 1
    or
@@ -2807,7 +2828,6 @@ module Impl<FullStateConfigSig Config> {
    }

  private newtype TPathNode =
-    pragma[assume_small_delta]
    TPathNodeMid(
      NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t, AccessPath ap
    ) {
@@ -2820,9 +2840,7 @@ module Impl<FullStateConfigSig Config> {
      ap = TAccessPathNil()
      or
      // ... or a step from an existing PathNode to another node.
-      pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox()) and
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
+      pathStep(_, node, state, cc, sc, t, ap)
    } or
    TPathNodeSink(NodeEx node, FlowState state) {
      exists(PathNodeMid sink |
@@ -2894,7 +2912,6 @@ module Impl<FullStateConfigSig Config> {

    override AccessPathFrontHead getFront() { result = TFrontHead(head_) }

-    pragma[assume_small_delta]
    override AccessPathApproxCons getApprox() {
      result = TConsNil(head_, t) and tail_ = TAccessPathNil()
      or
@@ -2903,7 +2920,6 @@ module Impl<FullStateConfigSig Config> {
      result = TCons1(head_, this.length())
    }

-    pragma[assume_small_delta]
    override int length() { result = 1 + tail_.length() }

    private string toStringImpl(boolean needsSuffix) {
@@ -3340,13 +3356,23 @@ module Impl<FullStateConfigSig Config> {
    ap = mid.getAp()
  }

+  private predicate pathStep(
+    PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t,
+    AccessPath ap
+  ) {
+    exists(DataFlowType t0 |
+      pathStep0(mid, node, state, cc, sc, t0, ap) and
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      strengthenType(node, t0, t)
+    )
+  }
+
  /**
   * Holds if data may flow from `mid` to `node`. The last step in or out of
   * a callable is recorded by `cc`.
   */
-  pragma[assume_small_delta]
  pragma[nomagic]
-  private predicate pathStep(
+  private predicate pathStep0(
    PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t,
    AccessPath ap
  ) {
@@ -3557,7 +3583,6 @@ module Impl<FullStateConfigSig Config> {
    )
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  private predicate pathThroughCallable0(
    DataFlowCall call, PathNodeMid mid, ReturnKindExt kind, FlowState state, CallContext cc,
@@ -3964,7 +3989,7 @@ module Impl<FullStateConfigSig Config> {
        ap = TPartialNil() and
        exists(explorationLimit())
        or
-        partialPathNodeMk0(node, state, cc, sc1, sc2, sc3, sc4, t, ap) and
+        partialPathStep(_, node, state, cc, sc1, sc2, sc3, sc4, t, ap) and
        distSrc(node.getEnclosingCallable()) <= explorationLimit()
      } or
      TPartialPathNodeRev(
@@ -3990,11 +4015,20 @@ module Impl<FullStateConfigSig Config> {
      }

    pragma[nomagic]
-    private predicate partialPathNodeMk0(
-      NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1, TSummaryCtx2 sc2,
-      TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
+    private predicate partialPathStep(
+      PartialPathNodeFwd mid, NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1,
+      TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
    ) {
-      partialPathStep(_, node, state, cc, sc1, sc2, sc3, sc4, t, ap) and
+      partialPathStep1(mid, node, state, cc, sc1, sc2, sc3, sc4, _, t, ap)
+    }
+
+    pragma[nomagic]
+    private predicate partialPathStep1(
+      PartialPathNodeFwd mid, NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1,
+      TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t0, DataFlowType t,
+      PartialAccessPath ap
+    ) {
+      partialPathStep0(mid, node, state, cc, sc1, sc2, sc3, sc4, t0, ap) and
      not fullBarrier(node) and
      not stateBarrier(node, state) and
      not clearsContentEx(node, ap.getHead()) and
@@ -4002,9 +4036,14 @@ module Impl<FullStateConfigSig Config> {
        notExpectsContent(node) or
        expectsContentEx(node, ap.getHead())
      ) and
-      if node.asNode() instanceof CastingNode
-      then compatibleTypes(node.getDataFlowType(), t)
-      else any()
+      strengthenType(node, t0, t)
+    }
+
+    pragma[nomagic]
+    private predicate partialPathTypeStrengthen(
+      DataFlowType t0, PartialAccessPath ap, DataFlowType t
+    ) {
+      partialPathStep1(_, _, _, _, _, _, _, _, t0, t, ap) and t0 != t
    }

    /**
@@ -4183,7 +4222,8 @@ module Impl<FullStateConfigSig Config> {
      }
    }

-    private predicate partialPathStep(
+    pragma[nomagic]
+    private predicate partialPathStep0(
      PartialPathNodeFwd mid, NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1,
      TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
    ) {
@@ -4309,6 +4349,11 @@ module Impl<FullStateConfigSig Config> {
      DataFlowType t1, PartialAccessPath ap1, Content c, DataFlowType t2, PartialAccessPath ap2
    ) {
      partialPathStoreStep(_, t1, ap1, c, _, t2, ap2)
+      or
+      exists(DataFlowType t0 |
+        partialPathTypeStrengthen(t0, ap2, t2) and
+        apConsFwd(t1, ap1, c, t0, ap2)
+      )
    }

    pragma[nomagic]
--- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplCommon.qll
@@ -187,7 +187,6 @@ private module LambdaFlow {
    else any()
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  predicate revLambdaFlow0(
    DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
@@ -274,7 +273,6 @@ private module LambdaFlow {
    )
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  predicate revLambdaFlowOut(
    DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
--- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowPrivate.qll
+++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowPrivate.qll
@@ -205,6 +205,8 @@ predicate clearsContent(Node n, Content c) {
 */
 predicate expectsContent(Node n, ContentSet c) { none() }

+predicate typeStrongerThan(DataFlowType t1, DataFlowType t2) { none() }
+
 /** Gets the type of `n` used for type pruning. */
 Type getNodeType(Node n) {
  suppressUnusedNode(n) and
@@ -233,6 +235,12 @@ class CastNode extends Node {
  CastNode() { none() } // stub implementation
 }

+/**
+ * Holds if `n` should never be skipped over in the `PathGraph` and in path
+ * explanations.
+ */
+predicate neverSkipInPathGraph(Node n) { none() }
+
 class DataFlowCallable = Function;

 class DataFlowExpr = Expr;
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll
@@ -460,7 +460,6 @@ module Impl<FullStateConfigSig Config> {
     * The Boolean `cc` records whether the node is reached through an
     * argument in a call.
     */
-    pragma[assume_small_delta]
    private predicate fwdFlow(NodeEx node, Cc cc) {
      sourceNode(node, _) and
      if hasSourceCallCtx() then cc = true else cc = false
@@ -570,7 +569,6 @@ module Impl<FullStateConfigSig Config> {
    /**
     * Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
     */
-    pragma[assume_small_delta]
    pragma[nomagic]
    private predicate fwdFlowConsCand(Content c) {
      exists(NodeEx mid, NodeEx node |
@@ -1135,8 +1133,8 @@ module Impl<FullStateConfigSig Config> {
        DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow
      );

-      bindingset[node, state, t, ap]
-      predicate filter(NodeEx node, FlowState state, Typ t, Ap ap);
+      bindingset[node, state, t0, ap]
+      predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t);

      bindingset[typ, contentType]
      predicate typecheckStore(Typ typ, DataFlowType contentType);
@@ -1199,20 +1197,23 @@ module Impl<FullStateConfigSig Config> {
        NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
        ApOption argAp, Typ t, Ap ap, ApApprox apa
      ) {
-        fwdFlow0(node, state, cc, summaryCtx, argT, argAp, t, ap, apa) and
-        PrevStage::revFlow(node, state, apa) and
-        filter(node, state, t, ap)
+        fwdFlow1(node, state, cc, summaryCtx, argT, argAp, _, t, ap, apa)
      }

-      pragma[inline]
-      additional predicate fwdFlow(
+      private predicate fwdFlow1(
        NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
-        ApOption argAp, Typ t, Ap ap
+        ApOption argAp, Typ t0, Typ t, Ap ap, ApApprox apa
      ) {
-        fwdFlow(node, state, cc, summaryCtx, argT, argAp, t, ap, _)
+        fwdFlow0(node, state, cc, summaryCtx, argT, argAp, t0, ap, apa) and
+        PrevStage::revFlow(node, state, apa) and
+        filter(node, state, t0, ap, t)
+      }
+
+      pragma[nomagic]
+      private predicate typeStrengthen(Typ t0, Ap ap, Typ t) {
+        fwdFlow1(_, _, _, _, _, _, t0, t, ap, _) and t0 != t
      }

-      pragma[assume_small_delta]
      pragma[nomagic]
      private predicate fwdFlow0(
        NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
@@ -1339,6 +1340,11 @@ module Impl<FullStateConfigSig Config> {
      private predicate fwdFlowConsCand(Typ t2, Ap cons, Content c, Typ t1, Ap tail) {
        fwdFlowStore(_, t1, tail, c, t2, _, _, _, _, _, _) and
        cons = apCons(c, t1, tail)
+        or
+        exists(Typ t0 |
+          typeStrengthen(t0, cons, t2) and
+          fwdFlowConsCand(t0, cons, c, t1, tail)
+        )
      }

      pragma[nomagic]
@@ -1359,7 +1365,7 @@ module Impl<FullStateConfigSig Config> {
        ParamNodeOption summaryCtx, TypOption argT, ApOption argAp
      ) {
        exists(ApHeadContent apc |
-          fwdFlow(node1, state, cc, summaryCtx, argT, argAp, t, ap) and
+          fwdFlow(node1, state, cc, summaryCtx, argT, argAp, t, ap, _) and
          apc = getHeadContent(ap) and
          readStepCand0(node1, apc, c, node2)
        )
@@ -1520,14 +1526,14 @@ module Impl<FullStateConfigSig Config> {
        NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap
      ) {
        revFlow0(node, state, returnCtx, returnAp, ap) and
-        fwdFlow(node, state, _, _, _, _, _, ap)
+        fwdFlow(node, state, _, _, _, _, _, ap, _)
      }

      pragma[nomagic]
      private predicate revFlow0(
        NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap
      ) {
-        fwdFlow(node, state, _, _, _, _, _, ap) and
+        fwdFlow(node, state, _, _, _, _, _, ap, _) and
        sinkNode(node, state) and
        (
          if hasSinkCallCtx()
@@ -1780,13 +1786,13 @@ module Impl<FullStateConfigSig Config> {
        boolean fwd, int nodes, int fields, int conscand, int states, int tuples
      ) {
        fwd = true and
-        nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _, _)) and
+        nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _, _, _)) and
        fields = count(Content f0 | fwdConsCand(f0, _, _)) and
        conscand = count(Content f0, Typ t, Ap ap | fwdConsCand(f0, t, ap)) and
-        states = count(FlowState state | fwdFlow(_, state, _, _, _, _, _, _)) and
+        states = count(FlowState state | fwdFlow(_, state, _, _, _, _, _, _, _)) and
        tuples =
          count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
-            ApOption argAp, Typ t, Ap ap | fwdFlow(n, state, cc, summaryCtx, argT, argAp, t, ap))
+            ApOption argAp, Typ t, Ap ap | fwdFlow(n, state, cc, summaryCtx, argT, argAp, t, ap, _))
        or
        fwd = false and
        nodes = count(NodeEx node | revFlow(node, _, _, _, _)) and
@@ -1963,10 +1969,10 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
      PrevStage::revFlowState(state) and
-      exists(t) and
+      t0 = t and
      exists(ap) and
      not stateBarrier(node, state) and
      (
@@ -2012,7 +2018,8 @@ module Impl<FullStateConfigSig Config> {
      FlowCheckNode() {
        castNode(this.asNode()) or
        clearsContentCached(this.asNode(), _) or
-        expectsContentCached(this.asNode(), _)
+        expectsContentCached(this.asNode(), _) or
+        neverSkipInPathGraph(this.asNode())
      }
    }

@@ -2197,8 +2204,8 @@ module Impl<FullStateConfigSig Config> {
    import BooleanCallContext

    predicate localStep(
-      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-      DataFlowType t, LocalCc lcc
+      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, Typ t,
+      LocalCc lcc
    ) {
      localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _) and
      exists(lcc)
@@ -2218,10 +2225,16 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
      exists(state) and
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      // We can get away with not using type strengthening here, since we aren't
+      // going to use the tracked types in the construction of Stage 4 access
+      // paths. For Stage 4 and onwards, the tracked types must be consistent as
+      // the cons candidates including types are used to construct subsequent
+      // access path approximations.
+      t0 = t and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t0) else any()) and
      (
        notExpectsContent(node)
        or
@@ -2241,6 +2254,16 @@ module Impl<FullStateConfigSig Config> {
    import MkStage<Stage2>::Stage<Stage3Param>
  }

+  bindingset[node, t0]
+  private predicate strengthenType(NodeEx node, DataFlowType t0, DataFlowType t) {
+    if castingNodeEx(node)
+    then
+      exists(DataFlowType nt | nt = node.getDataFlowType() |
+        if typeStrongerThan(nt, t0) then t = nt else (compatibleTypes(nt, t0) and t = t0)
+      )
+    else t = t0
+  }
+
  private module Stage4Param implements MkStage<Stage3>::StageParam {
    private module PrevStage = Stage3;

@@ -2274,8 +2297,8 @@ module Impl<FullStateConfigSig Config> {

    pragma[nomagic]
    predicate localStep(
-      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-      DataFlowType t, LocalCc lcc
+      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, Typ t,
+      LocalCc lcc
    ) {
      localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _) and
      PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
@@ -2333,11 +2356,11 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
      exists(state) and
      not clear(node, ap) and
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      strengthenType(node, t0, t) and
      (
        notExpectsContent(node)
        or
@@ -2365,7 +2388,7 @@ module Impl<FullStateConfigSig Config> {
    exists(AccessPathFront apf |
      Stage4::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf) and
      Stage4::fwdFlow(node, state, any(Stage4::CcCall ccc), _, _, TAccessPathFrontSome(argApf), _,
-        apf)
+        apf, _)
    )
  }

@@ -2579,8 +2602,8 @@ module Impl<FullStateConfigSig Config> {
    import LocalCallContext

    predicate localStep(
-      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-      DataFlowType t, LocalCc lcc
+      NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, Typ t,
+      LocalCc lcc
    ) {
      localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc) and
      PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
@@ -2609,9 +2632,9 @@ module Impl<FullStateConfigSig Config> {
      )
    }

-    bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+    bindingset[node, state, t0, ap]
+    predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
+      strengthenType(node, t0, t) and
      exists(state) and
      exists(ap)
    }
@@ -2632,7 +2655,7 @@ module Impl<FullStateConfigSig Config> {
      Stage5::parameterMayFlowThrough(p, _) and
      Stage5::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0) and
      Stage5::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()), _,
-        TAccessPathApproxSome(apa), _, apa0)
+        TAccessPathApproxSome(apa), _, apa0, _)
    )
  }

@@ -2649,7 +2672,7 @@ module Impl<FullStateConfigSig Config> {
    TSummaryCtxSome(ParamNodeEx p, FlowState state, DataFlowType t, AccessPath ap) {
      exists(AccessPathApprox apa | ap.getApprox() = apa |
        Stage5::parameterMayFlowThrough(p, apa) and
-        Stage5::fwdFlow(p, state, _, _, _, _, t, apa) and
+        Stage5::fwdFlow(p, state, _, _, Option<DataFlowType>::some(t), _, _, apa, _) and
        Stage5::revFlow(p, state, _)
      )
    }
@@ -2751,7 +2774,6 @@ module Impl<FullStateConfigSig Config> {
  /**
   * Gets the number of `AccessPath`s that correspond to `apa`.
   */
-  pragma[assume_small_delta]
  private int countAps(AccessPathApprox apa) {
    evalUnfold(apa, false) and
    result = 1 and
@@ -2770,7 +2792,6 @@ module Impl<FullStateConfigSig Config> {
   * that it is expanded to a precise head-tail representation.
   */
  language[monotonicAggregates]
-  pragma[assume_small_delta]
  private int countPotentialAps(AccessPathApprox apa) {
    apa instanceof AccessPathApproxNil and result = 1
    or
@@ -2807,7 +2828,6 @@ module Impl<FullStateConfigSig Config> {
    }

  private newtype TPathNode =
-    pragma[assume_small_delta]
    TPathNodeMid(
      NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t, AccessPath ap
    ) {
@@ -2820,9 +2840,7 @@ module Impl<FullStateConfigSig Config> {
      ap = TAccessPathNil()
      or
      // ... or a step from an existing PathNode to another node.
-      pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox()) and
-      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
+      pathStep(_, node, state, cc, sc, t, ap)
    } or
    TPathNodeSink(NodeEx node, FlowState state) {
      exists(PathNodeMid sink |
@@ -2894,7 +2912,6 @@ module Impl<FullStateConfigSig Config> {

    override AccessPathFrontHead getFront() { result = TFrontHead(head_) }

-    pragma[assume_small_delta]
    override AccessPathApproxCons getApprox() {
      result = TConsNil(head_, t) and tail_ = TAccessPathNil()
      or
@@ -2903,7 +2920,6 @@ module Impl<FullStateConfigSig Config> {
      result = TCons1(head_, this.length())
    }

-    pragma[assume_small_delta]
    override int length() { result = 1 + tail_.length() }

    private string toStringImpl(boolean needsSuffix) {
@@ -3340,13 +3356,23 @@ module Impl<FullStateConfigSig Config> {
    ap = mid.getAp()
  }

+  private predicate pathStep(
+    PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t,
+    AccessPath ap
+  ) {
+    exists(DataFlowType t0 |
+      pathStep0(mid, node, state, cc, sc, t0, ap) and
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      strengthenType(node, t0, t)
+    )
+  }
+
  /**
   * Holds if data may flow from `mid` to `node`. The last step in or out of
   * a callable is recorded by `cc`.
   */
-  pragma[assume_small_delta]
  pragma[nomagic]
-  private predicate pathStep(
+  private predicate pathStep0(
    PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t,
    AccessPath ap
  ) {
@@ -3557,7 +3583,6 @@ module Impl<FullStateConfigSig Config> {
    )
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  private predicate pathThroughCallable0(
    DataFlowCall call, PathNodeMid mid, ReturnKindExt kind, FlowState state, CallContext cc,
@@ -3964,7 +3989,7 @@ module Impl<FullStateConfigSig Config> {
        ap = TPartialNil() and
        exists(explorationLimit())
        or
-        partialPathNodeMk0(node, state, cc, sc1, sc2, sc3, sc4, t, ap) and
+        partialPathStep(_, node, state, cc, sc1, sc2, sc3, sc4, t, ap) and
        distSrc(node.getEnclosingCallable()) <= explorationLimit()
      } or
      TPartialPathNodeRev(
@@ -3990,11 +4015,20 @@ module Impl<FullStateConfigSig Config> {
      }

    pragma[nomagic]
-    private predicate partialPathNodeMk0(
-      NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1, TSummaryCtx2 sc2,
-      TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
+    private predicate partialPathStep(
+      PartialPathNodeFwd mid, NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1,
+      TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
    ) {
-      partialPathStep(_, node, state, cc, sc1, sc2, sc3, sc4, t, ap) and
+      partialPathStep1(mid, node, state, cc, sc1, sc2, sc3, sc4, _, t, ap)
+    }
+
+    pragma[nomagic]
+    private predicate partialPathStep1(
+      PartialPathNodeFwd mid, NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1,
+      TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t0, DataFlowType t,
+      PartialAccessPath ap
+    ) {
+      partialPathStep0(mid, node, state, cc, sc1, sc2, sc3, sc4, t0, ap) and
      not fullBarrier(node) and
      not stateBarrier(node, state) and
      not clearsContentEx(node, ap.getHead()) and
@@ -4002,9 +4036,14 @@ module Impl<FullStateConfigSig Config> {
        notExpectsContent(node) or
        expectsContentEx(node, ap.getHead())
      ) and
-      if node.asNode() instanceof CastingNode
-      then compatibleTypes(node.getDataFlowType(), t)
-      else any()
+      strengthenType(node, t0, t)
+    }
+
+    pragma[nomagic]
+    private predicate partialPathTypeStrengthen(
+      DataFlowType t0, PartialAccessPath ap, DataFlowType t
+    ) {
+      partialPathStep1(_, _, _, _, _, _, _, _, t0, t, ap) and t0 != t
    }

    /**
@@ -4183,7 +4222,8 @@ module Impl<FullStateConfigSig Config> {
      }
    }

-    private predicate partialPathStep(
+    pragma[nomagic]
+    private predicate partialPathStep0(
      PartialPathNodeFwd mid, NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1,
      TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
    ) {
@@ -4309,6 +4349,11 @@ module Impl<FullStateConfigSig Config> {
      DataFlowType t1, PartialAccessPath ap1, Content c, DataFlowType t2, PartialAccessPath ap2
    ) {
      partialPathStoreStep(_, t1, ap1, c, _, t2, ap2)
+      or
+      exists(DataFlowType t0 |
+        partialPathTypeStrengthen(t0, ap2, t2) and
+        apConsFwd(t1, ap1, c, t0, ap2)
+      )
    }

    pragma[nomagic]
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImplCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImplCommon.qll
@@ -187,7 +187,6 @@ private module LambdaFlow {
    else any()
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  predicate revLambdaFlow0(
    DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
@@ -274,7 +273,6 @@ private module LambdaFlow {
    )
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  predicate revLambdaFlowOut(
    DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
@@ -193,86 +193,89 @@ private class SingleUseOperandNode0 extends OperandNode0, TSingleUseOperandNode0
  SingleUseOperandNode0() { this = TSingleUseOperandNode0(op) }
 }

-/**
- * INTERNAL: Do not use.
- *
- * A node that represents the indirect value of an operand in the IR
- * after `index` number of loads.
- *
- * Note: Unlike `RawIndirectOperand`, a value of type `IndirectOperand` may
- * be an `OperandNode`.
- */
-class IndirectOperand extends Node {
-  Operand operand;
-  int indirectionIndex;
-
-  IndirectOperand() {
-    this.(RawIndirectOperand).getOperand() = operand and
-    this.(RawIndirectOperand).getIndirectionIndex() = indirectionIndex
-    or
-    nodeHasOperand(this, Ssa::getIRRepresentationOfIndirectOperand(operand, indirectionIndex),
-      indirectionIndex - 1)
+private module IndirectOperands {
+  /**
+   * INTERNAL: Do not use.
+   *
+   * A node that represents the indirect value of an operand in the IR
+   * after `index` number of loads.
+   *
+   * Note: Unlike `RawIndirectOperand`, a value of type `IndirectOperand` may
+   * be an `OperandNode`.
+   */
+  abstract class IndirectOperand extends Node {
+    /** Gets the underlying operand and the underlying indirection index. */
+    abstract predicate hasOperandAndIndirectionIndex(Operand operand, int indirectionIndex);
  }

-  /** Gets the underlying operand. */
-  Operand getOperand() { result = operand }
+  private class IndirectOperandFromRaw extends IndirectOperand instanceof RawIndirectOperand {
+    override predicate hasOperandAndIndirectionIndex(Operand operand, int indirectionIndex) {
+      operand = RawIndirectOperand.super.getOperand() and
+      indirectionIndex = RawIndirectOperand.super.getIndirectionIndex()
+    }
+  }

-  /** Gets the underlying indirection index. */
-  int getIndirectionIndex() { result = indirectionIndex }
+  private class IndirectOperandFromIRRepr extends IndirectOperand {
+    Operand operand;
+    int indirectionIndex;

-  /**
-   * Holds if this `IndirectOperand` is represented directly in the IR instead of
-   * a `RawIndirectionOperand` with operand `op` and indirection index `index`.
-   */
-  predicate isIRRepresentationOf(Operand op, int index) {
-    this instanceof OperandNode and
-    (
-      op = operand and
-      index = indirectionIndex
-    )
+    IndirectOperandFromIRRepr() {
+      exists(Operand repr |
+        repr = Ssa::getIRRepresentationOfIndirectOperand(operand, indirectionIndex) and
+        nodeHasOperand(this, repr, indirectionIndex - 1)
+      )
+    }
+
+    override predicate hasOperandAndIndirectionIndex(Operand op, int index) {
+      op = operand and index = indirectionIndex
+    }
  }
 }

-/**
- * INTERNAL: Do not use.
- *
- * A node that represents the indirect value of an instruction in the IR
- * after `index` number of loads.
- *
- * Note: Unlike `RawIndirectInstruction`, a value of type `IndirectInstruction` may
- * be an `InstructionNode`.
- */
-class IndirectInstruction extends Node {
-  Instruction instr;
-  int indirectionIndex;
+import IndirectOperands

-  IndirectInstruction() {
-    this.(RawIndirectInstruction).getInstruction() = instr and
-    this.(RawIndirectInstruction).getIndirectionIndex() = indirectionIndex
-    or
-    nodeHasInstruction(this, Ssa::getIRRepresentationOfIndirectInstruction(instr, indirectionIndex),
-      indirectionIndex - 1)
+private module IndirectInstructions {
+  /**
+   * INTERNAL: Do not use.
+   *
+   * A node that represents the indirect value of an instruction in the IR
+   * after `index` number of loads.
+   *
+   * Note: Unlike `RawIndirectInstruction`, a value of type `IndirectInstruction` may
+   * be an `InstructionNode`.
+   */
+  abstract class IndirectInstruction extends Node {
+    /** Gets the underlying operand and the underlying indirection index. */
+    abstract predicate hasInstructionAndIndirectionIndex(Instruction instr, int index);
  }

-  /** Gets the underlying instruction. */
-  Instruction getInstruction() { result = instr }
+  private class IndirectInstructionFromRaw extends IndirectInstruction instanceof RawIndirectInstruction
+  {
+    override predicate hasInstructionAndIndirectionIndex(Instruction instr, int index) {
+      instr = RawIndirectInstruction.super.getInstruction() and
+      index = RawIndirectInstruction.super.getIndirectionIndex()
+    }
+  }

-  /** Gets the underlying indirection index. */
-  int getIndirectionIndex() { result = indirectionIndex }
+  private class IndirectInstructionFromIRRepr extends IndirectInstruction {
+    Instruction instr;
+    int indirectionIndex;

-  /**
-   * Holds if this `IndirectInstruction` is represented directly in the IR instead of
-   * a `RawIndirectionInstruction` with instruction `i` and indirection index `index`.
-   */
-  predicate isIRRepresentationOf(Instruction i, int index) {
-    this instanceof InstructionNode and
-    (
-      i = instr and
-      index = indirectionIndex
-    )
+    IndirectInstructionFromIRRepr() {
+      exists(Instruction repr |
+        repr = Ssa::getIRRepresentationOfIndirectInstruction(instr, indirectionIndex) and
+        nodeHasInstruction(this, repr, indirectionIndex - 1)
+      )
+    }
+
+    override predicate hasInstructionAndIndirectionIndex(Instruction i, int index) {
+      i = instr and index = indirectionIndex
+    }
  }
 }

+import IndirectInstructions
+
 /** Gets the callable in which this node occurs. */
 DataFlowCallable nodeGetEnclosingCallable(Node n) { result = n.getEnclosingCallable() }

@@ -318,9 +321,11 @@ private class PrimaryArgumentNode extends ArgumentNode, OperandNode {

 private class SideEffectArgumentNode extends ArgumentNode, SideEffectOperandNode {
  override predicate argumentOf(DataFlowCall dfCall, ArgumentPosition pos) {
-    this.getCallInstruction() = dfCall and
-    pos.(IndirectionPosition).getArgumentIndex() = this.getArgumentIndex() and
-    pos.(IndirectionPosition).getIndirectionIndex() = super.getIndirectionIndex()
+    exists(int indirectionIndex |
+      pos = TIndirectionPosition(argumentIndex, pragma[only_bind_into](indirectionIndex)) and
+      this.getCallInstruction() = dfCall and
+      super.hasAddressOperandAndIndirectionIndex(_, pragma[only_bind_into](indirectionIndex))
+    )
  }
 }

@@ -648,13 +653,16 @@ predicate jumpStep(Node n1, Node n2) {
 * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
 * Thus, `node2` references an object with a field `f` that contains the
 * value of `node1`.
+ *
+ * The boolean `certain` is true if the destination address does not involve
+ * any pointer arithmetic, and false otherwise.
 */
-predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
+predicate storeStepImpl(Node node1, Content c, PostFieldUpdateNode node2, boolean certain) {
  exists(int indirectionIndex1, int numberOfLoads, StoreInstruction store |
    nodeHasInstruction(node1, store, pragma[only_bind_into](indirectionIndex1)) and
    node2.getIndirectionIndex() = 1 and
    numberOfLoadsFromOperand(node2.getFieldAddress(), store.getDestinationAddressOperand(),
-      numberOfLoads)
+      numberOfLoads, certain)
  |
    exists(FieldContent fc | fc = c |
      fc.getField() = node2.getUpdatedField() and
@@ -668,21 +676,34 @@ predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
  )
 }

+/**
+ * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
+ * Thus, `node2` references an object with a field `f` that contains the
+ * value of `node1`.
+ */
+predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
+  storeStepImpl(node1, c, node2, _)
+}
+
 /**
 * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
 * operations and exactly `n` `LoadInstruction` operations.
 */
-private predicate numberOfLoadsFromOperandRec(Operand operandFrom, Operand operandTo, int ind) {
+private predicate numberOfLoadsFromOperandRec(
+  Operand operandFrom, Operand operandTo, int ind, boolean certain
+) {
  exists(Instruction load | Ssa::isDereference(load, operandFrom) |
-    operandTo = operandFrom and ind = 0
+    operandTo = operandFrom and ind = 0 and certain = true
    or
-    numberOfLoadsFromOperand(load.getAUse(), operandTo, ind - 1)
+    numberOfLoadsFromOperand(load.getAUse(), operandTo, ind - 1, certain)
  )
  or
-  exists(Operand op, Instruction instr |
+  exists(Operand op, Instruction instr, boolean isPointerArith, boolean certain0 |
    instr = op.getDef() and
-    conversionFlow(operandFrom, instr, _, _) and
-    numberOfLoadsFromOperand(op, operandTo, ind)
+    conversionFlow(operandFrom, instr, isPointerArith, _) and
+    numberOfLoadsFromOperand(op, operandTo, ind, certain0)
+  |
+    if isPointerArith = true then certain = false else certain = certain0
  )
 }

@@ -690,13 +711,16 @@ private predicate numberOfLoadsFromOperandRec(Operand operandFrom, Operand opera
 * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
 * operations and exactly `n` `LoadInstruction` operations.
 */
-private predicate numberOfLoadsFromOperand(Operand operandFrom, Operand operandTo, int n) {
-  numberOfLoadsFromOperandRec(operandFrom, operandTo, n)
+private predicate numberOfLoadsFromOperand(
+  Operand operandFrom, Operand operandTo, int n, boolean certain
+) {
+  numberOfLoadsFromOperandRec(operandFrom, operandTo, n, certain)
  or
  not Ssa::isDereference(_, operandFrom) and
  not conversionFlow(operandFrom, _, _, _) and
  operandFrom = operandTo and
-  n = 0
+  n = 0 and
+  certain = true
 }

 // Needed to join on both an operand and an index at the same time.
@@ -726,7 +750,7 @@ predicate readStep(Node node1, Content c, Node node2) {
    // The `1` here matches the `node2.getIndirectionIndex() = 1` conjunct
    // in `storeStep`.
    nodeHasOperand(node1, fa1.getObjectAddressOperand(), 1) and
-    numberOfLoadsFromOperand(fa1, operand, numberOfLoads)
+    numberOfLoadsFromOperand(fa1, operand, numberOfLoads, _)
  |
    exists(FieldContent fc | fc = c |
      fc.getField() = fa1.getField() and
@@ -744,7 +768,33 @@ predicate readStep(Node node1, Content c, Node node2) {
 * Holds if values stored inside content `c` are cleared at node `n`.
 */
 predicate clearsContent(Node n, Content c) {
-  none() // stub implementation
+  n =
+    any(PostUpdateNode pun, Content d | d.impliesClearOf(c) and storeStepImpl(_, d, pun, true) | pun)
+        .getPreUpdateNode() and
+  (
+    // The crement operations and pointer addition and subtraction self-assign. We do not
+    // want to clear the contents if it is indirectly pointed at by any of these operations,
+    // as part of the contents might still be accessible afterwards. If there is no such
+    // indirection clearing the contents is safe.
+    not exists(Operand op, Cpp::Operation p |
+      n.(IndirectOperand).hasOperandAndIndirectionIndex(op, _) and
+      (
+        p instanceof Cpp::AssignPointerAddExpr or
+        p instanceof Cpp::AssignPointerSubExpr or
+        p instanceof Cpp::CrementOperation
+      )
+    |
+      p.getAnOperand() = op.getUse().getAst()
+    )
+    or
+    forex(PostUpdateNode pun, Content d |
+      pragma[only_bind_into](d).impliesClearOf(pragma[only_bind_into](c)) and
+      storeStepImpl(_, d, pun, true) and
+      pun.getPreUpdateNode() = n
+    |
+      c.getIndirectionIndex() = d.getIndirectionIndex()
+    )
+  )
 }

 /**
@@ -753,6 +803,8 @@ predicate clearsContent(Node n, Content c) {
 */
 predicate expectsContent(Node n, ContentSet c) { none() }

+predicate typeStrongerThan(DataFlowType t1, DataFlowType t2) { none() }
+
 /** Gets the type of `n` used for type pruning. */
 DataFlowType getNodeType(Node n) {
  suppressUnusedNode(n) and
@@ -781,6 +833,12 @@ class CastNode extends Node {
  CastNode() { none() } // stub implementation
 }

+/**
+ * Holds if `n` should never be skipped over in the `PathGraph` and in path
+ * explanations.
+ */
+predicate neverSkipInPathGraph(Node n) { none() }
+
 /**
 * A function that may contain code or a variable that may contain itself. When
 * flow crosses from one _enclosing callable_ to another, the interprocedural
@@ -798,7 +856,73 @@ class DataFlowCall extends CallInstruction {
  Function getEnclosingCallable() { result = this.getEnclosingFunction() }
 }

-predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub implementation
+module IsUnreachableInCall {
+  private import semmle.code.cpp.ir.ValueNumbering
+  private import semmle.code.cpp.controlflow.IRGuards as G
+
+  private class ConstantIntegralTypeArgumentNode extends PrimaryArgumentNode {
+    int value;
+
+    ConstantIntegralTypeArgumentNode() {
+      value = op.getDef().(IntegerConstantInstruction).getValue().toInt()
+    }
+
+    int getValue() { result = value }
+  }
+
+  pragma[nomagic]
+  private predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
+    any(G::IRGuardCondition guard).ensuresEq(left, right, k, block, areEqual)
+  }
+
+  pragma[nomagic]
+  private predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
+    any(G::IRGuardCondition guard).ensuresLt(left, right, k, block, areEqual)
+  }
+
+  predicate isUnreachableInCall(Node n, DataFlowCall call) {
+    exists(
+      DirectParameterNode paramNode, ConstantIntegralTypeArgumentNode arg,
+      IntegerConstantInstruction constant, int k, Operand left, Operand right, IRBlock block
+    |
+      // arg flows into `paramNode`
+      DataFlowImplCommon::viableParamArg(call, paramNode, arg) and
+      left = constant.getAUse() and
+      right = valueNumber(paramNode.getInstruction()).getAUse() and
+      block = n.getBasicBlock()
+    |
+      // and there's a guard condition which ensures that the result of `left == right + k` is `areEqual`
+      exists(boolean areEqual |
+        ensuresEq(pragma[only_bind_into](left), pragma[only_bind_into](right),
+          pragma[only_bind_into](k), pragma[only_bind_into](block), areEqual)
+      |
+        // this block ensures that left = right + k, but it holds that `left != right + k`
+        areEqual = true and
+        constant.getValue().toInt() != arg.getValue() + k
+        or
+        // this block ensures that or `left != right + k`, but it holds that `left = right + k`
+        areEqual = false and
+        constant.getValue().toInt() = arg.getValue() + k
+      )
+      or
+      // or there's a guard condition which ensures that the result of `left < right + k` is `isLessThan`
+      exists(boolean isLessThan |
+        ensuresLt(pragma[only_bind_into](left), pragma[only_bind_into](right),
+          pragma[only_bind_into](k), pragma[only_bind_into](block), isLessThan)
+      |
+        isLessThan = true and
+        // this block ensures that `left < right + k`, but it holds that `left >= right + k`
+        constant.getValue().toInt() >= arg.getValue() + k
+        or
+        // this block ensures that `left >= right + k`, but it holds that `left < right + k`
+        isLessThan = false and
+        constant.getValue().toInt() < arg.getValue() + k
+      )
+    )
+  }
+}
+
+import IsUnreachableInCall

 int accessPathLimit() { result = 5 }

@@ -837,7 +961,7 @@ predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preserves
 * One example would be to allow flow like `p.foo = p.bar;`, which is disallowed
 * by default as a heuristic.
 */
-predicate allowParameterReturnInSelf(ParameterNode p) { none() }
+predicate allowParameterReturnInSelf(ParameterNode p) { p instanceof IndirectParameterNode }

 private predicate fieldHasApproxName(Field f, string s) {
  s = f.getName().charAt(0) and
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
@@ -274,7 +274,7 @@ class Node extends TIRDataFlowNode {
   * represents the value of `**x` going into `f`.
   */
  Expr asIndirectArgument(int index) {
-    this.(SideEffectOperandNode).getIndirectionIndex() = index and
+    this.(SideEffectOperandNode).hasAddressOperandAndIndirectionIndex(_, index) and
    result = this.(SideEffectOperandNode).getArgument()
  }

@@ -317,7 +317,7 @@ class Node extends TIRDataFlowNode {
    index = 0 and
    result = this.(ExplicitParameterNode).getParameter()
    or
-    this.(IndirectParameterNode).getIndirectionIndex() = index and
+    this.(IndirectParameterNode).hasInstructionAndIndirectionIndex(_, index) and
    result = this.(IndirectParameterNode).getParameter()
  }

@@ -577,15 +577,20 @@ class SsaPhiNode extends Node, TSsaPhiNode {
 *
 * A node representing a value after leaving a function.
 */
-class SideEffectOperandNode extends Node, IndirectOperand {
+class SideEffectOperandNode extends Node instanceof IndirectOperand {
  CallInstruction call;
  int argumentIndex;

-  SideEffectOperandNode() { operand = call.getArgumentOperand(argumentIndex) }
+  SideEffectOperandNode() {
+    IndirectOperand.super.hasOperandAndIndirectionIndex(call.getArgumentOperand(argumentIndex), _)
+  }

  CallInstruction getCallInstruction() { result = call }

-  Operand getAddressOperand() { result = operand }
+  /** Gets the underlying operand and the underlying indirection index. */
+  predicate hasAddressOperandAndIndirectionIndex(Operand operand, int indirectionIndex) {
+    IndirectOperand.super.hasOperandAndIndirectionIndex(operand, indirectionIndex)
+  }

  int getArgumentIndex() { result = argumentIndex }

@@ -665,10 +670,10 @@ class InitialGlobalValue extends Node, TInitialGlobalValue {
 *
 * A node representing an indirection of a parameter.
 */
-class IndirectParameterNode extends Node, IndirectInstruction {
+class IndirectParameterNode extends Node instanceof IndirectInstruction {
  InitializeParameterInstruction init;

-  IndirectParameterNode() { this.getInstruction() = init }
+  IndirectParameterNode() { IndirectInstruction.super.hasInstructionAndIndirectionIndex(init, _) }

  int getArgumentIndex() { init.hasIndex(result) }

@@ -677,7 +682,12 @@ class IndirectParameterNode extends Node, IndirectInstruction {

  override Declaration getEnclosingCallable() { result = this.getFunction() }

-  override Declaration getFunction() { result = this.getInstruction().getEnclosingFunction() }
+  override Declaration getFunction() { result = init.getEnclosingFunction() }
+
+  /** Gets the underlying operand and the underlying indirection index. */
+  predicate hasInstructionAndIndirectionIndex(Instruction instr, int index) {
+    IndirectInstruction.super.hasInstructionAndIndirectionIndex(instr, index)
+  }

  override Location getLocationImpl() { result = this.getParameter().getLocation() }

@@ -699,7 +709,8 @@ class IndirectReturnNode extends Node {
  IndirectReturnNode() {
    this instanceof FinalParameterNode
    or
-    this.(IndirectOperand).getOperand() = any(ReturnValueInstruction ret).getReturnAddressOperand()
+    this.(IndirectOperand)
+        .hasOperandAndIndirectionIndex(any(ReturnValueInstruction ret).getReturnAddressOperand(), _)
  }

  override Declaration getEnclosingCallable() { result = this.getFunction() }
@@ -722,7 +733,7 @@ class IndirectReturnNode extends Node {
  int getIndirectionIndex() {
    result = this.(FinalParameterNode).getIndirectionIndex()
    or
-    result = this.(IndirectOperand).getIndirectionIndex()
+    this.(IndirectOperand).hasOperandAndIndirectionIndex(_, result)
  }
 }

@@ -1106,7 +1117,8 @@ predicate exprNodeShouldBeInstruction(Node node, Expr e) {
 /** Holds if `node` should be an `IndirectInstruction` that maps `node.asIndirectExpr()` to `e`. */
 predicate indirectExprNodeShouldBeIndirectInstruction(IndirectInstruction node, Expr e) {
  exists(Instruction instr |
-    instr = node.getInstruction() and not indirectExprNodeShouldBeIndirectOperand(_, e)
+    node.hasInstructionAndIndirectionIndex(instr, _) and
+    not indirectExprNodeShouldBeIndirectOperand(_, e)
  |
    e = instr.(VariableAddressInstruction).getAst().(Expr).getFullyConverted()
    or
@@ -1307,8 +1319,8 @@ pragma[noinline]
 private predicate indirectParameterNodeHasArgumentIndexAndIndex(
  IndirectParameterNode node, int argumentIndex, int indirectionIndex
 ) {
-  node.getArgumentIndex() = argumentIndex and
-  node.getIndirectionIndex() = indirectionIndex
+  node.hasInstructionAndIndirectionIndex(_, indirectionIndex) and
+  node.getArgumentIndex() = argumentIndex
 }

 /** A synthetic parameter to model the pointed-to object of a pointer parameter. */
@@ -1479,18 +1491,14 @@ VariableNode variableNode(Variable v) {
 */
 Node uninitializedNode(LocalVariable v) { none() }

-pragma[noinline]
 predicate hasOperandAndIndex(IndirectOperand indirectOperand, Operand operand, int indirectionIndex) {
-  indirectOperand.getOperand() = operand and
-  indirectOperand.getIndirectionIndex() = indirectionIndex
+  indirectOperand.hasOperandAndIndirectionIndex(operand, indirectionIndex)
 }

-pragma[noinline]
 predicate hasInstructionAndIndex(
  IndirectInstruction indirectInstr, Instruction instr, int indirectionIndex
 ) {
-  indirectInstr.getInstruction() = instr and
-  indirectInstr.getIndirectionIndex() = indirectionIndex
+  indirectInstr.hasInstructionAndIndirectionIndex(instr, indirectionIndex)
 }

 cached
@@ -1656,8 +1664,7 @@ module ExprFlowCached {
  private predicate isIndirectBaseOfArrayAccess(IndirectOperand n, Expr e) {
    exists(LoadInstruction load, PointerArithmeticInstruction pai |
      pai = load.getSourceAddress() and
-      pai.getLeftOperand() = n.getOperand() and
-      n.getIndirectionIndex() = 1 and
+      n.hasOperandAndIndirectionIndex(pai.getLeftOperand(), 1) and
      e = load.getConvertedResultExpression()
    )
  }
@@ -1825,6 +1832,20 @@ class Content extends TContent {
  predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
    path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
  }
+
+  /** Gets the indirection index of this `Content`. */
+  abstract int getIndirectionIndex();
+
+  /**
+   * INTERNAL: Do not use.
+   *
+   * Holds if a write to this `Content` implies that `c` is
+   * also cleared.
+   *
+   * For example, a write to a field `f` implies that any content of
+   * the form `*f` is also cleared.
+   */
+  abstract predicate impliesClearOf(Content c);
 }

 /** A reference through a non-union instance field. */
@@ -1842,10 +1863,21 @@ class FieldContent extends Content, TFieldContent {

  Field getField() { result = f }

+  /** Gets the indirection index of this `FieldContent`. */
  pragma[inline]
-  int getIndirectionIndex() {
+  override int getIndirectionIndex() {
    pragma[only_bind_into](result) = pragma[only_bind_out](indirectionIndex)
  }
+
+  override predicate impliesClearOf(Content c) {
+    exists(FieldContent fc |
+      fc = c and
+      fc.getField() = f and
+      // If `this` is `f` then `c` is cleared if it's of the
+      // form `*f`, `**f`, etc.
+      fc.getIndirectionIndex() >= indirectionIndex
+    )
+  }
 }

 /** A reference through an instance field of a union. */
@@ -1870,9 +1902,21 @@ class UnionContent extends Content, TUnionContent {

  /** Gets the indirection index of this `UnionContent`. */
  pragma[inline]
-  int getIndirectionIndex() {
+  override int getIndirectionIndex() {
    pragma[only_bind_into](result) = pragma[only_bind_out](indirectionIndex)
  }
+
+  override predicate impliesClearOf(Content c) {
+    exists(UnionContent uc |
+      uc = c and
+      uc.getUnion() = u and
+      // If `this` is `u` then `c` is cleared if it's of the
+      // form `*u`, `**u`, etc. (and we ignore `bytes` because
+      // we know the entire union is overwritten because it's a
+      // union).
+      uc.getIndirectionIndex() >= indirectionIndex
+    )
+  }
 }

 /**
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/PrintIRFieldFlowSteps.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/PrintIRFieldFlowSteps.qll
@@ -13,7 +13,7 @@ class FieldFlowPropertyProvider extends IRPropertyProvider {
  override string getOperandProperty(Operand operand, string key) {
    exists(PostFieldUpdateNode pfun, Content content |
      key = "store " + content.toString() and
-      operand = pfun.getPreUpdateNode().(IndirectOperand).getOperand() and
+      pfun.getPreUpdateNode().(IndirectOperand).hasOperandAndIndirectionIndex(operand, _) and
      result =
        strictconcat(string element, Node node |
          storeStep(node, content, pfun) and
@@ -25,7 +25,7 @@ class FieldFlowPropertyProvider extends IRPropertyProvider {
    or
    exists(Node node2, Content content |
      key = "read " + content.toString() and
-      operand = node2.(IndirectOperand).getOperand() and
+      node2.(IndirectOperand).hasOperandAndIndirectionIndex(operand, _) and
      result =
        strictconcat(string element, Node node1 |
          readStep(node1, content, node2) and
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/PrintIRUtilities.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/PrintIRUtilities.qll
@@ -18,9 +18,12 @@ private string stars(int k) {
 }

 string starsForNode(Node node) {
-  result = stars(node.(IndirectInstruction).getIndirectionIndex())
-  or
-  result = stars(node.(IndirectOperand).getIndirectionIndex())
+  exists(int indirectionIndex |
+    node.(IndirectInstruction).hasInstructionAndIndirectionIndex(_, indirectionIndex) or
+    node.(IndirectOperand).hasOperandAndIndirectionIndex(_, indirectionIndex)
+  |
+    result = stars(indirectionIndex)
+  )
  or
  not node instanceof IndirectInstruction and
  not node instanceof IndirectOperand and
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ProductFlow.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ProductFlow.qll
@@ -192,13 +192,13 @@ module ProductFlow {
     * Holds if data flow through `node` is prohibited through the first projection of the product
     * dataflow graph when the flow state is `state`.
     */
-    predicate isBarrier1(DataFlow::Node node, FlowState1 state);
+    default predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }

    /**
     * Holds if data flow through `node` is prohibited through the second projection of the product
     * dataflow graph when the flow state is `state`.
     */
-    predicate isBarrier2(DataFlow::Node node, FlowState2 state);
+    default predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }

    /**
     * Holds if data flow through `node` is prohibited through the first projection of the product
@@ -237,9 +237,11 @@ module ProductFlow {
     *
     * This step is only applicable in `state1` and updates the flow state to `state2`.
     */
-    predicate isAdditionalFlowStep1(
+    default predicate isAdditionalFlowStep1(
      DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
-    );
+    ) {
+      none()
+    }

    /**
     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
@@ -253,9 +255,11 @@ module ProductFlow {
     *
     * This step is only applicable in `state1` and updates the flow state to `state2`.
     */
-    predicate isAdditionalFlowStep2(
+    default predicate isAdditionalFlowStep2(
      DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
-    );
+    ) {
+      none()
+    }

    /**
     * Holds if data flow into `node` is prohibited in the first projection of the product
@@ -359,7 +363,6 @@ module ProductFlow {
      Config::isSinkPair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState())
    }

-    pragma[assume_small_delta]
    pragma[nomagic]
    private predicate fwdReachableInterprocEntry(Flow1::PathNode node1, Flow2::PathNode node2) {
      isSourcePair(node1, node2)
@@ -396,7 +399,6 @@ module ProductFlow {
      fwdIsSuccessorExit(pragma[only_bind_into](mid1), pragma[only_bind_into](mid2), succ1, succ2)
    }

-    pragma[assume_small_delta]
    private predicate fwdIsSuccessor(
      Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2
    ) {
@@ -406,7 +408,6 @@ module ProductFlow {
      )
    }

-    pragma[assume_small_delta]
    pragma[nomagic]
    private predicate revReachableInterprocEntry(Flow1::PathNode node1, Flow2::PathNode node2) {
      fwdReachableInterprocEntry(node1, node2) and
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
@@ -364,7 +364,25 @@ abstract private class OperandBasedUse extends UseImpl {
  OperandBasedUse() { any() }

  final override predicate hasIndexInBlock(IRBlock block, int index) {
-    operand.getUse() = block.getInstruction(index)
+    // See the comment in `ssa0`'s `OperandBasedUse` for an explanation of this
+    // predicate's implementation.
+    exists(BaseSourceVariableInstruction base | base = this.getBase() |
+      if base.getAst() = any(Cpp::PostfixCrementOperation c).getOperand()
+      then
+        exists(Operand op, int indirectionIndex, int indirection |
+          indirectionIndex = this.getIndirectionIndex() and
+          indirection = this.getIndirection() and
+          op =
+            min(Operand cand, int i |
+              isUse(_, cand, base, indirection, indirectionIndex) and
+              block.getInstruction(i) = cand.getUse()
+            |
+              cand order by i
+            ) and
+          block.getInstruction(index) = op.getUse()
+        )
+      else operand.getUse() = block.getInstruction(index)
+    )
  }

  final Operand getOperand() { result = operand }
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternalsCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternalsCommon.qll
@@ -117,6 +117,16 @@ private int countIndirections(Type t) {
  else (
    result = any(Indirection ind | ind.getType() = t).getNumberOfIndirections()
    or
+    // If there is an indirection for the type, but we cannot count the number of indirections
+    // it means we couldn't reach a non-indirection type by stripping off indirections. This
+    // can occur if an iterator specifies itself as the value type. In this case we default to
+    // 1 indirection fore the type.
+    exists(Indirection ind |
+      ind.getType() = t and
+      not exists(ind.getNumberOfIndirections()) and
+      result = 1
+    )
+    or
    not exists(Indirection ind | ind.getType() = t) and
    result = 0
  )
@@ -263,7 +273,7 @@ private module IteratorIndirections {
        // Taint through `operator+=` and `operator-=` on iterators.
        call.getStaticCallTarget() instanceof Iterator::IteratorAssignArithmeticOperator and
        node2.(IndirectArgumentOutNode).getPreUpdateNode() = node1 and
-        node1.(IndirectOperand).getOperand() = call.getArgumentOperand(0) and
+        node1.(IndirectOperand).hasOperandAndIndirectionIndex(call.getArgumentOperand(0), _) and
        node1.getType().getUnspecifiedType() = this
      )
    }
@@ -578,7 +588,6 @@ private module Cached {
    )
  }

-  pragma[assume_small_delta]
  private predicate convertsIntoArgumentRev(Instruction instr) {
    convertsIntoArgumentFwd(instr) and
    (
@@ -796,7 +805,7 @@ private module Cached {
      address.getDef() = instr and
      isDereference(load, address) and
      isUseImpl(address, _, indirectionIndex - 1) and
-      result = instr
+      result = load
    )
  }

--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TaintTrackingUtil.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TaintTrackingUtil.qll
@@ -160,7 +160,7 @@ predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut) {
    FunctionInput modelIn, FunctionOutput modelOut
  |
    indirectArgument = callInput(call, modelIn) and
-    indirectArgument.getAddressOperand() = nodeIn.asOperand() and
+    indirectArgument.hasAddressOperandAndIndirectionIndex(nodeIn.asOperand(), _) and
    call.getStaticCallTarget() = func and
    (
      func.(DataFlowFunction).hasDataFlow(modelIn, modelOut)
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ssa0/SsaInternals.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ssa0/SsaInternals.qll
@@ -122,7 +122,46 @@ abstract private class OperandBasedUse extends UseImpl {
  override string toString() { result = operand.toString() }

  final override predicate hasIndexInBlock(IRBlock block, int index) {
-    operand.getUse() = block.getInstruction(index)
+    // Ideally, this would just be implemented as:
+    // ```
+    // operand.getUse() = block.getInstruction(index)
+    // ```
+    // but because the IR generated for a snippet such as
+    // ```
+    // int x = *p++;
+    // ```
+    // looks like
+    // ```
+    // r1(glval<int>)   = VariableAddress[x]  :
+    // r2(glval<int *>) = VariableAddress[p]  :
+    // r3(int *)        = Load[p]             : &:r2, m1
+    // r4(int)          = Constant[1]         :
+    // r5(int *)        = PointerAdd[4]       : r3, r4
+    // m3(int *)        = Store[p]            : &:r2, r5
+    // r6(int *)        = CopyValue           : r3
+    // r7(int)          = Load[?]             : &:r6, ~m2
+    // m2(int)          = Store[x]            : &:r1, r7
+    // ```
+    // we need to ensure that the `r3` operand of the `CopyValue` instruction isn't seen as a fresh use
+    // of `p` that happens after the increment. So if the base instruction of this use comes from a
+    // post-fix crement operation we set the index of the SSA use that wraps the `r3` operand at the
+    // `CopyValue` instruction to be the same index as the `r3` operand at the `PointerAdd` instruction.
+    // This ensures that the SSA library doesn't create flow from the `PointerAdd` to `r6`.
+    exists(BaseSourceVariableInstruction base | base = this.getBase() |
+      if base.getAst() = any(Cpp::PostfixCrementOperation c).getOperand()
+      then
+        exists(Operand op |
+          op =
+            min(Operand cand, int i |
+              isUse(_, cand, base, _, _) and
+              block.getInstruction(i) = cand.getUse()
+            |
+              cand order by i
+            ) and
+          block.getInstruction(index) = op.getUse()
+        )
+      else operand.getUse() = block.getInstruction(index)
+    )
  }

  final override Cpp::Location getLocation() { result = operand.getLocation() }
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll
@@ -176,7 +176,6 @@ private predicate binaryValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate binaryValueNumber(
  BinaryInstruction instr, IRFunction irFunc, Opcode opcode, TValueNumber leftOperand,
  TValueNumber rightOperand
@@ -202,7 +201,6 @@ private predicate pointerArithmeticValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate pointerArithmeticValueNumber(
  PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, int elementSize,
  TValueNumber leftOperand, TValueNumber rightOperand
@@ -249,7 +247,6 @@ private predicate loadTotalOverlapValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate loadTotalOverlapValueNumber(
  LoadTotalOverlapInstruction instr, IRFunction irFunc, IRType type, TValueNumber memOperand,
  TValueNumber operand
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll
@@ -176,7 +176,6 @@ private predicate binaryValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate binaryValueNumber(
  BinaryInstruction instr, IRFunction irFunc, Opcode opcode, TValueNumber leftOperand,
  TValueNumber rightOperand
@@ -202,7 +201,6 @@ private predicate pointerArithmeticValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate pointerArithmeticValueNumber(
  PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, int elementSize,
  TValueNumber leftOperand, TValueNumber rightOperand
@@ -249,7 +247,6 @@ private predicate loadTotalOverlapValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate loadTotalOverlapValueNumber(
  LoadTotalOverlapInstruction instr, IRFunction irFunc, IRType type, TValueNumber memOperand,
  TValueNumber operand
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll
@@ -176,7 +176,6 @@ private predicate binaryValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate binaryValueNumber(
  BinaryInstruction instr, IRFunction irFunc, Opcode opcode, TValueNumber leftOperand,
  TValueNumber rightOperand
@@ -202,7 +201,6 @@ private predicate pointerArithmeticValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate pointerArithmeticValueNumber(
  PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, int elementSize,
  TValueNumber leftOperand, TValueNumber rightOperand
@@ -249,7 +247,6 @@ private predicate loadTotalOverlapValueNumber0(
  )
 }

-pragma[assume_small_delta]
 private predicate loadTotalOverlapValueNumber(
  LoadTotalOverlapInstruction instr, IRFunction irFunc, IRType type, TValueNumber memOperand,
  TValueNumber operand
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
@@ -108,7 +108,7 @@ class StrcpyFunction extends ArrayFunction, DataFlowFunction, TaintFunction, Sid
    // these may do only a partial copy of the input buffer to the output
    // buffer
    exists(this.getParamSize()) and
-    input.isParameter(this.getParamSrc()) and
+    input.isParameterDeref(this.getParamSrc()) and
    (
      output.isParameterDeref(this.getParamDest()) or
      output.isReturnValueDeref()
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
@@ -70,6 +70,27 @@ predicate semBackEdge(SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionP
  // Conservatively assume that every edge is a back edge if we don't have dominance information.
  (
    phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
+    irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock()) or
    not edge.getOrigBlock().hasDominanceInformation()
  )
 }
+
+/**
+ * Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
+ * graph.
+ *
+ * An ireducible control flow graph is one where the usual dominance-based back edge detection does
+ * not work, because there is a cycle with multiple entry points, meaning there are
+ * mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
+ * remove all detectable back-edges using the normal condition that the predecessor block is
+ * dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
+ * edges.
+ */
+private predicate irreducibleSccEdge(SemBasicBlock b1, SemBasicBlock b2) {
+  trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
+}
+
+private predicate trimmedEdge(SemBasicBlock pred, SemBasicBlock succ) {
+  pred.getASuccessor() = succ and
+  not succ.bbDominates(pred)
+}
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
@@ -877,7 +877,6 @@ module RangeStage<
    )
  }

-  pragma[assume_small_delta]
  pragma[nomagic]
  private predicate boundedPhiRankStep(
    SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,