C++: Refactor ProductFlow to have a DataFlow::ConfigSig-like interface

2025-12-24 04:36:35 +01:00 · 2023-03-21 11:21:32 +01:00
parent c8798637fa
commit 4e12924521
4 changed files with 400 additions and 216 deletions
--- a/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll
@@ -1,17 +1,208 @@
 import semmle.code.cpp.ir.dataflow.DataFlow
-import semmle.code.cpp.ir.dataflow.DataFlow2

 module ProductFlow {
-  abstract class Configuration extends string {
-    bindingset[this]
-    Configuration() { any() }
-
+  signature module ConfigSig {
    /**
     * Holds if `(source1, source2)` is a relevant data flow source.
     *
     * `source1` and `source2` must belong to the same callable.
     */
-    predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) { none() }
+    predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2);
+
+    /**
+     * Holds if `(sink1, sink2)` is a relevant data flow sink.
+     *
+     * `sink1` and `sink2` must belong to the same callable.
+     */
+    predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2);
+
+    /**
+     * Holds if data flow through `node` is prohibited through the first projection of the product
+     * dataflow graph.
+     */
+    default predicate isBarrier1(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow through `node` is prohibited through the second projection of the product
+     * dataflow graph.
+     */
+    default predicate isBarrier2(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow out of `node` is prohibited in the first projection of the product
+     * dataflow graph.
+     */
+    default predicate isBarrierOut1(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow out of `node` is prohibited in the second projection of the product
+     * dataflow graph.
+     */
+    default predicate isBarrierOut2(DataFlow::Node node) { none() }
+
+    /*
+     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
+     * the first projection of the product dataflow graph.
+     */
+
+    default predicate isAdditionalFlowStep1(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+    /**
+     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
+     * the second projection of the product dataflow graph.
+     */
+    default predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+    /**
+     * Holds if data flow into `node` is prohibited in the first projection of the product
+     * dataflow graph.
+     */
+    default predicate isBarrierIn1(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow into `node` is prohibited in the second projection of the product
+     * dataflow graph.
+     */
+    default predicate isBarrierIn2(DataFlow::Node node) { none() }
+  }
+
+  module Make<ConfigSig Config> {
+    class PathNode1 = Flow1::PathNode;
+
+    class PathNode2 = Flow2::PathNode;
+
+    module PathGraph1 = Flow1::PathGraph;
+
+    module PathGraph2 = Flow2::PathGraph;
+
+    predicate hasFlowPath(PathNode1 source1, PathNode2 source2, PathNode1 sink1, PathNode2 sink2) {
+      reachable(source1, source2, sink1, sink2)
+    }
+
+    private module Config1 implements DataFlow::ConfigSig {
+      predicate isSource(DataFlow::Node source) { Config::isSourcePair(source, _) }
+
+      predicate isSink(DataFlow::Node sink) { Config::isSinkPair(sink, _) }
+
+      predicate isBarrier(DataFlow::Node node) { Config::isBarrier1(node) }
+
+      predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut1(node) }
+
+      predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+        Config::isAdditionalFlowStep1(node1, node2)
+      }
+
+      predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) }
+    }
+
+    private module Flow1 = DataFlow::Make<Config1>;
+
+    private module Config2 implements DataFlow::ConfigSig {
+      predicate isSource(DataFlow::Node source) {
+        exists(Flow1::PathNode source1 |
+          Config::isSourcePair(source1.getNode(), source) and
+          Flow1::hasFlowPath(source1, _)
+        )
+      }
+
+      predicate isSink(DataFlow::Node sink) {
+        exists(Flow1::PathNode sink1 |
+          Config::isSinkPair(sink1.getNode(), sink) and
+          Flow1::hasFlowPath(_, sink1)
+        )
+      }
+
+      predicate isBarrier(DataFlow::Node node) { Config::isBarrier2(node) }
+
+      predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut2(node) }
+
+      predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+        Config::isAdditionalFlowStep2(node1, node2)
+      }
+
+      predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) }
+    }
+
+    private module Flow2 = DataFlow::Make<Config2>;
+
+    pragma[nomagic]
+    private predicate reachableInterprocEntry(
+      Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode node1, Flow2::PathNode node2
+    ) {
+      Config::isSourcePair(node1.getNode(), node2.getNode()) and
+      node1 = source1 and
+      node2 = source2
+      or
+      exists(
+        Flow1::PathNode midEntry1, Flow2::PathNode midEntry2, Flow1::PathNode midExit1,
+        Flow2::PathNode midExit2
+      |
+        reachableInterprocEntry(source1, source2, midEntry1, midEntry2) and
+        interprocEdgePair(midExit1, midExit2, node1, node2) and
+        localPathStep1*(midEntry1, midExit1) and
+        localPathStep2*(midEntry2, midExit2)
+      )
+    }
+
+    private predicate localPathStep1(Flow1::PathNode pred, Flow1::PathNode succ) {
+      Flow1::PathGraph::edges(pred, succ) and
+      pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
+        pragma[only_bind_out](succ.getNode().getEnclosingCallable())
+    }
+
+    private predicate localPathStep2(Flow2::PathNode pred, Flow2::PathNode succ) {
+      Flow2::PathGraph::edges(pred, succ) and
+      pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
+        pragma[only_bind_out](succ.getNode().getEnclosingCallable())
+    }
+
+    pragma[nomagic]
+    private predicate interprocEdge1(
+      Declaration predDecl, Declaration succDecl, Flow1::PathNode pred1, Flow1::PathNode succ1
+    ) {
+      Flow1::PathGraph::edges(pred1, succ1) and
+      predDecl != succDecl and
+      pred1.getNode().getEnclosingCallable() = predDecl and
+      succ1.getNode().getEnclosingCallable() = succDecl
+    }
+
+    pragma[nomagic]
+    private predicate interprocEdge2(
+      Declaration predDecl, Declaration succDecl, Flow2::PathNode pred2, Flow2::PathNode succ2
+    ) {
+      Flow2::PathGraph::edges(pred2, succ2) and
+      predDecl != succDecl and
+      pred2.getNode().getEnclosingCallable() = predDecl and
+      succ2.getNode().getEnclosingCallable() = succDecl
+    }
+
+    private predicate interprocEdgePair(
+      Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2
+    ) {
+      exists(Declaration predDecl, Declaration succDecl |
+        interprocEdge1(predDecl, succDecl, pred1, succ1) and
+        interprocEdge2(predDecl, succDecl, pred2, succ2)
+      )
+    }
+
+    private predicate reachable(
+      Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2
+    ) {
+      exists(Flow1::PathNode mid1, Flow2::PathNode mid2 |
+        reachableInterprocEntry(source1, source2, mid1, mid2) and
+        Config::isSinkPair(sink1.getNode(), sink2.getNode()) and
+        localPathStep1*(mid1, sink1) and
+        localPathStep2*(mid2, sink2)
+      )
+    }
+  }
+
+  signature module StateConfigSig {
+    bindingset[this]
+    class FlowState1;
+
+    bindingset[this]
+    class FlowState2;

    /**
     * Holds if `(source1, source2)` is a relevant data flow source with initial states `state1`
@@ -20,20 +211,8 @@ module ProductFlow {
     * `source1` and `source2` must belong to the same callable.
     */
    predicate isSourcePair(
-      DataFlow::Node source1, DataFlow::FlowState state1, DataFlow::Node source2,
-      DataFlow::FlowState state2
-    ) {
-      state1 = "" and
-      state2 = "" and
-      this.isSourcePair(source1, source2)
-    }
-
-    /**
-     * Holds if `(sink1, sink2)` is a relevant data flow sink.
-     *
-     * `sink1` and `sink2` must belong to the same callable.
-     */
-    predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) { none() }
+      DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
+    );

    /**
     * Holds if `(sink1, sink2)` is a relevant data flow sink with final states `state1`
@@ -42,60 +221,51 @@ module ProductFlow {
     * `sink1` and `sink2` must belong to the same callable.
     */
    predicate isSinkPair(
-      DataFlow::Node sink1, DataFlow::FlowState state1, DataFlow::Node sink2,
-      DataFlow::FlowState state2
-    ) {
-      state1 = "" and
-      state2 = "" and
-      this.isSinkPair(sink1, sink2)
-    }
+      DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
+    );

    /**
     * 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, DataFlow::FlowState state) {
-      this.isBarrier1(node) and state = ""
-    }
+    predicate isBarrier1(DataFlow::Node node, FlowState1 state);

    /**
     * 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, DataFlow::FlowState state) {
-      this.isBarrier2(node) and state = ""
-    }
+    predicate isBarrier2(DataFlow::Node node, FlowState2 state);

    /**
     * Holds if data flow through `node` is prohibited through the first projection of the product
     * dataflow graph.
     */
