@@ -1495,6 +1495,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1495
1495
1496
1496
/** Holds if `guard` controls block `bb` upon evaluating to `branch`. */
1497
1497
predicate guardControlsBlock ( Guard guard , BasicBlock bb , boolean branch ) ;
1498
+
1499
+ /**
1500
+ * Holds if `WriteDefinition`s should be included as an intermediate node
1501
+ * between the assigned `Expr` or `Parameter` and the first read of the SSA
1502
+ * definition.
1503
+ */
1504
+ default predicate includeWriteDefsInFlowStep ( ) { any ( ) }
1498
1505
}
1499
1506
1500
1507
/**
@@ -1783,42 +1790,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1783
1790
exists ( DefinitionExt def |
1784
1791
nodeFrom .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = def and
1785
1792
def .definesAt ( v , bb , i , _) and
1786
- isUseStep = false
1793
+ isUseStep = false and
1794
+ if DfInput:: includeWriteDefsInFlowStep ( )
1795
+ then any ( )
1796
+ else (
1797
+ def instanceof PhiNode or
1798
+ def instanceof PhiReadNode or
1799
+ DfInput:: allowFlowIntoUncertainDef ( def )
1800
+ )
1787
1801
)
1788
1802
or
1789
1803
[ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] .( ReadNode ) .readsAt ( bb , i , v ) and
1790
1804
isUseStep = true
1791
1805
}
1792
1806
1793
- /**
1794
- * Holds if there is a local flow step from `nodeFrom` to `nodeTo`.
1795
- *
1796
- * `isUseStep` is `true` when `nodeFrom` is a (post-update) read node and
1797
- * `nodeTo` is a read node or phi (read) node.
1798
- */
1799
- predicate localFlowStep ( SourceVariable v , Node nodeFrom , Node nodeTo , boolean isUseStep ) {
1800
- exists ( Definition def |
1801
- // Flow from assignment into SSA definition
1802
- DfInput:: ssaDefAssigns ( def , nodeFrom .( ExprNode ) .getExpr ( ) )
1803
- or
1804
- // Flow from parameter into entry definition
1805
- DfInput:: ssaDefInitializesParam ( def , nodeFrom .( ParameterNode ) .getParameter ( ) )
1806
- |
1807
- nodeTo .( SsaDefinitionNode ) .getDefinition ( ) = def and
1808
- v = def .getSourceVariable ( ) and
1809
- isUseStep = false
1810
- )
1811
- or
1807
+ private predicate flowFromRefToNode ( SourceVariable v , BasicBlock bb1 , int i1 , Node nodeTo ) {
1812
1808
// Flow from definition/read to next read
1813
- exists ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1814
- flowOutOf ( nodeFrom , v , bb1 , i1 , isUseStep ) and
1809
+ exists ( BasicBlock bb2 , int i2 |
1815
1810
AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
1816
1811
nodeTo .( ReadNode ) .readsAt ( bb2 , i2 , v )
1817
1812
)
1818
1813
or
1819
1814
// Flow from definition/read to next uncertain write
1820
- exists ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1821
- flowOutOf ( nodeFrom , v , bb1 , i1 , isUseStep ) and
1815
+ exists ( BasicBlock bb2 , int i2 |
1822
1816
AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
1823
1817
exists ( UncertainWriteDefinition def2 |
1824
1818
DfInput:: allowFlowIntoUncertainDef ( def2 ) and
@@ -1828,12 +1822,43 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1828
1822
)
1829
1823
or
1830
1824
// Flow from definition/read to phi input
1831
- exists ( BasicBlock bb , int i , BasicBlock input , BasicBlock bbPhi , DefinitionExt phi |
1832
- flowOutOf ( nodeFrom , v , bb , i , isUseStep ) and
1833
- AdjacentSsaRefs:: adjacentRefPhi ( bb , i , input , bbPhi , v ) and
1825
+ exists ( BasicBlock input , BasicBlock bbPhi , DefinitionExt phi |
1826
+ AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i1 , input , bbPhi , v ) and
1834
1827
nodeTo = TSsaInputNode ( phi , input ) and
1835
1828
phi .definesAt ( v , bbPhi , - 1 , _)
1836
1829
)
1830
+ }
1831
+
1832
+ /**
1833
+ * Holds if there is a local flow step from `nodeFrom` to `nodeTo`.
1834
+ *
1835
+ * `isUseStep` is `true` when `nodeFrom` is a (post-update) read node and
1836
+ * `nodeTo` is a read node or phi (read) node.
1837
+ */
1838
+ predicate localFlowStep ( SourceVariable v , Node nodeFrom , Node nodeTo , boolean isUseStep ) {
1839
+ exists ( Definition def |
1840
+ // Flow from assignment into SSA definition
1841
+ DfInput:: ssaDefAssigns ( def , nodeFrom .( ExprNode ) .getExpr ( ) )
1842
+ or
1843
+ // Flow from parameter into entry definition
1844
+ DfInput:: ssaDefInitializesParam ( def , nodeFrom .( ParameterNode ) .getParameter ( ) )
1845
+ |
1846
+ isUseStep = false and
1847
+ if DfInput:: includeWriteDefsInFlowStep ( )
1848
+ then
1849
+ nodeTo .( SsaDefinitionNode ) .getDefinition ( ) = def and
1850
+ v = def .getSourceVariable ( )
1851
+ else
1852
+ exists ( BasicBlock bb1 , int i1 |
1853
+ def .definesAt ( v , bb1 , i1 ) and
1854
+ flowFromRefToNode ( v , bb1 , i1 , nodeTo )
1855
+ )
1856
+ )
1857
+ or
1858
+ exists ( BasicBlock bb1 , int i1 |
1859
+ flowOutOf ( nodeFrom , v , bb1 , i1 , isUseStep ) and
1860
+ flowFromRefToNode ( v , bb1 , i1 , nodeTo )
1861
+ )
1837
1862
or
1838
1863
// Flow from input node to def
1839
1864
exists ( DefinitionExt def |
@@ -1853,8 +1878,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1853
1878
// Flow from parameter into entry definition
1854
1879
DfInput:: ssaDefInitializesParam ( def , nodeFrom .( ParameterNode ) .getParameter ( ) )
1855
1880
|
1856
- nodeTo .( SsaDefinitionNode ) .getDefinition ( ) = def and
1857
- v = def .getSourceVariable ( )
1881
+ v = def .getSourceVariable ( ) and
1882
+ if DfInput:: includeWriteDefsInFlowStep ( )
1883
+ then nodeTo .( SsaDefinitionNode ) .getDefinition ( ) = def
1884
+ else nodeTo .( ExprNode ) .getExpr ( ) = DfInput:: getARead ( def )
1858
1885
)
1859
1886
or
1860
1887
// Flow from SSA definition to read
0 commit comments