@@ -354,15 +354,19 @@ private predicate hasStoreSummary(
354
354
SummarizedCallable callable , DataFlow:: ContentSet contents , SummaryComponentStack input ,
355
355
SummaryComponentStack output
356
356
) {
357
- callable .propagatesFlow ( input , push ( SummaryComponent:: content ( contents ) , output ) , true )
357
+ callable .propagatesFlow ( input , push ( SummaryComponent:: content ( contents ) , output ) , true ) and
358
+ not isNonLocal ( input .head ( ) ) and
359
+ not isNonLocal ( output .head ( ) )
358
360
}
359
361
360
362
pragma [ nomagic]
361
363
private predicate hasLoadSummary (
362
364
SummarizedCallable callable , DataFlow:: ContentSet contents , SummaryComponentStack input ,
363
365
SummaryComponentStack output
364
366
) {
365
- callable .propagatesFlow ( push ( SummaryComponent:: content ( contents ) , input ) , output , true )
367
+ callable .propagatesFlow ( push ( SummaryComponent:: content ( contents ) , input ) , output , true ) and
368
+ not isNonLocal ( input .head ( ) ) and
369
+ not isNonLocal ( output .head ( ) )
366
370
}
367
371
368
372
pragma [ nomagic]
@@ -373,6 +377,8 @@ private predicate hasLoadStoreSummary(
373
377
callable
374
378
.propagatesFlow ( push ( SummaryComponent:: content ( loadContents ) , input ) ,
375
379
push ( SummaryComponent:: content ( storeContents ) , output ) , true ) and
380
+ not isNonLocal ( input .head ( ) ) and
381
+ not isNonLocal ( output .head ( ) ) and
376
382
callable != "Hash.[]" // Special-cased due to having a huge number of summaries
377
383
}
378
384
@@ -408,6 +414,8 @@ private predicate hasWithoutContentSummary(
408
414
exists ( DataFlow:: ContentSet content |
409
415
callable .propagatesFlow ( push ( SummaryComponent:: withoutContent ( content ) , input ) , output , true ) and
410
416
filter = getFilterFromWithoutContentStep ( content ) and
417
+ not isNonLocal ( input .head ( ) ) and
418
+ not isNonLocal ( output .head ( ) ) and
411
419
input != output
412
420
)
413
421
}
@@ -444,10 +452,22 @@ private predicate hasWithContentSummary(
444
452
exists ( DataFlow:: ContentSet content |
445
453
callable .propagatesFlow ( push ( SummaryComponent:: withContent ( content ) , input ) , output , true ) and
446
454
filter = getFilterFromWithContentStep ( content ) and
455
+ not isNonLocal ( input .head ( ) ) and
456
+ not isNonLocal ( output .head ( ) ) and
447
457
input != output
448
458
)
449
459
}
450
460
461
+ /**
462
+ * Holds if the given component can't be evaluated by `evaluateSummaryComponentStackLocal`.
463
+ */
464
+ pragma [ nomagic]
465
+ predicate isNonLocal ( SummaryComponent component ) {
466
+ component = SC:: content ( _)
467
+ or
468
+ component = SC:: withContent ( _)
469
+ }
470
+
451
471
/**
452
472
* Gets a data flow node corresponding an argument or return value of `call`,
453
473
* as specified by `component`.
@@ -490,6 +510,14 @@ private predicate dependsOnSummaryComponentStackCons(
490
510
dependsOnSummaryComponentStack ( callable , SCS:: push ( head , tail ) )
491
511
}
492
512
513
+ pragma [ nomagic]
514
+ private predicate dependsOnSummaryComponentStackConsLocal (
515
+ SummarizedCallable callable , SummaryComponent head , SummaryComponentStack tail
516
+ ) {
517
+ dependsOnSummaryComponentStackCons ( callable , head , tail ) and
518
+ not isNonLocal ( head )
519
+ }
520
+
493
521
pragma [ nomagic]
494
522
private predicate dependsOnSummaryComponentStackLeaf (
495
523
SummarizedCallable callable , SummaryComponent leaf
@@ -514,7 +542,7 @@ private DataFlow::Node evaluateSummaryComponentStackLocal(
514
542
or
515
543
exists ( DataFlow:: Node prev , SummaryComponent head , SummaryComponentStack tail |
516
544
prev = evaluateSummaryComponentStackLocal ( callable , call , tail ) and
517
- dependsOnSummaryComponentStackCons ( callable , pragma [ only_bind_into ] ( head ) ,
545
+ dependsOnSummaryComponentStackConsLocal ( callable , pragma [ only_bind_into ] ( head ) ,
518
546
pragma [ only_bind_out ] ( tail ) ) and
519
547
stack = SCS:: push ( pragma [ only_bind_out ] ( head ) , pragma [ only_bind_out ] ( tail ) )
520
548
|
0 commit comments