-    predicate isBarrier1(DataFlow::Node node) { none() }
+    default predicate isBarrier1(DataFlow::Node node) { none() }

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

    /**
     * Holds if data flow out of `node` is prohibited in the first projection of the product
     * dataflow graph.
     */
-    predicate isBarrierOut1(DataFlow::Node node) { none() }
+    default predicate isBarrierOut1(DataFlow::Node node) { none() }

    /**
     * Holds if data flow out of `node` is prohibited in the second projection of the product
     * dataflow graph.
     */
-    predicate isBarrierOut2(DataFlow::Node node) { none() }
+    default predicate isBarrierOut2(DataFlow::Node node) { none() }

    /*
     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
     * the first projection of the product dataflow graph.
     */

-    predicate isAdditionalFlowStep1(DataFlow::Node node1, DataFlow::Node node2) { none() }
+    default predicate isAdditionalFlowStep1(DataFlow::Node node1, DataFlow::Node node2) { none() }

    /**
     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
@@ -104,19 +274,14 @@ module ProductFlow {
     * This step is only applicable in `state1` and updates the flow state to `state2`.
     */
    predicate isAdditionalFlowStep1(
-      DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
-      DataFlow::FlowState state2
-    ) {
-      state1 instanceof DataFlow::FlowStateEmpty and
-      state2 instanceof DataFlow::FlowStateEmpty and
-      this.isAdditionalFlowStep1(node1, node2)
-    }
+      DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
+    );

    /**
     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
     * the second projection of the product dataflow graph.
     */
