@@ -17,6 +17,10 @@ class TypeTrackingNode = DataFlowPublic::LocalSourceNode;
17
17
18
18
class TypeTrackerContent = DataFlowPublic:: ContentSet ;
19
19
20
+ private module SCS = SummaryComponentStack;
21
+
22
+ private module SC = SummaryComponent;
23
+
20
24
/**
21
25
* An optional content set, that is, a `ContentSet` or the special "no content set" value.
22
26
*/
@@ -64,13 +68,13 @@ private predicate summarizedLocalStep(Node nodeFrom, Node nodeTo) {
64
68
)
65
69
or
66
70
exists (
67
- SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponent input ,
68
- SummaryComponent output
71
+ SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponentStack input ,
72
+ SummaryComponentStack output
69
73
|
70
- hasLevelSummary ( callable , input , output ) and
74
+ callable . propagatesFlow ( input , output , true ) and
71
75
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
72
- nodeFrom = evaluateSummaryComponentLocal ( call , input ) and
73
- nodeTo = evaluateSummaryComponentLocal ( call , output )
76
+ nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
77
+ nodeTo = evaluateSummaryComponentStackLocal ( call , output )
74
78
)
75
79
}
76
80
@@ -181,13 +185,13 @@ predicate basicStoreStep(Node nodeFrom, Node nodeTo, DataFlow::ContentSet conten
181
185
postUpdateStoreStep ( nodeFrom , nodeTo , contents )
182
186
or
183
187
exists (
184
- SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponent input ,
185
- SummaryComponent output
188
+ SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponentStack input ,
189
+ SummaryComponentStack output
186
190
|
187
191
hasStoreSummary ( callable , contents , input , output ) and
188
192
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
189
- nodeFrom = evaluateSummaryComponentLocal ( call , input ) and
190
- nodeTo = evaluateSummaryComponentLocal ( call , output )
193
+ nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
194
+ nodeTo = evaluateSummaryComponentStackLocal ( call , output )
191
195
)
192
196
}
193
197
@@ -221,13 +225,13 @@ predicate basicLoadStep(Node nodeFrom, Node nodeTo, DataFlow::ContentSet content
221
225
)
222
226
or
223
227
exists (
224
- SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponent input ,
225
- SummaryComponent output
228
+ SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponentStack input ,
229
+ SummaryComponentStack output
226
230
|
227
231
hasLoadSummary ( callable , contents , input , output ) and
228
232
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
229
- nodeFrom = evaluateSummaryComponentLocal ( call , input ) and
230
- nodeTo = evaluateSummaryComponentLocal ( call , output )
233
+ nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
234
+ nodeTo = evaluateSummaryComponentStackLocal ( call , output )
231
235
)
232
236
}
233
237
@@ -238,13 +242,13 @@ predicate basicLoadStoreStep(
238
242
Node nodeFrom , Node nodeTo , DataFlow:: ContentSet loadContent , DataFlow:: ContentSet storeContent
239
243
) {
240
244
exists (
241
- SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponent input ,
242
- SummaryComponent output
245
+ SummarizedCallable callable , DataFlowPublic:: CallNode call , SummaryComponentStack input ,
246
+ SummaryComponentStack output
243
247
|
244
248
hasLoadStoreSummary ( callable , loadContent , storeContent , input , output ) and
245
249
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
246
- nodeFrom = evaluateSummaryComponentLocal ( call , input ) and
247
- nodeTo = evaluateSummaryComponentLocal ( call , output )
250
+ nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
251
+ nodeTo = evaluateSummaryComponentStackLocal ( call , output )
248
252
)
249
253
}
250
254
@@ -257,46 +261,39 @@ class Boolean extends boolean {
257
261
258
262
private import SummaryComponentStack
259
263
260
- private predicate hasLevelSummary (
261
- SummarizedCallable callable , SummaryComponent input , SummaryComponent output
262
- ) {
263
- callable .propagatesFlow ( singleton ( input ) , singleton ( output ) , true )
264
- }
265
-
264
+ pragma [ nomagic]
266
265
private predicate hasStoreSummary (
267
- SummarizedCallable callable , DataFlow:: ContentSet contents , SummaryComponent input ,
268
- SummaryComponent output
266
+ SummarizedCallable callable , DataFlow:: ContentSet contents , SummaryComponentStack input ,
267
+ SummaryComponentStack output
269
268
) {
270
- callable
271
- .propagatesFlow ( singleton ( input ) ,
272
- push ( SummaryComponent:: content ( contents ) , singleton ( output ) ) , true )
269
+ callable .propagatesFlow ( input , push ( SummaryComponent:: content ( contents ) , output ) , true )
273
270
}
274
271
272
+ pragma [ nomagic]
275
273
private predicate hasLoadSummary (
276
- SummarizedCallable callable , DataFlow:: ContentSet contents , SummaryComponent input ,
277
- SummaryComponent output
274
+ SummarizedCallable callable , DataFlow:: ContentSet contents , SummaryComponentStack input ,
275
+ SummaryComponentStack output
278
276
) {
279
- callable
280
- .propagatesFlow ( push ( SummaryComponent:: content ( contents ) , singleton ( input ) ) ,
281
- singleton ( output ) , true )
277
+ callable .propagatesFlow ( push ( SummaryComponent:: content ( contents ) , input ) , output , true )
282
278
}
283
279
280
+ pragma [ nomagic]
284
281
private predicate hasLoadStoreSummary (
285
282
SummarizedCallable callable , DataFlow:: ContentSet loadContents ,
286
- DataFlow:: ContentSet storeContents , SummaryComponent input , SummaryComponent output
283
+ DataFlow:: ContentSet storeContents , SummaryComponentStack input , SummaryComponentStack output
287
284
) {
288
285
callable
289
- .propagatesFlow ( push ( SummaryComponent:: content ( loadContents ) , singleton ( input ) ) ,
290
- push ( SummaryComponent:: content ( storeContents ) , singleton ( output ) ) , true )
286
+ .propagatesFlow ( push ( SummaryComponent:: content ( loadContents ) , input ) ,
287
+ push ( SummaryComponent:: content ( storeContents ) , output ) , true )
291
288
}
292
289
293
290
/**
294
291
* Gets a data flow node corresponding an argument or return value of `call`,
295
292
* as specified by `component`.
296
293
*/
297
294
bindingset [ call, component]
298
- private DataFlowPublic :: Node evaluateSummaryComponentLocal (
299
- DataFlowPublic :: CallNode call , SummaryComponent component
295
+ private DataFlow :: Node evaluateSummaryComponentLocal (
296
+ DataFlow :: CallNode call , SummaryComponent component
300
297
) {
301
298
exists ( DataFlowDispatch:: ParameterPosition pos |
302
299
component = SummaryComponent:: argument ( pos ) and
@@ -306,3 +303,49 @@ private DataFlowPublic::Node evaluateSummaryComponentLocal(
306
303
component = SummaryComponent:: return ( ) and
307
304
result = call
308
305
}
306
+
307
+ /**
308
+ * Holds if `callable` is relevant for type-tracking and we therefore want `stack` to
309
+ * be evaluated locally at its call sites.
310
+ */
311
+ private predicate dependsOnSummaryComponentStack (
312
+ SummarizedCallable callable , SummaryComponentStack stack
313
+ ) {
314
+ exists ( callable .getACallSimple ( ) ) and
315
+ (
316
+ callable .propagatesFlow ( stack , _, true )
317
+ or
318
+ callable .propagatesFlow ( _, stack , true )
319
+ )
320
+ or
321
+ dependsOnSummaryComponentStack ( callable , SCS:: push ( _, stack ) )
322
+ }
323
+
324
+ /**
325
+ * Gets a data flow node corresponding to the local input or output of `call`
326
+ * identified by `stack`, if possible.
327
+ */
328
+ private DataFlow:: Node evaluateSummaryComponentStackLocal (
329
+ DataFlow:: CallNode call , SummaryComponentStack stack
330
+ ) {
331
+ exists ( SummarizedCallable callable , SummaryComponent component |
332
+ dependsOnSummaryComponentStack ( callable , stack ) and
333
+ stack = SCS:: singleton ( component ) and
334
+ call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
335
+ result = evaluateSummaryComponentLocal ( call , component )
336
+ )
337
+ or
338
+ exists ( DataFlow:: Node prev , SummaryComponent head , SummaryComponentStack tail |
339
+ stack = SCS:: push ( head , tail ) and
340
+ prev = evaluateSummaryComponentStackLocal ( call , tail )
341
+ |
342
+ exists ( DataFlowDispatch:: ArgumentPosition apos , DataFlowDispatch:: ParameterPosition ppos |
343
+ head = SummaryComponent:: parameter ( apos ) and
344
+ DataFlowDispatch:: parameterMatch ( ppos , apos ) and
345
+ result .( DataFlowPrivate:: ParameterNodeImpl ) .isSourceParameterOf ( prev .asExpr ( ) .getExpr ( ) , ppos )
346
+ )
347
+ or
348
+ head = SummaryComponent:: return ( ) and
349
+ result .( DataFlowPrivate:: SynthReturnNode ) .getCfgScope ( ) = prev .asExpr ( ) .getExpr ( )
350
+ )
351
+ }
0 commit comments