Data flow: Introduce ApproxContent in a new pruning stage between existing stages 2 and 3

2026-04-28 02:05:14 +02:00 · 2022-12-08 11:15:03 +01:00
parent 557a5b469f
commit d11cb2ee0f
4 changed files with 548 additions and 132 deletions
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll
@@ -621,23 +621,6 @@ private predicate parameterFlowThroughAllowed(ParamNodeEx p, ReturnKindExt kind)
  )
 }

-/**
- * Holds if flow from a parameter at position `pos` inside `c` to a return node of
- * kind `kind` is allowed.
- *
- * We don't expect a parameter to return stored in itself, unless
- * explicitly allowed
- */
-bindingset[c, pos, kind]
-private predicate parameterFlowThroughAllowed(
-  DataFlowCallable c, ParameterPosition pos, ReturnKindExt kind
-) {
-  exists(ParamNodeEx p |
-    p.isParameterOf(c, pos) and
-    parameterFlowThroughAllowed(p, kind)
-  )
-}
-
 private module Stage1 implements StageSig {
  class Ap = Unit;

@@ -980,6 +963,12 @@ private module Stage1 implements StageSig {
  pragma[nomagic]
  predicate revFlow(NodeEx node, Configuration config) { revFlow(node, _, config) }

+  pragma[nomagic]
+  predicate revFlowAp(NodeEx node, Ap ap, Configuration config) {
+    revFlow(node, config) and
+    exists(ap)
+  }
+
  bindingset[node, state, config]
  predicate revFlow(NodeEx node, FlowState state, Ap ap, Configuration config) {
    revFlow(node, _, pragma[only_bind_into](config)) and
@@ -1022,9 +1011,13 @@ private module Stage1 implements StageSig {
  }

  pragma[nomagic]
-  predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind, Configuration config) {
+  predicate returnMayFlowThrough(
+    RetNodeEx ret, Ap argAp, Ap ap, ReturnKindExt kind, Configuration config
+  ) {
    throughFlowNodeCand(ret, config) and
-    kind = ret.getKind()
+    kind = ret.getKind() and
+    exists(argAp) and
+    exists(ap)
  }

  pragma[nomagic]
@@ -1189,6 +1182,8 @@ private signature module StageSig {

  predicate revFlow(NodeEx node, Configuration config);

+  predicate revFlowAp(NodeEx node, Ap ap, Configuration config);
+
  bindingset[node, state, config]
  predicate revFlow(NodeEx node, FlowState state, Ap ap, Configuration config);

@@ -1196,7 +1191,9 @@ private signature module StageSig {

  predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config);

-  predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind, Configuration config);
+  predicate returnMayFlowThrough(
+    RetNodeEx ret, Ap argAp, Ap ap, ReturnKindExt kind, Configuration config
+  );

  predicate storeStepCand(
    NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, DataFlowType contentType,
@@ -1281,21 +1278,43 @@ private module MkStage<StageSig PrevStage> {
    import Param

    /* Begin: Stage logic. */
-    bindingset[result, apa]
-    private ApApprox unbindApa(ApApprox apa) {
-      pragma[only_bind_out](apa) = pragma[only_bind_out](result)
+    // use an alias as a workaround for bad functionality-induced joins
+    pragma[nomagic]
+    private predicate revFlowApAlias(NodeEx node, ApApprox apa, Configuration config) {
+      PrevStage::revFlowAp(node, apa, config)
+    }
+
+    pragma[nomagic]
+    private predicate flowIntoCallApa(
+      DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, ApApprox apa,
+      Configuration config
+    ) {
+      flowIntoCall(call, arg, p, allowsFieldFlow, config) and
+      PrevStage::revFlowAp(p, pragma[only_bind_into](apa), pragma[only_bind_into](config)) and
+      revFlowApAlias(arg, pragma[only_bind_into](apa), pragma[only_bind_into](config))
+    }
+
+    pragma[nomagic]
+    private predicate flowOutOfCallApa(
+      DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out, boolean allowsFieldFlow,
+      ApApprox apa, Configuration config
+    ) {
+      flowOutOfCall(call, ret, kind, out, allowsFieldFlow, config) and
+      PrevStage::revFlowAp(out, pragma[only_bind_into](apa), pragma[only_bind_into](config)) and
+      revFlowApAlias(ret, pragma[only_bind_into](apa), pragma[only_bind_into](config))
    }

    pragma[nomagic]
    private predicate flowThroughOutOfCall(
-      DataFlowCall call, DataFlowCallable c, CcCall ccc, RetNodeEx ret, ReturnKindExt kind,
-      NodeEx out, boolean allowsFieldFlow, Configuration config
+      DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
+      ApApprox argApa, ApApprox apa, Configuration config
    ) {
-      flowOutOfCall(call, ret, kind, out, allowsFieldFlow, pragma[only_bind_into](config)) and
-      PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
-      PrevStage::returnMayFlowThrough(ret, kind, pragma[only_bind_into](config)) and
-      matchesCall(ccc, call) and
-      c = ret.getEnclosingCallable()
+      exists(ReturnKindExt kind |
+        flowOutOfCallApa(call, ret, kind, out, allowsFieldFlow, apa, pragma[only_bind_into](config)) and
+        PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
+        PrevStage::returnMayFlowThrough(ret, argApa, apa, kind, pragma[only_bind_into](config)) and
+        matchesCall(ccc, call)
+      )
    }

    /**
@@ -1307,39 +1326,50 @@ private module MkStage<StageSig PrevStage> {
     * corresponding parameter position and access path of that argument, respectively.
     */
    pragma[nomagic]
+    additional predicate fwdFlow(
+      NodeEx node, FlowState state, Cc cc, ParameterPositionOption summaryCtx, ApOption argAp,
+      Ap ap, ApApprox apa, Configuration config
+    ) {
+      fwdFlow0(node, state, cc, summaryCtx, argAp, ap, apa, config) and
+      PrevStage::revFlow(node, state, apa, config) and
+      filter(node, state, ap, config)
+    }
+
+    pragma[inline]
    additional predicate fwdFlow(
      NodeEx node, FlowState state, Cc cc, ParameterPositionOption summaryCtx, ApOption argAp,
      Ap ap, Configuration config
    ) {
-      fwdFlow0(node, state, cc, summaryCtx, argAp, ap, config) and
-      PrevStage::revFlow(node, state, unbindApa(getApprox(ap)), config) and
-      filter(node, state, ap, config)
+      fwdFlow(node, state, cc, summaryCtx, argAp, ap, _, config)
    }

    pragma[nomagic]
    private predicate fwdFlow0(
      NodeEx node, FlowState state, Cc cc, ParameterPositionOption summaryCtx, ApOption argAp,
-      Ap ap, Configuration config
+      Ap ap, ApApprox apa, Configuration config
    ) {
      sourceNode(node, state, config) and
      (if hasSourceCallCtx(config) then cc = ccSomeCall() else cc = ccNone()) and
      argAp = apNone() and
      summaryCtx = TParameterPositionNone() and
-      ap = getApNil(node)
+      ap = getApNil(node) and
+      apa = getApprox(ap)
      or
-      exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
-        fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, config) and
+      exists(NodeEx mid, FlowState state0, Ap ap0, ApApprox apa0, LocalCc localCc |
+        fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, apa0, config) and
        localCc = getLocalCc(mid, cc)
      |
        localStep(mid, state0, node, state, true, _, config, localCc) and
-        ap = ap0
+        ap = ap0 and
+        apa = apa0
        or
        localStep(mid, state0, node, state, false, ap, config, localCc) and
-        ap0 instanceof ApNil
+        ap0 instanceof ApNil and
+        apa = getApprox(ap)
      )
      or
      exists(NodeEx mid |
-        fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
+        fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, apa, pragma[only_bind_into](config)) and
        jumpStep(mid, node, config) and
        cc = ccNone() and
        summaryCtx = TParameterPositionNone() and
@@ -1352,7 +1382,8 @@ private module MkStage<StageSig PrevStage> {
        cc = ccNone() and
        summaryCtx = TParameterPositionNone() and
        argAp = apNone() and
-        ap = getApNil(node)
+        ap = getApNil(node) and
+        apa = getApprox(ap)
      )
      or
      exists(NodeEx mid, FlowState state0, ApNil nil |
@@ -1361,32 +1392,32 @@ private module MkStage<StageSig PrevStage> {
        cc = ccNone() and
        summaryCtx = TParameterPositionNone() and
        argAp = apNone() and
-        ap = getApNil(node)
+        ap = getApNil(node) and
+        apa = getApprox(ap)
      )
      or
      // store
      exists(TypedContent tc, Ap ap0 |
        fwdFlowStore(_, ap0, tc, node, state, cc, summaryCtx, argAp, config) and
-        ap = apCons(tc, ap0)
+        ap = apCons(tc, ap0) and
+        apa = getApprox(ap)
      )
      or
      // read
      exists(Ap ap0, Content c |
        fwdFlowRead(ap0, c, _, node, state, cc, summaryCtx, argAp, config) and
-        fwdFlowConsCand(ap0, c, ap, config)
+        fwdFlowConsCand(ap0, c, ap, config) and
+        apa = getApprox(ap)
      )
      or
      // flow into a callable
-      exists(ApApprox apa |
-        fwdFlowIn(_, node, state, _, cc, _, _, ap, config) and
-        apa = getApprox(ap) and
-        if PrevStage::parameterMayFlowThrough(node, apa, config)
-        then (
-          summaryCtx = TParameterPositionSome(node.(ParamNodeEx).getPosition()) and
-          argAp = apSome(ap)
-        ) else (
-          summaryCtx = TParameterPositionNone() and argAp = apNone()
-        )
+      fwdFlowIn(_, node, state, _, cc, _, _, ap, apa, config) and
+      if PrevStage::parameterMayFlowThrough(node, apa, config)
+      then (
+        summaryCtx = TParameterPositionSome(node.(ParamNodeEx).getPosition()) and
+        argAp = apSome(ap)
+      ) else (
+        summaryCtx = TParameterPositionNone() and argAp = apNone()
      )
      or
      // flow out of a callable
@@ -1394,8 +1425,8 @@ private module MkStage<StageSig PrevStage> {
        DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
        DataFlowCallable inner
      |
-        fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, config) and
-        flowOutOfCall(call, ret, _, node, allowsFieldFlow, config) and
+        fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, apa, config) and
+        flowOutOfCallApa(call, ret, _, node, allowsFieldFlow, apa, config) and
        inner = ret.getEnclosingCallable() and
        cc = getCallContextReturn(inner, call, innercc) and
        if allowsFieldFlow = false then ap instanceof ApNil else any()
@@ -1403,7 +1434,7 @@ private module MkStage<StageSig PrevStage> {
      or
      // flow through a callable
      exists(DataFlowCall call, ParameterPosition summaryCtx0, Ap argAp0 |
-        fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, config) and
+        fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, apa, config) and
        fwdFlowIsEntered(call, cc, summaryCtx, argAp, summaryCtx0, argAp0, config)
      )
    }
@@ -1413,9 +1444,9 @@ private module MkStage<StageSig PrevStage> {
      NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc,
      ParameterPositionOption summaryCtx, ApOption argAp, Configuration config
    ) {
-      exists(DataFlowType contentType |
-        fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, config) and
-        PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
+      exists(DataFlowType contentType, ApApprox apa1 |
+        fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, apa1, config) and
+        PrevStage::storeStepCand(node1, apa1, tc, node2, contentType, config) and
        typecheckStore(ap1, contentType)
      )
    }
@@ -1433,43 +1464,104 @@ private module MkStage<StageSig PrevStage> {
      )
    }

+    private class ApNonNil instanceof Ap {
+      pragma[nomagic]
+      ApNonNil() { not this instanceof ApNil }
+
+      string toString() { result = "" }
+    }
+
+    pragma[nomagic]
+    private predicate fwdFlowRead0(
+      NodeEx node1, FlowState state, Cc cc, ParameterPositionOption summaryCtx, ApOption argAp,
+      ApNonNil ap, Configuration config
+    ) {
+      fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
+      PrevStage::readStepCand(node1, _, _, config)
+    }
+
    pragma[nomagic]
    private predicate fwdFlowRead(
      Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
      ParameterPositionOption summaryCtx, ApOption argAp, Configuration config
    ) {
-      fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
+      fwdFlowRead0(node1, state, cc, summaryCtx, argAp, ap, config) and
      PrevStage::readStepCand(node1, c, node2, config) and
      getHeadContent(ap) = c
    }

    pragma[nomagic]
    private predicate fwdFlowIn(
-      DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc,
-      ParameterPositionOption summaryCtx, ApOption argAp, Ap ap, Configuration config
+      DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, CcCall innercc,
+      ParameterPositionOption summaryCtx, ApOption argAp, Ap ap, ApApprox apa, Configuration config
    ) {
      exists(ArgNodeEx arg, boolean allowsFieldFlow |
-        fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, config) and
-        flowIntoCall(call, arg, p, allowsFieldFlow, config) and
+        fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, apa, config) and
+        flowIntoCallApa(call, arg, p, allowsFieldFlow, apa, config) and
        innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
        if allowsFieldFlow = false then ap instanceof ApNil else any()
      )
    }

