@@ -470,10 +470,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
470
470
private module Stage1 {
471
471
private import Stage1Common
472
472
473
- class Ap = Unit ;
474
-
475
- class ApNil = Ap ;
476
-
477
473
private class Cc = boolean ;
478
474
479
475
/* Begin: Stage 1 logic. */
@@ -954,14 +950,6 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
954
950
c = ret .getEnclosingCallable ( )
955
951
}
956
952
957
- predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
958
- callEdgeArgParam ( call , c , _, _, _)
959
- }
960
-
961
- predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
962
- callEdgeReturn ( call , c , _, _, _, _)
963
- }
964
-
965
953
predicate stats (
966
954
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges
967
955
) {
@@ -991,6 +979,10 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
991
979
private module Stage1Common {
992
980
predicate isRelevantSourceSinkPair = SourceSinkFiltering:: isRelevantSourceSinkPair / 2 ;
993
981
982
+ class Ap = Unit ;
983
+
984
+ class ApNil = Ap ;
985
+
994
986
predicate hasSourceCallCtx ( ) {
995
987
exists ( FlowFeature feature | feature = Config:: getAFeature ( ) |
996
988
feature instanceof FeatureHasSourceCallContext or
@@ -1004,6 +996,20 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1004
996
feature instanceof FeatureEqualSourceSinkCallContext
1005
997
)
1006
998
}
999
+
1000
+ predicate revFlowIsReadAndStored = Stage1:: revFlowIsReadAndStored / 1 ;
1001
+
1002
+ predicate callMayFlowThroughRev = Stage1:: callMayFlowThroughRev / 1 ;
1003
+
1004
+ predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
1005
+ Stage1:: callEdgeArgParam ( call , c , _, _, _)
1006
+ }
1007
+
1008
+ predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
1009
+ Stage1:: callEdgeReturn ( call , c , _, _, _, _)
1010
+ }
1011
+
1012
+ predicate stats = Stage1:: stats / 7 ;
1007
1013
}
1008
1014
1009
1015
pragma [ nomagic]
@@ -1294,6 +1300,235 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
1294
1300
predicate localStateStepNodeCand1 = localStateStepNodeCand1Alias / 7 ;
1295
1301
}
1296
1302
1303
+ // TODO: implements Stage1Output<FlowState>
1304
+ module Stage1WithState {
1305
+ private predicate flowState ( NodeEx node , FlowState state ) {
1306
+ Stage1:: revFlow ( node ) and
1307
+ Stage1:: revFlowState ( state ) and
1308
+ not stateBarrier ( node , state ) and
1309
+ (
1310
+ sourceNode ( node , state )
1311
+ or
1312
+ exists ( NodeEx mid , FlowState state0 | flowState ( mid , state0 ) |
1313
+ additionalLocalStateStep ( mid , state0 , node , state , _) or
1314
+ additionalJumpStateStep ( mid , state0 , node , state , _)
1315
+ )
1316
+ or
1317
+ exists ( NodeEx mid | flowState ( mid , state ) |
1318
+ localFlowStepEx ( mid , node , _) or
1319
+ additionalLocalFlowStep ( mid , node , _) or
1320
+ jumpStepExAlias ( mid , node ) or
1321
+ additionalJumpStepAlias ( mid , node , _) or
1322
+ store ( mid , _, node , _, _) or
1323
+ readSetEx ( mid , _, node ) or
1324
+ flowIntoCallNodeCand1 ( _, mid , node ) or
1325
+ flowOutOfCallNodeCand1 ( _, mid , _, node )
1326
+ )
1327
+ )
1328
+ }
1329
+
1330
+ private newtype TNd = TNodeState ( NodeEx node , FlowState state ) { flowState ( node , state ) }
1331
+
1332
+ class Nd extends TNd {
1333
+ NodeEx node ;
1334
+
1335
+ Nd ( ) { this = TNodeState ( node , _) }
1336
+
1337
+ NodeEx getNodeEx ( ) { result = node }
1338
+
1339
+ FlowState getState ( ) { this = TNodeState ( _, result ) }
1340
+
1341
+ string toString ( ) { result = node .toString ( ) }
1342
+
1343
+ Location getLocation ( ) { result = node .getLocation ( ) }
1344
+
1345
+ DataFlowType getDataFlowType ( ) { result = node .getDataFlowType ( ) }
1346
+
1347
+ DataFlowCallable getEnclosingCallable ( ) { result = node .getEnclosingCallable ( ) }
1348
+ }
1349
+
1350
+ class ArgNd extends Nd {
1351
+ ArgNd ( ) { node instanceof ArgNodeEx }
1352
+ }
1353
+
1354
+ class ParamNd extends Nd {
1355
+ ParamNd ( ) { node instanceof ParamNodeEx }
1356
+ }
1357
+
1358
+ class RetNd extends Nd {
1359
+ override RetNodeEx node ;
1360
+
1361
+ ReturnPosition getReturnPosition ( ) { result = node .getReturnPosition ( ) }
1362
+
1363
+ ReturnKindExt getKind ( ) { result = node .getKind ( ) }
1364
+ }
1365
+
1366
+ class OutNd extends Nd {
1367
+ OutNd ( ) { node instanceof OutNodeEx }
1368
+ }
1369
+
1370
+ class CastingNd extends Nd {
1371
+ CastingNd ( ) { node instanceof CastingNodeEx }
1372
+ }
1373
+
1374
+ // inline to reduce fan-out via `getAReadContent`
1375
+ bindingset [ c]
1376
+ predicate expectsContentEx ( Nd n , Content c ) {
1377
+ Stage1NoState:: expectsContentEx ( n .getNodeEx ( ) , c )
1378
+ }
1379
+
1380
+ pragma [ nomagic]
1381
+ predicate notExpectsContent ( Nd n ) { Stage1NoState:: notExpectsContent ( n .getNodeEx ( ) ) }
1382
+
1383
+ bindingset [ p, kind]
1384
+ pragma [ inline_late]
1385
+ predicate parameterFlowThroughAllowed ( ParamNd p , ReturnKindExt kind ) {
1386
+ parameterFlowThroughAllowedEx ( p .getNodeEx ( ) , kind )
1387
+ }
1388
+
1389
+ import Stage1Common
1390
+
1391
+ predicate revFlow ( Nd node ) { Stage1:: revFlow ( node .getNodeEx ( ) ) }
1392
+
1393
+ predicate revFlow ( Nd node , Ap ap ) { Stage1:: revFlow ( node .getNodeEx ( ) ) and exists ( ap ) }
1394
+
1395
+ predicate parameterMayFlowThrough ( ParamNd p , boolean emptyAp ) {
1396
+ Stage1:: parameterMayFlowThrough ( p .getNodeEx ( ) , emptyAp )
1397
+ }
1398
+
1399
+ predicate returnMayFlowThrough ( RetNd ret , ReturnKindExt kind ) {
1400
+ Stage1:: returnMayFlowThrough ( ret .getNodeEx ( ) , kind )
1401
+ }
1402
+
1403
+ pragma [ nomagic]
1404
+ predicate storeStepCand (
1405
+ Nd node1 , Content c , Nd node2 , DataFlowType contentType , DataFlowType containerType
1406
+ ) {
1407
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1408
+ Stage1:: storeStepCand ( n1 , c , n2 , contentType , containerType ) and
1409
+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1410
+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1411
+ not outBarrier ( n1 , s ) and
1412
+ not inBarrier ( n2 , s )
1413
+ )
1414
+ }
1415
+
1416
+ pragma [ nomagic]
1417
+ predicate readStepCand ( Nd node1 , Content c , Nd node2 ) {
1418
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1419
+ Stage1:: readStepCand ( n1 , c , n2 ) and
1420
+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1421
+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1422
+ not outBarrier ( n1 , s ) and
1423
+ not inBarrier ( n2 , s )
1424
+ )
1425
+ }
1426
+
1427
+ predicate callEdgeArgParam (
1428
+ DataFlowCall call , DataFlowCallable c , ArgNd arg , ParamNd p , boolean emptyAp
1429
+ ) {
1430
+ exists ( ArgNodeEx arg0 , ParamNodeEx p0 , FlowState s |
1431
+ Stage1:: callEdgeArgParam ( call , c , arg0 , p0 , emptyAp ) and
1432
+ arg = TNodeState ( arg0 , pragma [ only_bind_into ] ( s ) ) and
1433
+ p = TNodeState ( p0 , pragma [ only_bind_into ] ( s ) ) and
1434
+ not outBarrier ( arg0 , s ) and
1435
+ not inBarrier ( p0 , s )
1436
+ )
1437
+ }
1438
+
1439
+ predicate callEdgeReturn (
1440
+ DataFlowCall call , DataFlowCallable c , RetNd ret , ReturnKindExt kind , Nd out ,
1441
+ boolean allowsFieldFlow
1442
+ ) {
1443
+ exists ( RetNodeEx ret0 , NodeEx out0 , FlowState s |
1444
+ Stage1:: callEdgeReturn ( call , c , ret0 , kind , out0 , allowsFieldFlow ) and
1445
+ ret = TNodeState ( ret0 , pragma [ only_bind_into ] ( s ) ) and
1446
+ out = TNodeState ( out0 , pragma [ only_bind_into ] ( s ) ) and
1447
+ not outBarrier ( ret0 , s ) and
1448
+ not inBarrier ( out0 , s )
1449
+ )
1450
+ }
1451
+
1452
+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
1453
+ Nd toNormalSinkNode ( Nd node ) {
1454
+ exists ( NodeEx res , NodeEx n , FlowState s |
1455
+ res = toNormalSinkNodeEx ( n ) and
1456
+ node = TNodeState ( n , pragma [ only_bind_into ] ( s ) ) and
1457
+ result = TNodeState ( res , pragma [ only_bind_into ] ( s ) )
1458
+ )
1459
+ }
1460
+
1461
+ predicate sourceNode ( Nd node ) {
1462
+ exists ( NodeEx n , FlowState state |
1463
+ sourceNode ( n , state ) and
1464
+ node = TNodeState ( n , state )
1465
+ )
1466
+ }
1467
+
1468
+ predicate sinkNode ( Nd node ) {
1469
+ exists ( NodeEx n , FlowState state |
1470
+ Stage1:: sinkNode ( n , state ) and
1471
+ node = TNodeState ( n , state )
1472
+ )
1473
+ }
1474
+
1475
+ predicate jumpStepEx ( Nd node1 , Nd node2 ) {
1476
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1477
+ jumpStepExAlias ( n1 , n2 ) and
1478
+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1479
+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1480
+ not outBarrier ( n1 , s ) and
1481
+ not inBarrier ( n2 , s )
1482
+ )
1483
+ }
1484
+
1485
+ predicate additionalJumpStep ( Nd node1 , Nd node2 , string model ) {
1486
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1487
+ additionalJumpStepAlias ( n1 , n2 , model ) and
1488
+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1489
+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1490
+ not outBarrier ( n1 , s ) and
1491
+ not inBarrier ( n2 , s )
1492
+ )
1493
+ or
1494
+ exists ( NodeEx n1 , FlowState s1 , NodeEx n2 , FlowState s2 |
1495
+ additionalJumpStateStep ( n1 , s1 , n2 , s2 , model ) and
1496
+ node1 = TNodeState ( n1 , s1 ) and
1497
+ node2 = TNodeState ( n2 , s2 )
1498
+ )
1499
+ }
1500
+
1501
+ pragma [ nomagic]
1502
+ predicate localStep1 (
1503
+ Nd node1 , Nd node2 , boolean preservesValue , DataFlowType t , LocalCallContext lcc ,
1504
+ string label
1505
+ ) {
1506
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s |
1507
+ localStepNodeCand1 ( n1 , n2 , preservesValue , t , lcc , label ) and
1508
+ node1 = TNodeState ( n1 , pragma [ only_bind_into ] ( s ) ) and
1509
+ node2 = TNodeState ( n2 , pragma [ only_bind_into ] ( s ) ) and
1510
+ not outBarrier ( n1 , s ) and
1511
+ not inBarrier ( n2 , s )
1512
+ )
1513
+ or
1514
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s1 , FlowState s2 |
1515
+ localStateStepNodeCand1 ( n1 , s1 , n2 , s2 , t , lcc , label ) and
1516
+ preservesValue = false and
1517
+ node1 = TNodeState ( n1 , s1 ) and
1518
+ node2 = TNodeState ( n2 , s2 )
1519
+ )
1520
+ }
1521
+
1522
+ predicate isStateStep ( Nd node1 , Nd node2 ) {
1523
+ exists ( NodeEx n1 , NodeEx n2 , FlowState s1 , FlowState s2 |
1524
+ localStateStepNodeCand1 ( n1 , s1 , n2 , s2 , _, _, _) and
1525
+ s1 != s2 and
1526
+ node1 = TNodeState ( n1 , s1 ) and
1527
+ node2 = TNodeState ( n2 , s2 )
1528
+ )
1529
+ }
1530
+ }
1531
+
1297
1532
private signature predicate flag ( ) ;
1298
1533
1299
1534
private predicate flagEnable ( ) { any ( ) }
0 commit comments