@@ -613,11 +613,28 @@ private predicate hasSinkCallCtx(Configuration config) {
613
613
* explicitly allowed
614
614
*/
615
615
bindingset [ p, kind]
616
- private predicate parameterFlowThroughAllowed ( ParamNode p , ReturnKindExt kind ) {
616
+ private predicate parameterFlowThroughAllowed ( ParamNodeEx p , ReturnKindExt kind ) {
617
617
exists ( ParameterPosition pos | p .isParameterOf ( _, pos ) |
618
618
not kind .( ParamUpdateReturnKind ) .getPosition ( ) = pos
619
619
or
620
- allowParameterReturnInSelfCached ( p )
620
+ allowParameterReturnInSelfCached ( p .asNode ( ) )
621
+ )
622
+ }
623
+
624
+ /**
625
+ * Holds if flow from a parameter at position `pos` inside `c` to a return node of
626
+ * kind `kind` is allowed.
627
+ *
628
+ * We don't expect a parameter to return stored in itself, unless
629
+ * explicitly allowed
630
+ */
631
+ bindingset [ c, pos, kind]
632
+ private predicate parameterFlowThroughAllowed (
633
+ DataFlowCallable c , ParameterPosition pos , ReturnKindExt kind
634
+ ) {
635
+ exists ( ParamNodeEx p |
636
+ p .isParameterOf ( c , pos ) and
637
+ parameterFlowThroughAllowed ( p , kind )
621
638
)
622
639
}
623
640
@@ -1000,7 +1017,7 @@ private module Stage1 implements StageSig {
1000
1017
returnFlowCallableNodeCand ( c , kind , config ) and
1001
1018
p .getEnclosingCallable ( ) = c and
1002
1019
exists ( ap ) and
1003
- parameterFlowThroughAllowed ( p . asNode ( ) , kind )
1020
+ parameterFlowThroughAllowed ( p , kind )
1004
1021
)
1005
1022
}
1006
1023
@@ -1102,6 +1119,7 @@ private predicate flowIntoCallNodeCand1(
1102
1119
* edge in the graph of paths between sources and sinks that ignores call
1103
1120
* contexts.
1104
1121
*/
1122
+ pragma [ nomagic]
1105
1123
private int branch ( NodeEx n1 , Configuration conf ) {
1106
1124
result =
1107
1125
strictcount ( NodeEx n |
@@ -1114,6 +1132,7 @@ private int branch(NodeEx n1, Configuration conf) {
1114
1132
* edge in the graph of paths between sources and sinks that ignores call
1115
1133
* contexts.
1116
1134
*/
1135
+ pragma [ nomagic]
1117
1136
private int join ( NodeEx n2 , Configuration conf ) {
1118
1137
result =
1119
1138
strictcount ( NodeEx n |
@@ -1152,10 +1171,10 @@ pragma[nomagic]
1152
1171
private predicate flowIntoCallNodeCand1 (
1153
1172
DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Configuration config
1154
1173
) {
1155
- flowIntoCallNodeCand1 ( call , arg , p , config ) and
1174
+ flowIntoCallNodeCand1 ( call , arg , p , pragma [ only_bind_into ] ( config ) ) and
1156
1175
exists ( int b , int j |
1157
- b = branch ( arg , config ) and
1158
- j = join ( p , config ) and
1176
+ b = branch ( arg , pragma [ only_bind_into ] ( config ) ) and
1177
+ j = join ( p , pragma [ only_bind_into ] ( config ) ) and
1159
1178
if b .minimum ( j ) <= config .fieldFlowBranchLimit ( )
1160
1179
then allowsFieldFlow = true
1161
1180
else allowsFieldFlow = false
@@ -1266,15 +1285,16 @@ private module MkStage<StageSig PrevStage> {
1266
1285
1267
1286
pragma [ nomagic]
1268
1287
private predicate flowThroughOutOfCall (
1269
- DataFlowCall call , CcCall ccc , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1270
- boolean allowsFieldFlow , Configuration config
1288
+ DataFlowCall call , DataFlowCallable c , CcCall ccc , RetNodeEx ret , ReturnKindExt kind ,
1289
+ NodeEx out , boolean allowsFieldFlow , Configuration config
1271
1290
) {
1272
1291
exists ( ReturnPosition pos |
1273
1292
flowOutOfCall ( call , ret , pos , out , allowsFieldFlow , pragma [ only_bind_into ] ( config ) ) and
1274
1293
kind = pos .getKind ( ) and
1275
1294
PrevStage:: callMayFlowThroughRev ( call , pragma [ only_bind_into ] ( config ) ) and
1276
1295
PrevStage:: returnMayFlowThrough ( ret , pos , pragma [ only_bind_into ] ( config ) ) and
1277
- matchesCall ( ccc , call )
1296
+ matchesCall ( ccc , call ) and
1297
+ c = ret .getEnclosingCallable ( )
1278
1298
)
1279
1299
}
1280
1300
@@ -1284,12 +1304,12 @@ private module MkStage<StageSig PrevStage> {
1284
1304
*
1285
1305
* The call context `cc` records whether the node is reached through an
1286
1306
* argument in a call, and if so, `summaryCtx` and `argAp` record the
1287
- * corresponding parameter and access path of that argument, respectively.
1307
+ * corresponding parameter position and access path of that argument, respectively.
1288
1308
*/
1289
1309
pragma [ nomagic]
1290
1310
additional predicate fwdFlow (
1291
- NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap ,
1292
- Configuration config
1311
+ NodeEx node , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1312
+ Ap ap , Configuration config
1293
1313
) {
1294
1314
fwdFlow0 ( node , state , cc , summaryCtx , argAp , ap , config ) and
1295
1315
PrevStage:: revFlow ( node , state , unbindApa ( getApprox ( ap ) ) , config ) and
@@ -1298,13 +1318,13 @@ private module MkStage<StageSig PrevStage> {
1298
1318
1299
1319
pragma [ nomagic]
1300
1320
private predicate fwdFlow0 (
1301
- NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap ,
1302
- Configuration config
1321
+ NodeEx node , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1322
+ Ap ap , Configuration config
1303
1323
) {
1304
1324
sourceNode ( node , state , config ) and
1305
1325
( if hasSourceCallCtx ( config ) then cc = ccSomeCall ( ) else cc = ccNone ( ) ) and
1306
1326
argAp = apNone ( ) and
1307
- summaryCtx = TParamNodeNone ( ) and
1327
+ summaryCtx = TParameterPositionNone ( ) and
1308
1328
ap = getApNil ( node )
1309
1329
or
1310
1330
exists ( NodeEx mid , FlowState state0 , Ap ap0 , LocalCc localCc |
@@ -1322,15 +1342,15 @@ private module MkStage<StageSig PrevStage> {
1322
1342
fwdFlow ( mid , pragma [ only_bind_into ] ( state ) , _, _, _, ap , pragma [ only_bind_into ] ( config ) ) and
1323
1343
jumpStep ( mid , node , config ) and
1324
1344
cc = ccNone ( ) and
1325
- summaryCtx = TParamNodeNone ( ) and
1345
+ summaryCtx = TParameterPositionNone ( ) and
1326
1346
argAp = apNone ( )
1327
1347
)
1328
1348
or
1329
1349
exists ( NodeEx mid , ApNil nil |
1330
1350
fwdFlow ( mid , state , _, _, _, nil , pragma [ only_bind_into ] ( config ) ) and
1331
1351
additionalJumpStep ( mid , node , config ) and
1332
1352
cc = ccNone ( ) and
1333
- summaryCtx = TParamNodeNone ( ) and
1353
+ summaryCtx = TParameterPositionNone ( ) and
1334
1354
argAp = apNone ( ) and
1335
1355
ap = getApNil ( node )
1336
1356
)
@@ -1339,7 +1359,7 @@ private module MkStage<StageSig PrevStage> {
1339
1359
fwdFlow ( mid , state0 , _, _, _, nil , pragma [ only_bind_into ] ( config ) ) and
1340
1360
additionalJumpStateStep ( mid , state0 , node , state , config ) and
1341
1361
cc = ccNone ( ) and
1342
- summaryCtx = TParamNodeNone ( ) and
1362
+ summaryCtx = TParameterPositionNone ( ) and
1343
1363
argAp = apNone ( ) and
1344
1364
ap = getApNil ( node )
1345
1365
)
@@ -1362,17 +1382,18 @@ private module MkStage<StageSig PrevStage> {
1362
1382
apa = getApprox ( ap ) and
1363
1383
if PrevStage:: parameterMayFlowThrough ( node , apa , config )
1364
1384
then (
1365
- summaryCtx = TParamNodeSome ( node .asNode ( ) ) and argAp = apSome ( ap )
1385
+ summaryCtx = TParameterPositionSome ( node .( ParamNodeEx ) .getPosition ( ) ) and
1386
+ argAp = apSome ( ap )
1366
1387
) else (
1367
- summaryCtx = TParamNodeNone ( ) and argAp = apNone ( )
1388
+ summaryCtx = TParameterPositionNone ( ) and argAp = apNone ( )
1368
1389
)
1369
1390
)
1370
1391
or
1371
1392
// flow out of a callable
1372
1393
fwdFlowOutNotFromArg ( node , state , cc , summaryCtx , argAp , ap , config )
1373
1394
or
1374
1395
// flow through a callable
1375
- exists ( DataFlowCall call , ParamNode summaryCtx0 , Ap argAp0 |
1396
+ exists ( DataFlowCall call , ParameterPosition summaryCtx0 , Ap argAp0 |
1376
1397
fwdFlowOutFromArg ( call , node , state , summaryCtx0 , argAp0 , ap , config ) and
1377
1398
fwdFlowIsEntered ( call , cc , summaryCtx , argAp , summaryCtx0 , argAp0 , config )
1378
1399
)
@@ -1381,7 +1402,7 @@ private module MkStage<StageSig PrevStage> {
1381
1402
pragma [ nomagic]
1382
1403
private predicate fwdFlowStore (
1383
1404
NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , FlowState state , Cc cc ,
1384
- ParamNodeOption summaryCtx , ApOption argAp , Configuration config
1405
+ ParameterPositionOption summaryCtx , ApOption argAp , Configuration config
1385
1406
) {
1386
1407
exists ( DataFlowType contentType |
1387
1408
fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap1 , config ) and
@@ -1406,7 +1427,7 @@ private module MkStage<StageSig PrevStage> {
1406
1427
pragma [ nomagic]
1407
1428
private predicate fwdFlowRead (
1408
1429
Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
1409
- ParamNodeOption summaryCtx , ApOption argAp , Configuration config
1430
+ ParameterPositionOption summaryCtx , ApOption argAp , Configuration config
1410
1431
) {
1411
1432
fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1412
1433
PrevStage:: readStepCand ( node1 , c , node2 , config ) and
@@ -1416,7 +1437,7 @@ private module MkStage<StageSig PrevStage> {
1416
1437
pragma [ nomagic]
1417
1438
private predicate fwdFlowIn (
1418
1439
DataFlowCall call , ParamNodeEx p , FlowState state , Cc outercc , Cc innercc ,
1419
- ParamNodeOption summaryCtx , ApOption argAp , Ap ap , Configuration config
1440
+ ParameterPositionOption summaryCtx , ApOption argAp , Ap ap , Configuration config
1420
1441
) {
1421
1442
exists ( ArgNodeEx arg , boolean allowsFieldFlow |
1422
1443
fwdFlow ( arg , state , outercc , summaryCtx , argAp , ap , config ) and
@@ -1428,8 +1449,8 @@ private module MkStage<StageSig PrevStage> {
1428
1449
1429
1450
pragma [ nomagic]
1430
1451
private predicate fwdFlowOutNotFromArg (
1431
- NodeEx out , FlowState state , Cc ccOut , ParamNodeOption summaryCtx , ApOption argAp , Ap ap ,
1432
- Configuration config
1452
+ NodeEx out , FlowState state , Cc ccOut , ParameterPositionOption summaryCtx , ApOption argAp ,
1453
+ Ap ap , Configuration config
1433
1454
) {
1434
1455
exists (
1435
1456
DataFlowCall call , RetNodeEx ret , boolean allowsFieldFlow , CcNoCall innercc ,
@@ -1445,14 +1466,18 @@ private module MkStage<StageSig PrevStage> {
1445
1466
1446
1467
pragma [ nomagic]
1447
1468
private predicate fwdFlowOutFromArg (
1448
- DataFlowCall call , NodeEx out , FlowState state , ParamNode summaryCtx , Ap argAp , Ap ap ,
1469
+ DataFlowCall call , NodeEx out , FlowState state , ParameterPosition summaryCtx , Ap argAp , Ap ap ,
1449
1470
Configuration config
1450
1471
) {
1451
- exists ( RetNodeEx ret , ReturnKindExt kind , boolean allowsFieldFlow , CcCall ccc |
1452
- fwdFlow ( ret , state , ccc , TParamNodeSome ( summaryCtx ) , apSome ( argAp ) , ap , config ) and
1453
- flowThroughOutOfCall ( call , ccc , ret , kind , out , allowsFieldFlow , config ) and
1472
+ exists (
1473
+ DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , boolean allowsFieldFlow , CcCall ccc
1474
+ |
1475
+ fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) ,
1476
+ TParameterPositionSome ( pragma [ only_bind_into ] ( summaryCtx ) ) , apSome ( argAp ) , ap , config ) and
1477
+ flowThroughOutOfCall ( call , pragma [ only_bind_into ] ( c ) , ccc , ret , kind , out , allowsFieldFlow ,
1478
+ config ) and
1454
1479
( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1455
- parameterFlowThroughAllowed ( summaryCtx , kind )
1480
+ parameterFlowThroughAllowed ( c , pragma [ only_bind_into ] ( summaryCtx ) , kind )
1456
1481
)
1457
1482
}
1458
1483
@@ -1462,13 +1487,13 @@ private module MkStage<StageSig PrevStage> {
1462
1487
*/
1463
1488
pragma [ nomagic]
1464
1489
private predicate fwdFlowIsEntered (
1465
- DataFlowCall call , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , ParamNode p , Ap ap ,
1466
- Configuration config
1490
+ DataFlowCall call , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1491
+ ParameterPosition pos , Ap ap , Configuration config
1467
1492
) {
1468
1493
exists ( ParamNodeEx param |
1469
1494
fwdFlowIn ( call , param , _, cc , _, summaryCtx , argAp , ap , config ) and
1470
1495
PrevStage:: parameterMayFlowThrough ( param , unbindApa ( getApprox ( ap ) ) , config ) and
1471
- p = param .asNode ( )
1496
+ pos = param .getPosition ( )
1472
1497
)
1473
1498
}
1474
1499
@@ -1488,14 +1513,30 @@ private module MkStage<StageSig PrevStage> {
1488
1513
fwdFlowConsCand ( ap1 , c , ap2 , config )
1489
1514
}
1490
1515
1516
+ pragma [ nomagic]
1517
+ private predicate returnFlowsThrough0 (
1518
+ RetNodeEx ret , FlowState state , CcCall ccc , DataFlowCallable c , ParameterPosition ppos ,
1519
+ Ap argAp , Ap ap , Configuration config
1520
+ ) {
1521
+ exists ( boolean allowsFieldFlow |
1522
+ fwdFlow ( ret , state , ccc , TParameterPositionSome ( ppos ) , apSome ( argAp ) , ap , config ) and
1523
+ flowThroughOutOfCall ( _, c , _, pragma [ only_bind_into ] ( ret ) , _, _, allowsFieldFlow ,
1524
+ pragma [ only_bind_into ] ( config ) ) and
1525
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1526
+ )
1527
+ }
1528
+
1491
1529
pragma [ nomagic]
1492
1530
private predicate returnFlowsThrough (
1493
- RetNodeEx ret , ReturnPosition pos , FlowState state , CcCall ccc , ParamNode p , Ap argAp , Ap ap ,
1494
- Configuration config
1531
+ RetNodeEx ret , ReturnPosition pos , FlowState state , CcCall ccc , ParamNodeEx p , Ap argAp ,
1532
+ Ap ap , Configuration config
1495
1533
) {
1496
- fwdFlow ( ret , state , ccc , TParamNodeSome ( p ) , apSome ( argAp ) , ap , config ) and
1497
- pos = ret .getReturnPosition ( ) and
1498
- parameterFlowThroughAllowed ( p , pos .getKind ( ) )
1534
+ exists ( DataFlowCallable c , ParameterPosition ppos |
1535
+ returnFlowsThrough0 ( ret , state , ccc , c , ppos , argAp , ap , config ) and
1536
+ p .isParameterOf ( c , ppos ) and
1537
+ pos = ret .getReturnPosition ( ) and
1538
+ parameterFlowThroughAllowed ( p , pos .getKind ( ) )
1539
+ )
1499
1540
}
1500
1541
1501
1542
pragma [ nomagic]
@@ -1506,7 +1547,7 @@ private module MkStage<StageSig PrevStage> {
1506
1547
flowIntoCall ( call , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) , allowsFieldFlow ,
1507
1548
pragma [ only_bind_into ] ( config ) ) and
1508
1549
fwdFlow ( arg , _, _, _, _, pragma [ only_bind_into ] ( argAp ) , pragma [ only_bind_into ] ( config ) ) and
1509
- returnFlowsThrough ( _, _, _, _, p . asNode ( ) , pragma [ only_bind_into ] ( argAp ) , _,
1550
+ returnFlowsThrough ( _, _, _, _, p , pragma [ only_bind_into ] ( argAp ) , _,
1510
1551
pragma [ only_bind_into ] ( config ) )
1511
1552
)
1512
1553
}
@@ -1671,7 +1712,7 @@ private module MkStage<StageSig PrevStage> {
1671
1712
revFlow ( p , state , TReturnCtxMaybeFlowThrough ( returnPos ) , apSome ( returnAp ) , ap , config ) and
1672
1713
flowThroughIntoCall ( call , arg , p , allowsFieldFlow , config ) and
1673
1714
( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1674
- parameterFlowThroughAllowed ( p . asNode ( ) , returnPos .getKind ( ) )
1715
+ parameterFlowThroughAllowed ( p , returnPos .getKind ( ) )
1675
1716
)
1676
1717
}
1677
1718
@@ -1763,21 +1804,21 @@ private module MkStage<StageSig PrevStage> {
1763
1804
ParamNodeEx p , Ap ap , ReturnPosition returnPos , Configuration config
1764
1805
) {
1765
1806
revFlow ( p , _, TReturnCtxMaybeFlowThrough ( returnPos ) , apSome ( _) , ap , config ) and
1766
- parameterFlowThroughAllowed ( p . asNode ( ) , returnPos .getKind ( ) )
1807
+ parameterFlowThroughAllowed ( p , returnPos .getKind ( ) )
1767
1808
}
1768
1809
1769
1810
pragma [ nomagic]
1770
1811
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) {
1771
1812
exists ( RetNodeEx ret , ReturnPosition pos |
1772
- returnFlowsThrough ( ret , pos , _, _, p . asNode ( ) , ap , _, config ) and
1813
+ returnFlowsThrough ( ret , pos , _, _, p , ap , _, config ) and
1773
1814
parameterFlowsThroughRev ( p , ap , pos , config )
1774
1815
)
1775
1816
}
1776
1817
1777
1818
pragma [ nomagic]
1778
1819
predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1779
1820
exists ( ParamNodeEx p , Ap ap |
1780
- returnFlowsThrough ( ret , pos , _, _, p . asNode ( ) , ap , _, config ) and
1821
+ returnFlowsThrough ( ret , pos , _, _, p , ap , _, config ) and
1781
1822
parameterFlowsThroughRev ( p , ap , pos , config )
1782
1823
)
1783
1824
}
@@ -1803,9 +1844,8 @@ private module MkStage<StageSig PrevStage> {
1803
1844
conscand = count ( TypedContent f0 , Ap ap | fwdConsCand ( f0 , ap , config ) ) and
1804
1845
states = count ( FlowState state | fwdFlow ( _, state , _, _, _, _, config ) ) and
1805
1846
tuples =
1806
- count ( NodeEx n , FlowState state , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , Ap ap |
1807
- fwdFlow ( n , state , cc , summaryCtx , argAp , ap , config )
1808
- )
1847
+ count ( NodeEx n , FlowState state , Cc cc , ParameterPositionOption summaryCtx , ApOption argAp ,
1848
+ Ap ap | fwdFlow ( n , state , cc , summaryCtx , argAp , ap , config ) )
1809
1849
or
1810
1850
fwd = false and
1811
1851
nodes = count ( NodeEx node | revFlow ( node , _, _, _, _, config ) ) and
@@ -2555,12 +2595,13 @@ private Configuration unbindConf(Configuration conf) {
2555
2595
2556
2596
pragma [ nomagic]
2557
2597
private predicate nodeMayUseSummary0 (
2558
- NodeEx n , ParamNodeEx p , FlowState state , AccessPathApprox apa , Configuration config
2598
+ NodeEx n , DataFlowCallable c , ParameterPosition pos , FlowState state , AccessPathApprox apa ,
2599
+ Configuration config
2559
2600
) {
2560
2601
exists ( AccessPathApprox apa0 |
2561
- Stage4 :: parameterMayFlowThrough ( p , _ , _ ) and
2602
+ c = n . getEnclosingCallable ( ) and
2562
2603
Stage4:: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 , config ) and
2563
- Stage4:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParamNodeSome ( p . asNode ( ) ) ,
2604
+ Stage4:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParameterPositionSome ( pos ) ,
2564
2605
TAccessPathApproxSome ( apa ) , apa0 , config )
2565
2606
)
2566
2607
}
@@ -2569,9 +2610,10 @@ pragma[nomagic]
2569
2610
private predicate nodeMayUseSummary (
2570
2611
NodeEx n , FlowState state , AccessPathApprox apa , Configuration config
2571
2612
) {
2572
- exists ( ParamNodeEx p |
2613
+ exists ( DataFlowCallable c , ParameterPosition pos , ParamNodeEx p |
2573
2614
Stage4:: parameterMayFlowThrough ( p , apa , config ) and
2574
- nodeMayUseSummary0 ( n , p , state , apa , config )
2615
+ nodeMayUseSummary0 ( n , c , pos , state , apa , config ) and
2616
+ p .isParameterOf ( c , pos )
2575
2617
)
2576
2618
}
2577
2619
@@ -3504,7 +3546,7 @@ private predicate paramFlowsThrough(
3504
3546
pathNode ( mid , ret , state , cc , sc , ap , config , _) and
3505
3547
kind = ret .getKind ( ) and
3506
3548
apa = ap .getApprox ( ) and
3507
- parameterFlowThroughAllowed ( sc .getParamNode ( ) . asNode ( ) , kind )
3549
+ parameterFlowThroughAllowed ( sc .getParamNode ( ) , kind )
3508
3550
)
3509
3551
}
3510
3552
0 commit comments