Restrict TNodeReverse

shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll

@@ -1046,6 +1046,102 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
   }
 
   private module ReverseFlow {
+    module Cand {
+      /**
+       * Holds if `p` can flow to `node` in the same callable using only
+       * value-preserving steps.
+       *
+       * `read` indicates whether it is contents of `p` that can flow to `node`.
+       */
+      pragma[nomagic]
+      private predicate parameterValueFlowCand(ParamNode p, Node node) {
+        (
+          p = node
+          or
+          // local flow
+          exists(Node mid |
+            parameterValueFlowCand(p, mid) and
+            simpleLocalFlowStep(mid, node, _) and
+            validParameterAliasStep(mid, node)
+          )
+          or
+          // store
+          exists(Node mid |
+            parameterValueFlowCand(p, mid) and
+            Lang::storeStep(mid, _, node)
+          )
+          or
+          // read
+          exists(Node mid |
+            parameterValueFlowCand(p, mid) and
+            Lang::readStep(mid, _, node)
+          )
+          or
+          // flow through
+          exists(ArgNode arg |
+            parameterValueFlowArgCand(p, arg) and
+            argumentValueFlowsThroughCand(arg, node)
+          )
+        )
+      }
+
+      pragma[nomagic]
+      private predicate parameterValueFlowArgCand(ParamNode p, ArgNode arg) {
+        parameterValueFlowCand(p, arg)
+      }
+
+      pragma[nomagic]
+      predicate parameterValueFlowsToPreUpdateCand(ParamNode p, PostUpdateNode n) {
+        parameterValueFlowCand(p, n.getPreUpdateNode())
+      }
+
+      /**
+       * Holds if `p` can flow to a return node of kind `kind` in the same
+       * callable using only value-preserving steps, not taking call contexts
+       * into account.
+       *
+       * `read` indicates whether it is contents of `p` that can flow to the return
+       * node.
+       */
+      predicate parameterValueFlowReturnCand(ParamNode p, ReturnKind kind) {
+        exists(ReturnNode ret |
+          parameterValueFlowCand(p, ret) and
+          kind = ret.getKind()
+        )
+      }
+
+      pragma[nomagic]
+      private predicate argumentValueFlowsThroughCand0(
+        DataFlowCall call, ArgNode arg, ReturnKind kind
+      ) {
+        exists(ParamNode param | viableParamArg(call, param, arg) |
+          parameterValueFlowReturnCand(param, kind)
+        )
+      }
+
+      /**
+       * Holds if `arg` flows to `out` through a call using only value-preserving steps,
+       * not taking call contexts into account.
+       *
+       * `read` indicates whether it is contents of `arg` that can flow to `out`.
+       */
+      predicate argumentValueFlowsThroughCand(ArgNode arg, Node out) {
+        exists(DataFlowCall call, ReturnKind kind |
+          argumentValueFlowsThroughCand0(call, arg, kind) and
+          out = getAnOutNode(call, kind)
+        )
+      }
+
+      predicate cand(ParamNode p, Node n) {
+        parameterValueFlowCand(p, n) and
+        (
+          parameterValueFlowReturnCand(p, _)
+          or
+          parameterValueFlowsToPreUpdateCand(p, _)
+        )
+      }
+    }
+
     /**
      * Holds if the local step from `arg` to `out` actually models a flow-through
      * step.
@@ -2091,7 +2187,9 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
     newtype TNodeEx =
       TNodeNormal(Node n) or
       TNodeImplicitRead(Node n) or // will be restricted to nodes with actual implicit reads in `DataFlowImpl.qll`
-      TNodeReverse(Node n, Boolean allowFwdFlowOut)
+      TNodeReverse(Node n, Boolean allowFwdFlowOut) {
+        ReverseFlow::Cand::cand(_, n) or n = any(PostUpdateNode p).getPreUpdateNode()
+      }
 
     /**
      * Holds if data can flow in one local step from `node1` to `node2`.