@@ -67,134 +67,71 @@ module ProductFlow {
67
67
}
68
68
69
69
module Make< ConfigSig Config> {
70
- class PathNode1 = Flow1:: PathNode ;
71
-
72
- class PathNode2 = Flow2:: PathNode ;
70
+ private module StateConfig implements StateConfigSig {
71
+ class FlowState1 = DataFlow:: FlowState ;
73
72
74
- module PathGraph1 = Flow1 :: PathGraph ;
73
+ class FlowState2 = DataFlow :: FlowState ;
75
74
76
- module PathGraph2 = Flow2:: PathGraph;
77
-
78
- predicate hasFlowPath ( PathNode1 source1 , PathNode2 source2 , PathNode1 sink1 , PathNode2 sink2 ) {
79
- reachable ( source1 , source2 , sink1 , sink2 )
80
- }
81
-
82
- private module Config1 implements DataFlow:: ConfigSig {
83
- predicate isSource ( DataFlow:: Node source ) { Config:: isSourcePair ( source , _) }
84
-
85
- predicate isSink ( DataFlow:: Node sink ) { Config:: isSinkPair ( sink , _) }
86
-
87
- predicate isBarrier ( DataFlow:: Node node ) { Config:: isBarrier1 ( node ) }
88
-
89
- predicate isBarrierOut ( DataFlow:: Node node ) { Config:: isBarrierOut1 ( node ) }
90
-
91
- predicate isAdditionalFlowStep ( DataFlow:: Node node1 , DataFlow:: Node node2 ) {
92
- Config:: isAdditionalFlowStep1 ( node1 , node2 )
75
+ predicate isSourcePair (
76
+ DataFlow:: Node source1 , FlowState1 state1 , DataFlow:: Node source2 , FlowState2 state2
77
+ ) {
78
+ state1 instanceof DataFlow:: FlowStateEmpty and
79
+ state2 instanceof DataFlow:: FlowStateEmpty and
80
+ Config:: isSourcePair ( source1 , source2 )
93
81
}
94
82
95
- predicate isBarrierIn ( DataFlow:: Node node ) { Config:: isBarrierIn1 ( node ) }
96
- }
97
-
98
- private module Flow1 = DataFlow:: Make< Config1 > ;
99
-
100
- private module Config2 implements DataFlow:: ConfigSig {
101
- predicate isSource ( DataFlow:: Node source ) {
102
- exists ( Flow1:: PathNode source1 |
103
- Config:: isSourcePair ( source1 .getNode ( ) , source ) and
104
- Flow1:: hasFlowPath ( source1 , _)
105
- )
83
+ predicate isSinkPair (
84
+ DataFlow:: Node sink1 , FlowState1 state1 , DataFlow:: Node sink2 , FlowState2 state2
85
+ ) {
86
+ state1 instanceof DataFlow:: FlowStateEmpty and
87
+ state2 instanceof DataFlow:: FlowStateEmpty and
88
+ Config:: isSinkPair ( sink1 , sink2 )
106
89
}
107
90
108
- predicate isSink ( DataFlow:: Node sink ) {
109
- exists ( Flow1:: PathNode sink1 |
110
- Config:: isSinkPair ( sink1 .getNode ( ) , sink ) and
111
- Flow1:: hasFlowPath ( _, sink1 )
112
- )
91
+ predicate isBarrier1 ( DataFlow:: Node node , FlowState1 state ) {
92
+ state instanceof DataFlow:: FlowStateEmpty and
93
+ Config:: isBarrier1 ( node )
113
94
}
114
95
115
- predicate isBarrier ( DataFlow:: Node node ) { Config:: isBarrier2 ( node ) }
96
+ predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) {
97
+ state instanceof DataFlow:: FlowStateEmpty and
98
+ Config:: isBarrier2 ( node )
99
+ }
116
100
117
- predicate isBarrierOut ( DataFlow :: Node node ) { Config:: isBarrierOut2 ( node ) }
101
+ predicate isBarrier1 = Config:: isBarrier1 / 1 ;
118
102
119
- predicate isAdditionalFlowStep ( DataFlow:: Node node1 , DataFlow:: Node node2 ) {
120
- Config:: isAdditionalFlowStep2 ( node1 , node2 )
121
- }
103
+ predicate isBarrier2 = Config:: isBarrier2 / 1 ;
122
104
123
- predicate isBarrierIn ( DataFlow:: Node node ) { Config:: isBarrierIn2 ( node ) }
124
- }
105
+ predicate isBarrierOut1 = Config:: isBarrierOut1 / 1 ;
125
106
126
- private module Flow2 = DataFlow :: Make < Config2 > ;
107
+ predicate isBarrierOut2 = Config :: isBarrierOut2 / 1 ;
127
108
128
- pragma [ nomagic]
129
- private predicate reachableInterprocEntry (
130
- Flow1:: PathNode source1 , Flow2:: PathNode source2 , Flow1:: PathNode node1 , Flow2:: PathNode node2
131
- ) {
132
- Config:: isSourcePair ( node1 .getNode ( ) , node2 .getNode ( ) ) and
133
- node1 = source1 and
134
- node2 = source2
135
- or
136
- exists (
137
- Flow1:: PathNode midEntry1 , Flow2:: PathNode midEntry2 , Flow1:: PathNode midExit1 ,
138
- Flow2:: PathNode midExit2
139
- |
140
- reachableInterprocEntry ( source1 , source2 , midEntry1 , midEntry2 ) and
141
- interprocEdgePair ( midExit1 , midExit2 , node1 , node2 ) and
142
- localPathStep1 * ( midEntry1 , midExit1 ) and
143
- localPathStep2 * ( midEntry2 , midExit2 )
144
- )
145
- }
109
+ predicate isAdditionalFlowStep1 = Config:: isAdditionalFlowStep1 / 2 ;
146
110
147
- private predicate localPathStep1 ( Flow1:: PathNode pred , Flow1:: PathNode succ ) {
148
- Flow1:: PathGraph:: edges ( pred , succ ) and
149
- pragma [ only_bind_out ] ( pred .getNode ( ) .getEnclosingCallable ( ) ) =
150
- pragma [ only_bind_out ] ( succ .getNode ( ) .getEnclosingCallable ( ) )
151
- }
111
+ predicate isAdditionalFlowStep1 (
112
+ DataFlow:: Node node1 , FlowState1 state1 , DataFlow:: Node node2 , FlowState1 state2
113
+ ) {
114
+ state1 instanceof DataFlow:: FlowStateEmpty and
115
+ state2 instanceof DataFlow:: FlowStateEmpty and
116
+ Config:: isAdditionalFlowStep1 ( node1 , node2 )
117
+ }
152
118
153
- private predicate localPathStep2 ( Flow2:: PathNode pred , Flow2:: PathNode succ ) {
154
- Flow2:: PathGraph:: edges ( pred , succ ) and
155
- pragma [ only_bind_out ] ( pred .getNode ( ) .getEnclosingCallable ( ) ) =
156
- pragma [ only_bind_out ] ( succ .getNode ( ) .getEnclosingCallable ( ) )
157
- }
119
+ predicate isAdditionalFlowStep2 = Config:: isAdditionalFlowStep2 / 2 ;
158
120
159
- pragma [ nomagic]
160
- private predicate interprocEdge1 (
161
- Declaration predDecl , Declaration succDecl , Flow1:: PathNode pred1 , Flow1:: PathNode succ1
162
- ) {
163
- Flow1:: PathGraph:: edges ( pred1 , succ1 ) and
164
- predDecl != succDecl and
165
- pred1 .getNode ( ) .getEnclosingCallable ( ) = predDecl and
166
- succ1 .getNode ( ) .getEnclosingCallable ( ) = succDecl
167
- }
121
+ predicate isAdditionalFlowStep2 (
122
+ DataFlow:: Node node1 , FlowState2 state1 , DataFlow:: Node node2 , FlowState2 state2
123
+ ) {
124
+ state1 instanceof DataFlow:: FlowStateEmpty and
125
+ state2 instanceof DataFlow:: FlowStateEmpty and
126
+ Config:: isAdditionalFlowStep2 ( node1 , node2 )
127
+ }
168
128
169
- pragma [ nomagic]
170
- private predicate interprocEdge2 (
171
- Declaration predDecl , Declaration succDecl , Flow2:: PathNode pred2 , Flow2:: PathNode succ2
172
- ) {
173
- Flow2:: PathGraph:: edges ( pred2 , succ2 ) and
174
- predDecl != succDecl and
175
- pred2 .getNode ( ) .getEnclosingCallable ( ) = predDecl and
176
- succ2 .getNode ( ) .getEnclosingCallable ( ) = succDecl
177
- }
129
+ predicate isBarrierIn1 = Config:: isBarrierIn1 / 1 ;
178
130
179
- private predicate interprocEdgePair (
180
- Flow1:: PathNode pred1 , Flow2:: PathNode pred2 , Flow1:: PathNode succ1 , Flow2:: PathNode succ2
181
- ) {
182
- exists ( Declaration predDecl , Declaration succDecl |
183
- interprocEdge1 ( predDecl , succDecl , pred1 , succ1 ) and
184
- interprocEdge2 ( predDecl , succDecl , pred2 , succ2 )
185
- )
131
+ predicate isBarrierIn2 = Config:: isBarrierIn2 / 1 ;
186
132
}
187
133
188
- private predicate reachable (
189
- Flow1:: PathNode source1 , Flow2:: PathNode source2 , Flow1:: PathNode sink1 , Flow2:: PathNode sink2
190
- ) {
191
- exists ( Flow1:: PathNode mid1 , Flow2:: PathNode mid2 |
192
- reachableInterprocEntry ( source1 , source2 , mid1 , mid2 ) and
193
- Config:: isSinkPair ( sink1 .getNode ( ) , sink2 .getNode ( ) ) and
194
- localPathStep1 * ( mid1 , sink1 ) and
195
- localPathStep2 * ( mid2 , sink2 )
196
- )
197
- }
134
+ import MakeWithState< StateConfig >
198
135
}
199
136
200
137
signature module StateConfigSig {
0 commit comments