@@ -85,6 +85,9 @@ module Public {
8585 /** Holds if this stack contains summary component `c`. */
8686 predicate contains ( SummaryComponent c ) { c = this .drop ( _) .head ( ) }
8787
88+ /** Gets the bottom element of this stack. */
89+ SummaryComponent bottom ( ) { result = this .drop ( this .length ( ) - 1 ) .head ( ) }
90+
8891 /** Gets a textual representation of this stack. */
8992 string toString ( ) {
9093 exists ( SummaryComponent head , SummaryComponentStack tail |
@@ -197,6 +200,8 @@ module Private {
197200 or
198201 tail .( RequiredSummaryComponentStack ) .required ( TParameterSummaryComponent ( _) ) and
199202 head = thisParam ( )
203+ or
204+ derivedFluentFlowPush ( _, _, _, head , tail , _)
200205 }
201206
202207 pragma [ nomagic]
@@ -210,7 +215,7 @@ module Private {
210215 c .propagatesFlow ( output , input , preservesValue ) and
211216 preservesValue = true and
212217 isCallbackParameter ( input ) and
213- isContentOfArgument ( output )
218+ isContentOfArgument ( output , _ )
214219 or
215220 // flow from the receiver of a callback into the instance-parameter
216221 exists ( SummaryComponentStack s , SummaryComponentStack callbackRef |
@@ -222,16 +227,81 @@ module Private {
222227 output = TConsSummaryComponentStack ( thisParam ( ) , input ) and
223228 preservesValue = true
224229 )
230+ or
231+ exists ( SummaryComponentStack arg , SummaryComponentStack return |
232+ derivedFluentFlow ( c , input , arg , return , preservesValue )
233+ |
234+ arg .length ( ) = 1 and
235+ output = return
236+ or
237+ exists ( SummaryComponent head , SummaryComponentStack tail |
238+ derivedFluentFlowPush ( c , input , arg , head , tail , 0 ) and
239+ output = SummaryComponentStack:: push ( head , tail )
240+ )
241+ )
242+ or
243+ // Chain together summaries where values get passed into callbacks along the way
244+ exists ( SummaryComponentStack mid , boolean preservesValue1 , boolean preservesValue2 |
245+ c .propagatesFlow ( input , mid , preservesValue1 ) and
246+ c .propagatesFlow ( mid , output , preservesValue2 ) and
247+ mid .drop ( mid .length ( ) - 2 ) =
248+ SummaryComponentStack:: push ( TParameterSummaryComponent ( _) ,
249+ SummaryComponentStack:: singleton ( TArgumentSummaryComponent ( _) ) ) and
250+ preservesValue = preservesValue1 .booleanAnd ( preservesValue2 )
251+ )
252+ }
253+
254+ /**
255+ * Holds if `c` has a flow summary from `input` to `arg`, where `arg`
256+ * writes to (contents of) the `i`th argument, and `c` has a
257+ * value-preserving flow summary from the `i`th argument to a return value
258+ * (`return`).
259+ *
260+ * In such a case, we derive flow from `input` to (contents of) the return
261+ * value.
262+ *
263+ * As an example, this simplifies modeling of fluent methods:
264+ * for `StringBuilder.append(x)` with a specified value flow from qualifier to
265+ * return value and taint flow from argument 0 to the qualifier, then this
266+ * allows us to infer taint flow from argument 0 to the return value.
267+ */
268+ pragma [ nomagic]
269+ private predicate derivedFluentFlow (
270+ SummarizedCallable c , SummaryComponentStack input , SummaryComponentStack arg ,
271+ SummaryComponentStack return , boolean preservesValue
272+ ) {
273+ exists ( int i |
274+ summary ( c , input , arg , preservesValue ) and
275+ isContentOfArgument ( arg , i ) and
276+ summary ( c , SummaryComponentStack:: singleton ( TArgumentSummaryComponent ( i ) ) , return , true ) and
277+ return .bottom ( ) = TReturnSummaryComponent ( _)
278+ )
279+ }
280+
281+ pragma [ nomagic]
282+ private predicate derivedFluentFlowPush (
283+ SummarizedCallable c , SummaryComponentStack input , SummaryComponentStack arg ,
284+ SummaryComponent head , SummaryComponentStack tail , int i
285+ ) {
286+ derivedFluentFlow ( c , input , arg , tail , _) and
287+ head = arg .drop ( i ) .head ( ) and
288+ i = arg .length ( ) - 2
289+ or
290+ exists ( SummaryComponent head0 , SummaryComponentStack tail0 |
291+ derivedFluentFlowPush ( c , input , arg , head0 , tail0 , i + 1 ) and
292+ head = arg .drop ( i ) .head ( ) and
293+ tail = SummaryComponentStack:: push ( head0 , tail0 )
294+ )
225295 }
226296
227297 private predicate isCallbackParameter ( SummaryComponentStack s ) {
228298 s .head ( ) = TParameterSummaryComponent ( _) and exists ( s .tail ( ) )
229299 }
230300
231- private predicate isContentOfArgument ( SummaryComponentStack s ) {
232- s .head ( ) = TContentSummaryComponent ( _) and isContentOfArgument ( s .tail ( ) )
301+ private predicate isContentOfArgument ( SummaryComponentStack s , int i ) {
302+ s .head ( ) = TContentSummaryComponent ( _) and isContentOfArgument ( s .tail ( ) , i )
233303 or
234- s = TSingletonSummaryComponentStack ( TArgumentSummaryComponent ( _ ) )
304+ s = TSingletonSummaryComponentStack ( TArgumentSummaryComponent ( i ) )
235305 }
236306
237307 private predicate outputState ( SummarizedCallable c , SummaryComponentStack s ) {
@@ -508,9 +578,14 @@ module Private {
508578 * node, and back out to `p`.
509579 */
510580 predicate summaryAllowParameterReturnInSelf ( ParamNode p ) {
511- exists ( SummarizedCallable c , int i |
512- c .clearsContent ( i , _) and
513- p .isParameterOf ( c , i )
581+ exists ( SummarizedCallable c , int i | p .isParameterOf ( c , i ) |
582+ c .clearsContent ( i , _)
583+ or
584+ exists ( SummaryComponentStack inputContents , SummaryComponentStack outputContents |
585+ summary ( c , inputContents , outputContents , _) and
586+ inputContents .bottom ( ) = pragma [ only_bind_into ] ( TArgumentSummaryComponent ( i ) ) and
587+ outputContents .bottom ( ) = pragma [ only_bind_into ] ( TArgumentSummaryComponent ( i ) )
588+ )
514589 )
515590 }
516591
@@ -534,22 +609,6 @@ module Private {
534609 preservesValue = false and not summary ( c , inputContents , outputContents , true )
535610 )
536611 or
537- // If flow through a method updates a parameter from some input A, and that
538- // parameter also is returned through B, then we'd like a combined flow from A
539- // to B as well. As an example, this simplifies modeling of fluent methods:
540- // for `StringBuilder.append(x)` with a specified value flow from qualifier to
541- // return value and taint flow from argument 0 to the qualifier, then this
542- // allows us to infer taint flow from argument 0 to the return value.
543- succ instanceof ParamNode and
544- summaryPostUpdateNode ( pred , succ ) and
545- preservesValue = true
546- or
547- // Similarly we would like to chain together summaries where values get passed
548- // into callbacks along the way.
549- pred instanceof ArgNode and
550- summaryPostUpdateNode ( succ , pred ) and
551- preservesValue = true
552- or
553612 exists ( SummarizedCallable c , int i |
554613 pred .( ParamNode ) .isParameterOf ( c , i ) and
555614 succ = summaryNode ( c , TSummaryNodeClearsContentState ( i , _) ) and
0 commit comments