@@ -514,7 +514,7 @@ private BasicBlock getADominatedBasicBlock(BarrierGuardNode guard, ConditionGuar
514
514
*
515
515
* Only holds for barriers that should apply to all flow labels.
516
516
*/
517
- private predicate isBarrierEdge ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ ) {
517
+ private predicate isBarrierEdgeRaw ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ ) {
518
518
cfg .isBarrierEdge ( pred , succ )
519
519
or
520
520
exists ( DataFlow:: BarrierGuardNode guard |
@@ -523,11 +523,26 @@ private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow
523
523
)
524
524
}
525
525
526
+ /**
527
+ * Holds if there is a barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
528
+ * or one implied by a barrier guard, or by an out/in barrier for `pred` or `succ`, respectively.
529
+ *
530
+ * Only holds for barriers that should apply to all flow labels.
531
+ */
532
+ pragma [ inline]
533
+ private predicate isBarrierEdge ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ ) {
534
+ isBarrierEdgeRaw ( cfg , pred , succ )
535
+ or
536
+ cfg .isBarrierOut ( pred )
537
+ or
538
+ cfg .isBarrierIn ( succ )
539
+ }
540
+
526
541
/**
527
542
* Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
528
543
* or one implied by a barrier guard.
529
544
*/
530
- private predicate isLabeledBarrierEdge (
545
+ private predicate isLabeledBarrierEdgeRaw (
531
546
Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: FlowLabel label
532
547
) {
533
548
cfg .isBarrierEdge ( pred , succ , label )
@@ -538,6 +553,21 @@ private predicate isLabeledBarrierEdge(
538
553
)
539
554
}
540
555
556
+ /**
557
+ * Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
558
+ * or one implied by a barrier guard, or by an out/in barrier for `pred` or `succ`, respectively.
559
+ */
560
+ pragma [ inline]
561
+ private predicate isLabeledBarrierEdge (
562
+ Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: FlowLabel label
563
+ ) {
564
+ isLabeledBarrierEdgeRaw ( cfg , pred , succ , label )
565
+ or
566
+ cfg .isBarrierOut ( pred , label )
567
+ or
568
+ cfg .isBarrierIn ( succ , label )
569
+ }
570
+
541
571
/**
542
572
* A guard node that only blocks specific labels.
543
573
*/
0 commit comments