@@ -1327,8 +1327,8 @@ private module MkStage<StageSig PrevStage> {
1327
1327
*/
1328
1328
pragma [ nomagic]
1329
1329
additional predicate fwdFlow (
1330
- NodeEx node , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1331
- Ap ap , ApApprox apa , Configuration config
1330
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap ,
1331
+ ApApprox apa , Configuration config
1332
1332
) {
1333
1333
fwdFlow0 ( node , state , cc , summaryCtx , argAp , ap , apa , config ) and
1334
1334
PrevStage:: revFlow ( node , state , apa , config ) and
@@ -1337,21 +1337,21 @@ private module MkStage<StageSig PrevStage> {
1337
1337
1338
1338
pragma [ inline]
1339
1339
additional predicate fwdFlow (
1340
- NodeEx node , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1341
- Ap ap , Configuration config
1340
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap ,
1341
+ Configuration config
1342
1342
) {
1343
1343
fwdFlow ( node , state , cc , summaryCtx , argAp , ap , _, config )
1344
1344
}
1345
1345
1346
1346
pragma [ nomagic]
1347
1347
private predicate fwdFlow0 (
1348
- NodeEx node , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1349
- Ap ap , ApApprox apa , Configuration config
1348
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap ,
1349
+ ApApprox apa , Configuration config
1350
1350
) {
1351
1351
sourceNode ( node , state , config ) and
1352
1352
( if hasSourceCallCtx ( config ) then cc = ccSomeCall ( ) else cc = ccNone ( ) ) and
1353
1353
argAp = apNone ( ) and
1354
- summaryCtx = TParameterPositionNone ( ) and
1354
+ summaryCtx = TParamNodeNone ( ) and
1355
1355
ap = getApNil ( node ) and
1356
1356
apa = getApprox ( ap )
1357
1357
or
@@ -1372,15 +1372,15 @@ private module MkStage<StageSig PrevStage> {
1372
1372
fwdFlow ( mid , pragma [ only_bind_into ] ( state ) , _, _, _, ap , apa , pragma [ only_bind_into ] ( config ) ) and
1373
1373
jumpStep ( mid , node , config ) and
1374
1374
cc = ccNone ( ) and
1375
- summaryCtx = TParameterPositionNone ( ) and
1375
+ summaryCtx = TParamNodeNone ( ) and
1376
1376
argAp = apNone ( )
1377
1377
)
1378
1378
or
1379
1379
exists ( NodeEx mid , ApNil nil |
1380
1380
fwdFlow ( mid , state , _, _, _, nil , pragma [ only_bind_into ] ( config ) ) and
1381
1381
additionalJumpStep ( mid , node , config ) and
1382
1382
cc = ccNone ( ) and
1383
- summaryCtx = TParameterPositionNone ( ) and
1383
+ summaryCtx = TParamNodeNone ( ) and
1384
1384
argAp = apNone ( ) and
1385
1385
ap = getApNil ( node ) and
1386
1386
apa = getApprox ( ap )
@@ -1390,7 +1390,7 @@ private module MkStage<StageSig PrevStage> {
1390
1390
fwdFlow ( mid , state0 , _, _, _, nil , pragma [ only_bind_into ] ( config ) ) and
1391
1391
additionalJumpStateStep ( mid , state0 , node , state , config ) and
1392
1392
cc = ccNone ( ) and
1393
- summaryCtx = TParameterPositionNone ( ) and
1393
+ summaryCtx = TParamNodeNone ( ) and
1394
1394
argAp = apNone ( ) and
1395
1395
ap = getApNil ( node ) and
1396
1396
apa = getApprox ( ap )
@@ -1414,10 +1414,10 @@ private module MkStage<StageSig PrevStage> {
1414
1414
fwdFlowIn ( _, node , state , _, cc , _, _, ap , apa , config ) and
1415
1415
if PrevStage:: parameterMayFlowThrough ( node , apa , config )
1416
1416
then (
1417
- summaryCtx = TParameterPositionSome ( node .( ParamNodeEx ) . getPosition ( ) ) and
1417
+ summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
1418
1418
argAp = apSome ( ap )
1419
1419
) else (
1420
- summaryCtx = TParameterPositionNone ( ) and argAp = apNone ( )
1420
+ summaryCtx = TParamNodeNone ( ) and argAp = apNone ( )
1421
1421
)
1422
1422
or
1423
1423
// flow out of a callable
@@ -1433,7 +1433,7 @@ private module MkStage<StageSig PrevStage> {
1433
1433
)
1434
1434
or
1435
1435
// flow through a callable
1436
- exists ( DataFlowCall call , ParameterPosition summaryCtx0 , Ap argAp0 |
1436
+ exists ( DataFlowCall call , ParamNodeEx summaryCtx0 , Ap argAp0 |
1437
1437
fwdFlowOutFromArg ( call , node , state , summaryCtx0 , argAp0 , ap , apa , config ) and
1438
1438
fwdFlowIsEntered ( call , cc , summaryCtx , argAp , summaryCtx0 , argAp0 , config )
1439
1439
)
@@ -1442,7 +1442,7 @@ private module MkStage<StageSig PrevStage> {
1442
1442
pragma [ nomagic]
1443
1443
private predicate fwdFlowStore (
1444
1444
NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , FlowState state , Cc cc ,
1445
- ParameterPositionOption summaryCtx , ApOption argAp , Configuration config
1445
+ ParamNodeOption summaryCtx , ApOption argAp , Configuration config
1446
1446
) {
1447
1447
exists ( DataFlowType contentType , ApApprox apa1 |
1448
1448
fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap1 , apa1 , config ) and
@@ -1473,8 +1473,8 @@ private module MkStage<StageSig PrevStage> {
1473
1473
1474
1474
pragma [ nomagic]
1475
1475
private predicate fwdFlowRead0 (
1476
- NodeEx node1 , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1477
- ApNonNil ap , Configuration config
1476
+ NodeEx node1 , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , ApNonNil ap ,
1477
+ Configuration config
1478
1478
) {
1479
1479
fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1480
1480
PrevStage:: readStepCand ( node1 , _, _, config )
@@ -1483,7 +1483,7 @@ private module MkStage<StageSig PrevStage> {
1483
1483
pragma [ nomagic]
1484
1484
private predicate fwdFlowRead (
1485
1485
Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
1486
- ParameterPositionOption summaryCtx , ApOption argAp , Configuration config
1486
+ ParamNodeOption summaryCtx , ApOption argAp , Configuration config
1487
1487
) {
1488
1488
fwdFlowRead0 ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1489
1489
PrevStage:: readStepCand ( node1 , c , node2 , config ) and
@@ -1493,7 +1493,7 @@ private module MkStage<StageSig PrevStage> {
1493
1493
pragma [ nomagic]
1494
1494
private predicate fwdFlowIn (
1495
1495
DataFlowCall call , ParamNodeEx p , FlowState state , Cc outercc , CcCall innercc ,
1496
- ParameterPositionOption summaryCtx , ApOption argAp , Ap ap , ApApprox apa , Configuration config
1496
+ ParamNodeOption summaryCtx , ApOption argAp , Ap ap , ApApprox apa , Configuration config
1497
1497
) {
1498
1498
exists ( ArgNodeEx arg , boolean allowsFieldFlow |
1499
1499
fwdFlow ( arg , state , outercc , summaryCtx , argAp , ap , apa , config ) and
@@ -1505,23 +1505,22 @@ private module MkStage<StageSig PrevStage> {
1505
1505
1506
1506
pragma [ nomagic]
1507
1507
private predicate fwdFlowRetFromArg (
1508
- RetNodeEx ret , FlowState state , CcCall ccc , ParameterPosition summaryCtx , ParamNodeEx p ,
1509
- Ap argAp , ApApprox argApa , Ap ap , ApApprox apa , Configuration config
1508
+ RetNodeEx ret , FlowState state , CcCall ccc , ParamNodeEx summaryCtx , Ap argAp , ApApprox argApa ,
1509
+ Ap ap , ApApprox apa , Configuration config
1510
1510
) {
1511
- exists ( DataFlowCallable c , ReturnKindExt kind |
1511
+ exists ( ReturnKindExt kind |
1512
1512
fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc ,
1513
- TParameterPositionSome ( pragma [ only_bind_into ] ( summaryCtx ) ) , apSome ( argAp ) , ap , apa , config ) and
1513
+ TParamNodeSome ( pragma [ only_bind_into ] ( summaryCtx .asNode ( ) ) ) , apSome ( argAp ) , ap , apa ,
1514
+ config ) and
1514
1515
getApprox ( argAp ) = argApa and
1515
- c = ret .getEnclosingCallable ( ) and
1516
1516
kind = ret .getKind ( ) and
1517
- p .isParameterOf ( c , pragma [ only_bind_into ] ( summaryCtx ) ) and
1518
- parameterFlowThroughAllowed ( p , kind )
1517
+ parameterFlowThroughAllowed ( summaryCtx , kind )
1519
1518
)
1520
1519
}
1521
1520
1522
1521
pragma [ inline]
1523
1522
private predicate fwdFlowInMayFlowThrough (
1524
- DataFlowCall call , Cc cc , CcCall innerCc , ParameterPositionOption summaryCtx , ApOption argAp ,
1523
+ DataFlowCall call , Cc cc , CcCall innerCc , ParamNodeOption summaryCtx , ApOption argAp ,
1525
1524
ParamNodeEx param , Ap ap , ApApprox apa , Configuration config
1526
1525
) {
1527
1526
fwdFlowIn ( call , pragma [ only_bind_into ] ( param ) , _, cc , innerCc , summaryCtx , argAp , ap ,
@@ -1553,13 +1552,12 @@ private module MkStage<StageSig PrevStage> {
1553
1552
1554
1553
pragma [ nomagic]
1555
1554
private predicate fwdFlowOutFromArg (
1556
- DataFlowCall call , NodeEx out , FlowState state , ParameterPosition summaryCtx , Ap argAp , Ap ap ,
1555
+ DataFlowCall call , NodeEx out , FlowState state , ParamNodeEx summaryCtx , Ap argAp , Ap ap ,
1557
1556
ApApprox apa , Configuration config
1558
1557
) {
1559
1558
exists ( RetNodeEx ret , boolean allowsFieldFlow , CcCall ccc , ApApprox argApa |
1560
1559
fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) ,
1561
- summaryCtx , _, argAp , pragma [ only_bind_into ] ( argApa ) , ap , pragma [ only_bind_into ] ( apa ) ,
1562
- config ) and
1560
+ summaryCtx , argAp , pragma [ only_bind_into ] ( argApa ) , ap , pragma [ only_bind_into ] ( apa ) , config ) and
1563
1561
fwdFlowThroughOutOfCall ( call , ccc , ret , out , allowsFieldFlow , argApa , apa , config ) and
1564
1562
( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) )
1565
1563
)
@@ -1571,13 +1569,10 @@ private module MkStage<StageSig PrevStage> {
1571
1569
*/
1572
1570
pragma [ nomagic]
1573
1571
private predicate fwdFlowIsEntered (
1574
- DataFlowCall call , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1575
- ParameterPosition pos , Ap ap , Configuration config
1572
+ DataFlowCall call , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , ParamNodeEx p , Ap ap ,
1573
+ Configuration config
1576
1574
) {
1577
- exists ( ParamNodeEx param |
1578
- fwdFlowInMayFlowThrough ( call , cc , _, summaryCtx , argAp , param , ap , _, config ) and
1579
- pos = param .getPosition ( )
1580
- )
1575
+ fwdFlowInMayFlowThrough ( call , cc , _, summaryCtx , argAp , p , ap , _, config )
1581
1576
}
1582
1577
1583
1578
pragma [ nomagic]
@@ -1602,8 +1597,8 @@ private module MkStage<StageSig PrevStage> {
1602
1597
Ap ap , Configuration config
1603
1598
) {
1604
1599
exists ( boolean allowsFieldFlow , ApApprox argApa , ApApprox apa |
1605
- fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) , _ , p ,
1606
- argAp , pragma [ only_bind_into ] ( argApa ) , ap , pragma [ only_bind_into ] ( apa ) , config ) and
1600
+ fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) , p , argAp ,
1601
+ pragma [ only_bind_into ] ( argApa ) , ap , pragma [ only_bind_into ] ( apa ) , config ) and
1607
1602
kind = ret .getKind ( ) and
1608
1603
fwdFlowThroughOutOfCall ( _, ccc , ret , _, allowsFieldFlow , argApa , apa , config ) and
1609
1604
( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) )
@@ -1967,8 +1962,9 @@ private module MkStage<StageSig PrevStage> {
1967
1962
conscand = count ( TypedContent f0 , Ap ap | fwdConsCand ( f0 , ap , config ) ) and
1968
1963
states = count ( FlowState state | fwdFlow ( _, state , _, _, _, _, config ) ) and
1969
1964
tuples =
1970
- count ( NodeEx n , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1971
- Ap ap | fwdFlow ( n , state , cc , summaryCtx , argAp , ap , config ) )
1965
+ count ( NodeEx n , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap |
1966
+ fwdFlow ( n , state , cc , summaryCtx , argAp , ap , config )
1967
+ )
1972
1968
or
1973
1969
fwd = false and
1974
1970
nodes = count ( NodeEx node | revFlow ( node , _, _, _, _, config ) ) and
@@ -2823,13 +2819,12 @@ private Configuration unbindConf(Configuration conf) {
2823
2819
2824
2820
pragma [ nomagic]
2825
2821
private predicate nodeMayUseSummary0 (
2826
- NodeEx n , DataFlowCallable c , ParameterPosition pos , FlowState state , AccessPathApprox apa ,
2827
- Configuration config
2822
+ NodeEx n , ParamNodeEx p , FlowState state , AccessPathApprox apa , Configuration config
2828
2823
) {
2829
2824
exists ( AccessPathApprox apa0 |
2830
- c = n . getEnclosingCallable ( ) and
2825
+ Stage5 :: parameterMayFlowThrough ( p , _ , _ ) and
2831
2826
Stage5:: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 , config ) and
2832
- Stage5:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParameterPositionSome ( pos ) ,
2827
+ Stage5:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParamNodeSome ( p . asNode ( ) ) ,
2833
2828
TAccessPathApproxSome ( apa ) , apa0 , config )
2834
2829
)
2835
2830
}
@@ -2838,10 +2833,9 @@ pragma[nomagic]
2838
2833
private predicate nodeMayUseSummary (
2839
2834
NodeEx n , FlowState state , AccessPathApprox apa , Configuration config
2840
2835
) {
2841
- exists ( DataFlowCallable c , ParameterPosition pos , ParamNodeEx p |
2836
+ exists ( ParamNodeEx p |
2842
2837
Stage5:: parameterMayFlowThrough ( p , apa , config ) and
2843
- nodeMayUseSummary0 ( n , c , pos , state , apa , config ) and
2844
- p .isParameterOf ( c , pos )
2838
+ nodeMayUseSummary0 ( n , p , state , apa , config )
2845
2839
)
2846
2840
}
2847
2841
0 commit comments