@@ -353,6 +353,17 @@ private predicate barrierGuardBlocksExpr(
353353 guard .( AdditionalBarrierGuardCall ) .internalBlocksLabel ( outcome , test , label )
354354}
355355
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+
356367/**
357368 * Holds if data flow node `nd` acts as a barrier for data flow due to aliasing through
358369 * an access path.
@@ -363,6 +374,7 @@ pragma[noinline]
363374private predicate barrierGuardBlocksAccessPath (
364375 BarrierGuardNode guard , boolean outcome , AccessPath ap , string label
365376) {
377+ barrierGuardIsRelevant ( guard ) and
366378 barrierGuardBlocksExpr ( guard , outcome , ap .getAnInstance ( ) , label )
367379}
368380
@@ -374,6 +386,7 @@ private predicate barrierGuardBlocksAccessPath(
374386private predicate barrierGuardBlocksSsaRefinement (
375387 BarrierGuardNode guard , boolean outcome , SsaRefinementNode ref , string label
376388) {
389+ barrierGuardIsRelevant ( guard ) and
377390 guard .getEnclosingExpr ( ) = ref .getGuard ( ) .getTest ( ) and
378391 forex ( SsaVariable input | input = ref .getAnInput ( ) |
379392 barrierGuardBlocksExpr ( guard , outcome , input .getAUse ( ) , label )
@@ -395,6 +408,7 @@ private predicate barrierGuardBlocksNode(BarrierGuardNode guard, DataFlow::Node
395408 )
396409 or
397410 // 2) `nd` is an instance of an access path `p`, and dominated by a barrier for `p`
411+ barrierGuardIsRelevant ( guard ) and
398412 exists ( AccessPath p , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
399413 nd = DataFlow:: valueNode ( p .getAnInstanceIn ( bb ) ) and
400414 guard .getEnclosingExpr ( ) = cond .getTest ( ) and
@@ -412,6 +426,7 @@ private predicate barrierGuardBlocksNode(BarrierGuardNode guard, DataFlow::Node
412426private predicate barrierGuardBlocksEdge (
413427 BarrierGuardNode guard , DataFlow:: Node pred , DataFlow:: Node succ , string label
414428) {
429+ barrierGuardIsRelevant ( guard ) and
415430 exists (
416431 SsaVariable input , SsaPhiNode phi , BasicBlock bb , ConditionGuardNode cond , boolean outcome
417432 |
@@ -573,11 +588,12 @@ private class FlowStepThroughImport extends AdditionalFlowStep, DataFlow::ValueN
573588
574589/**
575590 * Holds if there is a flow step from `pred` to `succ` described by `summary`
576- * under configuration `cfg`.
591+ * under configuration `cfg`, disregarding barriers .
577592 *
578593 * Summary steps through function calls are not taken into account.
579594 */
580- private predicate basicFlowStep (
595+ pragma [ inline]
596+ private predicate basicFlowStepNoBarrier (
581597 DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
582598) {
583599 isLive ( ) and
@@ -586,8 +602,7 @@ private predicate basicFlowStep(
586602 // Local flow
587603 exists ( FlowLabel predlbl , FlowLabel succlbl |
588604 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
591606 summary = MkPathSummary ( false , false , predlbl , succlbl )
592607 )
593608 or
@@ -609,6 +624,20 @@ private predicate basicFlowStep(
609624 )
610625}
611626
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+
612641/**
613642 * Holds if there is a flow step from `pred` to `succ` under configuration `cfg`,
614643 * including both basic flow steps and steps into/out of properties.
@@ -619,7 +648,7 @@ private predicate basicFlowStep(
619648private predicate exploratoryFlowStep (
620649 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
621650) {
622- basicFlowStep ( pred , succ , _, cfg ) or
651+ basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
623652 basicStoreStep ( pred , succ , _) or
624653 basicLoadStep ( pred , succ , _) or
625654 isAdditionalStoreStep ( pred , succ , _, cfg ) or
@@ -1446,6 +1475,7 @@ private class BarrierGuardFunction extends Function {
14461475 string label ;
14471476
14481477 BarrierGuardFunction ( ) {
1478+ barrierGuardIsRelevant ( guard ) and
14491479 exists ( Expr e |
14501480 exists ( Expr returnExpr |
14511481 returnExpr = guard .asExpr ( )
0 commit comments