Merge pull request #12615 from jketema/product-configsig

C++: Refactor `ProductFlow` to have a `DataFlow::ConfigSig`-like interface
2026-04-24 00:05:14 +02:00 · 2023-04-06 19:41:46 +02:00
parent e2cb209f95 12702b59d3
commit 5ee9711f03
4 changed files with 357 additions and 233 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,146 @@
 import semmle.code.cpp.ir.dataflow.DataFlow
-import semmle.code.cpp.ir.dataflow.DataFlow2
+private import codeql.util.Unit

 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 Global<ConfigSig Config> {
+    private module StateConfig implements StateConfigSig {
+      class FlowState1 = Unit;
+
+      class FlowState2 = Unit;
+
+      predicate isSourcePair(
+        DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
+      ) {
+        exists(state1) and
+        exists(state2) and
+        Config::isSourcePair(source1, source2)
+      }
+
+      predicate isSinkPair(
+        DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
+      ) {
+        exists(state1) and
+        exists(state2) and
+        Config::isSinkPair(sink1, sink2)
+      }
+
+      predicate isBarrier1(DataFlow::Node node, FlowState1 state) {
+        exists(state) and
+        Config::isBarrier1(node)
+      }
+
+      predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
+        exists(state) and
+        Config::isBarrier2(node)
+      }
+
+      predicate isBarrier1 = Config::isBarrier1/1;
+
+      predicate isBarrier2 = Config::isBarrier2/1;
+
+      predicate isBarrierOut1 = Config::isBarrierOut1/1;
+
+      predicate isBarrierOut2 = Config::isBarrierOut2/1;
+
+      predicate isAdditionalFlowStep1 = Config::isAdditionalFlowStep1/2;
+
+      predicate isAdditionalFlowStep1(
+        DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
+      ) {
+        exists(state1) and
+        exists(state2) and
+        Config::isAdditionalFlowStep1(node1, node2)
+      }
+
+      predicate isAdditionalFlowStep2 = Config::isAdditionalFlowStep2/2;
+
+      predicate isAdditionalFlowStep2(
+        DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
+      ) {
+        exists(state1) and
+        exists(state2) and
+        Config::isAdditionalFlowStep2(node1, node2)
+      }
+
+      predicate isBarrierIn1 = Config::isBarrierIn1/1;
+
+      predicate isBarrierIn2 = Config::isBarrierIn2/1;
+    }
+
+    import GlobalWithState<StateConfig>
+  }
+
+  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 +149,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 +159,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 +212,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 +228,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() }
+  }

