@@ -1502,6 +1502,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15021502 * definition.
15031503 */
15041504 default predicate includeWriteDefsInFlowStep ( ) { any ( ) }
1505+
1506+ /**
1507+ * Holds if barrier guards should be supported on input edges to phi
1508+ * nodes. Disable this only if barrier guards are not going to be used.
1509+ */
1510+ default predicate supportBarrierGuardsOnPhiEdges ( ) { any ( ) }
15051511 }
15061512
15071513 /**
@@ -1533,6 +1539,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15331539 )
15341540 }
15351541
1542+ /**
1543+ * Holds if the input to `phi` from the block `input` might be relevant for
1544+ * barrier guards as a separately synthesized `TSsaInputNode`.
1545+ */
1546+ private predicate relevantPhiInputNode ( SsaPhiExt phi , BasicBlock input ) {
1547+ DfInput:: supportBarrierGuardsOnPhiEdges ( ) and
1548+ // If the input isn't explicitly read then a guard cannot check it.
1549+ exists ( DfInput:: getARead ( getAPhiInputDef ( phi , input ) ) ) and
1550+ (
1551+ exists ( DfInput:: Guard g | g .controlsBranchEdge ( input , phi .getBasicBlock ( ) , _) )
1552+ or
1553+ exists ( BasicBlock prev |
1554+ AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) ,
1555+ phi .getSourceVariable ( ) ) and
1556+ prev != input and
1557+ exists ( DfInput:: Guard g , boolean branch |
1558+ DfInput:: guardControlsBlock ( g , input , branch ) and
1559+ not DfInput:: guardControlsBlock ( g , prev , branch )
1560+ )
1561+ )
1562+ )
1563+ }
1564+
15361565 private newtype TNode =
15371566 TParamNode ( DfInput:: Parameter p ) {
15381567 exists ( WriteDefinition def | DfInput:: ssaDefInitializesParam ( def , p ) )
@@ -1546,7 +1575,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15461575 )
15471576 } or
15481577 TSsaDefinitionNode ( DefinitionExt def ) or
1549- TSsaInputNode ( SsaPhiExt phi , BasicBlock input ) { exists ( getAPhiInputDef ( phi , input ) ) }
1578+ TSsaInputNode ( SsaPhiExt phi , BasicBlock input ) { relevantPhiInputNode ( phi , input ) }
15501579
15511580 /**
15521581 * A data flow node that we need to reference in the value step relation.
@@ -1822,8 +1851,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18221851 // Flow from definition/read to phi input
18231852 exists ( BasicBlock input , BasicBlock bbPhi , DefinitionExt phi |
18241853 AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i1 , input , bbPhi , v ) and
1825- nodeTo = TSsaInputNode ( phi , input ) and
18261854 phi .definesAt ( v , bbPhi , - 1 , _)
1855+ |
1856+ nodeTo = TSsaInputNode ( phi , input )
1857+ or
1858+ not relevantPhiInputNode ( phi , input ) and
1859+ nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
18271860 )
18281861 }
18291862
0 commit comments