@@ -1356,14 +1356,18 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
13561356 Stage1:: returnMayFlowThrough ( ret .getNodeEx ( ) , kind )
13571357 }
13581358
1359+ bindingset [ node]
1360+ pragma [ inline_late]
1361+ private Nd mkNodeState ( NodeEx node , FlowState state ) { result = TNodeState ( node , state ) }
1362+
13591363 pragma [ nomagic]
13601364 predicate storeStepCand (
13611365 Nd node1 , Content c , Nd node2 , DataFlowType contentType , DataFlowType containerType
13621366 ) {
13631367 exists ( NodeEx n1 , NodeEx n2 , FlowState s |
13641368 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
13671371 not outBarrier ( n1 , s ) and
13681372 not inBarrier ( n2 , s )
13691373 )
@@ -1373,8 +1377,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
13731377 predicate readStepCand ( Nd node1 , Content c , Nd node2 ) {
13741378 exists ( NodeEx n1 , NodeEx n2 , FlowState s |
13751379 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
13781382 not outBarrier ( n1 , s ) and
13791383 not inBarrier ( n2 , s )
13801384 )
@@ -1385,8 +1389,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
13851389 ) {
13861390 exists ( ArgNodeEx arg0 , ParamNodeEx p0 , FlowState s |
13871391 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
13901394 not outBarrier ( arg0 , s ) and
13911395 not inBarrier ( p0 , s )
13921396 )
@@ -1398,8 +1402,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
13981402 ) {
13991403 exists ( RetNodeEx ret0 , NodeEx out0 , FlowState s |
14001404 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
14031407 not outBarrier ( ret0 , s ) and
14041408 not inBarrier ( out0 , s )
14051409 )
@@ -1409,8 +1413,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
14091413 Nd toNormalSinkNode ( Nd node ) {
14101414 exists ( NodeEx res , NodeEx n , FlowState s |
14111415 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 )
14141418 )
14151419 }
14161420
@@ -1431,8 +1435,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
14311435 predicate jumpStepEx ( Nd node1 , Nd node2 ) {
14321436 exists ( NodeEx n1 , NodeEx n2 , FlowState s |
14331437 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
14361440 not outBarrier ( n1 , s ) and
14371441 not inBarrier ( n2 , s )
14381442 )
@@ -1441,16 +1445,16 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
14411445 predicate additionalJumpStep ( Nd node1 , Nd node2 , string model ) {
14421446 exists ( NodeEx n1 , NodeEx n2 , FlowState s |
14431447 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
14461450 not outBarrier ( n1 , s ) and
14471451 not inBarrier ( n2 , s )
14481452 )
14491453 or
14501454 exists ( NodeEx n1 , FlowState s1 , NodeEx n2 , FlowState s2 |
14511455 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 )
14541458 )
14551459 }
14561460
@@ -1461,17 +1465,17 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
14611465 ) {
14621466 exists ( NodeEx n1 , NodeEx n2 , FlowState s |
14631467 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
14661470 not outBarrier ( n1 , s ) and
14671471 not inBarrier ( n2 , s )
14681472 )
14691473 or
14701474 exists ( NodeEx n1 , NodeEx n2 , FlowState s1 , FlowState s2 |
14711475 localStateStepNodeCand1 ( n1 , s1 , n2 , s2 , t , lcc , label ) and
14721476 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 )
14751479 )
14761480 }
14771481
0 commit comments