@@ -186,10 +186,17 @@ module Private {
186186 TArgumentSummaryComponent ( int i ) { parameterPosition ( i ) } or
187187 TReturnSummaryComponent ( ReturnKind rk )
188188
189+ private TSummaryComponent thisParam ( ) {
190+ result = TParameterSummaryComponent ( instanceParameterPosition ( ) )
191+ }
192+
189193 newtype TSummaryComponentStack =
190194 TSingletonSummaryComponentStack ( SummaryComponent c ) or
191195 TConsSummaryComponentStack ( SummaryComponent head , SummaryComponentStack tail ) {
192196 tail .( RequiredSummaryComponentStack ) .required ( head )
197+ or
198+ tail .( RequiredSummaryComponentStack ) .required ( TParameterSummaryComponent ( _) ) and
199+ head = thisParam ( )
193200 }
194201
195202 pragma [ nomagic]
@@ -198,21 +205,63 @@ module Private {
198205 boolean preservesValue
199206 ) {
200207 c .propagatesFlow ( input , output , preservesValue )
208+ or
209+ // observe side effects of callbacks on input arguments
210+ c .propagatesFlow ( output , input , preservesValue ) and
211+ preservesValue = true and
212+ isCallbackParameter ( input ) and
213+ isContentOfArgument ( output )
214+ or
215+ // flow from the receiver of a callback into the instance-parameter
216+ exists ( SummaryComponentStack s , SummaryComponentStack callbackRef |
217+ c .propagatesFlow ( s , _, _) or c .propagatesFlow ( _, s , _)
218+ |
219+ callbackRef = s .drop ( _) and
220+ ( isCallbackParameter ( callbackRef ) or callbackRef .head ( ) = TReturnSummaryComponent ( _) ) and
221+ input = callbackRef .tail ( ) and
222+ output = TConsSummaryComponentStack ( thisParam ( ) , input ) and
223+ preservesValue = true
224+ )
225+ }
226+
227+ private predicate isCallbackParameter ( SummaryComponentStack s ) {
228+ s .head ( ) = TParameterSummaryComponent ( _) and exists ( s .tail ( ) )
229+ }
230+
231+ private predicate isContentOfArgument ( SummaryComponentStack s ) {
232+ s .head ( ) = TContentSummaryComponent ( _) and isContentOfArgument ( s .tail ( ) )
233+ or
234+ s = TSingletonSummaryComponentStack ( TArgumentSummaryComponent ( _) )
235+ }
236+
237+ private predicate outputState ( SummarizedCallable c , SummaryComponentStack s ) {
238+ summary ( c , _, s , _)
239+ or
240+ exists ( SummaryComponentStack out |
241+ outputState ( c , out ) and
242+ out .head ( ) = TContentSummaryComponent ( _) and
243+ s = out .tail ( )
244+ )
245+ or
246+ // Add the argument node corresponding to the requested post-update node
247+ inputState ( c , s ) and isCallbackParameter ( s )
248+ }
249+
250+ private predicate inputState ( SummarizedCallable c , SummaryComponentStack s ) {
251+ summary ( c , s , _, _)
252+ or
253+ exists ( SummaryComponentStack inp | inputState ( c , inp ) and s = inp .tail ( ) )
254+ or
255+ exists ( SummaryComponentStack out |
256+ outputState ( c , out ) and
257+ out .head ( ) = TParameterSummaryComponent ( _) and
258+ s = out .tail ( )
259+ )
201260 }
202261
203262 private newtype TSummaryNodeState =
204- TSummaryNodeInputState ( SummaryComponentStack s ) {
205- exists ( SummaryComponentStack input |
206- summary ( _, input , _, _) and
207- s = input .drop ( _)
208- )
209- } or
210- TSummaryNodeOutputState ( SummaryComponentStack s ) {
211- exists ( SummaryComponentStack output |
212- summary ( _, _, output , _) and
213- s = output .drop ( _)
214- )
215- }
263+ TSummaryNodeInputState ( SummaryComponentStack s ) { inputState ( _, s ) } or
264+ TSummaryNodeOutputState ( SummaryComponentStack s ) { outputState ( _, s ) }
216265
217266 /**
218267 * A state used to break up (complex) flow summaries into atomic flow steps.
@@ -238,20 +287,14 @@ module Private {
238287 pragma [ nomagic]
239288 predicate isInputState ( SummarizedCallable c , SummaryComponentStack s ) {
240289 this = TSummaryNodeInputState ( s ) and
241- exists ( SummaryComponentStack input |
242- summary ( c , input , _, _) and
243- s = input .drop ( _)
244- )
290+ inputState ( c , s )
245291 }
246292
247293 /** Holds if this state is a valid output state for `c`. */
248294 pragma [ nomagic]
249295 predicate isOutputState ( SummarizedCallable c , SummaryComponentStack s ) {
250296 this = TSummaryNodeOutputState ( s ) and
251- exists ( SummaryComponentStack output |
252- summary ( c , _, output , _) and
253- s = output .drop ( _)
254- )
297+ outputState ( c , s )
255298 }
256299
257300 /** Gets a textual representation of this state. */
@@ -331,19 +374,12 @@ module Private {
331374 receiver = summaryNodeInputState ( c , s .drop ( 1 ) )
332375 }
333376
334- private Node pre ( Node post ) {
335- summaryPostUpdateNode ( post , result )
336- or
337- not summaryPostUpdateNode ( post , _) and
338- result = post
339- }
340-
341377 private predicate callbackInput (
342378 SummarizedCallable c , SummaryComponentStack s , Node receiver , int i
343379 ) {
344380 any ( SummaryNodeState state ) .isOutputState ( c , s ) and
345381 s .head ( ) = TParameterSummaryComponent ( i ) and
346- receiver = pre ( summaryNodeOutputState ( c , s .drop ( 1 ) ) )
382+ receiver = summaryNodeInputState ( c , s .drop ( 1 ) )
347383 }
348384
349385 /** Holds if a call targeting `receiver` should be synthesized inside `c`. */
@@ -395,7 +431,7 @@ module Private {
395431 or
396432 exists ( int i | head = TParameterSummaryComponent ( i ) |
397433 result =
398- getCallbackParameterType ( getNodeType ( summaryNodeOutputState ( pragma [ only_bind_out ] ( c ) ,
434+ getCallbackParameterType ( getNodeType ( summaryNodeInputState ( pragma [ only_bind_out ] ( c ) ,
399435 s .drop ( 1 ) ) ) , i )
400436 )
401437 )
@@ -421,10 +457,16 @@ module Private {
421457 }
422458
423459 /** Holds if summary node `post` is a post-update node with pre-update node `pre`. */
424- predicate summaryPostUpdateNode ( Node post , ParamNode pre ) {
460+ predicate summaryPostUpdateNode ( Node post , Node pre ) {
425461 exists ( SummarizedCallable c , int i |
426462 isParameterPostUpdate ( post , c , i ) and
427- pre .isParameterOf ( c , i )
463+ pre .( ParamNode ) .isParameterOf ( c , i )
464+ )
465+ or
466+ exists ( SummarizedCallable callable , SummaryComponentStack s |
467+ callbackInput ( callable , s , _, _) and
468+ pre = summaryNodeOutputState ( callable , s ) and
469+ post = summaryNodeInputState ( callable , s )
428470 )
429471 }
430472
@@ -462,7 +504,11 @@ module Private {
462504 // for `StringBuilder.append(x)` with a specified value flow from qualifier to
463505 // return value and taint flow from argument 0 to the qualifier, then this
464506 // allows us to infer taint flow from argument 0 to the return value.
465- summaryPostUpdateNode ( pred , succ ) and preservesValue = true
507+ succ instanceof ParamNode and summaryPostUpdateNode ( pred , succ ) and preservesValue = true
508+ or
509+ // Similarly we would like to chain together summaries where values get passed
510+ // into callbacks along the way.
511+ pred instanceof ArgNode and summaryPostUpdateNode ( succ , pred ) and preservesValue = true
466512 }
467513
468514 /**
0 commit comments