@@ -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
@@ -319,43 +319,6 @@ module FlowLabel {
319319 * implementations of `blocks` will _both_ apply to any configuration that includes either of them.
320320 */
321321abstract 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- }
359322
360323 /**
361324 * Holds if this node blocks expression `e` provided it evaluates to `outcome`.
@@ -400,6 +363,42 @@ private predicate barrierGuardBlocksAccessPath(
400363 barrierGuardBlocksExpr ( guard , outcome , ap .getAnInstance ( ) , label )
401364}
402365
366+ /**
367+ * Holds if there exists an input variable of `ref` that blocks the label `label`.
368+ *
369+ * This predicate is outlined to give the optimizer a hint about the join ordering.
370+ */
371+ private predicate barrierGuardBlocksSsaRefinement ( BarrierGuardNode guard , boolean outcome , SsaRefinementNode ref , string label ) {
372+ guard .getEnclosingExpr ( ) = ref .getGuard ( ) .getTest ( ) and
373+ forex ( SsaVariable input | input = ref .getAnInput ( ) |
374+ barrierGuardBlocksExpr ( guard , outcome , input .getAUse ( ) , label )
375+ )
376+ }
377+
378+ /**
379+ * Holds if data flow node `nd` acts as a barrier for data flow, possibly due to aliasing
380+ * through an access path.
381+ *
382+ * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
383+ */
384+ private predicate barrierGuardBlocksNode ( BarrierGuardNode guard , DataFlow:: Node nd , string label ) {
385+ // 1) `nd` is a use of a refinement node that blocks its input variable
386+ exists ( SsaRefinementNode ref , boolean outcome |
387+ nd = DataFlow:: ssaDefinitionNode ( ref ) and
388+ outcome = ref .getGuard ( ) .( ConditionGuardNode ) .getOutcome ( ) and
389+ barrierGuardBlocksSsaRefinement ( guard , outcome , ref , label )
390+ )
391+ or
392+ // 2) `nd` is an instance of an access path `p`, and dominated by a barrier for `p`
393+ exists ( AccessPath p , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
394+ nd = DataFlow:: valueNode ( p .getAnInstanceIn ( bb ) ) and
395+ guard .getEnclosingExpr ( ) = cond .getTest ( ) and
396+ outcome = cond .getOutcome ( ) and
397+ barrierGuardBlocksAccessPath ( guard , outcome , p , label ) and
398+ cond .dominates ( bb )
399+ )
400+ }
401+
403402/**
404403 * Holds if `guard` should block flow along the edge `pred -> succ`.
405404 *
0 commit comments