@@ -21,6 +21,10 @@ signature module InputSig<LocationSig Location, DF::InputSig<Location> Lang> {
2121 string toString ( ) ;
2222 }
2323
24+ /** Holds if `c` is defined in source code. */
25+ bindingset [ c]
26+ predicate callableFromSource ( SummarizedCallableBase c ) ;
27+
2428 /**
2529 * A base class of elements that are candidates for flow source modeling.
2630 */
@@ -268,6 +272,9 @@ module Make<
268272 this = verification and verification = "manual"
269273 }
270274
275+ /** Gets the verification part of this provenance. */
276+ string getVerification ( ) { result = verification }
277+
271278 /**
272279 * Holds if this is a valid generated provenance value.
273280 */
@@ -289,55 +296,42 @@ module Make<
289296 *
290297 * `preservesValue` indicates whether this is a value-preserving step or a taint-step.
291298 *
292- * If `model` is non-empty then it indicates the provenance of the model
293- * defining this flow.
299+ * `p` indicates the provenance of the flow.
300+ *
301+ * `isExact` indicates whether there exists a model for which this callable is an exact
302+ * match, that is, no overriding was used to identify this callable from the model.
303+ *
304+ * If `model` is non-empty then it indicates the origin of the model defining this flow.
294305 */
295306 pragma [ nomagic]
296307 abstract predicate propagatesFlow (
297- string input , string output , boolean preservesValue , string model
308+ string input , string output , boolean preservesValue , Provenance p , boolean isExact ,
309+ string model
298310 ) ;
299311
300- /**
301- * Holds if there exists a generated summary that applies to this callable.
302- */
303- final predicate hasGeneratedModel ( ) {
304- exists ( Provenance p | p .isGenerated ( ) and this .hasProvenance ( p ) )
305- }
306-
307- /**
308- * Holds if all the summaries that apply to this callable are auto generated and not manually created.
309- * That is, only apply generated models, when there are no manual models.
310- */
311- final predicate applyGeneratedModel ( ) {
312- this .hasGeneratedModel ( ) and
313- not this .hasManualModel ( )
314- }
315-
316312 /**
317313 * Holds if there exists a manual summary that applies to this callable.
318314 */
319315 final predicate hasManualModel ( ) {
320- exists ( Provenance p | p . isManual ( ) and this . hasProvenance ( p ) )
316+ any ( Provenance p | this . propagatesFlow ( _ , _ , _ , p , _ , _ ) ) . isManual ( )
321317 }
318+ }
322319
323- /**
324- * Holds if there exists a manual summary that applies to this callable.
325- * Always apply manual models if they exist.
326- */
327- final predicate applyManualModel ( ) { this .hasManualModel ( ) }
328-
329- /**
330- * Holds if there exists a summary that applies to this callable
331- * that has provenance `provenance`.
332- */
333- predicate hasProvenance ( Provenance provenance ) { provenance = "manual" }
320+ final private class SummarizedCallableFinal = SummarizedCallable ;
334321
335- /**
336- * Holds if there exists a model for which this callable is an exact
337- * match, that is, no overriding was used to identify this callable from
338- * the model.
339- */
340- predicate hasExactModel ( ) { none ( ) }
322+ /**
323+ * A callable with a relevant flow summary.
324+ *
325+ * A flow summary is relevant if:
326+ *
327+ * - It is manual exact model, or
328+ * - It is a manual inexact model and there is no exact manual (neutral) model, or
329+ * - It is a generated model and (a) there is no source code available for the modeled
330+ * callable, (b) there is no manual (neutral) model, and (c) the model is inexact
331+ * and there is no generated exact (neutral) model.
332+ */
333+ final class RelevantSummarizedCallable extends SummarizedCallableFinal {
334+ RelevantSummarizedCallable ( ) { this instanceof SummarizedCallableImpl }
341335 }
342336
343337 /** A source element. */
@@ -476,6 +470,41 @@ module Make<
476470 module Private {
477471 private import Public
478472
473+ /**
474+ * Holds if `c` has a relevant flow summary.
475+ *
476+ * A flow summary is relevant if:
477+ *
478+ * - It is manual exact model, or
479+ * - It is a manual inexact model and there is no exact manual (neutral) model, or
480+ * - It is a generated model and (a) there is no source code available for the modeled
481+ * callable, (b) there is no manual (neutral) model, and (c) the model is inexact
482+ * and there is no generated exact (neutral) model.
483+ */
484+ predicate relevantSummary (
485+ SummarizedCallable c , string input , string output , boolean preservesValue , Provenance p ,
486+ boolean isExact , string model
487+ ) {
488+ c .propagatesFlow ( input , output , preservesValue , p , isExact , model ) and
489+ if p .isGenerated ( ) or isExact = false
490+ then
491+ // Only apply generated models to functions in library code
492+ not ( p .isGenerated ( ) and callableFromSource ( c ) ) and
493+ // Only apply generated or inexact models when no strictly better model exists
494+ not exists ( Provenance other , boolean isExactOther |
495+ c .propagatesFlow ( _, _, _, other , isExactOther , _)
496+ or
497+ neutralElement ( c , "summary" , other , isExactOther )
498+ |
499+ p .isGenerated ( ) and other .isManual ( )
500+ or
501+ p .getVerification ( ) = other .getVerification ( ) and
502+ isExact = false and
503+ isExactOther = true
504+ )
505+ else any ( )
506+ }
507+
479508 /**
480509 * A synthetic global. This represents some form of global state, which
481510 * summaries can read and write individually.
@@ -647,7 +676,7 @@ module Make<
647676 SummarizedCallableImpl callable , SummaryComponentStack input , SummaryComponentStack output ,
648677 string whichOne
649678 ) {
650- callable .propagatesFlow ( input , output , _, _) and
679+ callable .propagatesFlow ( input , output , _, _, _ , _ ) and
651680 (
652681 not isSupportedInputStack ( input ) and whichOne = "input"
653682 or
@@ -688,9 +717,9 @@ module Make<
688717
689718 private predicate summarySpec ( string spec ) {
690719 exists ( SummarizedCallable c |
691- c .propagatesFlow ( spec , _, _, _)
720+ c .propagatesFlow ( spec , _, _, _, _ , _ )
692721 or
693- c .propagatesFlow ( _, spec , _, _)
722+ c .propagatesFlow ( _, spec , _, _, _ , _ )
694723 )
695724 or
696725 isRelevantSource ( _, spec , _, _, _)
@@ -848,7 +877,7 @@ module Make<
848877 }
849878
850879 /**
851- * A callable with a flow summary.
880+ * A callable with a relevant flow summary.
852881 *
853882 * This interface is not meant to be used directly, instead use the public
854883 * `SummarizedCallable` interface. However, _if_ you need to use this, make
@@ -857,13 +886,9 @@ module Make<
857886 *
858887 * ```ql
859888 * private class CAdapter extends SummarizedCallable instanceof C {
860- * override predicate propagatesFlow(string input, string output, boolean preservesValue, string model) {
889+ * override predicate propagatesFlow(string input, string output, boolean preservesValue, Provenance p, string model) {
861890 * none()
862891 * }
863- *
864- * override predicate hasProvenance(Provenance provenance) {
865- * C.super.hasProvenance(provenance)
866- * }
867892 * }
868893 * ```
869894 */
@@ -897,32 +922,26 @@ module Make<
897922 pragma [ nomagic]
898923 abstract predicate propagatesFlow (
899924 SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
900- string model
925+ Provenance p , boolean isExact , string model
901926 ) ;
902-
903- /**
904- * Holds if there exists a summary that applies to this callable
905- * that has provenance `provenance`.
906- */
907- abstract predicate hasProvenance ( Provenance provenance ) ;
908927 }
909928
910929 pragma [ nomagic]
911930 private predicate summary (
912931 SummarizedCallableImpl c , SummaryComponentStack input , SummaryComponentStack output ,
913932 boolean preservesValue , string model
914933 ) {
915- c .propagatesFlow ( input , output , preservesValue , model )
934+ c .propagatesFlow ( input , output , preservesValue , _ , _ , model )
916935 or
917936 // observe side effects of callbacks on input arguments
918- c .propagatesFlow ( output , input , preservesValue , model ) and
937+ c .propagatesFlow ( output , input , preservesValue , _ , _ , model ) and
919938 preservesValue = true and
920939 isCallbackParameter ( input ) and
921940 isContentOfArgument ( output , _)
922941 or
923942 // flow from the receiver of a callback into the instance-parameter
924943 exists ( SummaryComponentStack s , SummaryComponentStack callbackRef |
925- c .propagatesFlow ( s , _, _, model ) or c .propagatesFlow ( _, s , _, model )
944+ c .propagatesFlow ( s , _, _, _ , _ , model ) or c .propagatesFlow ( _, s , _ , _ , _, model )
926945 |
927946 callbackRef = s .drop ( _) and
928947 ( isCallbackParameter ( callbackRef ) or callbackRef .head ( ) = TReturnSummaryComponent ( _) ) and
@@ -948,8 +967,8 @@ module Make<
948967 SummaryComponentStack mid , boolean preservesValue1 , boolean preservesValue2 , string model1 ,
949968 string model2
950969 |
951- c .propagatesFlow ( input , mid , preservesValue1 , model1 ) and
952- c .propagatesFlow ( mid , output , preservesValue2 , model2 ) and
970+ c .propagatesFlow ( input , mid , preservesValue1 , _ , _ , model1 ) and
971+ c .propagatesFlow ( mid , output , preservesValue2 , _ , _ , model2 ) and
953972 mid .drop ( mid .length ( ) - 2 ) =
954973 SummaryComponentStack:: push ( TParameterSummaryComponent ( _) ,
955974 SummaryComponentStack:: singleton ( TArgumentSummaryComponent ( _) ) ) and
@@ -2046,19 +2065,31 @@ module Make<
20462065 // adapter class for converting `SummarizedCallable`s to `SummarizedCallableImpl`s
20472066 private class SummarizedCallableImplAdapter extends SummarizedCallableImpl instanceof SummarizedCallable
20482067 {
2049- override predicate propagatesFlow (
2050- SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
2051- string model
2052- ) {
2068+ private SummaryComponentStack input_ ;
2069+ private SummaryComponentStack output_ ;
2070+ private boolean preservesValue_ ;
2071+ private Provenance p_ ;
2072+ private boolean isExact_ ;
2073+ private string model_ ;
2074+
2075+ SummarizedCallableImplAdapter ( ) {
20532076 exists ( AccessPath inSpec , AccessPath outSpec |
2054- SummarizedCallable . super . propagatesFlow ( inSpec , outSpec , preservesValue , model ) and
2055- interpretSpec ( inSpec , input ) and
2056- interpretSpec ( outSpec , output )
2077+ relevantSummary ( this , inSpec , outSpec , preservesValue_ , p_ , isExact_ , model_ ) and
2078+ interpretSpec ( inSpec , input_ ) and
2079+ interpretSpec ( outSpec , output_ )
20572080 )
20582081 }
20592082
2060- override predicate hasProvenance ( Provenance provenance ) {
2061- SummarizedCallable .super .hasProvenance ( provenance )
2083+ override predicate propagatesFlow (
2084+ SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
2085+ Provenance p , boolean isExact , string model
2086+ ) {
2087+ input = input_ and
2088+ output = output_ and
2089+ preservesValue = preservesValue_ and
2090+ p = p_ and
2091+ isExact = isExact_ and
2092+ model = model_
20622093 }
20632094 }
20642095
@@ -2492,26 +2523,20 @@ module Make<
24922523 string getCallableCsv ( ) ;
24932524
24942525 predicate relevantSummary (
2495- SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue
2526+ SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
2527+ Provenance p
24962528 ) ;
24972529 }
24982530
24992531 /** Provides a query predicate for outputting a set of relevant flow summaries. */
2500- module TestSummaryOutput< RelevantSummarizedCallableSig RelevantSummarizedCallable > {
2532+ module TestSummaryOutput< RelevantSummarizedCallableSig RelSummarizedCallable > {
25012533 /** Render the kind in the format used in flow summaries. */
25022534 private string renderKind ( boolean preservesValue ) {
25032535 preservesValue = true and result = "value"
25042536 or
25052537 preservesValue = false and result = "taint"
25062538 }
25072539
2508- private string renderProvenance ( SummarizedCallable c ) {
2509- exists ( Provenance p | p .isManual ( ) and c .hasProvenance ( p ) and result = p .toString ( ) )
2510- or
2511- not c .applyManualModel ( ) and
2512- c .hasProvenance ( result )
2513- }
2514-
25152540 /**
25162541 * Holds if there exists a relevant summary callable with information roughly corresponding to `csv`.
25172542 * Used for testing.
@@ -2520,16 +2545,16 @@ module Make<
25202545 */
25212546 query predicate summary ( string csv ) {
25222547 exists (
2523- RelevantSummarizedCallable c , SummaryComponentStack input , SummaryComponentStack output ,
2524- boolean preservesValue
2548+ RelSummarizedCallable c , SummaryComponentStack input , SummaryComponentStack output ,
2549+ boolean preservesValue , Provenance p
25252550 |
2526- c .relevantSummary ( input , output , preservesValue ) and
2551+ c .relevantSummary ( input , output , preservesValue , p ) and
25272552 csv =
25282553 c .getCallableCsv ( ) // Callable information
25292554 + input .getMadRepresentation ( ) + ";" // input
25302555 + output .getMadRepresentation ( ) + ";" // output
25312556 + renderKind ( preservesValue ) + ";" // kind
2532- + renderProvenance ( c ) // provenance
2557+ + p // provenance
25332558 )
25342559 }
25352560 }
0 commit comments