@@ -24,16 +24,15 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
2424 bindingset [ source, sink]
2525 predicate isRelevantSourceSinkPair ( Node source , Node sink ) ;
2626
27- predicate isRelevantSink ( Node sink , FlowState state ) ;
28-
29- predicate isRelevantSink ( Node sink ) ;
30-
3127 predicate inBarrier ( NodeEx node , FlowState state ) ;
3228
3329 predicate outBarrier ( NodeEx node , FlowState state ) ;
3430
3531 predicate stateBarrier ( NodeEx node , FlowState state ) ;
3632
33+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
34+ NodeEx toNormalSinkNode ( NodeEx node ) ;
35+
3736 predicate sourceNode ( NodeEx node , FlowState state ) ;
3837
3938 predicate sinkNode ( NodeEx node , FlowState state ) ;
@@ -269,6 +268,16 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
269268 not stateBarrier ( node , state )
270269 }
271270
271+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
272+ pragma [ nomagic]
273+ NodeEx toNormalSinkNodeEx ( NodeEx node ) {
274+ exists ( Node n |
275+ pragma [ only_bind_out ] ( node .asNodeOrImplicitRead ( ) ) = n and
276+ ( isRelevantSink ( n ) or isRelevantSink ( n , _) ) and
277+ result .asNode ( ) = n
278+ )
279+ }
280+
272281 /** Provides the relevant barriers for a step from `node1` to `node2`. */
273282 bindingset [ node1, node2]
274283 private predicate stepFilter ( NodeEx node1 , NodeEx node2 ) {
@@ -1212,12 +1221,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
12121221 private predicate localStateStepNodeCand1Alias = localStateStepNodeCand1 / 7 ;
12131222
12141223 module Stage1NoState implements Stage1Output< FlowState > {
1215- predicate isRelevantSink ( Node sink , FlowState state ) {
1216- SourceSinkFiltering:: isRelevantSink ( sink , state )
1217- }
1218-
1219- predicate isRelevantSink ( Node sink ) { SourceSinkFiltering:: isRelevantSink ( sink ) }
1220-
12211224 predicate inBarrier = inBarrierAlias / 2 ;
12221225
12231226 predicate outBarrier = outBarrierAlias / 2 ;
@@ -1241,6 +1244,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
12411244 import Stage1
12421245 import Stage1Common
12431246
1247+ predicate toNormalSinkNode = toNormalSinkNodeEx / 1 ;
1248+
12441249 predicate sourceNode = sourceNodeAlias / 2 ;
12451250
12461251 predicate jumpStepEx = jumpStepExAlias / 2 ;
0 commit comments