@@ -289,6 +289,7 @@ private predicate outBarrier(NodeEx node, Configuration config) {
289
289
)
290
290
}
291
291
292
+ pragma [ nomagic]
292
293
private predicate fullBarrier ( NodeEx node , Configuration config ) {
293
294
exists ( Node n | node .asNode ( ) = n |
294
295
config .isBarrier ( n )
@@ -307,11 +308,23 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
307
308
}
308
309
309
310
pragma [ 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
+ }
311
315
312
316
pragma [ nomagic]
313
317
private predicate sinkNode ( NodeEx node , Configuration config ) { config .isSink ( node .asNode ( ) ) }
314
318
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
+
315
328
/**
316
329
* Holds if data can flow in one local step from `node1` to `node2`.
317
330
*/
@@ -320,16 +333,14 @@ private predicate localFlowStep(NodeEx node1, NodeEx node2, Configuration config
320
333
node1 .asNode ( ) = n1 and
321
334
node2 .asNode ( ) = n2 and
322
335
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 )
327
337
)
328
338
or
329
339
exists ( Node n |
330
340
config .allowImplicitRead ( n , _) and
331
341
node1 .asNode ( ) = n and
332
- node2 .isImplicitReadNode ( n , false )
342
+ node2 .isImplicitReadNode ( n , false ) and
343
+ not fullBarrier ( node1 , config )
333
344
)
334
345
}
335
346
@@ -342,16 +353,14 @@ private predicate additionalLocalFlowStep(NodeEx node1, NodeEx node2, Configurat
342
353
node2 .asNode ( ) = n2 and
343
354
config .isAdditionalFlowStep ( n1 , n2 ) and
344
355
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 )
349
357
)
350
358
or
351
359
exists ( Node n |
352
360
config .allowImplicitRead ( n , _) and
353
361
node1 .isImplicitReadNode ( n , true ) and
354
- node2 .asNode ( ) = n
362
+ node2 .asNode ( ) = n and
363
+ not fullBarrier ( node2 , config )
355
364
)
356
365
}
357
366
@@ -363,10 +372,7 @@ private predicate jumpStep(NodeEx node1, NodeEx node2, Configuration config) {
363
372
node1 .asNode ( ) = n1 and
364
373
node2 .asNode ( ) = n2 and
365
374
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
370
376
not config .getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
371
377
)
372
378
}
@@ -380,16 +386,14 @@ private predicate additionalJumpStep(NodeEx node1, NodeEx node2, Configuration c
380
386
node2 .asNode ( ) = n2 and
381
387
config .isAdditionalFlowStep ( n1 , n2 ) and
382
388
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
387
390
not config .getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
388
391
)
389
392
}
390
393
391
394
private 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 )
393
397
or
394
398
exists ( Node n |
395
399
node2 .isImplicitReadNode ( n , true ) and
@@ -402,7 +406,8 @@ private predicate store(
402
406
NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType , Configuration config
403
407
) {
404
408
store ( node1 .asNode ( ) , tc , node2 .asNode ( ) , contentType ) and
405
- read ( _, tc .getContent ( ) , _, config )
409
+ read ( _, tc .getContent ( ) , _, config ) and
410
+ stepFilter ( node1 , node2 , config )
406
411
}
407
412
408
413
pragma [ nomagic]
@@ -451,63 +456,59 @@ private module Stage1 {
451
456
* argument in a call.
452
457
*/
453
458
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
502
509
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 )
511
512
)
512
513
}
513
514
@@ -547,7 +548,8 @@ private module Stage1 {
547
548
private predicate fwdFlowOut ( DataFlowCall call , NodeEx out , Cc cc , Configuration config ) {
548
549
exists ( ReturnPosition pos |
549
550
fwdFlowReturnPosition ( pos , cc , config ) and
550
- viableReturnPosOutEx ( call , pos , out )
551
+ viableReturnPosOutEx ( call , pos , out ) and
552
+ not fullBarrier ( out , config )
551
553
)
552
554
}
553
555
@@ -773,6 +775,7 @@ private module Stage1 {
773
775
* Holds if flow may enter through `p` and reach a return node making `p` a
774
776
* candidate for the origin of a summary.
775
777
*/
778
+ pragma [ nomagic]
776
779
predicate parameterMayFlowThrough ( ParamNodeEx p , DataFlowCallable c , Ap ap , Configuration config ) {
777
780
exists ( ReturnKindExt kind |
778
781
throughFlowNodeCand ( p , config ) and
0 commit comments