@@ -1356,14 +1356,18 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1356
1356
Stage1:: returnMayFlowThrough ( ret .getNodeEx ( ) , kind )
1357
1357
}
1358
1358
1359
+ bindingset [ node]
1360
+ pragma [ inline_late]
1361
+ private Nd mkNodeState ( NodeEx node , FlowState state ) { result = TNodeState ( node , state ) }
1362
+
1359
1363
pragma [ nomagic]
1360
1364
predicate storeStepCand (
1361
1365
Nd node1 , Content c , Nd node2 , DataFlowType contentType , DataFlowType containerType
1362
1366
) {
1363
1367
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1364
1368
Stage1:: storeStepCand ( n1 , c , n2 , contentType , containerType ) and
1365
- node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1366
- node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1369
+ node1 = mkNodeState ( n1 , s ) and
1370
+ node2 = mkNodeState ( n2 , s ) and
1367
1371
not outBarrier ( n1 , s ) and
1368
1372
not inBarrier ( n2 , s )
1369
1373
)
@@ -1373,8 +1377,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1373
1377
predicate readStepCand ( Nd node1 , Content c , Nd node2 ) {
1374
1378
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1375
1379
Stage1:: readStepCand ( n1 , c , n2 ) and
1376
- node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1377
- node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1380
+ node1 = mkNodeState ( n1 , s ) and
1381
+ node2 = mkNodeState ( n2 , s ) and
1378
1382
not outBarrier ( n1 , s ) and
1379
1383
not inBarrier ( n2 , s )
1380
1384
)
@@ -1385,8 +1389,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1385
1389
) {
1386
1390
exists ( ArgNodeEx arg0 , ParamNodeEx p0 , FlowState s |
1387
1391
Stage1:: callEdgeArgParam ( call , c , arg0 , p0 , emptyAp ) and
1388
- arg = TNodeState ( arg0 , pragma [ only_bind_into ] ( s ) ) and
1389
- p = TNodeState ( p0 , pragma [ only_bind_into ] ( s ) ) and
1392
+ arg = mkNodeState ( arg0 , s ) and
1393
+ p = mkNodeState ( p0 , s ) and
1390
1394
not outBarrier ( arg0 , s ) and
1391
1395
not inBarrier ( p0 , s )
1392
1396
)
@@ -1398,8 +1402,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1398
1402
) {
1399
1403
exists ( RetNodeEx ret0 , NodeEx out0 , FlowState s |
1400
1404
Stage1:: callEdgeReturn ( call , c , ret0 , kind , out0 , allowsFieldFlow ) and
1401
- ret = TNodeState ( ret0 , pragma [ only_bind_into ] ( s ) ) and
1402
- out = TNodeState ( out0 , pragma [ only_bind_into ] ( s ) ) and
1405
+ ret = mkNodeState ( ret0 , s ) and
1406
+ out = mkNodeState ( out0 , s ) and
1403
1407
not outBarrier ( ret0 , s ) and
1404
1408
not inBarrier ( out0 , s )
1405
1409
)
@@ -1409,8 +1413,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1409
1413
Nd toNormalSinkNode ( Nd node ) {
1410
1414
exists ( NodeEx res , NodeEx n , FlowState s |
1411
1415
res = toNormalSinkNodeEx ( n ) and
1412
- node = TNodeState ( n , pragma [ only_bind_into ] ( s ) ) and
1413
- result = TNodeState ( res , pragma [ only_bind_into ] ( s ) )
1416
+ node = mkNodeState ( n , s ) and
1417
+ result = mkNodeState ( res , s )
1414
1418
)
1415
1419
}
1416
1420
@@ -1431,8 +1435,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1431
1435
predicate jumpStepEx ( Nd node1 , Nd node2 ) {
1432
1436
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1433
1437
jumpStepEx1 ( n1 , n2 ) and
1434
- node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1435
- node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1438
+ node1 = mkNodeState ( n1 , s ) and
1439
+ node2 = mkNodeState ( n2 , s ) and
1436
1440
not outBarrier ( n1 , s ) and
1437
1441
not inBarrier ( n2 , s )
1438
1442
)
@@ -1441,16 +1445,16 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1441
1445
predicate additionalJumpStep ( Nd node1 , Nd node2 , string model ) {
1442
1446
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1443
1447
additionalJumpStep1 ( n1 , n2 , model ) and
1444
- node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1445
- node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1448
+ node1 = mkNodeState ( n1 , s ) and
1449
+ node2 = mkNodeState ( n2 , s ) and
1446
1450
not outBarrier ( n1 , s ) and
1447
1451
not inBarrier ( n2 , s )
1448
1452
)
1449
1453
or
1450
1454
exists ( NodeEx n1 , FlowState s1 , NodeEx n2 , FlowState s2 |
1451
1455
additionalJumpStateStep ( n1 , s1 , n2 , s2 , model ) and
1452
- node1 = TNodeState ( n1 , s1 ) and
1453
- node2 = TNodeState ( n2 , s2 )
1456
+ node1 = mkNodeState ( n1 , s1 ) and
1457
+ node2 = mkNodeState ( n2 , s2 )
1454
1458
)
1455
1459
}
1456
1460
@@ -1461,17 +1465,17 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1461
1465
) {
1462
1466
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1463
1467
localStepNodeCand1 ( n1 , n2 , preservesValue , t , lcc , label ) and
1464
- node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1465
- node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1468
+ node1 = mkNodeState ( n1 , s ) and
1469
+ node2 = mkNodeState ( n2 , s ) and
1466
1470
not outBarrier ( n1 , s ) and
1467
1471
not inBarrier ( n2 , s )
1468
1472
)
1469
1473
or
1470
1474
exists ( NodeEx n1 , NodeEx n2 , FlowState s1 , FlowState s2 |
1471
1475
localStateStepNodeCand1 ( n1 , s1 , n2 , s2 , t , lcc , label ) and
1472
1476
preservesValue = false and
1473
- node1 = TNodeState ( n1 , s1 ) and
1474
- node2 = TNodeState ( n2 , s2 )
1477
+ node1 = mkNodeState ( n1 , s1 ) and
1478
+ node2 = mkNodeState ( n2 , s2 )
1475
1479
)
1476
1480
}
1477
1481
0 commit comments