-    predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() }
+    default predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() }

    /**
     * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
@@ -125,177 +290,168 @@ module ProductFlow {
     * This step is only applicable in `state1` and updates the flow state to `state2`.
     */
    predicate isAdditionalFlowStep2(
-      DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
-      DataFlow::FlowState state2
-    ) {
-      state1 instanceof DataFlow::FlowStateEmpty and
-      state2 instanceof DataFlow::FlowStateEmpty and
-      this.isAdditionalFlowStep2(node1, node2)
-    }
+      DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
+    );

    /**
     * Holds if data flow into `node` is prohibited in the first projection of the product
     * dataflow graph.
     */
-    predicate isBarrierIn1(DataFlow::Node node) { none() }
+    default predicate isBarrierIn1(DataFlow::Node node) { none() }

    /**
     * Holds if data flow into `node` is prohibited in the second projection of the product
     * dataflow graph.
     */
-    predicate isBarrierIn2(DataFlow::Node node) { none() }
+    default predicate isBarrierIn2(DataFlow::Node node) { none() }
+  }
+
+  module MakeWithState<StateConfigSig Config> {
+    class PathNode1 = Flow1::PathNode;
+
+    class PathNode2 = Flow2::PathNode;
+
+    module PathGraph1 = Flow1::PathGraph;
+
+    module PathGraph2 = Flow2::PathGraph;
+
+    class FlowState1 = Config::FlowState1;
+
+    class FlowState2 = Config::FlowState2;

    predicate hasFlowPath(
-      DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
-      DataFlow2::PathNode sink2
+      Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2
    ) {
-      reachable(this, source1, source2, sink1, sink2)
+      reachable(source1, source2, sink1, sink2)
    }
-  }

