@@ -530,6 +530,85 @@ module Make<
530
530
}
531
531
}
532
532
533
+ private predicate isNonLocalSummaryComponent ( SummaryComponent c ) {
534
+ c instanceof TArgumentSummaryComponent or
535
+ c instanceof TParameterSummaryComponent or
536
+ c instanceof TReturnSummaryComponent
537
+ }
538
+
539
+ private predicate isLocalSummaryComponent ( SummaryComponent c ) {
540
+ not isNonLocalSummaryComponent ( c )
541
+ }
542
+
543
+ /**
544
+ * Holds if `s` is a valid input stack, in the sense that we generate data flow graph
545
+ * that faithfully represents this flow, and lambda-tracking can be expected to track
546
+ * lambdas to the relevant callbacks in practice.
547
+ */
548
+ private predicate isSupportedInputStack ( SummaryComponentStack s ) {
549
+ // Argument[n].*
550
+ s .length ( ) = 1 and
551
+ s .head ( ) instanceof TArgumentSummaryComponent
552
+ or
553
+ // Argument[n].ReturnValue.*
554
+ s .length ( ) = 2 and
555
+ s .head ( ) instanceof TReturnSummaryComponent and
556
+ s .tail ( ) .head ( ) instanceof TArgumentSummaryComponent
557
+ or
558
+ // Argument[n].Parameter[n].Content.*
559
+ s .length ( ) = 3 and
560
+ s .head ( ) instanceof TContentSummaryComponent and
561
+ s .tail ( ) .head ( ) instanceof TParameterSummaryComponent and
562
+ s .drop ( 2 ) .head ( ) instanceof TArgumentSummaryComponent
563
+ or
564
+ isSupportedInputStack ( s .tail ( ) ) and
565
+ isLocalSummaryComponent ( s .head ( ) )
566
+ }
567
+
568
+ /** Like `isSupportedInputStack` but for output stacks. */
569
+ private predicate isSupportedOutputStack ( SummaryComponentStack s ) {
570
+ // ReturnValue.*
571
+ s .length ( ) = 1 and
572
+ s .head ( ) instanceof TReturnSummaryComponent
573
+ or
574
+ // Argument[n].Content.*
575
+ s .length ( ) = 2 and
576
+ s .head ( ) instanceof TContentSummaryComponent and
577
+ s .tail ( ) .head ( ) instanceof TArgumentSummaryComponent
578
+ or
579
+ // Argument[n].Parameter[n].*
580
+ s .length ( ) = 2 and
581
+ s .head ( ) instanceof TParameterSummaryComponent and
582
+ s .tail ( ) .head ( ) instanceof TArgumentSummaryComponent
583
+ or
584
+ isSupportedOutputStack ( s .tail ( ) ) and
585
+ isLocalSummaryComponent ( s .head ( ) )
586
+ }
587
+
588
+ /**
589
+ * Holds if `callable` has an unsupported flow `input -> output`.
590
+ *
591
+ * `whichOne` indicates if the `input` or `output` contains the unsupported sequence.
592
+ */
593
+ predicate unsupportedCallable (
594
+ SummarizedCallableImpl callable , SummaryComponentStack input , SummaryComponentStack output ,
595
+ string whichOne
596
+ ) {
597
+ callable .propagatesFlow ( input , output , _, _) and
598
+ (
599
+ not isSupportedInputStack ( input ) and whichOne = "input"
600
+ or
601
+ not isSupportedOutputStack ( output ) and whichOne = "output"
602
+ )
603
+ }
604
+
605
+ /**
606
+ * Holds if `callable` has an unsupported flow.
607
+ */
608
+ predicate unsupportedCallable ( SummarizedCallableImpl callable ) {
609
+ unsupportedCallable ( callable , _, _, _)
610
+ }
611
+
533
612
private predicate summarySpec ( string spec ) {
534
613
exists ( SummarizedCallable c |
535
614
c .propagatesFlow ( spec , _, _, _)
0 commit comments