@@ -74,7 +74,7 @@ signature module Input {
7474
7575 // Relating nodes to summaries
7676 /** Gets a dataflow node respresenting the argument of `call` indicated by `arg`. */
77- Node argumentOf ( Node call , SummaryComponent arg ) ;
77+ Node argumentOf ( Node call , SummaryComponent arg , boolean isOutput ) ;
7878
7979 /** Gets a dataflow node respresenting the parameter of `callable` indicated by `param`. */
8080 Node parameterOf ( Node callable , SummaryComponent param ) ;
@@ -224,11 +224,14 @@ module SummaryFlow<Input I> implements Output<I> {
224224 * as specified by `component`.
225225 */
226226 bindingset [ call, component]
227- private I:: Node evaluateSummaryComponentLocal ( I:: Node call , I:: SummaryComponent component ) {
228- result = I:: argumentOf ( call , component )
227+ private I:: Node evaluateSummaryComponentLocal (
228+ I:: Node call , I:: SummaryComponent component , boolean isOutput
229+ ) {
230+ result = I:: argumentOf ( call , component , isOutput )
229231 or
230232 component = I:: return ( ) and
231- result = call
233+ result = call and
234+ isOutput = true
232235 }
233236
234237 /**
@@ -280,27 +283,34 @@ module SummaryFlow<Input I> implements Output<I> {
280283 */
281284 pragma [ nomagic]
282285 private I:: Node evaluateSummaryComponentStackLocal (
283- I:: SummarizedCallable callable , I:: Node call , I:: SummaryComponentStack stack
286+ I:: SummarizedCallable callable , I:: Node call , I:: SummaryComponentStack stack , boolean isOutput
284287 ) {
285288 exists ( I:: SummaryComponent component |
286289 dependsOnSummaryComponentStackLeaf ( callable , component ) and
287290 stack = I:: singleton ( component ) and
288291 call = I:: callTo ( callable ) and
289- result = evaluateSummaryComponentLocal ( call , component )
292+ result = evaluateSummaryComponentLocal ( call , component , isOutput )
290293 )
291294 or
292- exists ( I:: Node prev , I:: SummaryComponent head , I:: SummaryComponentStack tail |
293- prev = evaluateSummaryComponentStackLocal ( callable , call , tail ) and
295+ exists (
296+ I:: Node prev , I:: SummaryComponent head , I:: SummaryComponentStack tail , boolean isOutput0
297+ |
298+ prev = evaluateSummaryComponentStackLocal ( callable , call , tail , isOutput0 ) and
294299 dependsOnSummaryComponentStackConsLocal ( callable , pragma [ only_bind_into ] ( head ) ,
295300 pragma [ only_bind_out ] ( tail ) ) and
296301 stack = I:: push ( pragma [ only_bind_out ] ( head ) , pragma [ only_bind_out ] ( tail ) )
297302 |
298- result = I:: parameterOf ( prev , head )
303+ result = I:: parameterOf ( prev , head ) and
304+ isOutput0 = false and
305+ isOutput = true
299306 or
300- result = I:: returnOf ( prev , head )
307+ result = I:: returnOf ( prev , head ) and
308+ isOutput0 = false and
309+ isOutput = false
301310 or
302311 componentLevelStep ( head ) and
303- result = prev
312+ result = prev and
313+ isOutput = isOutput0
304314 )
305315 }
306316
@@ -312,8 +322,8 @@ module SummaryFlow<Input I> implements Output<I> {
312322 |
313323 callable .propagatesFlow ( input , output , true ) and
314324 call = I:: callTo ( callable ) and
315- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
316- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
325+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
326+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
317327 )
318328 }
319329
@@ -325,8 +335,8 @@ module SummaryFlow<Input I> implements Output<I> {
325335 hasLoadSummary ( callable , content , pragma [ only_bind_into ] ( input ) ,
326336 pragma [ only_bind_into ] ( output ) ) and
327337 call = I:: callTo ( callable ) and
328- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
329- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
338+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
339+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
330340 )
331341 }
332342
@@ -338,8 +348,8 @@ module SummaryFlow<Input I> implements Output<I> {
338348 hasStoreSummary ( callable , content , pragma [ only_bind_into ] ( input ) ,
339349 pragma [ only_bind_into ] ( output ) ) and
340350 call = I:: callTo ( callable ) and
341- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
342- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
351+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
352+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
343353 )
344354 }
345355
@@ -354,8 +364,8 @@ module SummaryFlow<Input I> implements Output<I> {
354364 hasLoadStoreSummary ( callable , loadContent , storeContent , pragma [ only_bind_into ] ( input ) ,
355365 pragma [ only_bind_into ] ( output ) ) and
356366 call = I:: callTo ( callable ) and
357- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
358- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
367+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
368+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
359369 )
360370 }
361371
@@ -369,8 +379,8 @@ module SummaryFlow<Input I> implements Output<I> {
369379 hasWithoutContentSummary ( callable , filter , pragma [ only_bind_into ] ( input ) ,
370380 pragma [ only_bind_into ] ( output ) ) and
371381 call = I:: callTo ( callable ) and
372- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
373- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
382+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
383+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
374384 )
375385 }
376386
@@ -384,8 +394,8 @@ module SummaryFlow<Input I> implements Output<I> {
384394 hasWithContentSummary ( callable , filter , pragma [ only_bind_into ] ( input ) ,
385395 pragma [ only_bind_into ] ( output ) ) and
386396 call = I:: callTo ( callable ) and
387- nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input ) and
388- nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output )
397+ nodeFrom = evaluateSummaryComponentStackLocal ( callable , call , input , false ) and
398+ nodeTo = evaluateSummaryComponentStackLocal ( callable , call , output , true )
389399 )
390400 }
391401}
0 commit comments