-  private import Internal
+    private module Config1 implements DataFlow::StateConfigSig {
+      class FlowState = FlowState1;

-  module Internal {
-    class Conf1 extends DataFlow::Configuration {
-      Conf1() { this = "Conf1" }
-
-      override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
-        exists(Configuration conf | conf.isSourcePair(source, state, _, _))
+      predicate isSource(DataFlow::Node source, FlowState state) {
+        Config::isSourcePair(source, state, _, _)
      }

-      override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) {
-        exists(Configuration conf | conf.isSinkPair(sink, state, _, _))
+      predicate isSink(DataFlow::Node sink, FlowState state) {
+        Config::isSinkPair(sink, state, _, _)
      }

-      override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
-        exists(Configuration conf | conf.isBarrier1(node, state))
-      }
+      predicate isBarrier(DataFlow::Node node, FlowState state) { Config::isBarrier1(node, state) }

-      override predicate isBarrierOut(DataFlow::Node node) {
-        exists(Configuration conf | conf.isBarrierOut1(node))
-      }
+      predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut1(node) }

-      override predicate isAdditionalFlowStep(
-        DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
-        DataFlow::FlowState state2
+      predicate isAdditionalFlowStep(
+        DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState state2
      ) {
-        exists(Configuration conf | conf.isAdditionalFlowStep1(node1, state1, node2, state2))
+        Config::isAdditionalFlowStep1(node1, state1, node2, state2)
      }

-      override predicate isBarrierIn(DataFlow::Node node) {
-        exists(Configuration conf | conf.isBarrierIn1(node))
-      }
+      predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) }
    }

-    class Conf2 extends DataFlow2::Configuration {
-      Conf2() { this = "Conf2" }
+    module Flow1 = DataFlow::MakeWithState<Config1>;

-      override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
-        exists(Configuration conf, DataFlow::PathNode source1 |
-          conf.isSourcePair(source1.getNode(), source1.getState(), source, state) and
-          any(Conf1 c).hasFlowPath(source1, _)
+    module Config2 implements DataFlow::StateConfigSig {
+      class FlowState = FlowState2;
+
+      predicate isSource(DataFlow::Node source, FlowState state) {
+        exists(Flow1::PathNode source1 |
+          Config::isSourcePair(source1.getNode(), source1.getState(), source, state) and
+          Flow1::hasFlowPath(source1, _)
        )
      }

-      override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) {
-        exists(Configuration conf, DataFlow::PathNode sink1 |
-          conf.isSinkPair(sink1.getNode(), sink1.getState(), sink, state) and
-          any(Conf1 c).hasFlowPath(_, sink1)
+      predicate isSink(DataFlow::Node sink, FlowState state) {
+        exists(Flow1::PathNode sink1 |
+          Config::isSinkPair(sink1.getNode(), sink1.getState(), sink, state) and
+          Flow1::hasFlowPath(_, sink1)
        )
      }

-      override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
-        exists(Configuration conf | conf.isBarrier2(node, state))
-      }
+      predicate isBarrier(DataFlow::Node node, FlowState state) { Config::isBarrier2(node, state) }

-      override predicate isBarrierOut(DataFlow::Node node) {
-        exists(Configuration conf | conf.isBarrierOut2(node))
-      }
+      predicate isBarrierOut(DataFlow::Node node) { Config::isBarrierOut2(node) }

-      override predicate isAdditionalFlowStep(
-        DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
-        DataFlow::FlowState state2
+      predicate isAdditionalFlowStep(
+        DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2
      ) {
-        exists(Configuration conf | conf.isAdditionalFlowStep2(node1, state1, node2, state2))
+        Config::isAdditionalFlowStep2(node1, state1, node2, state2)
      }

-      override predicate isBarrierIn(DataFlow::Node node) {
-        exists(Configuration conf | conf.isBarrierIn2(node))
-      }
+      predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) }
    }
-  }

-  pragma[nomagic]
-  private predicate reachableInterprocEntry(
-    Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
-    DataFlow::PathNode node1, DataFlow2::PathNode node2
-  ) {
-    conf.isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and
-    node1 = source1 and
-    node2 = source2
-    or
-    exists(
-      DataFlow::PathNode midEntry1, DataFlow2::PathNode midEntry2, DataFlow::PathNode midExit1,
-      DataFlow2::PathNode midExit2
-    |
-      reachableInterprocEntry(conf, source1, source2, midEntry1, midEntry2) and
-      interprocEdgePair(midExit1, midExit2, node1, node2) and
-      localPathStep1*(midEntry1, midExit1) and
-      localPathStep2*(midEntry2, midExit2)
-    )
-  }
+    module Flow2 = DataFlow::MakeWithState<Config2>;

