@@ -24,16 +24,15 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
24
24
bindingset [ source, sink]
25
25
predicate isRelevantSourceSinkPair ( Node source , Node sink ) ;
26
26
27
- predicate isRelevantSink ( Node sink , FlowState state ) ;
28
-
29
- predicate isRelevantSink ( Node sink ) ;
30
-
31
27
predicate inBarrier ( NodeEx node , FlowState state ) ;
32
28
33
29
predicate outBarrier ( NodeEx node , FlowState state ) ;
34
30
35
31
predicate stateBarrier ( NodeEx node , FlowState state ) ;
36
32
33
+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
34
+ NodeEx toNormalSinkNode ( NodeEx node ) ;
35
+
37
36
predicate sourceNode ( NodeEx node , FlowState state ) ;
38
37
39
38
predicate sinkNode ( NodeEx node , FlowState state ) ;
@@ -269,6 +268,16 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
269
268
not stateBarrier ( node , state )
270
269
}
271
270
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
+
272
281
/** Provides the relevant barriers for a step from `node1` to `node2`. */
273
282
bindingset [ node1, node2]
274
283
private predicate stepFilter ( NodeEx node1 , NodeEx node2 ) {
@@ -1212,12 +1221,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1212
1221
private predicate localStateStepNodeCand1Alias = localStateStepNodeCand1 / 7 ;
1213
1222
1214
1223
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
-
1221
1224
predicate inBarrier = inBarrierAlias / 2 ;
1222
1225
1223
1226
predicate outBarrier = outBarrierAlias / 2 ;
@@ -1241,6 +1244,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1241
1244
import Stage1
1242
1245
import Stage1Common
1243
1246
1247
+ predicate toNormalSinkNode = toNormalSinkNodeEx / 1 ;
1248
+
1244
1249
predicate sourceNode = sourceNodeAlias / 2 ;
1245
1250
1246
1251
predicate jumpStepEx = jumpStepExAlias / 2 ;
0 commit comments