@@ -73,8 +73,12 @@ signature module Input {
7373 }
7474
7575 // 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 ) ;
7882
7983 /** Gets a dataflow node respresenting the parameter of `callable` indicated by `param`. */
8084 Node parameterOf ( Node callable , SummaryComponent param ) ;
@@ -221,14 +225,18 @@ module SummaryFlow<Input I> implements Output<I> {
221225
222226 /**
223227 * 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.
225230 */
226231 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 )
229236 or
230237 component = I:: return ( ) and
231- result = call
238+ result = call and
239+ isOutput = true
232240 }
233241
234242 /**
@@ -280,27 +288,40 @@ module SummaryFlow<Input I> implements Output<I> {
280288 */
281289 pragma [ nomagic]
282290 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
284292 ) {
285293 exists ( I:: SummaryComponent component |
286294 dependsOnSummaryComponentStackLeaf ( callable , component ) and
287295 stack = I:: singleton ( component ) and
288296 call = I:: callTo ( callable ) and
289- result = evaluateSummaryComponentLocal ( call , component )
297+ result = evaluateSummaryComponentLocal ( call , component , isOutput )
290298 )
291299 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
294304 dependsOnSummaryComponentStackConsLocal ( callable , pragma [ only_bind_into ] ( head ) ,
295305 pragma [ only_bind_out ] ( tail ) ) and
296306 stack = I:: push ( pragma [ only_bind_out ] ( head ) , pragma [ only_bind_out ] ( tail ) )
297307 |
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
299314 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
301321 or
302322 componentLevelStep ( head ) and
303- result = prev
323+ result = prev and
324+ isOutput = isOutput0
304325 )
305326 }
306327
@@ -312,8 +333,8 @@ module SummaryFlow<Input I> implements Output<I> {
312333 |
313334 callable .propagatesFlow ( input , output , true ) and
314335 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 )
317338 )
318339 }
319340
@@ -325,8 +346,8 @@ module SummaryFlow<Input I> implements Output<I> {
325346 hasLoadSummary ( callable , content , pragma [ only_bind_into ] ( input ) ,
326347 pragma [ only_bind_into ] ( output ) ) and
327348 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 )
330351 )
331352 }
332353
@@ -338,8 +359,8 @@ module SummaryFlow<Input I> implements Output<I> {
338359 hasStoreSummary ( callable , content , pragma [ only_bind_into ] ( input ) ,
339360 pragma [ only_bind_into ] ( output ) ) and
340361 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 )
343364 )
344365 }
345366
@@ -354,8 +375,8 @@ module SummaryFlow<Input I> implements Output<I> {
354375 hasLoadStoreSummary ( callable , loadContent , storeContent , pragma [ only_bind_into ] ( input ) ,
355376 pragma [ only_bind_into ] ( output ) ) and
356377 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 )
359380 )
360381 }
361382
@@ -369,8 +390,8 @@ module SummaryFlow<Input I> implements Output<I> {
369390 hasWithoutContentSummary ( callable , filter , pragma [ only_bind_into ] ( input ) ,
370391 pragma [ only_bind_into ] ( output ) ) and
371392 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 )
374395 )
375396 }
376397
@@ -384,8 +405,8 @@ module SummaryFlow<Input I> implements Output<I> {
384405 hasWithContentSummary ( callable , filter , pragma [ only_bind_into ] ( input ) ,
385406 pragma [ only_bind_into ] ( output ) ) and
386407 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 )
389410 )
390411 }
391412}
0 commit comments