@@ -380,20 +380,23 @@ private Declaration interpretExt(Declaration d, ExtPath ext) {
380380/** Gets the source/sink/summary/neutral element corresponding to the supplied parameters. */
381381pragma [ nomagic]
382382Declaration interpretElement (
383- string namespace , string type , boolean subtypes , string name , string signature , string ext
383+ string namespace , string type , boolean subtypes , string name , string signature , string ext ,
384+ boolean isExact
384385) {
385386 elementSpec ( namespace , type , subtypes , name , signature , ext ) and
386387 exists ( Declaration base , Declaration d |
387388 base = interpretBaseDeclaration ( namespace , type , name , signature ) and
388389 (
389- d = base
390+ d = base and
391+ isExact = true
390392 or
391393 subtypes = true and
392394 (
393395 d .( UnboundCallable ) .overridesOrImplementsUnbound ( base )
394396 or
395397 d = base .( UnboundValueOrRefType ) .getASubTypeUnbound + ( )
396- )
398+ ) and
399+ isExact = false
397400 )
398401 |
399402 result = interpretExt ( d , ext )
@@ -586,71 +589,47 @@ string getSignature(UnboundCallable c) {
586589}
587590
588591private predicate interpretSummary (
589- UnboundCallable c , string input , string output , string kind , string provenance , string model
592+ UnboundCallable c , string input , string output , string kind , string provenance , boolean isExact ,
593+ string model
590594) {
591595 exists (
592596 string namespace , string type , boolean subtypes , string name , string signature , string ext
593597 |
594598 summaryModel ( namespace , type , subtypes , name , signature , ext , input , output , kind , provenance ,
595599 model ) and
596- c = interpretElement ( namespace , type , subtypes , name , signature , ext )
600+ c = interpretElement ( namespace , type , subtypes , name , signature , ext , isExact )
597601 )
598602}
599603
600- predicate interpretNeutral ( UnboundCallable c , string kind , string provenance ) {
604+ predicate interpretNeutral ( UnboundCallable c , string kind , string provenance , boolean isExact ) {
601605 exists ( string namespace , string type , string name , string signature |
602606 Extensions:: neutralModel ( namespace , type , name , signature , kind , provenance ) and
603- c = interpretElement ( namespace , type , true , name , signature , "" )
607+ c = interpretElement ( namespace , type , true , name , signature , "" , isExact )
604608 )
605609}
606610
607611// adapter class for converting Mad summaries to `SummarizedCallable`s
608612private class SummarizedCallableAdapter extends SummarizedCallable {
609- SummarizedCallableAdapter ( ) {
610- exists ( Provenance provenance | interpretSummary ( this , _, _, _, provenance , _) |
611- not this .fromSource ( )
612- or
613- this .fromSource ( ) and provenance .isManual ( )
614- )
615- }
616-
617- private predicate relevantSummaryElementManual (
618- string input , string output , string kind , string model
619- ) {
620- exists ( Provenance provenance |
621- interpretSummary ( this , input , output , kind , provenance , model ) and
622- provenance .isManual ( )
623- )
624- }
613+ string input_ ;
614+ string output_ ;
615+ string kind ;
616+ Provenance p_ ;
617+ boolean isExact_ ;
618+ string model_ ;
625619
626- private predicate relevantSummaryElementGenerated (
627- string input , string output , string kind , string model
628- ) {
629- exists ( Provenance provenance |
630- interpretSummary ( this , input , output , kind , provenance , model ) and
631- provenance .isGenerated ( )
632- ) and
633- not exists ( Provenance provenance |
634- interpretNeutral ( this , "summary" , provenance ) and
635- provenance .isManual ( )
636- )
620+ SummarizedCallableAdapter ( ) {
621+ interpretSummary ( this , input_ , output_ , kind , p_ , isExact_ , model_ )
637622 }
638623
639624 override predicate propagatesFlow (
640- string input , string output , boolean preservesValue , string model
625+ string input , string output , boolean preservesValue , Provenance p , boolean isExact , string model
641626 ) {
642- exists ( string kind |
643- this .relevantSummaryElementManual ( input , output , kind , model )
644- or
645- not this .relevantSummaryElementManual ( _, _, _, _) and
646- this .relevantSummaryElementGenerated ( input , output , kind , model )
647- |
648- if kind = "value" then preservesValue = true else preservesValue = false
649- )
650- }
651-
652- override predicate hasProvenance ( Provenance provenance ) {
653- interpretSummary ( this , _, _, _, provenance , _)
627+ input = input_ and
628+ output = output_ and
629+ ( if kind = "value" then preservesValue = true else preservesValue = false ) and
630+ p = p_ and
631+ isExact = isExact_ and
632+ model = model_
654633 }
655634}
656635
0 commit comments