@@ -1562,6 +1562,58 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1562
1562
)
1563
1563
}
1564
1564
1565
+ /**
1566
+ * Holds if a next adjacent use of `phi` is as input to `phi2` through
1567
+ * `input`. The boolean `relevant` indicates whether the input edge might
1568
+ * be relevant for barrier guards.
1569
+ */
1570
+ private predicate phiStepsToPhiInput (
1571
+ SsaPhiExt phi , SsaPhiExt phi2 , BasicBlock input , boolean relevant
1572
+ ) {
1573
+ exists ( BasicBlock bb1 , int i , SourceVariable v , BasicBlock bb2 |
1574
+ phi .definesAt ( v , bb1 , i , _) and
1575
+ AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i , input , bb2 , v ) and
1576
+ phi2 .definesAt ( v , bb2 , _, _) and
1577
+ if relevantPhiInputNode ( phi2 , input ) then relevant = true else relevant = false
1578
+ )
1579
+ }
1580
+
1581
+ /**
1582
+ * Holds if a next adjacent use of `phi` occurs at index `i` in basic block
1583
+ * `bb`. The boolean `isUse` indicates whether the use is a read or an
1584
+ * uncertain write.
1585
+ */
1586
+ private predicate phiStepsToRef ( SsaPhiExt phi , BasicBlock bb , int i , boolean isUse ) {
1587
+ exists ( SourceVariable v , BasicBlock bb1 , int i1 |
1588
+ phi .definesAt ( v , bb1 , i1 , _) and
1589
+ AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb , i , v )
1590
+ |
1591
+ isUse = true and
1592
+ variableRead ( bb , i , v , true )
1593
+ or
1594
+ isUse = false and
1595
+ exists ( UncertainWriteDefinition def2 |
1596
+ DfInput:: allowFlowIntoUncertainDef ( def2 ) and
1597
+ def2 .definesAt ( v , bb , i )
1598
+ )
1599
+ )
1600
+ }
1601
+
1602
+ /**
1603
+ * Holds if the next adjacent use of `phi` is unique. In this case, we can
1604
+ * skip the phi in the use-use step relation without increasing the number
1605
+ * flow edges.
1606
+ */
1607
+ private predicate phiHasUniqNextNode ( SsaPhiExt phi ) {
1608
+ exists ( int nextPhiInput , int nextPhi , int nextRef |
1609
+ 1 = nextPhiInput + nextPhi + nextRef and
1610
+ nextPhiInput =
1611
+ count ( SsaPhiExt phi2 , BasicBlock input | phiStepsToPhiInput ( phi , phi2 , input , true ) ) and
1612
+ nextPhi = count ( SsaPhiExt phi2 | phiStepsToPhiInput ( phi , phi2 , _, false ) ) and
1613
+ nextRef = count ( BasicBlock bb , int i , boolean isUse | phiStepsToRef ( phi , bb , i , isUse ) )
1614
+ )
1615
+ }
1616
+
1565
1617
private newtype TNode =
1566
1618
TParamNode ( DfInput:: Parameter p ) {
1567
1619
exists ( WriteDefinition def | DfInput:: ssaDefInitializesParam ( def , p ) )
@@ -1574,7 +1626,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1574
1626
isPost = false
1575
1627
)
1576
1628
} or
1577
- TSsaDefinitionNode ( DefinitionExt def ) or
1629
+ TSsaDefinitionNode ( DefinitionExt def ) { not phiHasUniqNextNode ( def ) } or
1578
1630
TSsaInputNode ( SsaPhiExt phi , BasicBlock input ) { relevantPhiInputNode ( phi , input ) }
1579
1631
1580
1632
/**
@@ -1853,10 +1905,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1853
1905
AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i1 , input , bbPhi , v ) and
1854
1906
phi .definesAt ( v , bbPhi , - 1 , _)
1855
1907
|
1856
- nodeTo = TSsaInputNode ( phi , input )
1857
- or
1858
- not relevantPhiInputNode ( phi , input ) and
1859
- nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
1908
+ if relevantPhiInputNode ( phi , input )
1909
+ then nodeTo = TSsaInputNode ( phi , input )
1910
+ else
1911
+ if phiHasUniqNextNode ( phi )
1912
+ then flowFromRefToNode ( v , bbPhi , - 1 , nodeTo )
1913
+ else nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
1860
1914
)
1861
1915
}
1862
1916
@@ -1892,11 +1946,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1892
1946
)
1893
1947
or
1894
1948
// Flow from input node to def
1895
- exists ( DefinitionExt def |
1896
- nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = def and
1897
- def = nodeFrom .( SsaInputNodeImpl ) .getPhi ( ) and
1898
- v = def .getSourceVariable ( ) and
1899
- isUseStep = false
1949
+ exists ( DefinitionExt phi , BasicBlock bbPhi |
1950
+ phi = nodeFrom .( SsaInputNodeImpl ) .getPhi ( ) and
1951
+ phi .definesAt ( v , bbPhi , _, _) and
1952
+ isUseStep = false and
1953
+ if phiHasUniqNextNode ( phi )
1954
+ then flowFromRefToNode ( v , bbPhi , - 1 , nodeTo )
1955
+ else nodeTo .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = phi
1900
1956
)
1901
1957
}
1902
1958
0 commit comments