@@ -363,6 +363,51 @@ private predicate barrierGuardBlocksAccessPath(BarrierGuardNode guard, boolean o
363363 barrierGuardBlocksExpr ( guard , outcome , ap .getAnInstance ( ) , label )
364364}
365365
366+ /**
367+ * Holds if `guard` should block flow along the edge `pred -> succ`.
368+ *
369+ * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
370+ */
371+ private predicate barrierGuardBlocksEdge ( BarrierGuardNode guard , DataFlow:: Node pred , DataFlow:: Node succ , string label ) {
372+ exists ( SsaVariable input , SsaPhiNode phi , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
373+ pred = DataFlow:: ssaDefinitionNode ( input ) and
374+ succ = DataFlow:: ssaDefinitionNode ( phi ) and
375+ input = phi .getInputFromBlock ( bb ) and
376+ guard .getEnclosingExpr ( ) = cond .getTest ( ) and
377+ outcome = cond .getOutcome ( ) and
378+ barrierGuardBlocksExpr ( guard , outcome , input .getAUse ( ) , label ) and
379+ cond .dominates ( bb )
380+ )
381+ }
382+
383+ /**
384+ * Holds if there is a barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
385+ * or one implied by a barrier guard.
386+ *
387+ * Only holds for barriers that should apply to all flow labels.
388+ */
389+ private predicate isBarrierEdge ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ ) {
390+ cfg .isBarrierEdge ( pred , succ )
391+ or
392+ exists ( DataFlow:: BarrierGuardNode guard |
393+ cfg .isBarrierGuard ( guard ) and
394+ barrierGuardBlocksEdge ( guard , pred , succ , "" )
395+ )
396+ }
397+
398+ /**
399+ * Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
400+ * or one implied by a barrier guard.
401+ */
402+ private predicate isLabeledBarrierEdge ( Configuration cfg , DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: FlowLabel label ) {
403+ cfg .isBarrierEdge ( pred , succ , label )
404+ or
405+ exists ( DataFlow:: BarrierGuardNode guard |
406+ cfg .isBarrierGuard ( guard ) and
407+ barrierGuardBlocksEdge ( guard , pred , succ , label )
408+ )
409+ }
410+
366411/**
367412 * A guard node that only blocks specific labels.
368413 */
@@ -470,7 +515,8 @@ private predicate basicFlowStep(
470515 // Local flow
471516 exists ( FlowLabel predlbl , FlowLabel succlbl |
472517 localFlowStep ( pred , succ , cfg , predlbl , succlbl ) and
473- not cfg .isBarrierEdge ( pred , succ , predlbl ) and
518+ not isLabeledBarrierEdge ( cfg , pred , succ , predlbl ) and
519+ not isBarrierEdge ( cfg , pred , succ ) and
474520 summary = MkPathSummary ( false , false , predlbl , succlbl )
475521 )
476522 or
@@ -584,7 +630,7 @@ private predicate callInputStep(
584630 )
585631 ) and
586632 not cfg .isBarrier ( succ ) and
587- not cfg . isBarrierEdge ( pred , succ )
633+ not isBarrierEdge ( cfg , pred , succ )
588634}
589635
590636/**
@@ -638,7 +684,8 @@ private predicate flowThroughCall(
638684 ret .asExpr ( ) = f .getAReturnedExpr ( ) and
639685 calls ( output , f ) and // Do not consider partial calls
640686 reachableFromInput ( f , output , input , ret , cfg , summary ) and
641- not cfg .isBarrierEdge ( ret , output ) and
687+ not isBarrierEdge ( cfg , ret , output ) and
688+ not isLabeledBarrierEdge ( cfg , ret , output , summary .getEndLabel ( ) ) and
642689 not cfg .isLabeledBarrier ( output , summary .getEndLabel ( ) )
643690 )
644691 or
@@ -647,7 +694,8 @@ private predicate flowThroughCall(
647694 DataFlow:: exceptionalInvocationReturnNode ( output , invk .asExpr ( ) ) and
648695 calls ( invk , f ) and
649696 reachableFromInput ( f , invk , input , ret , cfg , summary ) and
650- not cfg .isBarrierEdge ( ret , output ) and
697+ not isBarrierEdge ( cfg , ret , output ) and
698+ not isLabeledBarrierEdge ( cfg , ret , output , summary .getEndLabel ( ) ) and
651699 not cfg .isLabeledBarrier ( output , summary .getEndLabel ( ) )
652700 )
653701}
@@ -886,7 +934,8 @@ private predicate flowStep(
886934 flowIntoHigherOrderCall ( pred , succ , cfg , summary )
887935 ) and
888936 not cfg .isBarrier ( succ ) and
889- not cfg .isBarrierEdge ( pred , succ ) and
937+ not isBarrierEdge ( cfg , pred , succ ) and
938+ not isLabeledBarrierEdge ( cfg , pred , succ , summary .getEndLabel ( ) ) and
890939 not cfg .isLabeledBarrier ( succ , summary .getEndLabel ( ) )
891940}
892941
0 commit comments