1
1
/**
2
- * Provides the implementation of a summary type tracker, that is type tracking through flow summaries.
2
+ * Provides the implementation of type tracking steps through flow summaries.
3
3
* To use this, you must implement the `Input` signature. You can then use the predicates in the `Output`
4
4
* signature to implement the predicates of the same names inside `TypeTrackerSpecific.qll`.
5
5
*/
6
6
7
- /** The classes and predicates needed to generate a summary type tracker . */
7
+ /** The classes and predicates needed to generate type-tracking steps from summaries . */
8
8
signature module Input {
9
9
// Dataflow nodes
10
10
class Node ;
@@ -80,13 +80,6 @@ signature module Input {
80
80
/** Gets a dataflow node respresenting the return of `callable` indicated by `return`. */
81
81
Node returnOf ( Node callable , SummaryComponent return ) ;
82
82
83
- // Specific summary handling
84
- /** Holds if component should be treated as a level step by type tracking. */
85
- predicate componentLevelStep ( SummaryComponent component ) ;
86
-
87
- /** Holds if the given component can't be evaluated by `evaluateSummaryComponentStackLocal`. */
88
- predicate isNonLocal ( SummaryComponent component ) ;
89
-
90
83
// Relating callables to nodes
91
84
/** Gets a dataflow node respresenting a call to `callable`. */
92
85
Node callTo ( SummarizedCallable callable ) ;
@@ -146,17 +139,17 @@ module SummaryFlow<Input I> implements Output<I> {
146
139
I:: SummaryComponentStack output
147
140
) {
148
141
callable .propagatesFlow ( I:: push ( I:: content ( contents ) , input ) , output , true ) and
149
- not I :: isNonLocal ( input .head ( ) ) and
150
- not I :: isNonLocal ( output .head ( ) )
142
+ not isNonLocal ( input .head ( ) ) and
143
+ not isNonLocal ( output .head ( ) )
151
144
}
152
145
153
146
pragma [ nomagic]
154
147
private predicate hasStoreSummary (
155
148
I:: SummarizedCallable callable , I:: TypeTrackerContent contents , I:: SummaryComponentStack input ,
156
149
I:: SummaryComponentStack output
157
150
) {
158
- not I :: isNonLocal ( input .head ( ) ) and
159
- not I :: isNonLocal ( output .head ( ) ) and
151
+ not isNonLocal ( input .head ( ) ) and
152
+ not isNonLocal ( output .head ( ) ) and
160
153
(
161
154
callable .propagatesFlow ( input , I:: push ( I:: content ( contents ) , output ) , true )
162
155
or
@@ -178,8 +171,8 @@ module SummaryFlow<Input I> implements Output<I> {
178
171
callable
179
172
.propagatesFlow ( I:: push ( I:: content ( loadContents ) , input ) ,
180
173
I:: push ( I:: content ( storeContents ) , output ) , true ) and
181
- not I :: isNonLocal ( input .head ( ) ) and
182
- not I :: isNonLocal ( output .head ( ) )
174
+ not isNonLocal ( input .head ( ) ) and
175
+ not isNonLocal ( output .head ( ) )
183
176
}
184
177
185
178
pragma [ nomagic]
@@ -190,8 +183,8 @@ module SummaryFlow<Input I> implements Output<I> {
190
183
exists ( I:: TypeTrackerContent content |
191
184
callable .propagatesFlow ( I:: push ( I:: withoutContent ( content ) , input ) , output , true ) and
192
185
filter = I:: getFilterFromWithoutContentStep ( content ) and
193
- not I :: isNonLocal ( input .head ( ) ) and
194
- not I :: isNonLocal ( output .head ( ) ) and
186
+ not isNonLocal ( input .head ( ) ) and
187
+ not isNonLocal ( output .head ( ) ) and
195
188
input != output
196
189
)
197
190
}
@@ -204,12 +197,26 @@ module SummaryFlow<Input I> implements Output<I> {
204
197
exists ( I:: TypeTrackerContent content |
205
198
callable .propagatesFlow ( I:: push ( I:: withContent ( content ) , input ) , output , true ) and
206
199
filter = I:: getFilterFromWithContentStep ( content ) and
207
- not I :: isNonLocal ( input .head ( ) ) and
208
- not I :: isNonLocal ( output .head ( ) ) and
200
+ not isNonLocal ( input .head ( ) ) and
201
+ not isNonLocal ( output .head ( ) ) and
209
202
input != output
210
203
)
211
204
}
212
205
206
+ private predicate componentLevelStep ( I:: SummaryComponent component ) {
207
+ exists ( I:: TypeTrackerContent content |
208
+ component = I:: withoutContent ( content ) and
209
+ not exists ( I:: getFilterFromWithoutContentStep ( content ) )
210
+ )
211
+ }
212
+
213
+ pragma [ nomagic]
214
+ private predicate isNonLocal ( I:: SummaryComponent component ) {
215
+ component = I:: content ( _)
216
+ or
217
+ component = I:: withContent ( _)
218
+ }
219
+
213
220
/**
214
221
* Gets a data flow I::Node corresponding an argument or return value of `call`,
215
222
* as specified by `component`.
@@ -255,7 +262,7 @@ module SummaryFlow<Input I> implements Output<I> {
255
262
I:: SummarizedCallable callable , I:: SummaryComponent head , I:: SummaryComponentStack tail
256
263
) {
257
264
dependsOnSummaryComponentStackCons ( callable , head , tail ) and
258
- not I :: isNonLocal ( head )
265
+ not isNonLocal ( head )
259
266
}
260
267
261
268
pragma [ nomagic]
@@ -290,7 +297,7 @@ module SummaryFlow<Input I> implements Output<I> {
290
297
or
291
298
result = I:: returnOf ( prev , head )
292
299
or
293
- I :: componentLevelStep ( head ) and
300
+ componentLevelStep ( head ) and
294
301
result = prev
295
302
)
296
303
}
0 commit comments