@@ -1495,6 +1495,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
14951495
14961496 /** Holds if `guard` controls block `bb` upon evaluating to `branch`. */
14971497 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 ( ) }
14981505 }
14991506
15001507 /**
@@ -1783,42 +1790,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
17831790 exists ( DefinitionExt def |
17841791 nodeFrom .( SsaDefinitionExtNodeImpl ) .getDefExt ( ) = def and
17851792 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+ )
17871801 )
17881802 or
17891803 [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] .( ReadNode ) .readsAt ( bb , i , v ) and
17901804 isUseStep = true
17911805 }
17921806
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 ) {
18121808 // 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 |
18151810 AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
18161811 nodeTo .( ReadNode ) .readsAt ( bb2 , i2 , v )
18171812 )
18181813 or
18191814 // 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 |
18221816 AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
18231817 exists ( UncertainWriteDefinition def2 |
18241818 DfInput:: allowFlowIntoUncertainDef ( def2 ) and
@@ -1828,12 +1822,43 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18281822 )
18291823 or
18301824 // 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
18341827 nodeTo = TSsaInputNode ( phi , input ) and
18351828 phi .definesAt ( v , bbPhi , - 1 , _)
18361829 )
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+ )
18371862 or
18381863 // Flow from input node to def
18391864 exists ( DefinitionExt def |
@@ -1853,8 +1878,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
18531878 // Flow from parameter into entry definition
18541879 DfInput:: ssaDefInitializesParam ( def , nodeFrom .( ParameterNode ) .getParameter ( ) )
18551880 |
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 )
18581885 )
18591886 or
18601887 // Flow from SSA definition to read
0 commit comments