@@ -1568,6 +1568,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15681568 /**
15691569 * Holds if the input to `phi` from the block `input` might be relevant for
15701570 * barrier guards as a separately synthesized `TSsaInputNode`.
1571+ *
1572+ * Note that `TSsaInputNode`s have both unique predecessors and unique
1573+ * successors, both of which are given by `adjacentRefPhi`, so we can
1574+ * always skip them in the flow graph without increasing the number of flow
1575+ * edges, if they are not needed for barrier guards.
15711576 */
15721577 private predicate relevantPhiInputNode ( SsaPhiExt phi , BasicBlock input ) {
15731578 relevantBackEdge ( phi , input )
@@ -1576,8 +1581,23 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15761581 // If the input isn't explicitly read then a guard cannot check it.
15771582 exists ( DfInput:: getARead ( getAPhiInputDef ( phi , input ) ) ) and
15781583 (
1584+ // The input node is relevant either if it sits directly on a branch
1585+ // edge for a guard,
15791586 exists ( DfInput:: Guard g | g .controlsBranchEdge ( input , phi .getBasicBlock ( ) , _) )
15801587 or
1588+ // or if the unique predecessor is not an equivalent substitute in
1589+ // terms of being controlled by the same guards.
1590+ // Example:
1591+ // ```
1592+ // if (g1) {
1593+ // use(x); // A
1594+ // if (g2) { .. }
1595+ // // no need for an input node here, as the set of guards controlling
1596+ // // this block is the same as the set of guards controlling the prior
1597+ // // use of `x` at A.
1598+ // }
1599+ // // phi-read node for `x`
1600+ // ```
15811601 exists ( BasicBlock prev |
15821602 AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) ,
15831603 phi .getSourceVariable ( ) ) and
@@ -1937,13 +1957,17 @@ module Make<LocationSig Location, InputSig<Location> Input> {
19371957 |
19381958 if relevantPhiInputNode ( phi , input )
19391959 then nodeTo = TSsaInputNode ( phi , input )
1940- else
1941- if phiHasUniqNextNode ( phi )
1942- then flowFromRefToNode ( v , bbPhi , - 1 , nodeTo )
1943- else nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
1960+ else flowIntoPhi ( phi , v , bbPhi , nodeTo )
19441961 )
19451962 }
19461963
1964+ private predicate flowIntoPhi ( DefinitionExt phi , SourceVariable v , BasicBlock bbPhi , Node nodeTo ) {
1965+ phi .definesAt ( v , bbPhi , - 1 , _) and
1966+ if phiHasUniqNextNode ( phi )
1967+ then flowFromRefToNode ( v , bbPhi , - 1 , nodeTo )
1968+ else nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
1969+ }
1970+
19471971 /**
19481972 * Holds if there is a local flow step from `nodeFrom` to `nodeTo`.
19491973 *
@@ -1977,14 +2001,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
19772001 )
19782002 or
19792003 // Flow from input node to def
1980- exists ( DefinitionExt phi , BasicBlock bbPhi |
2004+ exists ( DefinitionExt phi |
19812005 phi = nodeFrom .( SsaInputNodeImpl ) .getPhi ( ) and
1982- phi .definesAt ( v , bbPhi , _, _) and
19832006 isUseStep = false and
19842007 nodeFrom != nodeTo and
1985- if phiHasUniqNextNode ( phi )
1986- then flowFromRefToNode ( v , bbPhi , - 1 , nodeTo )
1987- else nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
2008+ flowIntoPhi ( phi , v , _, nodeTo )
19882009 )
19892010 }
19902011
0 commit comments