1
- import semmle.code.cpp.ir.dataflow.DataFlow
2
- private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
3
- private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
4
- private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplCommon
1
+ /**
2
+ * Provides a library for global (inter-procedural) data flow analysis of two
3
+ * values "simultaneously". This can be used, for example, if you want to track
4
+ * a memory allocation as well as the size of the allocation.
5
+ *
6
+ * Intuitively, you can think of this as regular dataflow, but where each node
7
+ * in the dataflow graph has been replaced by a pair of nodes `(node1, node2)`,
8
+ * and two node pairs `(n11, n12)`, `(n21, n22)` is then connected by a dataflow
9
+ * edge if there's a regular dataflow edge between `n11` and `n21`, and `n12`
10
+ * and `n22`.
11
+ *
12
+ * Note that the above intuition does not reflect the actual implementation.
13
+ */
14
+
15
+ import semmle.code.cpp.dataflow.new.DataFlow
16
+ private import DataFlowPrivate
17
+ private import DataFlowUtil
18
+ private import DataFlowImplCommon
5
19
private import codeql.util.Unit
6
20
21
+ /**
22
+ * Provides classes for performing global (inter-procedural) data flow analyses
23
+ * on a product dataflow graph.
24
+ */
7
25
module ProductFlow {
26
+ /** An input configuration for product data-flow. */
8
27
signature module ConfigSig {
9
28
/**
10
29
* Holds if `(source1, source2)` is a relevant data flow source.
@@ -70,6 +89,9 @@ module ProductFlow {
70
89
default predicate isBarrierIn2 ( DataFlow:: Node node ) { none ( ) }
71
90
}
72
91
92
+ /**
93
+ * The output of a global data flow computation.
94
+ */
73
95
module Global< ConfigSig Config> {
74
96
private module StateConfig implements StateConfigSig {
75
97
class FlowState1 = Unit ;
@@ -138,6 +160,7 @@ module ProductFlow {
138
160
import GlobalWithState< StateConfig >
139
161
}
140
162
163
+ /** An input configuration for data flow using flow state. */
141
164
signature module StateConfigSig {
142
165
bindingset [ this ]
143
166
class FlowState1 ;
@@ -247,6 +270,9 @@ module ProductFlow {
247
270
default predicate isBarrierIn2 ( DataFlow:: Node node ) { none ( ) }
248
271
}
249
272
273
+ /**
274
+ * The output of a global data flow computation.
275
+ */
250
276
module GlobalWithState< StateConfigSig Config> {
251
277
class PathNode1 = Flow1:: PathNode ;
252
278
@@ -260,6 +286,7 @@ module ProductFlow {
260
286
261
287
class FlowState2 = Config:: FlowState2 ;
262
288
289
+ /** Holds if data can flow from `(source1, source2)` to `(sink1, sink2)`. */
263
290
predicate flowPath (
264
291
Flow1:: PathNode source1 , Flow2:: PathNode source2 , Flow1:: PathNode sink1 , Flow2:: PathNode sink2
265
292
) {
0 commit comments