@@ -353,6 +353,17 @@ private predicate barrierGuardBlocksExpr(
353
353
guard .( AdditionalBarrierGuardCall ) .internalBlocksLabel ( outcome , test , label )
354
354
}
355
355
356
+ /**
357
+ * Holds if `guard` blocks the flow of a value reachable through exploratory flow.
358
+ */
359
+ pragma [ noinline]
360
+ private predicate barrierGuardIsRelevant ( BarrierGuardNode guard ) {
361
+ exists ( Expr e |
362
+ barrierGuardBlocksExpr ( guard , _, e , _) and
363
+ isRelevantForward ( e .flow ( ) , _)
364
+ )
365
+ }
366
+
356
367
/**
357
368
* Holds if data flow node `nd` acts as a barrier for data flow due to aliasing through
358
369
* an access path.
@@ -363,6 +374,7 @@ pragma[noinline]
363
374
private predicate barrierGuardBlocksAccessPath (
364
375
BarrierGuardNode guard , boolean outcome , AccessPath ap , string label
365
376
) {
377
+ barrierGuardIsRelevant ( guard ) and
366
378
barrierGuardBlocksExpr ( guard , outcome , ap .getAnInstance ( ) , label )
367
379
}
368
380
@@ -374,6 +386,7 @@ private predicate barrierGuardBlocksAccessPath(
374
386
private predicate barrierGuardBlocksSsaRefinement (
375
387
BarrierGuardNode guard , boolean outcome , SsaRefinementNode ref , string label
376
388
) {
389
+ barrierGuardIsRelevant ( guard ) and
377
390
guard .getEnclosingExpr ( ) = ref .getGuard ( ) .getTest ( ) and
378
391
forex ( SsaVariable input | input = ref .getAnInput ( ) |
379
392
barrierGuardBlocksExpr ( guard , outcome , input .getAUse ( ) , label )
@@ -395,6 +408,7 @@ private predicate barrierGuardBlocksNode(BarrierGuardNode guard, DataFlow::Node
395
408
)
396
409
or
397
410
// 2) `nd` is an instance of an access path `p`, and dominated by a barrier for `p`
411
+ barrierGuardIsRelevant ( guard ) and
398
412
exists ( AccessPath p , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
399
413
nd = DataFlow:: valueNode ( p .getAnInstanceIn ( bb ) ) and
400
414
guard .getEnclosingExpr ( ) = cond .getTest ( ) and
@@ -412,6 +426,7 @@ private predicate barrierGuardBlocksNode(BarrierGuardNode guard, DataFlow::Node
412
426
private predicate barrierGuardBlocksEdge (
413
427
BarrierGuardNode guard , DataFlow:: Node pred , DataFlow:: Node succ , string label
414
428
) {
429
+ barrierGuardIsRelevant ( guard ) and
415
430
exists (
416
431
SsaVariable input , SsaPhiNode phi , BasicBlock bb , ConditionGuardNode cond , boolean outcome
417
432
|
@@ -573,11 +588,12 @@ private class FlowStepThroughImport extends AdditionalFlowStep, DataFlow::ValueN
573
588
574
589
/**
575
590
* Holds if there is a flow step from `pred` to `succ` described by `summary`
576
- * under configuration `cfg`.
591
+ * under configuration `cfg`, disregarding barriers .
577
592
*
578
593
* Summary steps through function calls are not taken into account.
579
594
*/
580
- private predicate basicFlowStep (
595
+ pragma [ inline]
596
+ private predicate basicFlowStepNoBarrier (
581
597
DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
582
598
) {
583
599
isLive ( ) and
@@ -586,8 +602,7 @@ private predicate basicFlowStep(
586
602
// Local flow
587
603
exists ( FlowLabel predlbl , FlowLabel succlbl |
588
604
localFlowStep ( pred , succ , cfg , predlbl , succlbl ) and
589
- not isLabeledBarrierEdge ( cfg , pred , succ , predlbl ) and
590
- not isBarrierEdge ( cfg , pred , succ ) and
605
+ not cfg .isBarrierEdge ( pred , succ ) and
591
606
summary = MkPathSummary ( false , false , predlbl , succlbl )
592
607
)
593
608
or
@@ -609,6 +624,20 @@ private predicate basicFlowStep(
609
624
)
610
625
}
611
626
627
+ /**
628
+ * Holds if there is a flow step from `pred` to `succ` described by `summary`
629
+ * under configuration `cfg`.
630
+ *
631
+ * Summary steps through function calls are not taken into account.
632
+ */
633
+ private predicate basicFlowStep (
634
+ DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
635
+ ) {
636
+ basicFlowStepNoBarrier ( pred , succ , summary , cfg ) and
637
+ not isLabeledBarrierEdge ( cfg , pred , succ , summary .getStartLabel ( ) ) and
638
+ not isBarrierEdge ( cfg , pred , succ )
639
+ }
640
+
612
641
/**
613
642
* Holds if there is a flow step from `pred` to `succ` under configuration `cfg`,
614
643
* including both basic flow steps and steps into/out of properties.
@@ -619,7 +648,7 @@ private predicate basicFlowStep(
619
648
private predicate exploratoryFlowStep (
620
649
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
621
650
) {
622
- basicFlowStep ( pred , succ , _, cfg ) or
651
+ basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
623
652
basicStoreStep ( pred , succ , _) or
624
653
basicLoadStep ( pred , succ , _) or
625
654
isAdditionalStoreStep ( pred , succ , _, cfg ) or
@@ -1446,6 +1475,7 @@ private class BarrierGuardFunction extends Function {
1446
1475
string label ;
1447
1476
1448
1477
BarrierGuardFunction ( ) {
1478
+ barrierGuardIsRelevant ( guard ) and
1449
1479
exists ( Expr e |
1450
1480
exists ( Expr returnExpr |
1451
1481
returnExpr = guard .asExpr ( )
0 commit comments