@@ -149,7 +149,7 @@ abstract class Configuration extends string {
149149 predicate isBarrier ( DataFlow:: Node node ) {
150150 exists ( BarrierGuardNode guard |
151151 isBarrierGuardInternal ( guard ) and
152- guard . internalBlocks ( node , "" )
152+ barrierGuardBlocksNode ( guard , node , "" )
153153 )
154154 }
155155
@@ -183,7 +183,7 @@ abstract class Configuration extends string {
183183 predicate isLabeledBarrier ( DataFlow:: Node node , FlowLabel lbl ) {
184184 exists ( BarrierGuardNode guard |
185185 isBarrierGuardInternal ( guard ) and
186- guard . internalBlocks ( node , lbl )
186+ barrierGuardBlocksNode ( guard , node , lbl )
187187 )
188188 or
189189 none ( ) // relax type inference to account for overriding
@@ -199,6 +199,10 @@ abstract class Configuration extends string {
199199 */
200200 predicate isBarrierGuard ( BarrierGuardNode guard ) { none ( ) }
201201
202+ /**
203+ * Holds if `guard` is a barrier guard for this configuration, added through
204+ * `isBarrierGuard` or `AdditionalBarrierGuardNode`.
205+ */
202206 private predicate isBarrierGuardInternal ( BarrierGuardNode guard ) {
203207 isBarrierGuard ( guard )
204208 or
@@ -319,44 +323,6 @@ module FlowLabel {
319323 * implementations of `blocks` will _both_ apply to any configuration that includes either of them.
320324 */
321325abstract class BarrierGuardNode extends DataFlow:: Node {
322- /**
323- * Holds if data flow node `nd` acts as a barrier for data flow, possibly due to aliasing
324- * through an access path.
325- *
326- * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
327- *
328- * INTERNAL: this predicate should only be used from within `blocks(boolean, Expr)`.
329- */
330- predicate internalBlocks ( DataFlow:: Node nd , string label ) {
331- // 1) `nd` is a use of a refinement node that blocks its input variable
332- exists ( SsaRefinementNode ref , boolean outcome |
333- nd = DataFlow:: ssaDefinitionNode ( ref ) and
334- outcome = ref .getGuard ( ) .( ConditionGuardNode ) .getOutcome ( ) and
335- ssaRefinementBlocks ( outcome , ref , label )
336- )
337- or
338- // 2) `nd` is an instance of an access path `p`, and dominated by a barrier for `p`
339- exists ( AccessPath p , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
340- nd = DataFlow:: valueNode ( p .getAnInstanceIn ( bb ) ) and
341- getEnclosingExpr ( ) = cond .getTest ( ) and
342- outcome = cond .getOutcome ( ) and
343- barrierGuardBlocksAccessPath ( this , outcome , p , label ) and
344- cond .dominates ( bb )
345- )
346- }
347-
348- /**
349- * Holds if there exists an input variable of `ref` that blocks the label `label`.
350- *
351- * This predicate is outlined to give the optimizer a hint about the join ordering.
352- */
353- private predicate ssaRefinementBlocks ( boolean outcome , SsaRefinementNode ref , string label ) {
354- getEnclosingExpr ( ) = ref .getGuard ( ) .getTest ( ) and
355- forex ( SsaVariable input | input = ref .getAnInput ( ) |
356- barrierGuardBlocksExpr ( this , outcome , input .getAUse ( ) , label )
357- )
358- }
359-
360326 /**
361327 * Holds if this node blocks expression `e` provided it evaluates to `outcome`.
362328 *
@@ -387,6 +353,17 @@ private predicate barrierGuardBlocksExpr(
387353 guard .( AdditionalBarrierGuardCall ) .internalBlocksLabel ( outcome , test , label )
388354}
389355
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+
390367/**
391368 * Holds if data flow node `nd` acts as a barrier for data flow due to aliasing through
392369 * an access path.
@@ -397,9 +374,50 @@ pragma[noinline]
397374private predicate barrierGuardBlocksAccessPath (
398375 BarrierGuardNode guard , boolean outcome , AccessPath ap , string label
399376) {
377+ barrierGuardIsRelevant ( guard ) and
400378 barrierGuardBlocksExpr ( guard , outcome , ap .getAnInstance ( ) , label )
401379}
402380
381+ /**
382+ * Holds if there exists an input variable of `ref` that blocks the label `label`.
383+ *
384+ * This predicate is outlined to give the optimizer a hint about the join ordering.
385+ */
386+ private predicate barrierGuardBlocksSsaRefinement (
387+ BarrierGuardNode guard , boolean outcome , SsaRefinementNode ref , string label
388+ ) {
389+ barrierGuardIsRelevant ( guard ) and
390+ guard .getEnclosingExpr ( ) = ref .getGuard ( ) .getTest ( ) and
391+ forex ( SsaVariable input | input = ref .getAnInput ( ) |
392+ barrierGuardBlocksExpr ( guard , outcome , input .getAUse ( ) , label )
393+ )
394+ }
395+
396+ /**
397+ * Holds if data flow node `nd` acts as a barrier for data flow, possibly due to aliasing
398+ * through an access path.
399+ *
400+ * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
401+ */
402+ private predicate barrierGuardBlocksNode ( BarrierGuardNode guard , DataFlow:: Node nd , string label ) {
403+ // 1) `nd` is a use of a refinement node that blocks its input variable
404+ exists ( SsaRefinementNode ref , boolean outcome |
405+ nd = DataFlow:: ssaDefinitionNode ( ref ) and
406+ outcome = ref .getGuard ( ) .( ConditionGuardNode ) .getOutcome ( ) and
407+ barrierGuardBlocksSsaRefinement ( guard , outcome , ref , label )
408+ )
409+ or
410+ // 2) `nd` is an instance of an access path `p`, and dominated by a barrier for `p`
411+ barrierGuardIsRelevant ( guard ) and
412+ exists ( AccessPath p , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
413+ nd = DataFlow:: valueNode ( p .getAnInstanceIn ( bb ) ) and
414+ guard .getEnclosingExpr ( ) = cond .getTest ( ) and
415+ outcome = cond .getOutcome ( ) and
416+ barrierGuardBlocksAccessPath ( guard , outcome , p , label ) and
417+ cond .dominates ( bb )
418+ )
419+ }
420+
403421/**
404422 * Holds if `guard` should block flow along the edge `pred -> succ`.
405423 *
@@ -408,6 +426,7 @@ private predicate barrierGuardBlocksAccessPath(
408426private predicate barrierGuardBlocksEdge (
409427 BarrierGuardNode guard , DataFlow:: Node pred , DataFlow:: Node succ , string label
410428) {
429+ barrierGuardIsRelevant ( guard ) and
411430 exists (
412431 SsaVariable input , SsaPhiNode phi , BasicBlock bb , ConditionGuardNode cond , boolean outcome
413432 |
@@ -569,11 +588,12 @@ private class FlowStepThroughImport extends AdditionalFlowStep, DataFlow::ValueN
569588
570589/**
571590 * Holds if there is a flow step from `pred` to `succ` described by `summary`
572- * under configuration `cfg`.
591+ * under configuration `cfg`, disregarding barriers .
573592 *
574593 * Summary steps through function calls are not taken into account.
575594 */
576- private predicate basicFlowStep (
595+ pragma [ inline]
596+ private predicate basicFlowStepNoBarrier (
577597 DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
578598) {
579599 isLive ( ) and
@@ -582,8 +602,7 @@ private predicate basicFlowStep(
582602 // Local flow
583603 exists ( FlowLabel predlbl , FlowLabel succlbl |
584604 localFlowStep ( pred , succ , cfg , predlbl , succlbl ) and
585- not isLabeledBarrierEdge ( cfg , pred , succ , predlbl ) and
586- not isBarrierEdge ( cfg , pred , succ ) and
605+ not cfg .isBarrierEdge ( pred , succ ) and
587606 summary = MkPathSummary ( false , false , predlbl , succlbl )
588607 )
589608 or
@@ -605,6 +624,20 @@ private predicate basicFlowStep(
605624 )
606625}
607626
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+
608641/**
609642 * Holds if there is a flow step from `pred` to `succ` under configuration `cfg`,
610643 * including both basic flow steps and steps into/out of properties.
@@ -615,7 +648,7 @@ private predicate basicFlowStep(
615648private predicate exploratoryFlowStep (
616649 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
617650) {
618- basicFlowStep ( pred , succ , _, cfg ) or
651+ basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
619652 basicStoreStep ( pred , succ , _) or
620653 basicLoadStep ( pred , succ , _) or
621654 isAdditionalStoreStep ( pred , succ , _, cfg ) or
@@ -1442,6 +1475,7 @@ private class BarrierGuardFunction extends Function {
14421475 string label ;
14431476
14441477 BarrierGuardFunction ( ) {
1478+ barrierGuardIsRelevant ( guard ) and
14451479 exists ( Expr e |
14461480 exists ( Expr returnExpr |
14471481 returnExpr = guard .asExpr ( )
0 commit comments