@@ -1508,6 +1508,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15081508 * nodes. Disable this only if barrier guards are not going to be used.
15091509 */
15101510 default predicate supportBarrierGuardsOnPhiEdges ( ) { any ( ) }
1511+
1512+ /**
1513+ * Holds if all phi input back edges should be kept in the data flow graph.
1514+ *
1515+ * This is ordinarily not necessary and causes the retention of superfluous
1516+ * nodes.
1517+ */
1518+ default predicate keepAllPhiInputBackEdges ( ) { none ( ) }
15111519 }
15121520
15131521 /**
@@ -1539,11 +1547,26 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15391547 )
15401548 }
15411549
1550+ /**
1551+ * Holds if the phi input edge from `input` to `phi` is a back edge and
1552+ * must be kept.
1553+ */
1554+ private predicate relevantBackEdge ( SsaPhiExt phi , BasicBlock input ) {
1555+ exists ( BasicBlock bbPhi |
1556+ DfInput:: keepAllPhiInputBackEdges ( ) and
1557+ exists ( getAPhiInputDef ( phi , input ) ) and
1558+ phi .getBasicBlock ( ) = bbPhi and
1559+ getImmediateBasicBlockDominator + ( input ) = bbPhi
1560+ )
1561+ }
1562+
15421563 /**
15431564 * Holds if the input to `phi` from the block `input` might be relevant for
15441565 * barrier guards as a separately synthesized `TSsaInputNode`.
15451566 */
15461567 private predicate relevantPhiInputNode ( SsaPhiExt phi , BasicBlock input ) {
1568+ relevantBackEdge ( phi , input )
1569+ or
15471570 DfInput:: supportBarrierGuardsOnPhiEdges ( ) and
15481571 // If the input isn't explicitly read then a guard cannot check it.
15491572 exists ( DfInput:: getARead ( getAPhiInputDef ( phi , input ) ) ) and
@@ -1605,6 +1628,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
16051628 * flow edges.
16061629 */
16071630 private predicate phiHasUniqNextNode ( SsaPhiExt phi ) {
1631+ not relevantBackEdge ( phi , _) and
16081632 exists ( int nextPhiInput , int nextPhi , int nextRef |
16091633 1 = nextPhiInput + nextPhi + nextRef and
16101634 nextPhiInput =
0 commit comments