@@ -1555,24 +1555,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15551555 )
15561556 }
15571557
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-
15761558 final private class DefinitionExtFinal = DefinitionExt ;
15771559
15781560 /** An SSA definition into which another SSA definition may flow. */
@@ -1808,41 +1790,22 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18081790 final class SsaInputNode = SsaInputNodeImpl ;
18091791
18101792 /**
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`.
18131798 */
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
18171801 ) {
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
18461809 }
18471810
18481811 /**
@@ -1862,23 +1825,34 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18621825 nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
18631826 isUseStep = false
18641827 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+ )
18741834 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+ )
18781845 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+ )
18821856 or
18831857 // Flow from input node to def
18841858 nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
0 commit comments