wip2

shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

@@ -2606,23 +2606,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
           );
         }
 
-        /**
-         * A node where some checking is required, and hence the big-step relation
-         * is not allowed to step over.
-         */
-        additional class FlowCheckNode extends NodeEx {
-          FlowCheckNode() {
-            revFlow(this, _, _) and
-            (
-              castNode(this.asNode()) or
-              clearsContentCached(this.asNode(), _) or
-              expectsContentCached(this.asNode(), _) or
-              neverSkipInPathGraph(this.asNode()) or
-              Config::neverSkip(this.asNode())
-            )
-          }
-        }
-
         /**
          * Provides a big-step relation for local flow steps.
          *
@@ -2631,6 +2614,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
          * reachable in this stage.
          */
         additional module LocalFlowBigStep<LocalFlowBigStepInputSig Input> {
+          /**
+           * A node where some checking is required, and hence the big-step relation
+           * is not allowed to step over.
+           */
+          private class FlowCheckNode extends NodeEx {
+            FlowCheckNode() {
+              revFlow(this, _, _) and
+              (
+                castNode(this.asNode()) or
+                clearsContentCached(this.asNode(), _) or
+                expectsContentCached(this.asNode(), _) or
+                neverSkipInPathGraph(this.asNode()) or
+                Config::neverSkip(this.asNode())
+              )
+            }
+          }
+
           private predicate additionalLocalStateStep(
             NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, DataFlowType t,
             LocalCallContext lcc, string label
@@ -2647,7 +2647,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
            * Holds if `node` can be the first node in a maximal subsequence of local
            * flow steps in a dataflow path.
            */
-          private predicate localFlowEntry(NodeEx node, FlowState state, Ap ap) {
+          predicate localFlowEntry(NodeEx node, FlowState state, Ap ap) {
             revFlow(node, state, ap) and
             (
               sourceNode(node, state)
@@ -2679,7 +2679,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
            * Holds if `node` can be the last node in a maximal subsequence of local
            * flow steps in a dataflow path.
            */
-          private predicate localFlowExit(NodeEx node, FlowState state, Ap ap) {
+          predicate localFlowExit(NodeEx node, FlowState state, Ap ap) {
             revFlow(node, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and
             (
               exists(NodeEx next, Ap apNext | revFlow(next, pragma[only_bind_into](state), apNext) |
@@ -4409,46 +4409,28 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
       import LocalCallContext
 
       private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig {
-        private predicate smallStep = Stage3Param::BigStepInput::localStep/8;
-
-        private predicate localStepCand(
-          NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue
-        ) {
-          Stage5Param::localStep(node1, state1, _, _, _, _, _, _) and
-          smallStep(node1, state1, node2, state2, preservesValue, _, _, _)
-          or
-          exists(FlowState midState, NodeEx midNode |
-            localStepCand(node1, state1, midNode, midState, preservesValue) and
-            smallStep(midNode, midState, node2, state2, _, _, _, _) and
-            not (
-              Stage5Param::localStep(midNode, midState, _, _, _, _, _, _) and
-              Stage5Param::localStep(_, _, midNode, midState, _, _, _, _)
-            ) and
-            not midNode instanceof Stage5::FlowCheckNode
-          )
-        }
-
-        /**
-         * When calculating `localFlowBigStep` based on `Stage5Param::localStep`, which
-         * is already a big-step relation, we must be careful to avoid quadratic blowup.
-         *
-         * This is achieved by restricting `Stage5Param::localStep` to those node pairs
-         * reacheable via 1 or more `smallStep`s, where any intermediate node is not
-         * already part of `Stage5Param::localStep`.
-         */
-        pragma[nomagic]
-        predicate localStep(
-          NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
-          DataFlowType t, LocalCallContext lcc, string label
-        ) {
-          localStepCand(node1, state1, node2, state2, preservesValue) and
-          Stage5Param::localStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and
-          PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
-          PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
-        }
+        predicate localStep = Stage5Param::localStep/8;
       }
 
-      predicate localStep = PrevStage::LocalFlowBigStep<BigStepInput>::localFlowBigStep/8;
+      pragma[nomagic]
+      predicate localStep(
+        NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
+        DataFlowType t, LocalCallContext lcc, string label
+      ) {
+        // The following should be equivalent to
+        //
+        // ```
+        // PrevStage::LocalFlowBigStep<BigStepInput>::localFlowBigStep
+        // ```
+        //
+        // but avoids computing the big-step relation based on an existing big-step
+        // releation, which may have worst-case quadratic complexity.
+        exists(AccessPathApprox ap |
+          BigStepInput::localStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and
+          PrevStage::LocalFlowBigStep<BigStepInput>::localFlowEntry(node1, state1, ap) and
+          PrevStage::LocalFlowBigStep<BigStepInput>::localFlowExit(node2, state2, ap)
+        )
+      }
 
       bindingset[node, state, t0, ap]
       predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {