1
1
private import codeql.dataflow.DataFlow as DF
2
2
private import codeql.util.Location
3
3
4
+ signature module DataFlowStackSig<
5
+ LocationSig Location, DF:: InputSig< Location > Lang, DF:: Configs< Location , Lang > :: ConfigSig Config>
6
+ {
7
+ Lang:: Node getNode ( DF:: DataFlowMake< Location , Lang > :: Global< Config > :: PathNode n ) ;
8
+
9
+ predicate isSource ( DF:: DataFlowMake< Location , Lang > :: Global< Config > :: PathNode n ) ;
10
+
11
+ DF:: DataFlowMake< Location , Lang > :: Global< Config > :: PathNode getASuccessor (
12
+ DF:: DataFlowMake< Location , Lang > :: Global< Config > :: PathNode n
13
+ ) ;
14
+
15
+ Lang:: DataFlowCallable getARuntimeTarget ( Lang:: DataFlowCall call ) ;
16
+
17
+ Lang:: Node getAnArgumentNode ( Lang:: DataFlowCall call ) ;
18
+ }
19
+
4
20
module DataFlowStackMake< LocationSig Location, DF:: InputSig< Location > Lang> {
5
- import DF:: DataFlowMake< Location , Lang > as DataFlow
21
+ module DataFlow = DF:: DataFlowMake< Location , Lang > ;
22
+
23
+ module BiStackAnalysis<
24
+ DF:: Configs< Location , Lang > :: ConfigSig ConfigA,
25
+ DataFlowStackSig< Location , Lang , ConfigA > DataFlowStackA,
26
+ DF:: Configs< Location , Lang > :: ConfigSig ConfigB,
27
+ DataFlowStackSig< Location , Lang , ConfigB > DataFlowStackB>
28
+ {
29
+ module FlowA = DataFlow:: Global< ConfigA > ;
6
30
7
- module BiStackAnalysis< DataFlow:: GlobalFlowSig FlowA, DataFlow:: GlobalFlowSig FlowB> {
8
- module FlowStackA = FlowStack< FlowA > ;
31
+ module FlowStackA = FlowStack< ConfigA , DataFlowStackA > ;
9
32
10
- module FlowStackB = FlowStack< FlowB > ;
33
+ module FlowB = DataFlow:: Global< ConfigB > ;
34
+
35
+ module FlowStackB = FlowStack< ConfigB , DataFlowStackB > ;
11
36
12
37
/**
13
38
* Holds if either the Stack associated with `sourceNodeA` is a subset of the stack associated with `sourceNodeB`
@@ -25,9 +50,11 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
25
50
flowStackA = FlowStackA:: createFlowStack ( sourceNodeA , sinkNodeA ) and
26
51
flowStackB = FlowStackB:: createFlowStack ( sourceNodeB , sinkNodeB ) and
27
52
(
28
- BiStackAnalysisImpl< FlowA , FlowB > :: flowStackIsSubsetOf ( flowStackA , flowStackB )
53
+ BiStackAnalysisImpl< ConfigA , DataFlowStackA , ConfigB , DataFlowStackB > :: flowStackIsSubsetOf ( flowStackA ,
54
+ flowStackB )
29
55
or
30
- BiStackAnalysisImpl< FlowB , FlowA > :: flowStackIsSubsetOf ( flowStackB , flowStackA )
56
+ BiStackAnalysisImpl< ConfigB , DataFlowStackB , ConfigA , DataFlowStackA > :: flowStackIsSubsetOf ( flowStackB ,
57
+ flowStackA )
31
58
)
32
59
)
33
60
}
@@ -51,10 +78,10 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
51
78
flowStackA = FlowStackA:: createFlowStack ( sourceNodeA , sinkNodeA ) and
52
79
flowStackB = FlowStackB:: createFlowStack ( sourceNodeB , sinkNodeB ) and
53
80
(
54
- BiStackAnalysisImpl< FlowA , FlowB > :: flowStackIsConvergingTerminatingSubsetOf ( flowStackA ,
81
+ BiStackAnalysisImpl< ConfigA , DataFlowStackA , ConfigB , DataFlowStackB > :: flowStackIsConvergingTerminatingSubsetOf ( flowStackA ,
55
82
flowStackB )
56
83
or
57
- BiStackAnalysisImpl< FlowB , FlowA > :: flowStackIsConvergingTerminatingSubsetOf ( flowStackB ,
84
+ BiStackAnalysisImpl< ConfigB , DataFlowStackB , ConfigA , DataFlowStackA > :: flowStackIsConvergingTerminatingSubsetOf ( flowStackB ,
58
85
flowStackA )
59
86
)
60
87
)
@@ -67,7 +94,8 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
67
94
* The top of stackA is in stackB and the bottom of stackA is then some successor further down stackB.
68
95
*/
69
96
predicate flowStackIsSubsetOf ( FlowStackA:: FlowStack flowStackA , FlowStackB:: FlowStack flowStackB ) {
70
- BiStackAnalysisImpl< FlowA , FlowB > :: flowStackIsSubsetOf ( flowStackA , flowStackB )
97
+ BiStackAnalysisImpl< ConfigA , DataFlowStackA , ConfigB , DataFlowStackB > :: flowStackIsSubsetOf ( flowStackA ,
98
+ flowStackB )
71
99
}
72
100
73
101
/**
@@ -78,15 +106,20 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
78
106
predicate flowStackIsConvergingTerminatingSubsetOf (
79
107
FlowStackA:: FlowStack flowStackA , FlowStackB:: FlowStack flowStackB
80
108
) {
81
- BiStackAnalysisImpl< FlowA , FlowB > :: flowStackIsConvergingTerminatingSubsetOf ( flowStackA ,
109
+ BiStackAnalysisImpl< ConfigA , DataFlowStackA , ConfigB , DataFlowStackB > :: flowStackIsConvergingTerminatingSubsetOf ( flowStackA ,
82
110
flowStackB )
83
111
}
84
112
}
85
113
86
- private module BiStackAnalysisImpl< DataFlow:: GlobalFlowSig FlowA, DataFlow:: GlobalFlowSig FlowB> {
87
- module FlowStackA = FlowStack< FlowA > ;
114
+ private module BiStackAnalysisImpl<
115
+ DF:: Configs< Location , Lang > :: ConfigSig ConfigA,
116
+ DataFlowStackSig< Location , Lang , ConfigA > DataFlowStackA,
117
+ DF:: Configs< Location , Lang > :: ConfigSig ConfigB,
118
+ DataFlowStackSig< Location , Lang , ConfigB > DataFlowStackB>
119
+ {
120
+ module FlowStackA = FlowStack< ConfigA , DataFlowStackA > ;
88
121
89
- module FlowStackB = FlowStack< FlowB > ;
122
+ module FlowStackB = FlowStack< ConfigB , DataFlowStackB > ;
90
123
91
124
/**
92
125
* Holds if stackA is a subset of stackB,
@@ -130,25 +163,30 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
130
163
}
131
164
}
132
165
133
- module FlowStack< DataFlow:: GlobalFlowSig Flow> {
166
+ module FlowStack<
167
+ DF:: Configs< Location , Lang > :: ConfigSig Config,
168
+ DataFlowStackSig< Location , Lang , Config > DataFlowStack>
169
+ {
170
+ private module Flow = DF:: DataFlowMake< Location , Lang > :: Global< Config > ;
171
+
134
172
/**
135
173
* Determines whether or not the given PathNode is a source
136
174
* TODO: Refactor to Flow::PathNode signature
137
175
*/
138
- predicate isSource ( Flow:: PathNode node ) { node . isSource ( ) }
176
+ predicate isSource ( Flow:: PathNode node ) { DataFlowStack :: isSource ( node ) }
139
177
140
178
/**
141
179
* Determines whether or not the given PathNode is a sink
142
180
* TODO: Refactor to Flow::PathNode signature
143
181
*/
144
- predicate isSink ( Flow:: PathNode node ) { not exists ( node . getASuccessor ( ) ) }
182
+ predicate isSink ( Flow:: PathNode node ) { not exists ( DataFlowStack :: getASuccessor ( node ) ) }
145
183
146
184
/** A FlowStack encapsulates flows between a source and a sink, and all the pathways inbetween (possibly multiple) */
147
185
private newtype FlowStackType =
148
186
TFlowStack ( Flow:: PathNode source , Flow:: PathNode sink ) {
149
- source . isSource ( ) and
150
- not exists ( sink . getASuccessor ( ) ) and
151
- source . getASuccessor * ( ) = sink
187
+ DataFlowStack :: isSource ( source ) and
188
+ not exists ( DataFlowStack :: getASuccessor ( sink ) ) and
189
+ DataFlowStack :: getASuccessor * ( source ) = sink
152
190
}
153
191
154
192
class FlowStack extends FlowStackType , TFlowStack {
@@ -197,8 +235,8 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
197
235
TFlowStackFrame ( FlowStack flowStack , CallFrame frame ) {
198
236
exists ( Flow:: PathNode source , Flow:: PathNode sink |
199
237
flowStack = TFlowStack ( source , sink ) and
200
- frame .getPathNode ( ) = source . getASuccessor * ( ) and
201
- frame .getPathNode ( ) . getASuccessor * ( ) = sink
238
+ frame .getPathNode ( ) = DataFlowStack :: getASuccessor * ( source ) and
239
+ DataFlowStack :: getASuccessor ( frame .getPathNode ( ) ) = sink
202
240
)
203
241
}
204
242
@@ -241,7 +279,8 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
241
279
FlowStackFrame getChildStackFrame ( ) {
242
280
exists ( FlowStackFrame transitiveSuccessor |
243
281
transitiveSuccessor = this .getASuccessor + ( ) and
244
- this .getCall ( ) .getARuntimeTarget ( ) = transitiveSuccessor .getCall ( ) .getEnclosingCallable ( ) and
282
+ DataFlowStack:: getARuntimeTarget ( this .getCall ( ) ) =
283
+ transitiveSuccessor .getCall ( ) .getEnclosingCallable ( ) and
245
284
result = transitiveSuccessor
246
285
)
247
286
}
@@ -272,7 +311,9 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
272
311
*/
273
312
private newtype TCallFrameType =
274
313
TCallFrame ( Flow:: PathNode node ) {
275
- exists ( Lang:: DataFlowCall c | c .getAnArgumentNode ( ) = node .getNode ( ) )
314
+ exists ( Lang:: DataFlowCall c |
315
+ DataFlowStack:: getAnArgumentNode ( c ) = DataFlowStack:: getNode ( node )
316
+ )
276
317
}
277
318
278
319
/**
@@ -307,7 +348,7 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
307
348
Lang:: DataFlowCall getCall ( ) {
308
349
exists ( Lang:: DataFlowCall call , Flow:: PathNode node |
309
350
this = TCallFrame ( node ) and
310
- call . getAnArgumentNode ( ) = node . getNode ( ) and
351
+ DataFlowStack :: getAnArgumentNode ( call ) = DataFlowStack :: getNode ( node ) and
311
352
result = call
312
353
)
313
354
}
@@ -329,8 +370,11 @@ module DataFlowStackMake<LocationSig Location, DF::InputSig<Location> Lang> {
329
370
*/
330
371
private Flow:: PathNode getSuccessorCall ( Flow:: PathNode n ) {
331
372
exists ( Flow:: PathNode succ |
332
- succ = n .getASuccessor ( ) and
333
- if exists ( Lang:: DataFlowCall c | c .getAnArgumentNode ( ) = succ .getNode ( ) )
373
+ succ = DataFlowStack:: getASuccessor ( n ) and
374
+ if
375
+ exists ( Lang:: DataFlowCall c |
376
+ DataFlowStack:: getAnArgumentNode ( c ) = DataFlowStack:: getNode ( succ )
377
+ )
334
378
then result = succ
335
379
else result = getSuccessorCall ( succ )
336
380
)
0 commit comments