@@ -1555,24 +1555,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1555
1555
)
1556
1556
}
1557
1557
1558
- /** Same as `adjacentDefReadExt`, but skips uncertain reads. */
1559
- pragma [ nomagic]
1560
- private predicate adjacentDefSkipUncertainReadsExt (
1561
- DefinitionExt def , SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
1562
- ) {
1563
- adjacentDefReachesReadExt ( def , v , bb1 , i1 , bb2 , i2 ) and
1564
- variableRead ( bb2 , i2 , v , true )
1565
- }
1566
-
1567
- pragma [ nomagic]
1568
- private predicate adjacentReadPairExt ( DefinitionExt def , ReadNode read1 , ReadNode read2 ) {
1569
- exists ( SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1570
- read1 .readsAt ( bb1 , i1 , v ) and
1571
- adjacentDefSkipUncertainReadsExt ( def , v , bb1 , i1 , bb2 , i2 ) and
1572
- read2 .readsAt ( bb2 , i2 , v )
1573
- )
1574
- }
1575
-
1576
1558
final private class DefinitionExtFinal = DefinitionExt ;
1577
1559
1578
1560
/** An SSA definition into which another SSA definition may flow. */
@@ -1808,41 +1790,22 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1808
1790
final class SsaInputNode = SsaInputNodeImpl ;
1809
1791
1810
1792
/**
1811
- * Holds if `nodeFrom` is a node for SSA definition `def`, which can input
1812
- * node `nodeTo`.
1793
+ * Holds if `nodeFrom` corresponds to the reference to `v` at index `i` in
1794
+ * `bb`. The boolean `isUseStep` indicates whether `nodeFrom` is an actual
1795
+ * read. If it is false then `nodeFrom` may be any of the following: an
1796
+ * uncertain write, a certain write, a phi, or a phi read. `def` is the SSA
1797
+ * definition that is read/defined at `nodeFrom`.
1813
1798
*/
1814
- pragma [ nomagic]
1815
- private predicate inputFromDef (
1816
- DefinitionExt def , SsaDefinitionExtNode nodeFrom , SsaInputNode nodeTo
1799
+ private predicate flowOutOf (
1800
+ DefinitionExt def , Node nodeFrom , SourceVariable v , BasicBlock bb , int i , boolean isUseStep
1817
1801
) {
1818
- exists ( SourceVariable v , BasicBlock bb , int i , BasicBlock input , SsaInputDefinitionExt next |
1819
- next .hasInputFromBlock ( def , v , bb , i , input ) and
1820
- def = nodeFrom .getDefinitionExt ( ) and
1821
- def .definesAt ( v , bb , i , _) and
1822
- nodeTo = TSsaInputNode ( next , input )
1823
- )
1824
- }
1825
-
1826
- /**
1827
- * Holds if `nodeFrom` is a last read of SSA definition `def`, which
1828
- * can reach input node `nodeTo`.
1829
- */
1830
- pragma [ nomagic]
1831
- private predicate inputFromRead ( DefinitionExt def , ReadNode nodeFrom , SsaInputNode nodeTo ) {
1832
- exists ( SourceVariable v , BasicBlock bb , int i , BasicBlock input , SsaInputDefinitionExt next |
1833
- next .hasInputFromBlock ( def , v , bb , i , input ) and
1834
- nodeFrom .readsAt ( bb , i , v ) and
1835
- nodeTo = TSsaInputNode ( next , input )
1836
- )
1837
- }
1838
-
1839
- pragma [ nomagic]
1840
- private predicate firstReadExt ( DefinitionExt def , ReadNode read ) {
1841
- exists ( SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1842
- def .definesAt ( v , bb1 , i1 , _) and
1843
- adjacentDefSkipUncertainReadsExt ( def , v , bb1 , i1 , bb2 , i2 ) and
1844
- read .readsAt ( bb2 , i2 , v )
1845
- )
1802
+ nodeFrom .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
1803
+ def .definesAt ( v , bb , i , _) and
1804
+ isUseStep = false
1805
+ or
1806
+ ssaDefReachesReadExt ( v , def , bb , i ) and
1807
+ [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] .( ReadNode ) .readsAt ( bb , i , v ) and
1808
+ isUseStep = true
1846
1809
}
1847
1810
1848
1811
/**
@@ -1862,23 +1825,34 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1862
1825
nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
1863
1826
isUseStep = false
1864
1827
or
1865
- // Flow from SSA definition to first read
1866
- def = nodeFrom .( SsaDefinitionExtNode ) .getDefinitionExt ( ) and
1867
- firstReadExt ( def , nodeTo ) and
1868
- isUseStep = false
1869
- or
1870
- // Flow from (post-update) read to next read
1871
- adjacentReadPairExt ( def , [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] , nodeTo ) and
1872
- nodeFrom != nodeTo and
1873
- isUseStep = true
1828
+ // Flow from definition/read to next read
1829
+ exists ( SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1830
+ flowOutOf ( def , nodeFrom , v , bb1 , i1 , isUseStep ) and
1831
+ AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
1832
+ nodeTo .( ReadNode ) .readsAt ( bb2 , i2 , v )
1833
+ )
1874
1834
or
1875
- // Flow into phi (read) SSA definition node from def
1876
- inputFromDef ( def , nodeFrom , nodeTo ) and
1877
- isUseStep = false
1835
+ // Flow from definition/read to next uncertain write
1836
+ exists ( SourceVariable v , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1837
+ flowOutOf ( def , nodeFrom , v , bb1 , i1 , isUseStep ) and
1838
+ AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
1839
+ exists ( UncertainWriteDefinition def2 |
1840
+ DfInput:: allowFlowIntoUncertainDef ( def2 ) and
1841
+ nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def2 and
1842
+ def2 .definesAt ( v , bb2 , i2 )
1843
+ )
1844
+ )
1878
1845
or
1879
- // Flow into phi (read) SSA definition node from (post-update) read
1880
- inputFromRead ( def , [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] , nodeTo ) and
1881
- isUseStep = true
1846
+ // Flow from definition/read to phi input
1847
+ exists (
1848
+ SourceVariable v , BasicBlock bb , int i , BasicBlock input , BasicBlock bbPhi ,
1849
+ DefinitionExt phi
1850
+ |
1851
+ flowOutOf ( def , nodeFrom , v , bb , i , isUseStep ) and
1852
+ AdjacentSsaRefs:: adjacentRefPhi ( bb , i , input , bbPhi , v ) and
1853
+ nodeTo = TSsaInputNode ( phi , input ) and
1854
+ phi .definesAt ( v , bbPhi , - 1 , _)
1855
+ )
1882
1856
or
1883
1857
// Flow from input node to def
1884
1858
nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
0 commit comments