@@ -351,7 +351,7 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
351
351
/**
352
352
* Holds if data can flow from `node1` to `node2` in a way that discards call contexts.
353
353
*/
354
- private predicate jumpStepEx ( NodeEx node1 , NodeEx node2 ) {
354
+ private predicate jumpStepEx1 ( NodeEx node1 , NodeEx node2 ) {
355
355
exists ( Node n1 , Node n2 |
356
356
node1 .asNode ( ) = n1 and
357
357
node2 .asNode ( ) = n2 and
@@ -364,7 +364,7 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
364
364
/**
365
365
* Holds if the additional step from `node1` to `node2` jumps between callables.
366
366
*/
367
- private predicate additionalJumpStep ( NodeEx node1 , NodeEx node2 , string model ) {
367
+ private predicate additionalJumpStep1 ( NodeEx node1 , NodeEx node2 , string model ) {
368
368
exists ( Node n1 , Node n2 |
369
369
node1 .asNodeOrImplicitRead ( ) = n1 and
370
370
node2 .asNode ( ) = n2 and
@@ -478,8 +478,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
478
478
)
479
479
or
480
480
exists ( NodeEx mid | fwdFlow ( mid , _) and cc = false |
481
- jumpStepEx ( mid , node ) or
482
- additionalJumpStep ( mid , node , _) or
481
+ jumpStepEx1 ( mid , node ) or
482
+ additionalJumpStep1 ( mid , node , _) or
483
483
additionalJumpStateStep ( mid , _, node , _, _)
484
484
)
485
485
or
@@ -693,8 +693,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
693
693
)
694
694
or
695
695
exists ( NodeEx mid | revFlow ( mid , _) and toReturn = false |
696
- jumpStepEx ( node , mid ) or
697
- additionalJumpStep ( node , mid , _) or
696
+ jumpStepEx1 ( node , mid ) or
697
+ additionalJumpStep1 ( node , mid , _) or
698
698
additionalJumpStateStep ( node , _, mid , _, _)
699
699
)
700
700
or
@@ -1212,11 +1212,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1212
1212
)
1213
1213
}
1214
1214
1215
- private predicate jumpStepExAlias = jumpStepEx / 2 ;
1216
-
1217
- private predicate additionalJumpStepAlias = additionalJumpStep / 3 ;
1218
-
1219
-
1220
1215
module Stage1NoState implements Stage1Output< Unit > {
1221
1216
class Nd = NodeEx ;
1222
1217
@@ -1255,9 +1250,9 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1255
1250
1256
1251
predicate sinkNode ( NodeEx node ) { sinkNode ( node , _) }
1257
1252
1258
- predicate jumpStepEx = jumpStepExAlias / 2 ;
1253
+ predicate jumpStepEx = jumpStepEx1 / 2 ;
1259
1254
1260
- predicate additionalJumpStep = additionalJumpStepAlias / 3 ;
1255
+ predicate additionalJumpStep = additionalJumpStep1 / 3 ;
1261
1256
1262
1257
predicate localStep1 = localStepNodeCand1 / 6 ;
1263
1258
@@ -1280,8 +1275,8 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1280
1275
exists ( NodeEx mid | flowState ( mid , state ) |
1281
1276
localFlowStepEx ( mid , node , _) or
1282
1277
additionalLocalFlowStep ( mid , node , _) or
1283
- jumpStepExAlias ( mid , node ) or
1284
- additionalJumpStepAlias ( mid , node , _) or
1278
+ jumpStepEx1 ( mid , node ) or
1279
+ additionalJumpStep1 ( mid , node , _) or
1285
1280
store ( mid , _, node , _, _) or
1286
1281
readSetEx ( mid , _, node ) or
1287
1282
flowIntoCallNodeCand1 ( _, mid , node ) or
@@ -1437,7 +1432,7 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1437
1432
1438
1433
predicate jumpStepEx ( Nd node1 , Nd node2 ) {
1439
1434
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1440
- jumpStepExAlias ( n1 , n2 ) and
1435
+ jumpStepEx1 ( n1 , n2 ) and
1441
1436
node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1442
1437
node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1443
1438
not outBarrier ( n1 , s ) and
@@ -1447,7 +1442,7 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1447
1442
1448
1443
predicate additionalJumpStep ( Nd node1 , Nd node2 , string model ) {
1449
1444
exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1450
- additionalJumpStepAlias ( n1 , n2 , model ) and
1445
+ additionalJumpStep1 ( n1 , n2 , model ) and
1451
1446
node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1452
1447
node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1453
1448
not outBarrier ( n1 , s ) and
@@ -1529,9 +1524,9 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1529
1524
1530
1525
private predicate callableStep ( DataFlowCallable c1 , DataFlowCallable c2 ) {
1531
1526
exists ( NodeEx node1 , NodeEx node2 |
1532
- jumpStepEx ( node1 , node2 )
1527
+ jumpStepEx1 ( node1 , node2 )
1533
1528
or
1534
- additionalJumpStep ( node1 , node2 , _)
1529
+ additionalJumpStep1 ( node1 , node2 , _)
1535
1530
or
1536
1531
additionalJumpStateStep ( node1 , _, node2 , _, _)
1537
1532
or
@@ -2012,7 +2007,7 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
2012
2007
) and
2013
2008
isStoreStep = false
2014
2009
or
2015
- jumpStepEx ( mid .getNodeEx ( ) , node ) and
2010
+ jumpStepEx1 ( mid .getNodeEx ( ) , node ) and
2016
2011
state = mid .getState ( ) and
2017
2012
cc = callContextNone ( ) and
2018
2013
sc1 = TSummaryCtx1None ( ) and
@@ -2023,7 +2018,7 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
2023
2018
ap = mid .getAp ( ) and
2024
2019
isStoreStep = false
2025
2020
or
2026
- additionalJumpStep ( mid .getNodeEx ( ) , node , _) and
2021
+ additionalJumpStep1 ( mid .getNodeEx ( ) , node , _) and
2027
2022
state = mid .getState ( ) and
2028
2023
cc = callContextNone ( ) and
2029
2024
sc1 = TSummaryCtx1None ( ) and
@@ -2314,15 +2309,15 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
2314
2309
ap = TPartialNil ( ) and
2315
2310
isStoreStep = false
2316
2311
or
2317
- jumpStepEx ( node , mid .getNodeEx ( ) ) and
2312
+ jumpStepEx1 ( node , mid .getNodeEx ( ) ) and
2318
2313
state = mid .getState ( ) and
2319
2314
sc1 = TRevSummaryCtx1None ( ) and
2320
2315
sc2 = TRevSummaryCtx2None ( ) and
2321
2316
sc3 = TRevSummaryCtx3None ( ) and
2322
2317
ap = mid .getAp ( ) and
2323
2318
isStoreStep = false
2324
2319
or
2325
- additionalJumpStep ( node , mid .getNodeEx ( ) , _) and
2320
+ additionalJumpStep1 ( node , mid .getNodeEx ( ) , _) and
2326
2321
state = mid .getState ( ) and
2327
2322
sc1 = TRevSummaryCtx1None ( ) and
2328
2323
sc2 = TRevSummaryCtx2None ( ) and
0 commit comments