@@ -1502,6 +1502,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1502
1502
* definition.
1503
1503
*/
1504
1504
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 ( ) }
1505
1511
}
1506
1512
1507
1513
/**
@@ -1533,6 +1539,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1533
1539
)
1534
1540
}
1535
1541
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
+
1536
1565
private newtype TNode =
1537
1566
TParamNode ( DfInput:: Parameter p ) {
1538
1567
exists ( WriteDefinition def | DfInput:: ssaDefInitializesParam ( def , p ) )
@@ -1546,7 +1575,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1546
1575
)
1547
1576
} or
1548
1577
TSsaDefinitionNode ( DefinitionExt def ) or
1549
- TSsaInputNode ( SsaPhiExt phi , BasicBlock input ) { exists ( getAPhiInputDef ( phi , input ) ) }
1578
+ TSsaInputNode ( SsaPhiExt phi , BasicBlock input ) { relevantPhiInputNode ( phi , input ) }
1550
1579
1551
1580
/**
1552
1581
* 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> {
1822
1851
// Flow from definition/read to phi input
1823
1852
exists ( BasicBlock input , BasicBlock bbPhi , DefinitionExt phi |
1824
1853
AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i1 , input , bbPhi , v ) and
1825
- nodeTo = TSsaInputNode ( phi , input ) and
1826
1854
phi .definesAt ( v , bbPhi , - 1 , _)
1855
+ |
1856
+ nodeTo = TSsaInputNode ( phi , input )
1857
+ or
1858
+ not relevantPhiInputNode ( phi , input ) and
1859
+ nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
1827
1860
)
1828
1861
}
1829
1862
0 commit comments