-  private predicate localPathStep1(DataFlow::PathNode pred, DataFlow::PathNode succ) {
-    DataFlow::PathGraph::edges(pred, succ) and
-    pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
-      pragma[only_bind_out](succ.getNode().getEnclosingCallable())
-  }
+    pragma[nomagic]
+    private predicate reachableInterprocEntry(
+      Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode node1, Flow2::PathNode node2
+    ) {
+      Config::isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and
+      node1 = source1 and
+      node2 = source2
+      or
+      exists(
+        Flow1::PathNode midEntry1, Flow2::PathNode midEntry2, Flow1::PathNode midExit1,
+        Flow2::PathNode midExit2
+      |
+        reachableInterprocEntry(source1, source2, midEntry1, midEntry2) and
+        interprocEdgePair(midExit1, midExit2, node1, node2) and
+        localPathStep1*(midEntry1, midExit1) and
+        localPathStep2*(midEntry2, midExit2)
+      )
+    }

-  private predicate localPathStep2(DataFlow2::PathNode pred, DataFlow2::PathNode succ) {
-    DataFlow2::PathGraph::edges(pred, succ) and
-    pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
-      pragma[only_bind_out](succ.getNode().getEnclosingCallable())
-  }
+    private predicate localPathStep1(Flow1::PathNode pred, Flow1::PathNode succ) {
+      Flow1::PathGraph::edges(pred, succ) and
+      pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
+        pragma[only_bind_out](succ.getNode().getEnclosingCallable())
+    }

-  pragma[nomagic]
-  private predicate interprocEdge1(
-    Declaration predDecl, Declaration succDecl, DataFlow::PathNode pred1, DataFlow::PathNode succ1
-  ) {
-    DataFlow::PathGraph::edges(pred1, succ1) and
-    predDecl != succDecl and
-    pred1.getNode().getEnclosingCallable() = predDecl and
-    succ1.getNode().getEnclosingCallable() = succDecl
-  }
+    private predicate localPathStep2(Flow2::PathNode pred, Flow2::PathNode succ) {
+      Flow2::PathGraph::edges(pred, succ) and
+      pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
+        pragma[only_bind_out](succ.getNode().getEnclosingCallable())
+    }

-  pragma[nomagic]
-  private predicate interprocEdge2(
-    Declaration predDecl, Declaration succDecl, DataFlow2::PathNode pred2, DataFlow2::PathNode succ2
-  ) {
-    DataFlow2::PathGraph::edges(pred2, succ2) and
-    predDecl != succDecl and
-    pred2.getNode().getEnclosingCallable() = predDecl and
-    succ2.getNode().getEnclosingCallable() = succDecl
-  }
+    pragma[nomagic]
+    private predicate interprocEdge1(
+      Declaration predDecl, Declaration succDecl, Flow1::PathNode pred1, Flow1::PathNode succ1
+    ) {
+      Flow1::PathGraph::edges(pred1, succ1) and
+      predDecl != succDecl and
+      pred1.getNode().getEnclosingCallable() = predDecl and
+      succ1.getNode().getEnclosingCallable() = succDecl
+    }

-  private predicate interprocEdgePair(
-    DataFlow::PathNode pred1, DataFlow2::PathNode pred2, DataFlow::PathNode succ1,
-    DataFlow2::PathNode succ2
-  ) {
-    exists(Declaration predDecl, Declaration succDecl |
-      interprocEdge1(predDecl, succDecl, pred1, succ1) and
-      interprocEdge2(predDecl, succDecl, pred2, succ2)
-    )
-  }
+    pragma[nomagic]
+    private predicate interprocEdge2(
+      Declaration predDecl, Declaration succDecl, Flow2::PathNode pred2, Flow2::PathNode succ2
+    ) {
+      Flow2::PathGraph::edges(pred2, succ2) and
+      predDecl != succDecl and
+      pred2.getNode().getEnclosingCallable() = predDecl and
+      succ2.getNode().getEnclosingCallable() = succDecl
+    }

