@@ -73,8 +73,8 @@ private predicate summarizedLocalStep(Node nodeFrom, Node nodeTo) {
73
73
|
74
74
callable .propagatesFlow ( input , output , true ) and
75
75
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
76
- nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
77
- nodeTo = evaluateSummaryComponentStackLocal ( call , output )
76
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
77
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
78
78
)
79
79
}
80
80
@@ -191,8 +191,8 @@ predicate basicStoreStep(Node nodeFrom, Node nodeTo, DataFlow::ContentSet conten
191
191
hasStoreSummary ( callable , contents , pragma [ only_bind_into ] ( input ) ,
192
192
pragma [ only_bind_into ] ( output ) ) and
193
193
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
194
- nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
195
- nodeTo = evaluateSummaryComponentStackLocal ( call , output )
194
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
195
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
196
196
)
197
197
}
198
198
@@ -231,8 +231,8 @@ predicate basicLoadStep(Node nodeFrom, Node nodeTo, DataFlow::ContentSet content
231
231
|
232
232
hasLoadSummary ( callable , contents , pragma [ only_bind_into ] ( input ) , pragma [ only_bind_into ] ( output ) ) and
233
233
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
234
- nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
235
- nodeTo = evaluateSummaryComponentStackLocal ( call , output )
234
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
235
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
236
236
)
237
237
}
238
238
@@ -249,8 +249,8 @@ predicate basicLoadStoreStep(
249
249
hasLoadStoreSummary ( callable , loadContent , storeContent , pragma [ only_bind_into ] ( input ) ,
250
250
pragma [ only_bind_into ] ( output ) ) and
251
251
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
252
- nodeFrom = evaluateSummaryComponentStackLocal ( call , input ) and
253
- nodeTo = evaluateSummaryComponentStackLocal ( call , output )
252
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
253
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
254
254
)
255
255
}
256
256
@@ -310,6 +310,7 @@ private DataFlow::Node evaluateSummaryComponentLocal(
310
310
* Holds if `callable` is relevant for type-tracking and we therefore want `stack` to
311
311
* be evaluated locally at its call sites.
312
312
*/
313
+ pragma [ nomagic]
313
314
private predicate dependsOnSummaryComponentStack (
314
315
SummarizedCallable callable , SummaryComponentStack stack
315
316
) {
@@ -320,26 +321,43 @@ private predicate dependsOnSummaryComponentStack(
320
321
callable .propagatesFlow ( _, stack , true )
321
322
)
322
323
or
323
- dependsOnSummaryComponentStack ( callable , SCS:: push ( _, stack ) )
324
+ dependsOnSummaryComponentStackCons ( callable , _, stack )
325
+ }
326
+
327
+ pragma [ nomagic]
328
+ private predicate dependsOnSummaryComponentStackCons (
329
+ SummarizedCallable callable , SummaryComponent head , SummaryComponentStack tail
330
+ ) {
331
+ dependsOnSummaryComponentStack ( callable , SCS:: push ( head , tail ) )
332
+ }
333
+
334
+ pragma [ nomagic]
335
+ private predicate dependsOnSummaryComponentStackLeaf (
336
+ SummarizedCallable callable , SummaryComponent leaf
337
+ ) {
338
+ dependsOnSummaryComponentStack ( callable , SCS:: singleton ( leaf ) )
324
339
}
325
340
326
341
/**
327
342
* Gets a data flow node corresponding to the local input or output of `call`
328
343
* identified by `stack`, if possible.
329
344
*/
345
+ pragma [ nomagic]
330
346
private DataFlow:: Node evaluateSummaryComponentStackLocal (
331
- DataFlow:: CallNode call , SummaryComponentStack stack
347
+ SummarizedCallable callable , DataFlow:: CallNode call , SummaryComponentStack stack
332
348
) {
333
- exists ( SummarizedCallable callable , SummaryComponent component |
334
- dependsOnSummaryComponentStack ( callable , stack ) and
349
+ exists ( SummaryComponent component |
350
+ dependsOnSummaryComponentStackLeaf ( callable , component ) and
335
351
stack = SCS:: singleton ( component ) and
336
352
call .asExpr ( ) .getExpr ( ) = callable .getACallSimple ( ) and
337
353
result = evaluateSummaryComponentLocal ( call , component )
338
354
)
339
355
or
340
356
exists ( DataFlow:: Node prev , SummaryComponent head , SummaryComponentStack tail |
341
- stack = SCS:: push ( head , tail ) and
342
- prev = evaluateSummaryComponentStackLocal ( call , tail )
357
+ prev = evaluateSummaryComponentStackLocal ( callable , call , tail ) and
358
+ dependsOnSummaryComponentStackCons ( callable , pragma [ only_bind_into ] ( head ) ,
359
+ pragma [ only_bind_out ] ( tail ) ) and
360
+ stack = SCS:: push ( pragma [ only_bind_out ] ( head ) , pragma [ only_bind_out ] ( tail ) )
343
361
|
344
362
exists ( DataFlowDispatch:: ArgumentPosition apos , DataFlowDispatch:: ParameterPosition ppos |
345
363
head = SummaryComponent:: parameter ( apos ) and
0 commit comments