@@ -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,25 @@ 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 }
322-
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" }
334-
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 ( ) }
341318 }
342319
343320 /** A source element. */
@@ -647,7 +624,7 @@ module Make<
647624 SummarizedCallableImpl callable , SummaryComponentStack input , SummaryComponentStack output ,
648625 string whichOne
649626 ) {
650- callable .propagatesFlow ( input , output , _, _) and
627+ callable .propagatesFlow ( input , output , _, _, _ , _ ) and
651628 (
652629 not isSupportedInputStack ( input ) and whichOne = "input"
653630 or
@@ -688,9 +665,9 @@ module Make<
688665
689666 private predicate summarySpec ( string spec ) {
690667 exists ( SummarizedCallable c |
691- c .propagatesFlow ( spec , _, _, _)
668+ c .propagatesFlow ( spec , _, _, _, _ , _ )
692669 or
693- c .propagatesFlow ( _, spec , _, _)
670+ c .propagatesFlow ( _, spec , _, _, _ , _ )
694671 )
695672 or
696673 isRelevantSource ( _, spec , _, _, _)
@@ -857,13 +834,9 @@ module Make<
857834 *
858835 * ```ql
859836 * private class CAdapter extends SummarizedCallable instanceof C {
860- * override predicate propagatesFlow(string input, string output, boolean preservesValue, string model) {
837+ * override predicate propagatesFlow(string input, string output, boolean preservesValue, Provenance p, string model) {
861838 * none()
862839 * }
863- *
864- * override predicate hasProvenance(Provenance provenance) {
865- * C.super.hasProvenance(provenance)
866- * }
867840 * }
868841 * ```
869842 */
@@ -897,32 +870,26 @@ module Make<
897870 pragma [ nomagic]
898871 abstract predicate propagatesFlow (
899872 SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
900- string model
873+ Provenance p , boolean isExact , string model
901874 ) ;
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 ) ;
908875 }
909876
910877 pragma [ nomagic]
911878 private predicate summary (
912879 SummarizedCallableImpl c , SummaryComponentStack input , SummaryComponentStack output ,
913880 boolean preservesValue , string model
914881 ) {
915- c .propagatesFlow ( input , output , preservesValue , model )
882+ c .propagatesFlow ( input , output , preservesValue , _ , _ , model )
916883 or
917884 // observe side effects of callbacks on input arguments
918- c .propagatesFlow ( output , input , preservesValue , model ) and
885+ c .propagatesFlow ( output , input , preservesValue , _ , _ , model ) and
919886 preservesValue = true and
920887 isCallbackParameter ( input ) and
921888 isContentOfArgument ( output , _)
922889 or
923890 // flow from the receiver of a callback into the instance-parameter
924891 exists ( SummaryComponentStack s , SummaryComponentStack callbackRef |
925- c .propagatesFlow ( s , _, _, model ) or c .propagatesFlow ( _, s , _, model )
892+ c .propagatesFlow ( s , _, _, _ , _ , model ) or c .propagatesFlow ( _, s , _ , _ , _, model )
926893 |
927894 callbackRef = s .drop ( _) and
928895 ( isCallbackParameter ( callbackRef ) or callbackRef .head ( ) = TReturnSummaryComponent ( _) ) and
@@ -948,8 +915,8 @@ module Make<
948915 SummaryComponentStack mid , boolean preservesValue1 , boolean preservesValue2 , string model1 ,
949916 string model2
950917 |
951- c .propagatesFlow ( input , mid , preservesValue1 , model1 ) and
952- c .propagatesFlow ( mid , output , preservesValue2 , model2 ) and
918+ c .propagatesFlow ( input , mid , preservesValue1 , _ , _ , model1 ) and
919+ c .propagatesFlow ( mid , output , preservesValue2 , _ , _ , model2 ) and
953920 mid .drop ( mid .length ( ) - 2 ) =
954921 SummaryComponentStack:: push ( TParameterSummaryComponent ( _) ,
955922 SummaryComponentStack:: singleton ( TArgumentSummaryComponent ( _) ) ) and
@@ -2048,18 +2015,29 @@ module Make<
20482015 {
20492016 override predicate propagatesFlow (
20502017 SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
2051- string model
2018+ Provenance p , boolean isExact , string model
20522019 ) {
20532020 exists ( AccessPath inSpec , AccessPath outSpec |
2054- SummarizedCallable .super .propagatesFlow ( inSpec , outSpec , preservesValue , model ) and
2021+ SummarizedCallable .super
2022+ .propagatesFlow ( inSpec , outSpec , preservesValue , p , isExact , model ) and
20552023 interpretSpec ( inSpec , input ) and
20562024 interpretSpec ( outSpec , output )
2025+ |
2026+ // Only apply generated or inexact models to functions in library code and
2027+ // when no strictly better model exists
2028+ if p .isGenerated ( ) or isExact = false
2029+ then
2030+ not callableFromSource ( this ) and
2031+ not exists ( Provenance other |
2032+ SummarizedCallable .super .propagatesFlow ( _, _, _, other , true , _)
2033+ |
2034+ p .isGenerated ( ) and other .isManual ( )
2035+ or
2036+ p .getVerification ( ) = other .getVerification ( ) and isExact = false
2037+ )
2038+ else any ( )
20572039 )
20582040 }
2059-
2060- override predicate hasProvenance ( Provenance provenance ) {
2061- SummarizedCallable .super .hasProvenance ( provenance )
2062- }
20632041 }
20642042
20652043 /** Holds if component `c` of specification `spec` cannot be parsed. */
@@ -2492,7 +2470,8 @@ module Make<
24922470 string getCallableCsv ( ) ;
24932471
24942472 predicate relevantSummary (
2495- SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue
2473+ SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue ,
2474+ Provenance p
24962475 ) ;
24972476 }
24982477
@@ -2505,13 +2484,6 @@ module Make<
25052484 preservesValue = false and result = "taint"
25062485 }
25072486
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-
25152487 /**
25162488 * Holds if there exists a relevant summary callable with information roughly corresponding to `csv`.
25172489 * Used for testing.
@@ -2521,15 +2493,15 @@ module Make<
25212493 query predicate summary ( string csv ) {
25222494 exists (
25232495 RelevantSummarizedCallable c , SummaryComponentStack input , SummaryComponentStack output ,
2524- boolean preservesValue
2496+ boolean preservesValue , Provenance p
25252497 |
2526- c .relevantSummary ( input , output , preservesValue ) and
2498+ c .relevantSummary ( input , output , preservesValue , p ) and
25272499 csv =
25282500 c .getCallableCsv ( ) // Callable information
25292501 + input .getMadRepresentation ( ) + ";" // input
25302502 + output .getMadRepresentation ( ) + ";" // output
25312503 + renderKind ( preservesValue ) + ";" // kind
2532- + renderProvenance ( c ) // provenance
2504+ + p // provenance
25332505 )
25342506 }
25352507 }
0 commit comments