@@ -289,6 +289,7 @@ private predicate outBarrier(NodeEx node, Configuration config) {
289289 )
290290}
291291
292+ pragma [ nomagic]
292293private predicate fullBarrier ( NodeEx node , Configuration config ) {
293294 exists ( Node n | node .asNode ( ) = n |
294295 config .isBarrier ( n )
@@ -307,11 +308,23 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
307308}
308309
309310pragma [ nomagic]
310- private predicate sourceNode ( NodeEx node , Configuration config ) { config .isSource ( node .asNode ( ) ) }
311+ private predicate sourceNode ( NodeEx node , Configuration config ) {
312+ config .isSource ( node .asNode ( ) ) and
313+ not fullBarrier ( node , config )
314+ }
311315
312316pragma [ nomagic]
313317private predicate sinkNode ( NodeEx node , Configuration config ) { config .isSink ( node .asNode ( ) ) }
314318
319+ /** Provides the relevant barriers for a step from `node1` to `node2`. */
320+ pragma [ inline]
321+ private predicate stepFilter ( NodeEx node1 , NodeEx node2 , Configuration config ) {
322+ not outBarrier ( node1 , config ) and
323+ not inBarrier ( node2 , config ) and
324+ not fullBarrier ( node1 , config ) and
325+ not fullBarrier ( node2 , config )
326+ }
327+
315328/**
316329 * Holds if data can flow in one local step from `node1` to `node2`.
317330 */
@@ -320,16 +333,14 @@ private predicate localFlowStep(NodeEx node1, NodeEx node2, Configuration config
320333 node1 .asNode ( ) = n1 and
321334 node2 .asNode ( ) = n2 and
322335 simpleLocalFlowStepExt ( n1 , n2 ) and
323- not outBarrier ( node1 , config ) and
324- not inBarrier ( node2 , config ) and
325- not fullBarrier ( node1 , config ) and
326- not fullBarrier ( node2 , config )
336+ stepFilter ( node1 , node2 , config )
327337 )
328338 or
329339 exists ( Node n |
330340 config .allowImplicitRead ( n , _) and
331341 node1 .asNode ( ) = n and
332- node2 .isImplicitReadNode ( n , false )
342+ node2 .isImplicitReadNode ( n , false ) and
343+ not fullBarrier ( node1 , config )
333344 )
334345}
335346
@@ -342,16 +353,14 @@ private predicate additionalLocalFlowStep(NodeEx node1, NodeEx node2, Configurat
342353 node2 .asNode ( ) = n2 and
343354 config .isAdditionalFlowStep ( n1 , n2 ) and
344355 getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
345- not outBarrier ( node1 , config ) and
346- not inBarrier ( node2 , config ) and
347- not fullBarrier ( node1 , config ) and
348- not fullBarrier ( node2 , config )
356+ stepFilter ( node1 , node2 , config )
349357 )
350358 or
351359 exists ( Node n |
352360 config .allowImplicitRead ( n , _) and
353361 node1 .isImplicitReadNode ( n , true ) and
354- node2 .asNode ( ) = n
362+ node2 .asNode ( ) = n and
363+ not fullBarrier ( node2 , config )
355364 )
356365}
357366
@@ -363,10 +372,7 @@ private predicate jumpStep(NodeEx node1, NodeEx node2, Configuration config) {
363372 node1 .asNode ( ) = n1 and
364373 node2 .asNode ( ) = n2 and
365374 jumpStepCached ( n1 , n2 ) and
366- not outBarrier ( node1 , config ) and
367- not inBarrier ( node2 , config ) and
368- not fullBarrier ( node1 , config ) and
369- not fullBarrier ( node2 , config ) and
375+ stepFilter ( node1 , node2 , config ) and
370376 not config .getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
371377 )
372378}
@@ -380,16 +386,14 @@ private predicate additionalJumpStep(NodeEx node1, NodeEx node2, Configuration c
380386 node2 .asNode ( ) = n2 and
381387 config .isAdditionalFlowStep ( n1 , n2 ) and
382388 getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
383- not outBarrier ( node1 , config ) and
384- not inBarrier ( node2 , config ) and
385- not fullBarrier ( node1 , config ) and
386- not fullBarrier ( node2 , config ) and
389+ stepFilter ( node1 , node2 , config ) and
387390 not config .getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
388391 )
389392}
390393
391394private predicate read ( NodeEx node1 , Content c , NodeEx node2 , Configuration config ) {
392- read ( node1 .asNode ( ) , c , node2 .asNode ( ) )
395+ read ( node1 .asNode ( ) , c , node2 .asNode ( ) ) and
396+ stepFilter ( node1 , node2 , config )
393397 or
394398 exists ( Node n |
395399 node2 .isImplicitReadNode ( n , true ) and
@@ -402,7 +406,8 @@ private predicate store(
402406 NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType , Configuration config
403407) {
404408 store ( node1 .asNode ( ) , tc , node2 .asNode ( ) , contentType ) and
405- read ( _, tc .getContent ( ) , _, config )
409+ read ( _, tc .getContent ( ) , _, config ) and
410+ stepFilter ( node1 , node2 , config )
406411}
407412
408413pragma [ nomagic]
@@ -451,63 +456,59 @@ private module Stage1 {
451456 * argument in a call.
452457 */
453458 predicate fwdFlow ( NodeEx node , Cc cc , Configuration config ) {
454- not fullBarrier ( node , config ) and
455- (
456- sourceNode ( node , config ) and
457- if hasSourceCallCtx ( config ) then cc = true else cc = false
458- or
459- exists ( NodeEx mid |
460- fwdFlow ( mid , cc , config ) and
461- localFlowStep ( mid , node , config )
462- )
463- or
464- exists ( NodeEx mid |
465- fwdFlow ( mid , cc , config ) and
466- additionalLocalFlowStep ( mid , node , config )
467- )
468- or
469- exists ( NodeEx mid |
470- fwdFlow ( mid , _, config ) and
471- jumpStep ( mid , node , config ) and
472- cc = false
473- )
474- or
475- exists ( NodeEx mid |
476- fwdFlow ( mid , _, config ) and
477- additionalJumpStep ( mid , node , config ) and
478- cc = false
479- )
480- or
481- // store
482- exists ( NodeEx mid |
483- useFieldFlow ( config ) and
484- fwdFlow ( mid , cc , config ) and
485- store ( mid , _, node , _, config ) and
486- not outBarrier ( mid , config )
487- )
488- or
489- // read
490- exists ( Content c |
491- fwdFlowRead ( c , node , cc , config ) and
492- fwdFlowConsCand ( c , config ) and
493- not inBarrier ( node , config )
494- )
495- or
496- // flow into a callable
497- exists ( NodeEx arg |
498- fwdFlow ( arg , _, config ) and
499- viableParamArgEx ( _, node , arg ) and
500- cc = true
501- )
459+ sourceNode ( node , config ) and
460+ if hasSourceCallCtx ( config ) then cc = true else cc = false
461+ or
462+ exists ( NodeEx mid |
463+ fwdFlow ( mid , cc , config ) and
464+ localFlowStep ( mid , node , config )
465+ )
466+ or
467+ exists ( NodeEx mid |
468+ fwdFlow ( mid , cc , config ) and
469+ additionalLocalFlowStep ( mid , node , config )
470+ )
471+ or
472+ exists ( NodeEx mid |
473+ fwdFlow ( mid , _, config ) and
474+ jumpStep ( mid , node , config ) and
475+ cc = false
476+ )
477+ or
478+ exists ( NodeEx mid |
479+ fwdFlow ( mid , _, config ) and
480+ additionalJumpStep ( mid , node , config ) and
481+ cc = false
482+ )
483+ or
484+ // store
485+ exists ( NodeEx mid |
486+ useFieldFlow ( config ) and
487+ fwdFlow ( mid , cc , config ) and
488+ store ( mid , _, node , _, config )
489+ )
490+ or
491+ // read
492+ exists ( Content c |
493+ fwdFlowRead ( c , node , cc , config ) and
494+ fwdFlowConsCand ( c , config )
495+ )
496+ or
497+ // flow into a callable
498+ exists ( NodeEx arg |
499+ fwdFlow ( arg , _, config ) and
500+ viableParamArgEx ( _, node , arg ) and
501+ cc = true and
502+ not fullBarrier ( node , config )
503+ )
504+ or
505+ // flow out of a callable
506+ exists ( DataFlowCall call |
507+ fwdFlowOut ( call , node , false , config ) and
508+ cc = false
502509 or
503- // flow out of a callable
504- exists ( DataFlowCall call |
505- fwdFlowOut ( call , node , false , config ) and
506- cc = false
507- or
508- fwdFlowOutFromArg ( call , node , config ) and
509- fwdFlowIsEntered ( call , cc , config )
510- )
510+ fwdFlowOutFromArg ( call , node , config ) and
511+ fwdFlowIsEntered ( call , cc , config )
511512 )
512513 }
513514
@@ -547,7 +548,8 @@ private module Stage1 {
547548 private predicate fwdFlowOut ( DataFlowCall call , NodeEx out , Cc cc , Configuration config ) {
548549 exists ( ReturnPosition pos |
549550 fwdFlowReturnPosition ( pos , cc , config ) and
550- viableReturnPosOutEx ( call , pos , out )
551+ viableReturnPosOutEx ( call , pos , out ) and
552+ not fullBarrier ( out , config )
551553 )
552554 }
553555
@@ -773,6 +775,7 @@ private module Stage1 {
773775 * Holds if flow may enter through `p` and reach a return node making `p` a
774776 * candidate for the origin of a summary.
775777 */
778+ pragma [ nomagic]
776779 predicate parameterMayFlowThrough ( ParamNodeEx p , DataFlowCallable c , Ap ap , Configuration config ) {
777780 exists ( ReturnKindExt kind |
778781 throughFlowNodeCand ( p , config ) and
0 commit comments