1- import semmle.code.cpp.ir.dataflow.DataFlow
2- import semmle.code.cpp.ir.dataflow.DataFlow2
1+ import experimental. semmle.code.cpp.ir.dataflow.DataFlow
2+ import experimental. semmle.code.cpp.ir.dataflow.DataFlow2
33
44module ProductFlow {
55 abstract class Configuration extends string {
@@ -11,14 +11,43 @@ module ProductFlow {
1111 *
1212 * `source1` and `source2` must belong to the same callable.
1313 */
14- abstract predicate isSourcePair ( DataFlow:: Node source1 , DataFlow:: Node source2 ) ;
14+ predicate isSourcePair ( DataFlow:: Node source1 , DataFlow:: Node source2 ) { none ( ) }
15+
16+ /**
17+ * Holds if `(source1, source2)` is a relevant data flow source with initial states `state1`
18+ * and `state2`, respectively.
19+ *
20+ * `source1` and `source2` must belong to the same callable.
21+ */
22+ predicate isSourcePair (
23+ DataFlow:: Node source1 , string state1 , DataFlow:: Node source2 , string state2
24+ ) {
25+ state1 = "" and
26+ state2 = "" and
27+ this .isSourcePair ( source1 , source2 )
28+ }
1529
1630 /**
1731 * Holds if `(sink1, sink2)` is a relevant data flow sink.
1832 *
1933 * `sink1` and `sink2` must belong to the same callable.
2034 */
21- abstract predicate isSinkPair ( DataFlow:: Node sink1 , DataFlow:: Node sink2 ) ;
35+ predicate isSinkPair ( DataFlow:: Node sink1 , DataFlow:: Node sink2 ) { none ( ) }
36+
37+ /**
38+ * Holds if `(sink1, sink2)` is a relevant data flow sink with final states `state1`
39+ * and `state2`, respectively.
40+ *
41+ * `sink1` and `sink2` must belong to the same callable.
42+ */
43+ predicate isSinkPair (
44+ DataFlow:: Node sink1 , DataFlow:: FlowState state1 , DataFlow:: Node sink2 ,
45+ DataFlow:: FlowState state2
46+ ) {
47+ state1 = "" and
48+ state2 = "" and
49+ this .isSinkPair ( sink1 , sink2 )
50+ }
2251
2352 predicate hasFlowPath (
2453 DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 , DataFlow:: PathNode sink1 ,
@@ -34,28 +63,28 @@ module ProductFlow {
3463 class Conf1 extends DataFlow:: Configuration {
3564 Conf1 ( ) { this = "Conf1" }
3665
37- override predicate isSource ( DataFlow:: Node source ) {
38- exists ( Configuration conf | conf .isSourcePair ( source , _) )
66+ override predicate isSource ( DataFlow:: Node source , string state ) {
67+ exists ( Configuration conf | conf .isSourcePair ( source , state , _ , _) )
3968 }
4069
41- override predicate isSink ( DataFlow:: Node sink ) {
42- exists ( Configuration conf | conf .isSinkPair ( sink , _) )
70+ override predicate isSink ( DataFlow:: Node sink , string state ) {
71+ exists ( Configuration conf | conf .isSinkPair ( sink , state , _ , _) )
4372 }
4473 }
4574
4675 class Conf2 extends DataFlow2:: Configuration {
4776 Conf2 ( ) { this = "Conf2" }
4877
49- override predicate isSource ( DataFlow:: Node source ) {
78+ override predicate isSource ( DataFlow:: Node source , string state ) {
5079 exists ( Configuration conf , DataFlow:: Node source1 |
51- conf .isSourcePair ( source1 , source ) and
80+ conf .isSourcePair ( source1 , _ , source , state ) and
5281 any ( Conf1 c ) .hasFlow ( source1 , _)
5382 )
5483 }
5584
56- override predicate isSink ( DataFlow:: Node sink ) {
85+ override predicate isSink ( DataFlow:: Node sink , string state ) {
5786 exists ( Configuration conf , DataFlow:: Node sink1 |
58- conf .isSinkPair ( sink1 , sink ) and any ( Conf1 c ) .hasFlow ( _, sink1 )
87+ conf .isSinkPair ( sink1 , _ , sink , state ) and any ( Conf1 c ) .hasFlow ( _, sink1 )
5988 )
6089 }
6190 }
@@ -65,7 +94,7 @@ module ProductFlow {
6594 Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
6695 DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
6796 ) {
68- conf .isSourcePair ( node1 .getNode ( ) , node2 .getNode ( ) ) and
97+ conf .isSourcePair ( node1 .getNode ( ) , _ , node2 .getNode ( ) , _ ) and
6998 node1 = source1 and
7099 node2 = source2
71100 or
@@ -128,7 +157,7 @@ module ProductFlow {
128157 ) {
129158 exists ( DataFlow:: PathNode mid1 , DataFlow2:: PathNode mid2 |
130159 reachableInterprocEntry ( conf , source1 , source2 , mid1 , mid2 ) and
131- conf .isSinkPair ( sink1 .getNode ( ) , sink2 .getNode ( ) ) and
160+ conf .isSinkPair ( sink1 .getNode ( ) , _ , sink2 .getNode ( ) , _ ) and
132161 localPathStep1 * ( mid1 , sink1 ) and
133162 localPathStep2 * ( mid2 , sink2 )
134163 )
0 commit comments