-  private predicate reachable(
-    Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
-    DataFlow::PathNode sink1, DataFlow2::PathNode sink2
-  ) {
-    exists(DataFlow::PathNode mid1, DataFlow2::PathNode mid2 |
-      reachableInterprocEntry(conf, source1, source2, mid1, mid2) and
-      conf.isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and
-      localPathStep1*(mid1, sink1) and
-      localPathStep2*(mid2, sink2)
-    )
+    private predicate interprocEdgePair(
+      Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2
+    ) {
+      exists(Declaration predDecl, Declaration succDecl |
+        interprocEdge1(predDecl, succDecl, pred1, succ1) and
+        interprocEdge2(predDecl, succDecl, pred2, succ2)
+      )
+    }
+
+    private predicate reachable(
+      Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2
+    ) {
+      exists(Flow1::PathNode mid1, Flow2::PathNode mid2 |
+        reachableInterprocEntry(source1, source2, mid1, mid2) and
+        Config::isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and
+        localPathStep1*(mid1, sink1) and
+        localPathStep2*(mid2, sink2)
+      )
+    }
  }
 }
--- a/Bugs/ArrayAccessProductFlow.ql
+++ b/Bugs/ArrayAccessProductFlow.ql
@@ -18,7 +18,7 @@ import semmle.code.cpp.ir.IR
 import semmle.code.cpp.valuenumbering.GlobalValueNumbering
 import semmle.code.cpp.models.interfaces.Allocation
 import semmle.code.cpp.ir.IRConfiguration