-    predicate hasFlowPath(
-      DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
-      DataFlow2::PathNode sink2
+  module GlobalWithState<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 flowPath(
+      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::GlobalWithState<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::flowPath(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::flowPath(_, 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::GlobalWithState<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::Global<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)
+  ArraySizeFlow::PathNode1 source1, ArraySizeFlow::PathNode2 source2,
+  ArraySizeFlow::PathNode1 sink1, ArraySizeFlow::PathNode2 sink2
+where ArraySizeFlow::flowPath(source1, source2, sink1, sink2)
 // TODO: pull delta out 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,8 @@ 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
+import codeql.util.Unit

 pragma[nomagic]
 Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -46,7 +47,7 @@ VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
 * Holds if `(n, state)` pair represents the source of flow for the size
 * expression associated with `alloc`.
 */
-predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
+predicate hasSize(AllocationExpr alloc, DataFlow::Node n, int state) {
  exists(VariableAccess va, Expr size, int delta |
    size = alloc.getSizeExpr() and
    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
@@ -55,7 +56,7 @@ predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
    bounded(any(Instruction instr | instr.getUnconvertedResultExpression() = size),
      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
    n.asConvertedExpr() = va.getFullyConverted() and
-    state = delta.toString()
+    state = delta
  )
 }

@@ -77,12 +78,13 @@ predicate isSinkPairImpl(
  )
 }

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

-  override predicate isSourcePair(
-    DataFlow::Node bufSource, DataFlow::FlowState state1, DataFlow::Node sizeSource,
-    DataFlow::FlowState state2
+  class FlowState2 = int;
+
+  predicate isSourcePair(
+    DataFlow::Node bufSource, FlowState1 state1, DataFlow::Node sizeSource, FlowState2 state2
  ) {
    // In the case of an allocation like
    // ```cpp
@@ -90,30 +92,38 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
    // ```
    // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
    // to the size of the allocation. This state is then checked in `isSinkPair`.
-    state1 instanceof DataFlow::FlowStateEmpty and
+    exists(state1) and
    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`
+    exists(state1) and
+    state2 = [-32 .. 32] and // An arbitrary bound because we need to bound `state2`
    exists(int delta |
      isSinkPairImpl(_, bufSink, sizeSink, delta, _) and
-      delta > state2.toInt()
+      delta > state2
    )
  }

-  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, FlowState1 state2
+  ) {
+    none()
+  }
+
+  predicate isAdditionalFlowStep2(
+    DataFlow::Node node1, FlowState2 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`
-      state1 = s1.toString() and
-      state2 = s2.toString() and
+      state1 = s1 and
+      state2 = s2 and
      add.hasOperands(node1.asOperand(), op) and
      semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
      node2.asInstruction() = add and
@@ -122,13 +132,15 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
  }
 }

+module StringSizeFlow = ProductFlow::GlobalWithState<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
-  sinkState = sink2.getState().toInt() and
+  StringSizeFlow::flowPath(source1, source2, sink1, sink2) and
+  sinkState = sink2.getState() and
  isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and
  overflow > 0 and
  sourceNode = source1.getNode() and
--- a/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql
+++ b/cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql
@@ -20,6 +20,7 @@ import experimental.semmle.code.cpp.dataflow.ProductFlow
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
 import semmle.code.cpp.ir.IR
+import codeql.util.Unit

 pragma[nomagic]
 Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -51,14 +52,14 @@ predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b,
 * Holds if the combination of `n` and `state` represents an appropriate
 * source for the expression `e` suitable for use-use flow.
 */
-private predicate hasSizeImpl(Expr e, DataFlow::Node n, string state) {
+private predicate hasSizeImpl(Expr e, DataFlow::Node n, int state) {
  // The simple case: If the size is a variable access with no qualifier we can just use the
  // dataflow node for that expression and no state.
  exists(VariableAccess va |
    va = e and
    not va instanceof FieldAccess and
    n.asConvertedExpr() = va.getFullyConverted() and
-    state = "0"
+    state = 0
  )
  or
  // If the size is a choice between two expressions we allow both to be nodes representing the size.
@@ -68,13 +69,13 @@ private predicate hasSizeImpl(Expr e, DataFlow::Node n, string state) {
  // remember the constant in the state.
  exists(Expr const, Expr nonconst |
    e.(AddExpr).hasOperands(const, nonconst) and
-    state = const.getValue() and
+    state = const.getValue().toInt() and
    hasSizeImpl(nonconst, n, _)
  )
  or
  exists(Expr const, Expr nonconst |
    e.(SubExpr).hasOperands(const, nonconst) and
-    state = "-" + const.getValue() and
+    state = -const.getValue().toInt() and
    hasSizeImpl(nonconst, n, _)
  )
 }
@@ -83,7 +84,7 @@ private predicate hasSizeImpl(Expr e, DataFlow::Node n, string state) {
 * Holds if `(n, state)` pair represents the source of flow for the size
 * expression associated with `alloc`.
 */
-predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, string state) {
+predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
  hasSizeImpl(alloc.getSizeExpr(), n, state)
 }

@@ -107,11 +108,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 = Unit;

-  override predicate isSourcePair(
-    DataFlow::Node source1, string state1, DataFlow::Node source2, string state2
+  class FlowState2 = int;
+
+  predicate isSourcePair(
+    DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
  ) {
    // In the case of an allocation like
    // ```cpp
@@ -119,30 +122,47 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
    // ```
    // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
    // to the size of the allocation. This state is then checked in `isSinkPair`.
-    state1 = "" and
+    exists(state1) and
    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
+    exists(state1) and
    // We check that the delta computed by the range analysis matches the
    // state value that we set in `isSourcePair`.
    exists(int delta |
      isSinkImpl(_, sink1, sink2, delta) and
-      state2 = delta.toString()
+      state2 = delta
    )
  }

-  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::GlobalWithState<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 +244,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::flowPath(_, _, pragma[only_bind_into](p), _) and
    isSinkImpl(pai, sink1, _, _) and
    bounded2(source.asInstruction(), pai, delta) and
    delta >= 0
@@ -235,7 +255,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 +271,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 +286,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 +346,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 +367,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::flowPath(source1.asPathNode1(), _, sink1, _) and
    joinOn1(pai, sink1, source3) and
    InvalidPointerToDerefFlow::flowPath(source3, sink3) and
    joinOn2(sink3, sink.asSinkNode(), operation)