+    pragma[nomagic]
+    private predicate fwdFlowRetFromArg(
+      RetNodeEx ret, FlowState state, CcCall ccc, ParameterPosition summaryCtx, ParamNodeEx p,
+      Ap argAp, ApApprox argApa, Ap ap, ApApprox apa, Configuration config
+    ) {
+      exists(DataFlowCallable c, ReturnKindExt kind |
+        fwdFlow(pragma[only_bind_into](ret), state, ccc,
+          TParameterPositionSome(pragma[only_bind_into](summaryCtx)), apSome(argAp), ap, apa, config) and
+        getApprox(argAp) = argApa and
+        c = ret.getEnclosingCallable() and
+        kind = ret.getKind() and
+        p.isParameterOf(c, pragma[only_bind_into](summaryCtx)) and
+        parameterFlowThroughAllowed(p, kind)
+      )
+    }
+
+    pragma[inline]
+    private predicate fwdFlowInMayFlowThrough(
+      DataFlowCall call, Cc cc, CcCall innerCc, ParameterPositionOption summaryCtx, ApOption argAp,
+      ParamNodeEx param, Ap ap, ApApprox apa, Configuration config
+    ) {
+      fwdFlowIn(call, pragma[only_bind_into](param), _, cc, innerCc, summaryCtx, argAp, ap,
+        pragma[only_bind_into](apa), pragma[only_bind_into](config)) and
+      PrevStage::parameterMayFlowThrough(param, apa, config)
+    }
+
+    // dedup before joining with `flowThroughOutOfCall`
+    pragma[nomagic]
+    private predicate fwdFlowInMayFlowThroughProj(
+      DataFlowCall call, CcCall innerCc, ApApprox apa, Configuration config
+    ) {
+      fwdFlowInMayFlowThrough(call, _, innerCc, _, _, _, _, apa, config)
+    }
+
+    /**
+     * Same as `flowThroughOutOfCall`, but restricted to calls that are reached
+     * in the flow covered by `fwdFlow`, where data might flow through the target
+     * callable and back out at `call`.
+     */
+    pragma[nomagic]
+    private predicate fwdFlowThroughOutOfCall(
+      DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
+      ApApprox argApa, ApApprox apa, Configuration config
+    ) {
+      fwdFlowInMayFlowThroughProj(call, ccc, argApa, config) and
+      flowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, argApa, apa, config)
+    }
+
    pragma[nomagic]
    private predicate fwdFlowOutFromArg(
      DataFlowCall call, NodeEx out, FlowState state, ParameterPosition summaryCtx, Ap argAp, Ap ap,
-      Configuration config
+      ApApprox apa, Configuration config
    ) {
-      exists(
-        DataFlowCallable c, RetNodeEx ret, ReturnKindExt kind, boolean allowsFieldFlow, CcCall ccc
-      |
-        fwdFlow(pragma[only_bind_into](ret), state, pragma[only_bind_into](ccc),
-          TParameterPositionSome(pragma[only_bind_into](summaryCtx)), apSome(argAp), ap, config) and
-        flowThroughOutOfCall(call, pragma[only_bind_into](c), ccc, ret, kind, out, allowsFieldFlow,
+      exists(RetNodeEx ret, boolean allowsFieldFlow, CcCall ccc, ApApprox argApa |
+        fwdFlowRetFromArg(pragma[only_bind_into](ret), state, pragma[only_bind_into](ccc),
+          summaryCtx, _, argAp, pragma[only_bind_into](argApa), ap, pragma[only_bind_into](apa),
          config) and
-        (if allowsFieldFlow = false then ap instanceof ApNil else any()) and
-        parameterFlowThroughAllowed(c, pragma[only_bind_into](summaryCtx), kind)
+        fwdFlowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, argApa, apa, config) and
+        (if allowsFieldFlow = false then ap instanceof ApNil else any())
      )
    }

@@ -1483,8 +1575,7 @@ private module MkStage<StageSig PrevStage> {
      ParameterPosition pos, Ap ap, Configuration config
    ) {
      exists(ParamNodeEx param |
-        fwdFlowIn(call, param, _, cc, _, summaryCtx, argAp, ap, config) and
-        PrevStage::parameterMayFlowThrough(param, unbindApa(getApprox(ap)), config) and
+        fwdFlowInMayFlowThrough(call, cc, _, summaryCtx, argAp, param, ap, _, config) and
        pos = param.getPosition()
      )
    }
@@ -1505,41 +1596,55 @@ private module MkStage<StageSig PrevStage> {
      fwdFlowConsCand(ap1, c, ap2, config)
    }

-    pragma[nomagic]
-    private predicate returnFlowsThrough0(
-      RetNodeEx ret, ReturnKindExt kind, FlowState state, CcCall ccc, DataFlowCallable c,
-      ParameterPosition ppos, Ap argAp, Ap ap, Configuration config
-    ) {
-      exists(boolean allowsFieldFlow |
-        fwdFlow(ret, state, ccc, TParameterPositionSome(ppos), apSome(argAp), ap, config) and
-        flowThroughOutOfCall(_, c, _, pragma[only_bind_into](ret), kind, _, allowsFieldFlow,
-          pragma[only_bind_into](config)) and
-        if allowsFieldFlow = false then ap instanceof ApNil else any()
-      )
-    }
-
    pragma[nomagic]
    private predicate returnFlowsThrough(
      RetNodeEx ret, ReturnKindExt kind, FlowState state, CcCall ccc, ParamNodeEx p, Ap argAp,
      Ap ap, Configuration config
    ) {
-      exists(DataFlowCallable c, ParameterPosition ppos |
-        returnFlowsThrough0(ret, kind, state, ccc, c, ppos, argAp, ap, config) and
-        p.isParameterOf(c, ppos) and
-        parameterFlowThroughAllowed(p, kind)
+      exists(boolean allowsFieldFlow, ApApprox argApa, ApApprox apa |
+        fwdFlowRetFromArg(pragma[only_bind_into](ret), state, pragma[only_bind_into](ccc), _, p,
+          argAp, pragma[only_bind_into](argApa), ap, pragma[only_bind_into](apa), config) and
+        kind = ret.getKind() and
+        fwdFlowThroughOutOfCall(_, ccc, ret, _, allowsFieldFlow, argApa, apa, config) and
+        (if allowsFieldFlow = false then ap instanceof ApNil else any())
      )
    }

    pragma[nomagic]
    private predicate flowThroughIntoCall(
-      DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Configuration config
+      DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Ap argAp,
+      Configuration config
    ) {
-      exists(Ap argAp |
-        flowIntoCall(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), allowsFieldFlow,
+      exists(ApApprox argApa |
+        flowIntoCallApa(call, pragma[only_bind_into](arg), pragma[only_bind_into](p),
+          allowsFieldFlow, argApa, pragma[only_bind_into](config)) and
+        fwdFlow(arg, _, _, _, _, pragma[only_bind_into](argAp), argApa,
          pragma[only_bind_into](config)) and
-        fwdFlow(arg, _, _, _, _, pragma[only_bind_into](argAp), pragma[only_bind_into](config)) and
        returnFlowsThrough(_, _, _, _, p, pragma[only_bind_into](argAp), _,
-          pragma[only_bind_into](config))
+          pragma[only_bind_into](config)) and
+        if allowsFieldFlow = false then argAp instanceof ApNil else any()
+      )
+    }
+
+    pragma[nomagic]
+    private predicate flowIntoCallAp(
+      DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Ap ap,
+      Configuration config
+    ) {
+      exists(ApApprox apa |
+        flowIntoCallApa(call, arg, p, allowsFieldFlow, apa, config) and
+        fwdFlow(arg, _, _, _, _, ap, apa, config)
+      )
+    }
+
+    pragma[nomagic]
+    private predicate flowOutOfCallAp(
+      DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out, boolean allowsFieldFlow,
+      Ap ap, Configuration config
+    ) {
+      exists(ApApprox apa |
+        flowOutOfCallApa(call, ret, kind, out, allowsFieldFlow, apa, config) and
+        fwdFlow(ret, _, _, _, _, ap, apa, config)
      )
    }

@@ -1628,7 +1733,7 @@ private module MkStage<StageSig PrevStage> {
      // flow into a callable
      exists(ParamNodeEx p, boolean allowsFieldFlow |
        revFlow(p, state, TReturnCtxNone(), returnAp, ap, config) and
-        flowIntoCall(_, node, p, allowsFieldFlow, config) and
+        flowIntoCallAp(_, node, p, allowsFieldFlow, ap, config) and
        (if allowsFieldFlow = false then ap instanceof ApNil else any()) and
        returnCtx = TReturnCtxNone()
      )
@@ -1682,22 +1787,41 @@ private module MkStage<StageSig PrevStage> {
    ) {
      exists(NodeEx out, boolean allowsFieldFlow |
        revFlow(out, state, returnCtx, returnAp, ap, config) and
-        flowOutOfCall(call, ret, kind, out, allowsFieldFlow, config) and
+        flowOutOfCallAp(call, ret, kind, out, allowsFieldFlow, ap, config) and
        if allowsFieldFlow = false then ap instanceof ApNil else any()
      )
    }

+    /**
+     * Same as `flowThroughIntoCall`, but restricted to calls that are reached
+     * in the flow covered by `revFlow`, where data might flow through the target
+     * callable and back out at `call`.
+     */
+    pragma[nomagic]
+    private predicate revFlowThroughIntoCall(
+      DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Ap argAp,
+      Configuration config
+    ) {
+      flowThroughIntoCall(call, arg, p, allowsFieldFlow, argAp, config) and
+      revFlowIsReturned(call, _, _, _, _, config)
+    }
+
+    pragma[nomagic]
+    private predicate revFlowParamToReturn(
+      ParamNodeEx p, FlowState state, ReturnKindExt kind, Ap returnAp, Ap ap, Configuration config
+    ) {
+      revFlow(p, state, TReturnCtxMaybeFlowThrough(kind), apSome(returnAp), ap, config) and
+      parameterFlowThroughAllowed(p, kind)
+    }
+
    pragma[nomagic]
    private predicate revFlowInToReturn(
      DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnKindExt kind, Ap returnAp, Ap ap,
      Configuration config
    ) {
      exists(ParamNodeEx p, boolean allowsFieldFlow |
-        revFlow(pragma[only_bind_into](p), state,
-          TReturnCtxMaybeFlowThrough(pragma[only_bind_into](kind)), apSome(returnAp), ap, config) and
-        flowThroughIntoCall(call, arg, p, allowsFieldFlow, config) and
-        (if allowsFieldFlow = false then ap instanceof ApNil else any()) and
-        parameterFlowThroughAllowed(p, kind)
+        revFlowParamToReturn(p, state, kind, returnAp, ap, config) and
+        revFlowThroughIntoCall(call, arg, p, allowsFieldFlow, ap, config)
      )
    }

@@ -1750,6 +1874,11 @@ private module MkStage<StageSig PrevStage> {
    pragma[nomagic]
    predicate revFlow(NodeEx node, Configuration config) { revFlow(node, _, _, _, _, config) }

+    pragma[nomagic]
+    predicate revFlowAp(NodeEx node, Ap ap, Configuration config) {
+      revFlow(node, _, _, _, ap, config)
+    }
+
    // use an alias as a workaround for bad functionality-induced joins
    pragma[nomagic]
    additional predicate revFlowAlias(NodeEx node, Configuration config) {
@@ -1786,9 +1915,9 @@ private module MkStage<StageSig PrevStage> {

    pragma[nomagic]
    private predicate parameterFlowsThroughRev(
-      ParamNodeEx p, Ap ap, ReturnKindExt kind, Configuration config
+      ParamNodeEx p, Ap ap, ReturnKindExt kind, Ap returnAp, Configuration config
    ) {
-      revFlow(p, _, TReturnCtxMaybeFlowThrough(kind), apSome(_), ap, config) and
+      revFlow(p, _, TReturnCtxMaybeFlowThrough(kind), apSome(returnAp), ap, config) and
      parameterFlowThroughAllowed(p, kind)
    }

@@ -1796,27 +1925,36 @@ private module MkStage<StageSig PrevStage> {
    predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
      exists(RetNodeEx ret, ReturnKindExt kind |
        returnFlowsThrough(ret, kind, _, _, p, ap, _, config) and
-        parameterFlowsThroughRev(p, ap, kind, config)
+        parameterFlowsThroughRev(p, ap, kind, _, config)
      )
    }

    pragma[nomagic]
-    predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind, Configuration config) {
-      exists(ParamNodeEx p, Ap ap |
-        returnFlowsThrough(ret, kind, _, _, p, ap, _, config) and
-        parameterFlowsThroughRev(p, ap, kind, config)
+    predicate returnMayFlowThrough(
+      RetNodeEx ret, Ap argAp, Ap ap, ReturnKindExt kind, Configuration config
+    ) {
+      exists(ParamNodeEx p |
+        returnFlowsThrough(ret, kind, _, _, p, argAp, ap, config) and
+        parameterFlowsThroughRev(p, argAp, kind, ap, config)
+      )
+    }
+
+    pragma[nomagic]
+    predicate revFlowInToReturnIsReturned(
+      DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnCtx returnCtx, ApOption returnAp,
+      Ap ap, Configuration config
+    ) {
+      exists(ReturnKindExt returnKind0, Ap returnAp0 |
+        revFlowInToReturn(call, arg, state, returnKind0, returnAp0, ap, config) and
+        revFlowIsReturned(call, returnCtx, returnAp, returnKind0, returnAp0, config)
      )
    }

    pragma[nomagic]
    predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
-      exists(
-        ReturnKindExt returnKind0, Ap returnAp0, ArgNodeEx arg, FlowState state,
-        ReturnCtx returnCtx, ApOption returnAp, Ap ap
-      |
+      exists(ArgNodeEx arg, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap |
        revFlow(arg, state, returnCtx, returnAp, ap, config) and
-        revFlowInToReturn(call, arg, state, returnKind0, returnAp0, ap, config) and
-        revFlowIsReturned(call, returnCtx, returnAp, returnKind0, returnAp0, config)
+        revFlowInToReturnIsReturned(call, arg, state, returnCtx, returnAp, ap, config)
      )
    }

@@ -2179,16 +2317,16 @@ private module LocalFlowBigStep {
  pragma[nomagic]
  predicate localFlowBigStep(
    NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-    AccessPathFrontNil apf, Configuration config, LocalCallContext callContext
+    DataFlowType t, Configuration config, LocalCallContext callContext
  ) {
-    localFlowStepPlus(node1, state1, node2, preservesValue, apf.getType(), config, callContext) and
+    localFlowStepPlus(node1, state1, node2, preservesValue, t, config, callContext) and
    localFlowExit(node2, state1, config) and
    state1 = state2
    or
    additionalLocalFlowStepNodeCand2(node1, state1, node2, state2, config) and
    state1 != state2 and
    preservesValue = false and
-    apf = TFrontNil(node2.getDataFlowType()) and
+    t = node2.getDataFlowType() and
    callContext.relevantFor(node1.getEnclosingCallable()) and
    not exists(DataFlowCall call | call = callContext.(LocalCallContextSpecificCall).getCall() |
      isUnreachableInCallCached(node1.asNode(), call) or
@@ -2199,14 +2337,90 @@ private module LocalFlowBigStep {

 private import LocalFlowBigStep

-private module Stage3Param implements MkStage<Stage2>::StageParam {
+private module Stage2Point5Param implements MkStage<Stage2>::StageParam {
  private module PrevStage = Stage2;

+  class Ap = ApproxAccessPathFront;
+
+  class ApNil = ApproxAccessPathFrontNil;
+
+  PrevStage::Ap getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
+
+  ApNil getApNil(NodeEx node) {
+    PrevStage::revFlow(node, _) and result = TApproxFrontNil(node.getDataFlowType())
+  }
+
+  bindingset[tc, tail]
+  Ap apCons(TypedContent tc, Ap tail) { result.getAHead() = tc and exists(tail) }
+
+  pragma[noinline]
+  Content getHeadContent(Ap ap) { result = ap.getAHead().getContent() }
+
+  class ApOption = ApproxAccessPathFrontOption;
+
+  ApOption apNone() { result = TApproxAccessPathFrontNone() }
+
+  ApOption apSome(Ap ap) { result = TApproxAccessPathFrontSome(ap) }
+
+  import BooleanCallContext
+
+  predicate localStep(
+    NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
+    ApproxAccessPathFrontNil ap, Configuration config, LocalCc lcc
+  ) {
+    localFlowBigStep(node1, state1, node2, state2, preservesValue, ap.getType(), config, _) and
+    exists(lcc)
+  }
+
+  predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
+
+  predicate flowIntoCall = flowIntoCallNodeCand2/5;
+
+  pragma[nomagic]
+  private predicate expectsContentCand(NodeEx node, Ap ap, Configuration config) {
+    exists(Content c |
+      PrevStage::revFlow(node, pragma[only_bind_into](config)) and
+      PrevStage::readStepCand(_, c, _, pragma[only_bind_into](config)) and
+      expectsContentEx(node, c) and
+      c = ap.getAHead().getContent()
+    )
+  }
+
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
+  bindingset[node, state, ap, config]
+  predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
+    exists(state) and
+    exists(config) and
+    (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()) and
+    (
+      notExpectsContent(node)
+      or
+      expectsContentCand(node, ap, config)
+    )
+  }
+
+  bindingset[ap, contentType]
+  predicate typecheckStore(Ap ap, DataFlowType contentType) {
+    // We need to typecheck stores here, since reverse flow through a getter
+    // might have a different type here compared to inside the getter.
+    compatibleTypes(ap.getType(), contentType)
+  }
+}
+
+private module Stage2Point5 implements StageSig {
+  import MkStage<Stage2>::Stage<Stage2Point5Param>
+}
+
+private module Stage3Param implements MkStage<Stage2Point5>::StageParam {
+  private module PrevStage = Stage2Point5;
+
  class Ap = AccessPathFront;

  class ApNil = AccessPathFrontNil;

-  PrevStage::Ap getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
+  PrevStage::Ap getApprox(Ap ap) { result = ap.toApprox() }

  ApNil getApNil(NodeEx node) {
    PrevStage::revFlow(node, _) and result = TFrontNil(node.getDataFlowType())
@@ -2226,16 +2440,42 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {

  import BooleanCallContext

+  pragma[nomagic]
  predicate localStep(
    NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
    ApNil ap, Configuration config, LocalCc lcc
  ) {
-    localFlowBigStep(node1, state1, node2, state2, preservesValue, ap, config, _) and exists(lcc)
+    localFlowBigStep(node1, state1, node2, state2, preservesValue, ap.getType(), config, _) and
+    PrevStage::revFlow(node1, pragma[only_bind_into](state1), _, pragma[only_bind_into](config)) and
+    PrevStage::revFlowAlias(node2, pragma[only_bind_into](state2), _, pragma[only_bind_into](config)) and
+    exists(lcc)
  }

-  predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
+  pragma[nomagic]
+  predicate flowOutOfCall(
+    DataFlowCall call, RetNodeEx node1, ReturnKindExt kind, NodeEx node2, boolean allowsFieldFlow,
+    Configuration config
+  ) {
+    exists(FlowState state |
+      flowOutOfCallNodeCand2(call, node1, kind, node2, allowsFieldFlow, config) and
+      PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
+      PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
+        pragma[only_bind_into](config))
+    )
+  }

-  predicate flowIntoCall = flowIntoCallNodeCand2/5;
+  pragma[nomagic]
+  predicate flowIntoCall(
+    DataFlowCall call, ArgNodeEx node1, ParamNodeEx node2, boolean allowsFieldFlow,
+    Configuration config
+  ) {
+    exists(FlowState state |
+      flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
+      PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
+      PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
+        pragma[only_bind_into](config))
+    )
+  }

  pragma[nomagic]
  private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
@@ -2292,7 +2532,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
 }

 private module Stage3 implements StageSig {
-  import MkStage<Stage2>::Stage<Stage3Param>
+  import MkStage<Stage2Point5>::Stage<Stage3Param>
 }

 /**
@@ -2509,6 +2749,7 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {

  class ApNil = AccessPathApproxNil;

+  pragma[nomagic]
  PrevStage::Ap getApprox(Ap ap) { result = ap.getFront() }

  ApNil getApNil(NodeEx node) {
@@ -2534,7 +2775,9 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
    NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
    ApNil ap, Configuration config, LocalCc lcc
  ) {
-    localFlowBigStep(node1, state1, node2, state2, preservesValue, ap.getFront(), config, lcc)
+    localFlowBigStep(node1, state1, node2, state2, preservesValue, ap.getType(), config, lcc) and
+    PrevStage::revFlow(node1, pragma[only_bind_into](state1), _, pragma[only_bind_into](config)) and
+    PrevStage::revFlowAlias(node2, pragma[only_bind_into](state2), _, pragma[only_bind_into](config))
  }

  pragma[nomagic]
@@ -3347,7 +3590,8 @@ private predicate pathStep(
    AccessPath ap0, NodeEx midnode, FlowState state0, Configuration conf, LocalCallContext localCC
  |
    pathNode(mid, midnode, state0, cc, sc, ap0, conf, localCC) and
-    localFlowBigStep(midnode, state0, node, state, false, ap.getFront(), conf, localCC) and
+    localFlowBigStep(midnode, state0, node, state, false, ap.(AccessPathNil).getType(), conf,
+      localCC) and
    ap0 instanceof AccessPathNil
  )
  or
@@ -3735,6 +3979,14 @@ predicate stageStats(
  n = 25 and
  Stage2::stats(false, nodes, fields, conscand, states, tuples, config)
  or
+  stage = "2.5 Fwd" and
+  n = 25 and
+  Stage2Point5::stats(true, nodes, fields, conscand, states, tuples, config)
+  or
+  stage = "2.5 Rev" and
+  n = 27 and
+  Stage2Point5::stats(false, nodes, fields, conscand, states, tuples, config)
+  or
  stage = "3 Fwd" and
  n = 30 and
  Stage3::stats(true, nodes, fields, conscand, states, tuples, config)
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplCommon.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplCommon.qll
@@ -926,18 +926,46 @@ private module Cached {
    TReturnCtxNoFlowThrough() or
    TReturnCtxMaybeFlowThrough(ReturnKindExt kind)

+  cached
+  newtype TTypedContentApprox =
+    MkTypedContentApprox(ContentApprox c, DataFlowType t) {
+      exists(Content cont |
+        c = getContentApprox(cont) and
+        store(_, cont, _, _, t)
+      )
+    }
+
  cached
  newtype TTypedContent = MkTypedContent(Content c, DataFlowType t) { store(_, c, _, _, t) }

+  cached
+  TypedContent getATypedContent(TypedContentApprox c) {
+    exists(ContentApprox cls, DataFlowType t, Content cont |
+      c = MkTypedContentApprox(cls, pragma[only_bind_into](t)) and
+      result = MkTypedContent(cont, pragma[only_bind_into](t)) and
+      cls = getContentApprox(cont)
+    )
+  }
+
  cached
  newtype TAccessPathFront =
    TFrontNil(DataFlowType t) or
    TFrontHead(TypedContent tc)

+  cached
+  newtype TApproxAccessPathFront =
+    TApproxFrontNil(DataFlowType t) or
+    TApproxFrontHead(TypedContentApprox tc)
+
  cached
  newtype TAccessPathFrontOption =
    TAccessPathFrontNone() or
    TAccessPathFrontSome(AccessPathFront apf)
+
+  cached
+  newtype TApproxAccessPathFrontOption =
+    TApproxAccessPathFrontNone() or
+    TApproxAccessPathFrontSome(ApproxAccessPathFront apf)
 }

 /**
@@ -1353,6 +1381,75 @@ class ReturnCtx extends TReturnCtx {
  }
 }

+/** An approximated `Content` tagged with the type of a containing object. */
+class TypedContentApprox extends MkTypedContentApprox {
+  private ContentApprox c;
+  private DataFlowType t;
+
+  TypedContentApprox() { this = MkTypedContentApprox(c, t) }
+
+  /** Gets a typed content approximated by this value. */
+  TypedContent getATypedContent() { result = getATypedContent(this) }
+
+  /** Gets the container type. */
+  DataFlowType getContainerType() { result = t }
+
+  /** Gets a textual representation of this approximated content. */
+  string toString() { result = c.toString() }
+}
+
+/**
+ * The front of an approximated access path. This is either a head or a nil.
+ */
+abstract class ApproxAccessPathFront extends TApproxAccessPathFront {
+  abstract string toString();
+
+  abstract DataFlowType getType();
+
+  abstract boolean toBoolNonEmpty();
+
+  pragma[nomagic]
+  TypedContent getAHead() {
+    exists(TypedContentApprox cont |
+      this = TApproxFrontHead(cont) and
+      result = cont.getATypedContent()
+    )
+  }
+}
+
+class ApproxAccessPathFrontNil extends ApproxAccessPathFront, TApproxFrontNil {
+  private DataFlowType t;
+
+  ApproxAccessPathFrontNil() { this = TApproxFrontNil(t) }
+
+  override string toString() { result = ppReprType(t) }
+
+  override DataFlowType getType() { result = t }
+
+  override boolean toBoolNonEmpty() { result = false }
+}
+
+class ApproxAccessPathFrontHead extends ApproxAccessPathFront, TApproxFrontHead {
+  private TypedContentApprox tc;
+
+  ApproxAccessPathFrontHead() { this = TApproxFrontHead(tc) }
+
+  override string toString() { result = tc.toString() }
+
+  override DataFlowType getType() { result = tc.getContainerType() }
+
+  override boolean toBoolNonEmpty() { result = true }
+}
+
+/** An optional approximated access path front. */
+class ApproxAccessPathFrontOption extends TApproxAccessPathFrontOption {
+  string toString() {
+    this = TApproxAccessPathFrontNone() and result = "<none>"
+    or
+    this = TApproxAccessPathFrontSome(any(ApproxAccessPathFront apf | result = apf.toString()))
+  }
+}
+
 /** A `Content` tagged with the type of a containing object. */
 class TypedContent extends MkTypedContent {
  private Content c;
@@ -1385,7 +1482,7 @@ abstract class AccessPathFront extends TAccessPathFront {

  abstract DataFlowType getType();

-  abstract boolean toBoolNonEmpty();
+  abstract ApproxAccessPathFront toApprox();

  TypedContent getHead() { this = TFrontHead(result) }
 }
@@ -1399,7 +1496,7 @@ class AccessPathFrontNil extends AccessPathFront, TFrontNil {

  override DataFlowType getType() { result = t }

-  override boolean toBoolNonEmpty() { result = false }
+  override ApproxAccessPathFront toApprox() { result = TApproxFrontNil(t) }
 }

 class AccessPathFrontHead extends AccessPathFront, TFrontHead {
@@ -1411,7 +1508,7 @@ class AccessPathFrontHead extends AccessPathFront, TFrontHead {

  override DataFlowType getType() { result = tc.getContainerType() }

-  override boolean toBoolNonEmpty() { result = true }
+  override ApproxAccessPathFront toApprox() { result.getAHead() = tc }
 }

 /** An optional access path front. */
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplConsistency.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplConsistency.qll
@@ -260,4 +260,9 @@ module Consistency {
    not exists(unique(ParameterPosition pos0 | isParameterNode(p, c, pos0))) and
    msg = "Parameter node with multiple positions."
  }
+
+  query predicate uniqueContentApprox(Content c, string msg) {
+    not exists(unique(ContentApprox approx | approx = getContentApprox(c))) and
+    msg = "Non-unique content approximation."
+  }
 }
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
@@ -520,6 +520,13 @@ private module Cached {
      )
    )
  }
+
+  cached
+  newtype TContentApprox =
+    TUnknownElementContentApprox() or
+    TKnownIntegerElementContentApprox() or
+    TKnownElementContentApprox(string approx) { approx = approxKnownElementIndex(_) } or
+    TNonElementContentApprox(Content c) { not c instanceof Content::ElementContent }
 }

 class TElementContent = TKnownElementContent or TUnknownElementContent;
@@ -1370,3 +1377,58 @@ predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preserves
 predicate allowParameterReturnInSelf(ParameterNode p) {
  FlowSummaryImpl::Private::summaryAllowParameterReturnInSelf(p)
 }
+
+/** An approximated `Content`. */
+class ContentApprox extends TContentApprox {
+  string toString() {
+    this = TUnknownElementContentApprox() and
+    result = "element"
+    or
+    this = TKnownIntegerElementContentApprox() and
+    result = "approximated integer element"
+    or
+    exists(string approx |
+      this = TKnownElementContentApprox(approx) and
+      result = "approximated element " + approx
+    )
+    or
+    exists(Content c |
+      this = TNonElementContentApprox(c) and
+      result = c.toString()
+    )
+  }
+}
+
+/**
+ * Gets a string for approximating known element indices.
+ *
+ * We take two characters from the serialized index as the projection,
+ * since for symbols this will include the first character.
+ */
+private string approxKnownElementIndex(Content::KnownElementContent c) {
+  not c.getIndex().isInt(_) and
+  exists(string s | s = c.getIndex().serialize() |
+    s.length() < 2 and
+    result = s
+    or
+    result = s.prefix(2)
+    or
+    // workaround for `prefix` not working with Unicode characters
+    s.length() >= 2 and
+    not exists(s.prefix(2)) and
+    result = s
+  )
+}
+
+/** Gets an approximated value for content `c`. */
+ContentApprox getContentApprox(Content c) {
+  c instanceof Content::UnknownElementContent and
+  result = TUnknownElementContentApprox()
+  or
+  c.(Content::KnownElementContent).getIndex().isInt(_) and
+  result = TKnownIntegerElementContentApprox()
+  or
+  result = TKnownElementContentApprox(approxKnownElementIndex(c))
+  or
+  result = TNonElementContentApprox(c)
+}