-import DataFlow::PathGraph
+import ArraySizeFlow::PathGraph1

 // temporary - custom allocator for ffmpeg
 class AvBufferAlloc extends AllocationFunction {
@@ -39,14 +39,12 @@ predicate bounded(Instruction i, Bound b, int delta, boolean upper) {
  semBounded(getSemanticExpr(i), b, delta, upper, _)
 }

-class ArraySizeConfiguration extends ProductFlow::Configuration {
-  ArraySizeConfiguration() { this = "ArraySizeConfiguration" }
-
-  override predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) {
+module ArraySizeConfig implements ProductFlow::ConfigSig {
+  predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) {
    source1.asConvertedExpr().(AllocationExpr).getSizeExpr() = source2.asConvertedExpr()
  }

-  override predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) {
+  predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) {
    exists(PointerAddInstruction pai, int delta |
      isSinkPair1(sink1, sink2, pai, delta) and
      (
@@ -63,6 +61,8 @@ class ArraySizeConfiguration extends ProductFlow::Configuration {
  }
 }

+module ArraySizeFlow = ProductFlow::Make<ArraySizeConfig>;
+
 pragma[nomagic]
 predicate isSinkPair1(
  DataFlow::Node sink1, DataFlow::Node sink2, PointerAddInstruction pai, int delta
@@ -76,9 +76,9 @@ predicate isSinkPair1(
 }

 from
-  ArraySizeConfiguration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
-  DataFlow::PathNode sink1, DataFlow2::PathNode sink2
-where conf.hasFlowPath(source1, source2, sink1, sink2)
-// TODO: pull delta out and display it
+  ArraySizeFlow::PathNode1 source1, ArraySizeFlow::PathNode2 source2,
+  ArraySizeFlow::PathNode1 sink1, ArraySizeFlow::PathNode2 sink2
+where ArraySizeFlow::hasFlowPath(source1, source2, sink1, sink2)
+// TODO: pull delta osut and display it
 select sink1.getNode(), source1, sink1, "Off-by one error allocated at $@ bounded by $@.", source1,
  source1.toString(), sink2, sink2.toString()
--- a/Bugs/OverrunWriteProductFlow.ql
+++ b/Bugs/OverrunWriteProductFlow.ql
@@ -19,7 +19,7 @@ import semmle.code.cpp.models.interfaces.Allocation
 import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
-import DataFlow::PathGraph
+import StringSizeFlow::PathGraph1

 pragma[nomagic]
 Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -77,12 +77,13 @@ predicate isSinkPairImpl(
  )
 }

-class StringSizeConfiguration extends ProductFlow::Configuration {
-  StringSizeConfiguration() { this = "StringSizeConfiguration" }
+module StringSizeConfig implements ProductFlow::StateConfigSig {
+  class FlowState1 = string;

-  override predicate isSourcePair(
-    DataFlow::Node bufSource, DataFlow::FlowState state1, DataFlow::Node sizeSource,
-    DataFlow::FlowState state2
+  class FlowState2 = string;
+
+  predicate isSourcePair(
+    DataFlow::Node bufSource, FlowState1 state1, DataFlow::Node sizeSource, FlowState2 state2
  ) {
    // In the case of an allocation like
    // ```cpp
@@ -94,9 +95,8 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
    hasSize(bufSource.asConvertedExpr(), sizeSource, state2)
  }

-  override predicate isSinkPair(
-    DataFlow::Node bufSink, DataFlow::FlowState state1, DataFlow::Node sizeSink,
-    DataFlow::FlowState state2
+  predicate isSinkPair(
+    DataFlow::Node bufSink, FlowState1 state1, DataFlow::Node sizeSink, FlowState2 state2
  ) {
    state1 instanceof DataFlow::FlowStateEmpty and
    state2 = [-32 .. 32].toString() and // An arbitrary bound because we need to bound `state2`
@@ -106,9 +106,18 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
    )
  }

-  override predicate isAdditionalFlowStep2(
-    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
-    DataFlow::FlowState state2
+  predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
+
+  predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
+
+  predicate isAdditionalFlowStep1(
+    DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState2 state2
+  ) {
+    none()
+  }
+
+  predicate isAdditionalFlowStep2(
+    DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState2 state2
  ) {
    exists(AddInstruction add, Operand op, int delta, int s1, int s2 |
      s1 = [-32 .. 32] and // An arbitrary bound because we need to bound `state`
@@ -122,12 +131,14 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
  }
 }

+module StringSizeFlow = ProductFlow::MakeWithState<StringSizeConfig>;
+
 from
-  StringSizeConfiguration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
-  DataFlow::PathNode sink1, DataFlow2::PathNode sink2, int overflow, int sinkState,
+  StringSizeFlow::PathNode1 source1, StringSizeFlow::PathNode2 source2,
+  StringSizeFlow::PathNode1 sink1, StringSizeFlow::PathNode2 sink2, int overflow, int sinkState,
  CallInstruction c, DataFlow::Node sourceNode, Expr buffer, string element
 where
-  conf.hasFlowPath(source1, source2, sink1, sink2) and
+  StringSizeFlow::hasFlowPath(source1, source2, sink1, sink2) and
  sinkState = sink2.getState().toInt() and
  isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and
  overflow > 0 and
--- a/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql
+++ b/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql
@@ -107,11 +107,13 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, string state)
 * Finally, the range-analysis library will find a load from (or store to) an address that
 * is non-strictly upper-bounded by `end` (which in this case is `*p`).
 */
-class AllocToInvalidPointerConf extends ProductFlow::Configuration {
-  AllocToInvalidPointerConf() { this = "AllocToInvalidPointerConf" }
+module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
+  class FlowState1 = string;

-  override predicate isSourcePair(
-    DataFlow::Node source1, string state1, DataFlow::Node source2, string state2
+  class FlowState2 = string;
+
+  predicate isSourcePair(
+    DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
  ) {
    // In the case of an allocation like
    // ```cpp
@@ -123,9 +125,8 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
    hasSize(source1.asConvertedExpr(), source2, state2)
  }

-  override predicate isSinkPair(
-    DataFlow::Node sink1, DataFlow::FlowState state1, DataFlow::Node sink2,
-    DataFlow::FlowState state2
+  predicate isSinkPair(
+    DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
  ) {
    state1 = "" and
    // We check that the delta computed by the range analysis matches the
@@ -136,13 +137,31 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
    )
  }

-  override predicate isBarrierOut2(DataFlow::Node node) {
+  predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
+
+  predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
+
+  predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
+
+  predicate isBarrierOut2(DataFlow::Node node) {
    node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
  }

-  override predicate isBarrierIn1(DataFlow::Node node) { this.isSourcePair(node, _, _, _) }
+  predicate isAdditionalFlowStep1(
+    DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
+  ) {
+    none()
+  }
+
+  predicate isAdditionalFlowStep2(
+    DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
+  ) {
+    none()
+  }
 }

+module AllocToInvalidPointerFlow = ProductFlow::MakeWithState<AllocToInvalidPointerConfig>;
+
 /**
 * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
 * left operand of the pointer-arithmetic operation.
@@ -224,9 +243,9 @@ module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>
 predicate invalidPointerToDerefSource(
  PointerArithmeticInstruction pai, DataFlow::Node source, int delta
 ) {
-  exists(ProductFlow::Configuration conf, DataFlow::PathNode p, DataFlow::Node sink1 |
+  exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 |
    pragma[only_bind_out](p.getNode()) = sink1 and
-    conf.hasFlowPath(_, _, pragma[only_bind_into](p), _) and
+    AllocToInvalidPointerFlow::hasFlowPath(_, _, pragma[only_bind_into](p), _) and
    isSinkImpl(pai, sink1, _, _) and
    bounded2(source.asInstruction(), pai, delta) and
    delta >= 0
@@ -235,7 +254,7 @@ predicate invalidPointerToDerefSource(

 newtype TMergedPathNode =
  // The path nodes computed by the first projection of `AllocToInvalidPointerConf`
-  TPathNode1(DataFlow::PathNode p) or
+  TPathNode1(AllocToInvalidPointerFlow::PathNode1 p) or
  // The path nodes computed by `InvalidPointerToDerefConf`
  TPathNode3(InvalidPointerToDerefFlow::PathNode p) or
  // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConf`.
@@ -251,7 +270,7 @@ newtype TMergedPathNode =
 class MergedPathNode extends TMergedPathNode {
  string toString() { none() }

-  final DataFlow::PathNode asPathNode1() { this = TPathNode1(result) }
+  final AllocToInvalidPointerFlow::PathNode1 asPathNode1() { this = TPathNode1(result) }

  final InvalidPointerToDerefFlow::PathNode asPathNode3() { this = TPathNode3(result) }

@@ -266,7 +285,7 @@ class MergedPathNode extends TMergedPathNode {

 class PathNode1 extends MergedPathNode, TPathNode1 {
  override string toString() {
-    exists(DataFlow::PathNode p |
+    exists(AllocToInvalidPointerFlow::PathNode1 p |
      this = TPathNode1(p) and
      result = p.toString()
    )
@@ -326,7 +345,8 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
 * of `InvalidPointerToDerefConf`, and they are connected through `pai`.
 */
 predicate joinOn1(
-  PointerArithmeticInstruction pai, DataFlow::PathNode p1, InvalidPointerToDerefFlow::PathNode p2
+  PointerArithmeticInstruction pai, AllocToInvalidPointerFlow::PathNode1 p1,
+  InvalidPointerToDerefFlow::PathNode p2
 ) {
  isSinkImpl(pai, p1.getNode(), _, _) and
  invalidPointerToDerefSource(pai, p2.getNode(), _)
@@ -346,11 +366,8 @@ predicate hasFlowPath(
  MergedPathNode source1, MergedPathNode sink, InvalidPointerToDerefFlow::PathNode source3,
  PointerArithmeticInstruction pai, string operation
 ) {
-  exists(
-    AllocToInvalidPointerConf conf1, InvalidPointerToDerefFlow::PathNode sink3,
-    DataFlow::PathNode sink1
-  |
-    conf1.hasFlowPath(source1.asPathNode1(), _, sink1, _) and
+  exists(InvalidPointerToDerefFlow::PathNode sink3, AllocToInvalidPointerFlow::PathNode1 sink1 |
+    AllocToInvalidPointerFlow::hasFlowPath(source1.asPathNode1(), _, sink1, _) and
    joinOn1(pai, sink1, source3) and
    InvalidPointerToDerefFlow::flowPath(source3, sink3) and
    joinOn2(sink3, sink.asSinkNode(), operation)