@@ -186,10 +186,15 @@ module Private {
186186 TArgumentSummaryComponent ( int i ) { parameterPosition ( i ) } or
187187 TReturnSummaryComponent ( ReturnKind rk )
188188
189+ private TSummaryComponent thisParam ( ) { result = TParameterSummaryComponent ( instanceParameterPosition ( ) ) }
190+
189191 newtype TSummaryComponentStack =
190192 TSingletonSummaryComponentStack ( SummaryComponent c ) or
191193 TConsSummaryComponentStack ( SummaryComponent head , SummaryComponentStack tail ) {
192194 tail .( RequiredSummaryComponentStack ) .required ( head )
195+ or
196+ tail .( RequiredSummaryComponentStack ) .required ( TParameterSummaryComponent ( _) ) and
197+ head = thisParam ( )
193198 }
194199
195200 pragma [ nomagic]
@@ -198,21 +203,63 @@ module Private {
198203 boolean preservesValue
199204 ) {
200205 c .propagatesFlow ( input , output , preservesValue )
206+ or
207+ // observe side effects of callbacks on input arguments
208+ c .propagatesFlow ( output , input , preservesValue ) and
209+ preservesValue = true and
210+ isCallbackParameter ( input ) and
211+ isContentOfArgument ( output )
212+ or
213+ // flow from the receiver of a callback into the instance-parameter
214+ exists ( SummaryComponentStack s , SummaryComponentStack callbackRef |
215+ c .propagatesFlow ( s , _, _) or c .propagatesFlow ( _, s , _)
216+ |
217+ callbackRef = s .drop ( _) and
218+ ( isCallbackParameter ( callbackRef ) or callbackRef .head ( ) = TReturnSummaryComponent ( _) ) and
219+ input = callbackRef .tail ( ) and
220+ output = TConsSummaryComponentStack ( thisParam ( ) , input ) and
221+ preservesValue = true
222+ )
223+ }
224+
225+ private predicate isCallbackParameter ( SummaryComponentStack s ) {
226+ s .head ( ) = TParameterSummaryComponent ( _) and exists ( s .tail ( ) )
227+ }
228+
229+ private predicate isContentOfArgument ( SummaryComponentStack s ) {
230+ s .head ( ) = TContentSummaryComponent ( _) and isContentOfArgument ( s .tail ( ) )
231+ or
232+ s = TSingletonSummaryComponentStack ( TArgumentSummaryComponent ( _) )
233+ }
234+
235+ private predicate outputState ( SummarizedCallable c , SummaryComponentStack s ) {
236+ summary ( c , _, s , _)
237+ or
238+ exists ( SummaryComponentStack out |
239+ outputState ( c , out ) and
240+ out .head ( ) = TContentSummaryComponent ( _) and
241+ s = out .tail ( )
242+ )
243+ or
244+ // Add the argument node corresponding to the requested post-update node
245+ inputState ( c , s ) and isCallbackParameter ( s )
246+ }
247+
248+ private predicate inputState ( SummarizedCallable c , SummaryComponentStack s ) {
249+ summary ( c , s , _, _)
250+ or
251+ exists ( SummaryComponentStack inp | inputState ( c , inp ) and s = inp .tail ( ) )
252+ or
253+ exists ( SummaryComponentStack out |
254+ outputState ( c , out ) and
255+ out .head ( ) = TParameterSummaryComponent ( _) and
256+ s = out .tail ( )
257+ )
201258 }
202259
203260 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- }
261+ TSummaryNodeInputState ( SummaryComponentStack s ) { inputState ( _, s ) } or
262+ TSummaryNodeOutputState ( SummaryComponentStack s ) { outputState ( _, s ) }
216263
217264 /**
218265 * A state used to break up (complex) flow summaries into atomic flow steps.
@@ -238,20 +285,14 @@ module Private {
238285 pragma [ nomagic]
239286 predicate isInputState ( SummarizedCallable c , SummaryComponentStack s ) {
240287 this = TSummaryNodeInputState ( s ) and
241- exists ( SummaryComponentStack input |
242- summary ( c , input , _, _) and
243- s = input .drop ( _)
244- )
288+ inputState ( c , s )
245289 }
246290
247291 /** Holds if this state is a valid output state for `c`. */
248292 pragma [ nomagic]
249293 predicate isOutputState ( SummarizedCallable c , SummaryComponentStack s ) {
250294 this = TSummaryNodeOutputState ( s ) and
251- exists ( SummaryComponentStack output |
252- summary ( c , _, output , _) and
253- s = output .drop ( _)
254- )
295+ outputState ( c , s )
255296 }
256297
257298 /** Gets a textual representation of this state. */
@@ -331,19 +372,12 @@ module Private {
331372 receiver = summaryNodeInputState ( c , s .drop ( 1 ) )
332373 }
333374
334- private Node pre ( Node post ) {
335- summaryPostUpdateNode ( post , result )
336- or
337- not summaryPostUpdateNode ( post , _) and
338- result = post
339- }
340-
341375 private predicate callbackInput (
342376 SummarizedCallable c , SummaryComponentStack s , Node receiver , int i
343377 ) {
344378 any ( SummaryNodeState state ) .isOutputState ( c , s ) and
345379 s .head ( ) = TParameterSummaryComponent ( i ) and
346- receiver = pre ( summaryNodeOutputState ( c , s .drop ( 1 ) ) )
380+ receiver = summaryNodeInputState ( c , s .drop ( 1 ) )
347381 }
348382
349383 /** Holds if a call targeting `receiver` should be synthesized inside `c`. */
@@ -395,7 +429,7 @@ module Private {
395429 or
396430 exists ( int i | head = TParameterSummaryComponent ( i ) |
397431 result =
398- getCallbackParameterType ( getNodeType ( summaryNodeOutputState ( pragma [ only_bind_out ] ( c ) ,
432+ getCallbackParameterType ( getNodeType ( summaryNodeInputState ( pragma [ only_bind_out ] ( c ) ,
399433 s .drop ( 1 ) ) ) , i )
400434 )
401435 )
@@ -421,10 +455,16 @@ module Private {
421455 }
422456
423457 /** Holds if summary node `post` is a post-update node with pre-update node `pre`. */
424- predicate summaryPostUpdateNode ( Node post , ParamNode pre ) {
458+ predicate summaryPostUpdateNode ( Node post , Node pre ) {
425459 exists ( SummarizedCallable c , int i |
426460 isParameterPostUpdate ( post , c , i ) and
427- pre .isParameterOf ( c , i )
461+ pre .( ParamNode ) .isParameterOf ( c , i )
462+ )
463+ or
464+ exists ( SummarizedCallable callable , SummaryComponentStack s |
465+ callbackInput ( callable , s , _, _) and
466+ pre = summaryNodeOutputState ( callable , s ) and
467+ post = summaryNodeInputState ( callable , s )
428468 )
429469 }
430470
@@ -462,7 +502,11 @@ module Private {
462502 // for `StringBuilder.append(x)` with a specified value flow from qualifier to
463503 // return value and taint flow from argument 0 to the qualifier, then this
464504 // allows us to infer taint flow from argument 0 to the return value.
465- summaryPostUpdateNode ( pred , succ ) and preservesValue = true
505+ succ instanceof ParamNode and summaryPostUpdateNode ( pred , succ ) and preservesValue = true
506+ or
507+ // Similarly we would like to chain together summaries where values get passed
508+ // into callbacks along the way.
509+ pred instanceof ArgNode and summaryPostUpdateNode ( succ , pred ) and preservesValue = true
466510 }
467511
468512 /**
0 commit comments