@@ -1562,6 +1562,58 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15621562 )
15631563 }
15641564
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+
15651617 private newtype TNode =
15661618 TParamNode ( DfInput:: Parameter p ) {
15671619 exists ( WriteDefinition def | DfInput:: ssaDefInitializesParam ( def , p ) )
@@ -1574,7 +1626,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15741626 isPost = false
15751627 )
15761628 } or
1577- TSsaDefinitionNode ( DefinitionExt def ) or
1629+ TSsaDefinitionNode ( DefinitionExt def ) { not phiHasUniqNextNode ( def ) } or
15781630 TSsaInputNode ( SsaPhiExt phi , BasicBlock input ) { relevantPhiInputNode ( phi , input ) }
15791631
15801632 /**
@@ -1853,10 +1905,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18531905 AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i1 , input , bbPhi , v ) and
18541906 phi .definesAt ( v , bbPhi , - 1 , _)
18551907 |
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
18601914 )
18611915 }
18621916
@@ -1892,11 +1946,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18921946 )
18931947 or
18941948 // 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
19001956 )
19011957 }
19021958
0 commit comments