@@ -73,8 +73,12 @@ signature module Input {
73
73
}
74
74
75
75
// Relating nodes to summaries
76
- /** Gets a dataflow node respresenting the argument of `call` indicated by `arg`. */
77
- Node argumentOf ( Node call , SummaryComponent arg ) ;
76
+ /**
77
+ * Gets a dataflow node respresenting the argument of `call` indicated by `arg`.
78
+ *
79
+ * Returns the post-update node of the argument when `isPostUpdate` is true.
80
+ */
81
+ Node argumentOf ( Node call , SummaryComponent arg , boolean isPostUpdate ) ;
78
82
79
83
/** Gets a dataflow node respresenting the parameter of `callable` indicated by `param`. */
80
84
Node parameterOf ( Node callable , SummaryComponent param ) ;
@@ -221,14 +225,18 @@ module SummaryFlow<Input I> implements Output<I> {
221
225
222
226
/**
223
227
* Gets a data flow `I::Node` corresponding an argument or return value of `call`,
224
- * as specified by `component`.
228
+ * as specified by `component`. `isOutput` indicates whether the node represents
229
+ * an output node or an input node.
225
230
*/
226
231
bindingset [ call, component]
227
- private I:: Node evaluateSummaryComponentLocal ( I:: Node call , I:: SummaryComponent component ) {
228
- result = I:: argumentOf ( call , component )
232
+ private I:: Node evaluateSummaryComponentLocal (
233
+ I:: Node call , I:: SummaryComponent component , boolean isOutput
234
+ ) {
235
+ result = I:: argumentOf ( call , component , isOutput )
229
236
or
230
237
component = I:: return ( ) and
231
- result = call
238
+ result = call and
239
+ isOutput = true
232
240
}
233
241
234
242
/**
@@ -280,27 +288,40 @@ module SummaryFlow<Input I> implements Output<I> {
280
288
*/
281
289
pragma [ nomagic]
282
290
private I:: Node evaluateSummaryComponentStackLocal (
283
- I:: SummarizedCallable callable , I:: Node call , I:: SummaryComponentStack stack
291
+ I:: SummarizedCallable callable , I:: Node call , I:: SummaryComponentStack stack , boolean isOutput
284
292
) {
285
293
exists ( I:: SummaryComponent component |
286
294
dependsOnSummaryComponentStackLeaf ( callable , component ) and
287
295
stack = I:: singleton ( component ) and
288
296
call = I:: callTo ( callable ) and
289
- result = evaluateSummaryComponentLocal ( call , component )
297
+ result = evaluateSummaryComponentLocal ( call , component , isOutput )
290
298
)
291
299
or
292
- exists ( I:: Node prev , I:: SummaryComponent head , I:: SummaryComponentStack tail |
293
- prev = evaluateSummaryComponentStackLocal ( callable , call , tail ) and
300
+ exists (
301
+ I:: Node prev , I:: SummaryComponent head , I:: SummaryComponentStack tail , boolean isOutput0
302
+ |
303
+ prev = evaluateSummaryComponentStackLocal ( callable , call , tail , isOutput0 ) and
294
304
dependsOnSummaryComponentStackConsLocal ( callable , pragma [ only_bind_into ] ( head ) ,
295
305
pragma [ only_bind_out ] ( tail ) ) and
296
306
stack = I:: push ( pragma [ only_bind_out ] ( head ) , pragma [ only_bind_out ] ( tail ) )
297
307
|
298
- result = I:: parameterOf ( prev , head )
308
+ // `Parameter[X]` is only allowed in the output of flow summaries (hence `isOutput = true`),
309
+ // however the target of the parameter (e.g. `Argument[Y].Parameter[X]`) should be fetched
310
+ // not from a post-update argument node (hence `isOutput0 = false`)
311
+ result = I:: parameterOf ( prev , head ) and
312
+ isOutput0 = false and
313
+ isOutput = true
299
314
or
300
- result = I:: returnOf ( prev , head )
315
+ // `ReturnValue` is only allowed in the input of flow summaries (hence `isOutput = false`),
316
+ // and the target of the return value (e.g. `Argument[X].ReturnValue`) should be fetched not
317
+ // from a post-update argument node (hence `isOutput0 = false`)
318
+ result = I:: returnOf ( prev , head ) and
319
+ isOutput0 = false and
320
+ isOutput = false
301
321
or
302
322
componentLevelStep ( head ) and
303
- result = prev
323
+ result = prev and
324
+ isOutput = isOutput0
304
325
)
305
326
}
306
327
@@ -312,8 +333,8 @@ module SummaryFlow<Input I> implements Output<I> {
312
333
|
313
334
callable .propagatesFlow ( input , output , true ) and
314
335
call = I:: callTo ( callable ) and
315
- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
316
- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
336
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
337
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
317
338
)
318
339
}
319
340
@@ -325,8 +346,8 @@ module SummaryFlow<Input I> implements Output<I> {
325
346
hasLoadSummary ( callable , content , pragma [ only_bind_into ] ( input ) ,
326
347
pragma [ only_bind_into ] ( output ) ) and
327
348
call = I:: callTo ( callable ) and
328
- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
329
- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
349
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
350
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
330
351
)
331
352
}
332
353
@@ -338,8 +359,8 @@ module SummaryFlow<Input I> implements Output<I> {
338
359
hasStoreSummary ( callable , content , pragma [ only_bind_into ] ( input ) ,
339
360
pragma [ only_bind_into ] ( output ) ) and
340
361
call = I:: callTo ( callable ) and
341
- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
342
- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
362
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
363
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
343
364
)
344
365
}
345
366
@@ -354,8 +375,8 @@ module SummaryFlow<Input I> implements Output<I> {
354
375
hasLoadStoreSummary ( callable , loadContent , storeContent , pragma [ only_bind_into ] ( input ) ,
355
376
pragma [ only_bind_into ] ( output ) ) and
356
377
call = I:: callTo ( callable ) and
357
- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
358
- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
378
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
379
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
359
380
)
360
381
}
361
382
@@ -369,8 +390,8 @@ module SummaryFlow<Input I> implements Output<I> {
369
390
hasWithoutContentSummary ( callable , filter , pragma [ only_bind_into ] ( input ) ,
370
391
pragma [ only_bind_into ] ( output ) ) and
371
392
call = I:: callTo ( callable ) and
372
- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
373
- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
393
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
394
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
374
395
)
375
396
}
376
397
@@ -384,8 +405,8 @@ module SummaryFlow<Input I> implements Output<I> {
384
405
hasWithContentSummary ( callable , filter , pragma [ only_bind_into ] ( input ) ,
385
406
pragma [ only_bind_into ] ( output ) ) and
386
407
call = I:: callTo ( callable ) and
387
- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
388
- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
408
+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
409
+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
389
410
)
390
411
}
391
412
}
0 commit comments