@@ -1568,6 +1568,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1568
1568
/**
1569
1569
* Holds if the input to `phi` from the block `input` might be relevant for
1570
1570
* 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.
1571
1576
*/
1572
1577
private predicate relevantPhiInputNode ( SsaPhiExt phi , BasicBlock input ) {
1573
1578
relevantBackEdge ( phi , input )
@@ -1576,8 +1581,23 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1576
1581
// If the input isn't explicitly read then a guard cannot check it.
1577
1582
exists ( DfInput:: getARead ( getAPhiInputDef ( phi , input ) ) ) and
1578
1583
(
1584
+ // The input node is relevant either if it sits directly on a branch
1585
+ // edge for a guard,
1579
1586
exists ( DfInput:: Guard g | g .controlsBranchEdge ( input , phi .getBasicBlock ( ) , _) )
1580
1587
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
+ // ```
1581
1601
exists ( BasicBlock prev |
1582
1602
AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) ,
1583
1603
phi .getSourceVariable ( ) ) and
@@ -1937,13 +1957,17 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1937
1957
|
1938
1958
if relevantPhiInputNode ( phi , input )
1939
1959
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 )
1944
1961
)
1945
1962
}
1946
1963
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
+
1947
1971
/**
1948
1972
* Holds if there is a local flow step from `nodeFrom` to `nodeTo`.
1949
1973
*
@@ -1977,14 +2001,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1977
2001
)
1978
2002
or
1979
2003
// Flow from input node to def
1980
- exists ( DefinitionExt phi , BasicBlock bbPhi |
2004
+ exists ( DefinitionExt phi |
1981
2005
phi = nodeFrom .( SsaInputNodeImpl ) .getPhi ( ) and
1982
- phi .definesAt ( v , bbPhi , _, _) and
1983
2006
isUseStep = false and
1984
2007
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 )
1988
2009
)
1989
2010
}
1990
2011
0 commit comments