@@ -166,6 +166,26 @@ abstract class Configuration extends string {
166166 )
167167 }
168168
169+ /**
170+ * Holds if flow into `node` is prohibited.
171+ */
172+ predicate isBarrierIn ( DataFlow:: Node node ) { none ( ) }
173+
174+ /**
175+ * Holds if flow out `node` is prohibited.
176+ */
177+ predicate isBarrierOut ( DataFlow:: Node node ) { none ( ) }
178+
179+ /**
180+ * Holds if flow into `node` is prohibited for the flow label `lbl`.
181+ */
182+ predicate isBarrierIn ( DataFlow:: Node node , FlowLabel lbl ) { none ( ) }
183+
184+ /**
185+ * Holds if flow out `node` is prohibited for the flow label `lbl`.
186+ */
187+ predicate isBarrierOut ( DataFlow:: Node node , FlowLabel lbl ) { none ( ) }
188+
169189 /**
170190 * Holds if flow from `pred` to `succ` is prohibited.
171191 */
@@ -494,7 +514,7 @@ private BasicBlock getADominatedBasicBlock(BarrierGuardNode guard, ConditionGuar
494514 *
495515 * Only holds for barriers that should apply to all flow labels.
496516 */
497- private predicate isBarrierEdge ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ ) {
517+ private predicate isBarrierEdgeRaw ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ ) {
498518 cfg .isBarrierEdge ( pred , succ )
499519 or
500520 exists ( DataFlow:: BarrierGuardNode guard |
@@ -503,11 +523,26 @@ private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow
503523 )
504524}
505525
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+
506541/**
507542 * Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
508543 * or one implied by a barrier guard.
509544 */
510- private predicate isLabeledBarrierEdge (
545+ private predicate isLabeledBarrierEdgeRaw (
511546 Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: FlowLabel label
512547) {
513548 cfg .isBarrierEdge ( pred , succ , label )
@@ -518,6 +553,21 @@ private predicate isLabeledBarrierEdge(
518553 )
519554}
520555
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+
521571/**
522572 * A guard node that only blocks specific labels.
523573 */
0 commit comments