@@ -1310,10 +1310,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
13101310 }
13111311
13121312 cached
1313- private predicate ssaInputNode ( SsaInputDefinitionExt def , BasicBlock input ) {
1314- def .hasInputFromBlock ( _, _, _, _, input )
1315- }
1316-
13171313 private newtype TNode =
13181314 TParamNode ( DfInput:: Parameter p ) or
13191315 TExprNode ( DfInput:: Expr e , Boolean isPost ) {
@@ -1325,7 +1321,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
13251321 isPost = false
13261322 } or
13271323 TSsaDefinitionNode ( DefinitionExt def ) or
1328- TSsaInputNode ( SsaInputDefinitionExt def , BasicBlock input ) { ssaInputNode ( def , input ) }
1324+ TSsaInputNode ( SsaInputDefinitionExt def , BasicBlock input ) {
1325+ def .hasInputFromBlock ( _, _, _, _, input )
1326+ }
13291327
13301328 /**
13311329 * A data flow node that we need to reference in the value step relation.
@@ -1541,33 +1539,39 @@ module Make<LocationSig Location, InputSig<Location> Input> {
15411539 }
15421540
15431541 /** Holds if there is a local flow step from `nodeFrom` to `nodeTo`. */
1544- predicate localFlowStep ( DefinitionExt def , Node nodeFrom , Node nodeTo ) {
1542+ predicate localFlowStep ( DefinitionExt def , Node nodeFrom , Node nodeTo , boolean isUseStep ) {
15451543 (
15461544 // Flow from assignment into SSA definition
15471545 DfInput:: ssaDefAssigns ( def , nodeFrom .( ExprNode ) .getExpr ( ) )
15481546 or
15491547 // Flow from parameter into entry definition
15501548 DfInput:: ssaDefInitializesParam ( def , nodeFrom .( ParameterNode ) .getParameter ( ) )
15511549 ) and
1552- nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def
1550+ nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
1551+ isUseStep = false
15531552 or
15541553 // Flow from SSA definition to first read
15551554 def = nodeFrom .( SsaDefinitionExtNode ) .getDefinitionExt ( ) and
1556- firstReadExt ( def , nodeTo )
1555+ firstReadExt ( def , nodeTo ) and
1556+ isUseStep = false
15571557 or
15581558 // Flow from (post-update) read to next read
15591559 adjacentReadPairExt ( def , [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] , nodeTo ) and
1560- nodeFrom != nodeTo
1560+ nodeFrom != nodeTo and
1561+ isUseStep = true
15611562 or
15621563 // Flow into phi (read) SSA definition node from def
1563- inputFromDef ( def , nodeFrom , nodeTo )
1564+ inputFromDef ( def , nodeFrom , nodeTo ) and
1565+ isUseStep = false
15641566 or
15651567 // Flow into phi (read) SSA definition node from (post-update) read
1566- inputFromRead ( def , [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] , nodeTo )
1568+ inputFromRead ( def , [ nodeFrom , nodeFrom .( ExprPostUpdateNode ) .getPreUpdateNode ( ) ] , nodeTo ) and
1569+ isUseStep = true
15671570 or
15681571 // Flow from input node to def
15691572 nodeTo .( SsaDefinitionExtNode ) .getDefinitionExt ( ) = def and
1570- def = nodeFrom .( SsaInputNode ) .getDefinitionExt ( )
1573+ def = nodeFrom .( SsaInputNode ) .getDefinitionExt ( ) and
1574+ isUseStep = false
15711575 }
15721576
15731577 pragma [ nomagic]
0 commit comments