@@ -20,7 +20,8 @@ module ProductFlow {
2020 * `source1` and `source2` must belong to the same callable.
2121 */
2222 predicate isSourcePair (
23- DataFlow:: Node source1 , string state1 , DataFlow:: Node source2 , string state2
23+ DataFlow:: Node source1 , DataFlow:: FlowState state1 , DataFlow:: Node source2 ,
24+ DataFlow:: FlowState state2
2425 ) {
2526 state1 = "" and
2627 state2 = "" and
@@ -49,6 +50,89 @@ module ProductFlow {
4950 this .isSinkPair ( sink1 , sink2 )
5051 }
5152
53+ /**
54+ * Holds if data flow through `node` is prohibited through the first projection of the product
55+ * dataflow graph when the flow state is `state`.
56+ */
57+ predicate isBarrier1 ( DataFlow:: Node node , DataFlow:: FlowState state ) {
58+ this .isBarrier1 ( node ) and state = ""
59+ }
60+
61+ /**
62+ * Holds if data flow through `node` is prohibited through the second projection of the product
63+ * dataflow graph when the flow state is `state`.
64+ */
65+ predicate isBarrier2 ( DataFlow:: Node node , DataFlow:: FlowState state ) {
66+ this .isBarrier2 ( node ) and state = ""
67+ }
68+
69+ /**
70+ * Holds if data flow through `node` is prohibited through the first projection of the product
71+ * dataflow graph.
72+ */
73+ predicate isBarrier1 ( DataFlow:: Node node ) { none ( ) }
74+
75+ /**
76+ * Holds if data flow through `node` is prohibited through the second projection of the product
77+ * dataflow graph.
78+ */
79+ predicate isBarrier2 ( DataFlow:: Node node ) { none ( ) }
80+
81+ /**
82+ * Holds if data flow out of `node` is prohibited in the first projection of the product
83+ * dataflow graph.
84+ */
85+ predicate isBarrierOut1 ( DataFlow:: Node node ) { none ( ) }
86+
87+ /**
88+ * Holds if data flow out of `node` is prohibited in the second projection of the product
89+ * dataflow graph.
90+ */
91+ predicate isBarrierOut2 ( DataFlow:: Node node ) { none ( ) }
92+
93+ /*
94+ * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
95+ * the first projection of the product dataflow graph.
96+ */
97+
98+ predicate isAdditionalFlowStep1 ( DataFlow:: Node node1 , DataFlow:: Node node2 ) { none ( ) }
99+
100+ /**
101+ * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
102+ * the first projection of the product dataflow graph.
103+ *
104+ * This step is only applicable in `state1` and updates the flow state to `state2`.
105+ */
106+ predicate isAdditionalFlowStep1 (
107+ DataFlow:: Node node1 , DataFlow:: FlowState state1 , DataFlow:: Node node2 ,
108+ DataFlow:: FlowState state2
109+ ) {
110+ state1 instanceof DataFlow:: FlowStateEmpty and
111+ state2 instanceof DataFlow:: FlowStateEmpty and
112+ this .isAdditionalFlowStep1 ( node1 , node2 )
113+ }
114+
115+ /**
116+ * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
117+ * the second projection of the product dataflow graph.
118+ */
119+ predicate isAdditionalFlowStep2 ( DataFlow:: Node node1 , DataFlow:: Node node2 ) { none ( ) }
120+
121+ /**
122+ * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
123+ * the second projection of the product dataflow graph.
124+ *
125+ * This step is only applicable in `state1` and updates the flow state to `state2`.
126+ */
127+ predicate isAdditionalFlowStep2 (
128+ DataFlow:: Node node1 , DataFlow:: FlowState state1 , DataFlow:: Node node2 ,
129+ DataFlow:: FlowState state2
130+ ) {
131+ state1 instanceof DataFlow:: FlowStateEmpty and
132+ state2 instanceof DataFlow:: FlowStateEmpty and
133+ this .isAdditionalFlowStep2 ( node1 , node2 )
134+ }
135+
52136 predicate hasFlowPath (
53137 DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 , DataFlow:: PathNode sink1 ,
54138 DataFlow2:: PathNode sink2
@@ -63,38 +147,69 @@ module ProductFlow {
63147 class Conf1 extends DataFlow:: Configuration {
64148 Conf1 ( ) { this = "Conf1" }
65149
66- override predicate isSource ( DataFlow:: Node source , string state ) {
150+ override predicate isSource ( DataFlow:: Node source , DataFlow :: FlowState state ) {
67151 exists ( Configuration conf | conf .isSourcePair ( source , state , _, _) )
68152 }
69153
70- override predicate isSink ( DataFlow:: Node sink , string state ) {
154+ override predicate isSink ( DataFlow:: Node sink , DataFlow :: FlowState state ) {
71155 exists ( Configuration conf | conf .isSinkPair ( sink , state , _, _) )
72156 }
157+
158+ override predicate isBarrier ( DataFlow:: Node node , DataFlow:: FlowState state ) {
159+ exists ( Configuration conf | conf .isBarrier1 ( node , state ) )
160+ }
161+
162+ override predicate isBarrierOut ( DataFlow:: Node node ) {
163+ exists ( Configuration conf | conf .isBarrierOut1 ( node ) )
164+ }
165+
166+ override predicate isAdditionalFlowStep (
167+ DataFlow:: Node node1 , DataFlow:: FlowState state1 , DataFlow:: Node node2 ,
168+ DataFlow:: FlowState state2
169+ ) {
170+ exists ( Configuration conf | conf .isAdditionalFlowStep1 ( node1 , state1 , node2 , state2 ) )
171+ }
73172 }
74173
75174 class Conf2 extends DataFlow2:: Configuration {
76175 Conf2 ( ) { this = "Conf2" }
77176
78- override predicate isSource ( DataFlow:: Node source , string state ) {
79- exists ( Configuration conf , DataFlow:: Node source1 |
80- conf .isSourcePair ( source1 , _ , source , state ) and
81- any ( Conf1 c ) .hasFlow ( source1 , _)
177+ override predicate isSource ( DataFlow:: Node source , DataFlow :: FlowState state ) {
178+ exists ( Configuration conf , DataFlow:: PathNode source1 |
179+ conf .isSourcePair ( source1 . getNode ( ) , source1 . getState ( ) , source , state ) and
180+ any ( Conf1 c ) .hasFlowPath ( source1 , _)
82181 )
83182 }
84183
85- override predicate isSink ( DataFlow:: Node sink , string state ) {
86- exists ( Configuration conf , DataFlow:: Node sink1 |
87- conf .isSinkPair ( sink1 , _, sink , state ) and any ( Conf1 c ) .hasFlow ( _, sink1 )
184+ override predicate isSink ( DataFlow:: Node sink , DataFlow:: FlowState state ) {
185+ exists ( Configuration conf , DataFlow:: PathNode sink1 |
186+ conf .isSinkPair ( sink1 .getNode ( ) , sink1 .getState ( ) , sink , state ) and
187+ any ( Conf1 c ) .hasFlowPath ( _, sink1 )
88188 )
89189 }
190+
191+ override predicate isBarrier ( DataFlow:: Node node , DataFlow:: FlowState state ) {
192+ exists ( Configuration conf | conf .isBarrier2 ( node , state ) )
193+ }
194+
195+ override predicate isBarrierOut ( DataFlow:: Node node ) {
196+ exists ( Configuration conf | conf .isBarrierOut2 ( node ) )
197+ }
198+
199+ override predicate isAdditionalFlowStep (
200+ DataFlow:: Node node1 , DataFlow:: FlowState state1 , DataFlow:: Node node2 ,
201+ DataFlow:: FlowState state2
202+ ) {
203+ exists ( Configuration conf | conf .isAdditionalFlowStep2 ( node1 , state1 , node2 , state2 ) )
204+ }
90205 }
91206 }
92207
93208 private predicate reachableInterprocEntry (
94209 Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
95210 DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
96211 ) {
97- conf .isSourcePair ( node1 .getNode ( ) , _ , node2 .getNode ( ) , _ ) and
212+ conf .isSourcePair ( node1 .getNode ( ) , node1 . getState ( ) , node2 .getNode ( ) , node2 . getState ( ) ) and
98213 node1 = source1 and
99214 node2 = source2
100215 or
@@ -157,7 +272,7 @@ module ProductFlow {
157272 ) {
158273 exists ( DataFlow:: PathNode mid1 , DataFlow2:: PathNode mid2 |
159274 reachableInterprocEntry ( conf , source1 , source2 , mid1 , mid2 ) and
160- conf .isSinkPair ( sink1 .getNode ( ) , _ , sink2 .getNode ( ) , _ ) and
275+ conf .isSinkPair ( sink1 .getNode ( ) , sink1 . getState ( ) , sink2 .getNode ( ) , sink2 . getState ( ) ) and
161276 localPathStep1 * ( mid1 , sink1 ) and
162277 localPathStep2 * ( mid2 , sink2 )
163278 )
0 commit comments