@@ -190,6 +190,8 @@ module MakeImpl<InputSig Lang> {
190
190
191
191
private class ArgNodeEx extends NodeEx {
192
192
ArgNodeEx ( ) { this .asNode ( ) instanceof ArgNode }
193
+
194
+ DataFlowCall getCall ( ) { this .asNode ( ) .( ArgNode ) .argumentOf ( result , _) }
193
195
}
194
196
195
197
private class ParamNodeEx extends NodeEx {
@@ -1145,11 +1147,20 @@ module MakeImpl<InputSig Lang> {
1145
1147
1146
1148
class LocalCc ;
1147
1149
1148
- bindingset [ call, c, outercc]
1149
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) ;
1150
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) ;
1151
+
1152
+ bindingset [ call, ctx]
1153
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) ;
1154
+
1155
+ bindingset [ call, c]
1156
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) ;
1150
1157
1151
- bindingset [ call, c, innercc]
1152
- CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call , Cc innercc ) ;
1158
+ DataFlowCallable viableImplCallContextReducedReverse ( DataFlowCall call , CcNoCall ctx ) ;
1159
+
1160
+ predicate viableImplNotCallContextReducedReverse ( CcNoCall ctx ) ;
1161
+
1162
+ bindingset [ call, c]
1163
+ CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) ;
1153
1164
1154
1165
bindingset [ node, cc]
1155
1166
LocalCc getLocalCc ( NodeEx node , Cc cc ) ;
@@ -1191,21 +1202,24 @@ module MakeImpl<InputSig Lang> {
1191
1202
1192
1203
pragma [ nomagic]
1193
1204
private predicate flowIntoCallApa (
1194
- DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , ApApprox apa
1205
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1206
+ boolean allowsFieldFlow , ApApprox apa
1195
1207
) {
1196
1208
flowIntoCall ( call , arg , p , allowsFieldFlow ) and
1197
1209
PrevStage:: revFlowAp ( p , pragma [ only_bind_into ] ( apa ) ) and
1198
- PrevStage:: revFlowAp ( arg , pragma [ only_bind_into ] ( apa ) )
1210
+ PrevStage:: revFlowAp ( arg , pragma [ only_bind_into ] ( apa ) ) and
1211
+ c = p .getEnclosingCallable ( )
1199
1212
}
1200
1213
1201
1214
pragma [ nomagic]
1202
1215
private predicate flowOutOfCallApa (
1203
- DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
1204
- ApApprox apa
1216
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1217
+ boolean allowsFieldFlow , ApApprox apa
1205
1218
) {
1206
1219
flowOutOfCall ( call , ret , kind , out , allowsFieldFlow ) and
1207
1220
PrevStage:: revFlowAp ( out , pragma [ only_bind_into ] ( apa ) ) and
1208
- PrevStage:: revFlowAp ( ret , pragma [ only_bind_into ] ( apa ) )
1221
+ PrevStage:: revFlowAp ( ret , pragma [ only_bind_into ] ( apa ) ) and
1222
+ c = ret .getEnclosingCallable ( )
1209
1223
}
1210
1224
1211
1225
pragma [ nomagic]
@@ -1214,7 +1228,7 @@ module MakeImpl<InputSig Lang> {
1214
1228
ApApprox argApa , ApApprox apa
1215
1229
) {
1216
1230
exists ( ReturnKindExt kind |
1217
- flowOutOfCallApa ( call , ret , kind , out , allowsFieldFlow , apa ) and
1231
+ flowOutOfCallApa ( call , _ , ret , kind , out , allowsFieldFlow , apa ) and
1218
1232
PrevStage:: callMayFlowThroughRev ( call ) and
1219
1233
PrevStage:: returnMayFlowThrough ( ret , argApa , apa , kind ) and
1220
1234
matchesCall ( ccc , call )
@@ -1332,16 +1346,7 @@ module MakeImpl<InputSig Lang> {
1332
1346
)
1333
1347
or
1334
1348
// flow out of a callable
1335
- exists (
1336
- DataFlowCall call , RetNodeEx ret , boolean allowsFieldFlow , CcNoCall innercc ,
1337
- DataFlowCallable inner
1338
- |
1339
- fwdFlow ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
1340
- flowOutOfCallApa ( call , ret , _, node , allowsFieldFlow , apa ) and
1341
- inner = ret .getEnclosingCallable ( ) and
1342
- cc = getCallContextReturn ( inner , call , innercc ) and
1343
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1344
- )
1349
+ fwdFlowOut ( node , state , cc , summaryCtx , argT , argAp , t , ap , apa )
1345
1350
or
1346
1351
// flow through a callable
1347
1352
exists (
@@ -1408,15 +1413,115 @@ module MakeImpl<InputSig Lang> {
1408
1413
)
1409
1414
}
1410
1415
1416
+ bindingset [ call, ctx]
1417
+ pragma [ inline_late]
1418
+ private DataFlowCallable viableImplCallContextReducedInlineLate (
1419
+ DataFlowCall call , CcCall ctx
1420
+ ) {
1421
+ result = viableImplCallContextReduced ( call , ctx )
1422
+ }
1423
+
1424
+ bindingset [ arg, ctx]
1425
+ pragma [ inline_late]
1426
+ private DataFlowCallable viableImplCallContextReducedInlineLate (
1427
+ DataFlowCall call , ArgNodeEx arg , CcCall ctx
1428
+ ) {
1429
+ call = arg .getCall ( ) and
1430
+ result = viableImplCallContextReducedInlineLate ( call , ctx )
1431
+ }
1432
+
1433
+ bindingset [ call]
1434
+ pragma [ inline_late]
1435
+ private predicate flowIntoCallApaInlineLate (
1436
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1437
+ boolean allowsFieldFlow , ApApprox apa
1438
+ ) {
1439
+ flowIntoCallApa ( call , c , arg , p , allowsFieldFlow , apa )
1440
+ }
1441
+
1442
+ bindingset [ call, ctx]
1443
+ pragma [ inline_late]
1444
+ private predicate viableImplNotCallContextReducedInlineLate ( DataFlowCall call , Cc ctx ) {
1445
+ viableImplNotCallContextReduced ( call , ctx )
1446
+ }
1447
+
1448
+ bindingset [ arg, outercc]
1449
+ pragma [ inline_late]
1450
+ private predicate viableImplArgNotCallContextReduced (
1451
+ DataFlowCall call , ArgNodeEx arg , Cc outercc
1452
+ ) {
1453
+ call = arg .getCall ( ) and
1454
+ viableImplNotCallContextReducedInlineLate ( call , outercc )
1455
+ }
1456
+
1411
1457
pragma [ nomagic]
1412
1458
private predicate fwdFlowIn (
1413
1459
DataFlowCall call , ParamNodeEx p , FlowState state , Cc outercc , CcCall innercc ,
1414
1460
ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa
1415
1461
) {
1416
- exists ( ArgNodeEx arg , boolean allowsFieldFlow |
1462
+ exists ( ArgNodeEx arg , boolean allowsFieldFlow , DataFlowCallable inner |
1417
1463
fwdFlow ( arg , state , outercc , summaryCtx , argT , argAp , t , ap , apa ) and
1418
- flowIntoCallApa ( call , arg , p , allowsFieldFlow , apa ) and
1419
- innercc = getCallContextCall ( call , p .getEnclosingCallable ( ) , outercc ) and
1464
+ (
1465
+ inner = viableImplCallContextReducedInlineLate ( call , arg , outercc )
1466
+ or
1467
+ viableImplArgNotCallContextReduced ( call , arg , outercc )
1468
+ ) and
1469
+ flowIntoCallApaInlineLate ( call , inner , arg , p , allowsFieldFlow , apa )
1470
+ |
1471
+ innercc = getCallContextCall ( call , inner ) and
1472
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1473
+ )
1474
+ }
1475
+
1476
+ bindingset [ ctx, result ]
1477
+ pragma [ inline_late]
1478
+ private DataFlowCallable viableImplCallContextReducedReverseInlineLate (
1479
+ DataFlowCall call , CcNoCall ctx
1480
+ ) {
1481
+ result = viableImplCallContextReducedReverse ( call , ctx )
1482
+ }
1483
+
1484
+ bindingset [ call]
1485
+ pragma [ inline_late]
1486
+ private predicate flowOutOfCallApaInlineLate (
1487
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1488
+ ApApprox apa
1489
+ ) {
1490
+ flowOutOfCallApa ( call , c , ret , _, out , allowsFieldFlow , apa )
1491
+ }
1492
+
1493
+ bindingset [ c, ret, apa, innercc]
1494
+ pragma [ inline_late]
1495
+ pragma [ noopt]
1496
+ private predicate flowOutOfCallApaNotCallContextReduced (
1497
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1498
+ ApApprox apa , CcNoCall innercc
1499
+ ) {
1500
+ viableImplNotCallContextReducedReverse ( innercc ) and
1501
+ flowOutOfCallApa ( call , c , ret , _, out , allowsFieldFlow , apa )
1502
+ }
1503
+
1504
+ // inline to reduce number of iterations
1505
+ pragma [ inline]
1506
+ private predicate fwdFlowOut (
1507
+ NodeEx out , FlowState state , CcNoCall outercc , ParamNodeOption summaryCtx , TypOption argT ,
1508
+ ApOption argAp , Typ t , Ap ap , ApApprox apa
1509
+ ) {
1510
+ exists (
1511
+ DataFlowCall call , RetNodeEx ret , boolean allowsFieldFlow , CcNoCall innercc ,
1512
+ DataFlowCallable inner
1513
+ |
1514
+ fwdFlow ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
1515
+ inner = ret .getEnclosingCallable ( ) and
1516
+ (
1517
+ inner = viableImplCallContextReducedReverseInlineLate ( call , innercc ) and
1518
+ flowOutOfCallApaInlineLate ( call , inner , ret , out , allowsFieldFlow , apa )
1519
+ or
1520
+ flowOutOfCallApaNotCallContextReduced ( call , inner , ret , out , allowsFieldFlow , apa ,
1521
+ innercc )
1522
+ )
1523
+ |
1524
+ outercc = getCallContextReturn ( inner , call ) and
1420
1525
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1421
1526
)
1422
1527
}
@@ -1518,7 +1623,7 @@ module MakeImpl<InputSig Lang> {
1518
1623
DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Ap argAp , Ap ap
1519
1624
) {
1520
1625
exists ( ApApprox argApa , Typ argT |
1521
- flowIntoCallApa ( call , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) ,
1626
+ flowIntoCallApa ( call , _ , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) ,
1522
1627
allowsFieldFlow , argApa ) and
1523
1628
fwdFlow ( arg , _, _, _, _, _, pragma [ only_bind_into ] ( argT ) , pragma [ only_bind_into ] ( argAp ) ,
1524
1629
argApa ) and
@@ -1529,24 +1634,23 @@ module MakeImpl<InputSig Lang> {
1529
1634
}
1530
1635
1531
1636
pragma [ nomagic]
1532
- private predicate flowIntoCallAp (
1533
- DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Ap ap
1534
- ) {
1535
- exists ( ApApprox apa |
1536
- flowIntoCallApa ( call , arg , p , allowsFieldFlow , apa ) and
1537
- fwdFlow ( arg , _, _, _, _, _, _, ap , apa )
1637
+ private predicate flowIntoCallAp ( DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , Ap ap ) {
1638
+ exists ( ApApprox apa , boolean allowsFieldFlow |
1639
+ flowIntoCallApa ( call , _, arg , p , allowsFieldFlow , apa ) and
1640
+ fwdFlow ( arg , _, _, _, _, _, _, ap , apa ) and
1641
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1538
1642
)
1539
1643
}
1540
1644
1541
1645
pragma [ nomagic]
1542
1646
private predicate flowOutOfCallAp (
1543
- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1544
- Ap ap
1647
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , Ap ap
1545
1648
) {
1546
- exists ( ApApprox apa |
1547
- flowOutOfCallApa ( call , ret , _, out , allowsFieldFlow , apa ) and
1649
+ exists ( ApApprox apa , boolean allowsFieldFlow |
1650
+ flowOutOfCallApa ( call , _ , ret , _, out , allowsFieldFlow , apa ) and
1548
1651
fwdFlow ( ret , _, _, _, _, _, _, ap , apa ) and
1549
- pos = ret .getReturnPosition ( )
1652
+ pos = ret .getReturnPosition ( ) and
1653
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1550
1654
)
1551
1655
}
1552
1656
@@ -1627,10 +1731,9 @@ module MakeImpl<InputSig Lang> {
1627
1731
)
1628
1732
or
1629
1733
// flow into a callable
1630
- exists ( ParamNodeEx p , boolean allowsFieldFlow |
1734
+ exists ( ParamNodeEx p |
1631
1735
revFlow ( p , state , TReturnCtxNone ( ) , returnAp , ap ) and
1632
- flowIntoCallAp ( _, node , p , allowsFieldFlow , ap ) and
1633
- ( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1736
+ flowIntoCallAp ( _, node , p , ap ) and
1634
1737
returnCtx = TReturnCtxNone ( )
1635
1738
)
1636
1739
or
@@ -1680,10 +1783,9 @@ module MakeImpl<InputSig Lang> {
1680
1783
DataFlowCall call , RetNodeEx ret , ReturnPosition pos , FlowState state ,
1681
1784
ReturnCtx returnCtx , ApOption returnAp , Ap ap
1682
1785
) {
1683
- exists ( NodeEx out , boolean allowsFieldFlow |
1786
+ exists ( NodeEx out |
1684
1787
revFlow ( out , state , returnCtx , returnAp , ap ) and
1685
- flowOutOfCallAp ( call , ret , pos , out , allowsFieldFlow , ap ) and
1686
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1788
+ flowOutOfCallAp ( call , ret , pos , out , ap )
1687
1789
)
1688
1790
}
1689
1791
@@ -1872,11 +1974,22 @@ module MakeImpl<InputSig Lang> {
1872
1974
bindingset [ node, cc]
1873
1975
LocalCc getLocalCc ( NodeEx node , Cc cc ) { any ( ) }
1874
1976
1875
- bindingset [ call, c, outercc]
1876
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) { any ( ) }
1977
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) { none ( ) }
1978
+
1979
+ bindingset [ call, ctx]
1980
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) { any ( ) }
1981
+
1982
+ bindingset [ call, c]
1983
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) { any ( ) }
1877
1984
1878
- bindingset [ call, c, innercc]
1879
- CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call , Cc innercc ) { any ( ) }
1985
+ DataFlowCallable viableImplCallContextReducedReverse ( DataFlowCall call , CcNoCall ctx ) {
1986
+ none ( )
1987
+ }
1988
+
1989
+ predicate viableImplNotCallContextReducedReverse ( CcNoCall ctx ) { any ( ) }
1990
+
1991
+ bindingset [ call, c]
1992
+ CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) { any ( ) }
1880
1993
}
1881
1994
1882
1995
private module Level1CallContext {
@@ -1899,9 +2012,17 @@ module MakeImpl<InputSig Lang> {
1899
2012
bindingset [ node, cc]
1900
2013
LocalCc getLocalCc ( NodeEx node , Cc cc ) { any ( ) }
1901
2014
1902
- bindingset [ call, c, outercc]
1903
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) {
1904
- checkCallContextCall ( outercc , call , c ) and
2015
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) {
2016
+ result = prunedViableImplInCallContext ( call , ctx )
2017
+ }
2018
+
2019
+ bindingset [ call, ctx]
2020
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) {
2021
+ noPrunedViableImplInCallContext ( call , ctx )
2022
+ }
2023
+
2024
+ bindingset [ call, c]
2025
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) {
1905
2026
if recordDataFlowCallSiteDispatch ( call , c )
1906
2027
then result = TSpecificCall ( call )
1907
2028
else result = TSomeCall ( )
@@ -1918,18 +2039,33 @@ module MakeImpl<InputSig Lang> {
1918
2039
node .getEnclosingCallable ( ) )
1919
2040
}
1920
2041
1921
- bindingset [ call, c, outercc]
1922
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) {
1923
- checkCallContextCall ( outercc , call , c ) and
2042
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) {
2043
+ result = prunedViableImplInCallContext ( call , ctx )
2044
+ }
2045
+
2046
+ bindingset [ call, ctx]
2047
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) {
2048
+ noPrunedViableImplInCallContext ( call , ctx )
2049
+ }
2050
+
2051
+ bindingset [ call, c]
2052
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) {
1924
2053
if recordDataFlowCallSite ( call , c )
1925
2054
then result = TSpecificCall ( call )
1926
2055
else result = TSomeCall ( )
1927
2056
}
1928
2057
}
1929
2058
1930
- bindingset [ call, c, innercc]
1931
- CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call , Cc innercc ) {
1932
- checkCallContextReturn ( innercc , c , call ) and
2059
+ DataFlowCallable viableImplCallContextReducedReverse ( DataFlowCall call , CcNoCall ctx ) {
2060
+ call = prunedViableImplInCallContextReverse ( result , ctx )
2061
+ }
2062
+
2063
+ predicate viableImplNotCallContextReducedReverse ( CcNoCall ctx ) {
2064
+ ctx instanceof CallContextAny
2065
+ }
2066
+
2067
+ bindingset [ call, c]
2068
+ CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) {
1933
2069
if reducedViableImplInReturn ( c , call ) then result = TReturn ( c , call ) else result = ccNone ( )
1934
2070
}
1935
2071
}
0 commit comments