@@ -1145,11 +1145,21 @@ module MakeImpl<InputSig Lang> {
1145
1145
1146
1146
class LocalCc ;
1147
1147
1148
- bindingset [ call, c, outercc]
1149
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) ;
1148
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) ;
1150
1149
1151
- bindingset [ call, c, innercc]
1152
- CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call , Cc innercc ) ;
1150
+ bindingset [ call, ctx]
1151
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) ;
1152
+
1153
+ bindingset [ call, c]
1154
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) ;
1155
+
1156
+ DataFlowCallable viableImplCallContextReducedReverse ( DataFlowCall call , CcNoCall ctx ) ;
1157
+
1158
+ bindingset [ ctx]
1159
+ predicate viableImplNotCallContextReducedReverse ( CcNoCall ctx ) ;
1160
+
1161
+ bindingset [ call, c]
1162
+ CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) ;
1153
1163
1154
1164
bindingset [ node, cc]
1155
1165
LocalCc getLocalCc ( NodeEx node , Cc cc ) ;
@@ -1191,21 +1201,24 @@ module MakeImpl<InputSig Lang> {
1191
1201
1192
1202
pragma [ nomagic]
1193
1203
private predicate flowIntoCallApa (
1194
- DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , ApApprox apa
1204
+ DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , DataFlowCallable c ,
1205
+ boolean allowsFieldFlow , ApApprox apa
1195
1206
) {
1196
1207
flowIntoCall ( call , arg , p , allowsFieldFlow ) and
1197
1208
PrevStage:: revFlowAp ( p , pragma [ only_bind_into ] ( apa ) ) and
1198
- PrevStage:: revFlowAp ( arg , pragma [ only_bind_into ] ( apa ) )
1209
+ PrevStage:: revFlowAp ( arg , pragma [ only_bind_into ] ( apa ) ) and
1210
+ c = p .getEnclosingCallable ( )
1199
1211
}
1200
1212
1201
1213
pragma [ nomagic]
1202
1214
private predicate flowOutOfCallApa (
1203
- DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
1204
- ApApprox apa
1215
+ DataFlowCall call , RetNodeEx ret , DataFlowCallable c , ReturnKindExt kind , NodeEx out ,
1216
+ boolean allowsFieldFlow , ApApprox apa
1205
1217
) {
1206
1218
flowOutOfCall ( call , ret , kind , out , allowsFieldFlow ) and
1207
1219
PrevStage:: revFlowAp ( out , pragma [ only_bind_into ] ( apa ) ) and
1208
- PrevStage:: revFlowAp ( ret , pragma [ only_bind_into ] ( apa ) )
1220
+ PrevStage:: revFlowAp ( ret , pragma [ only_bind_into ] ( apa ) ) and
1221
+ c = ret .getEnclosingCallable ( )
1209
1222
}
1210
1223
1211
1224
pragma [ nomagic]
@@ -1214,7 +1227,7 @@ module MakeImpl<InputSig Lang> {
1214
1227
ApApprox argApa , ApApprox apa
1215
1228
) {
1216
1229
exists ( ReturnKindExt kind |
1217
- flowOutOfCallApa ( call , ret , kind , out , allowsFieldFlow , apa ) and
1230
+ flowOutOfCallApa ( call , ret , _ , kind , out , allowsFieldFlow , apa ) and
1218
1231
PrevStage:: callMayFlowThroughRev ( call ) and
1219
1232
PrevStage:: returnMayFlowThrough ( ret , argApa , apa , kind ) and
1220
1233
matchesCall ( ccc , call )
@@ -1332,16 +1345,7 @@ module MakeImpl<InputSig Lang> {
1332
1345
)
1333
1346
or
1334
1347
// 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
- )
1348
+ fwdFlowOut ( node , state , cc , summaryCtx , argT , argAp , t , ap , apa )
1345
1349
or
1346
1350
// flow through a callable
1347
1351
exists (
@@ -1408,15 +1412,98 @@ module MakeImpl<InputSig Lang> {
1408
1412
)
1409
1413
}
1410
1414
1415
+ pragma [ nomagic]
1416
+ private predicate fwdFlowIn0 (
1417
+ DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , ParamNodeOption summaryCtx ,
1418
+ TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa
1419
+ ) {
1420
+ fwdFlow ( arg , state , outercc , summaryCtx , argT , argAp , t , ap , apa ) and
1421
+ flowIntoCallApa ( call , arg , _, _, _, _)
1422
+ }
1423
+
1424
+ pragma [ nomagic]
1425
+ private predicate fwdFlowInCallContextReduced (
1426
+ DataFlowCall call , ArgNodeEx arg , FlowState state , CcCall outercc ,
1427
+ ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa ,
1428
+ DataFlowCallable inner
1429
+ ) {
1430
+ fwdFlowIn0 ( call , arg , state , outercc , summaryCtx , argT , argAp , t , ap , apa ) and
1431
+ inner = viableImplCallContextReduced ( call , outercc )
1432
+ }
1433
+
1434
+ pragma [ nomagic]
1435
+ private predicate fwdFlowInNotCallContextReduced (
1436
+ DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , ParamNodeOption summaryCtx ,
1437
+ TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa
1438
+ ) {
1439
+ fwdFlowIn0 ( call , arg , state , outercc , summaryCtx , argT , argAp , t , ap , apa ) and
1440
+ viableImplNotCallContextReduced ( call , outercc )
1441
+ }
1442
+
1411
1443
pragma [ nomagic]
1412
1444
private predicate fwdFlowIn (
1413
1445
DataFlowCall call , ParamNodeEx p , FlowState state , Cc outercc , CcCall innercc ,
1414
1446
ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa
1415
1447
) {
1416
- exists ( ArgNodeEx arg , boolean allowsFieldFlow |
1417
- 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
1448
+ exists ( ArgNodeEx arg , boolean allowsFieldFlow , DataFlowCallable inner |
1449
+ fwdFlowInCallContextReduced ( call , arg , state , outercc , summaryCtx , argT , argAp , t , ap ,
1450
+ apa , inner )
1451
+ or
1452
+ fwdFlowInNotCallContextReduced ( call , arg , state , outercc , summaryCtx , argT , argAp , t ,
1453
+ ap , apa )
1454
+ |
1455
+ flowIntoCallApa ( call , arg , p , inner , allowsFieldFlow , apa ) and
1456
+ innercc = getCallContextCall ( call , inner ) and
1457
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1458
+ )
1459
+ }
1460
+
1461
+ pragma [ nomagic]
1462
+ private predicate fwdFlowOut0 (
1463
+ RetNodeEx ret , FlowState state , CcNoCall innercc , ParamNodeOption summaryCtx ,
1464
+ TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa , DataFlowCallable inner
1465
+ ) {
1466
+ fwdFlow ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
1467
+ inner = ret .getEnclosingCallable ( )
1468
+ }
1469
+
1470
+ pragma [ nomagic]
1471
+ private predicate fwdFlowOutCallContextReduced (
1472
+ DataFlowCall call , RetNodeEx ret , FlowState state , CcNoCall innercc ,
1473
+ ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa ,
1474
+ DataFlowCallable inner
1475
+ ) {
1476
+ fwdFlowOut0 ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa , inner ) and
1477
+ inner = viableImplCallContextReducedReverse ( call , innercc )
1478
+ }
1479
+
1480
+ pragma [ nomagic]
1481
+ private predicate fwdFlowOutNotCallContextReduced (
1482
+ RetNodeEx ret , FlowState state , CcNoCall innercc , ParamNodeOption summaryCtx ,
1483
+ TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa , DataFlowCallable inner
1484
+ ) {
1485
+ fwdFlowOut0 ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa , inner ) and
1486
+ viableImplNotCallContextReducedReverse ( innercc )
1487
+ }
1488
+
1489
+ // inline to reduce number of iterations
1490
+ pragma [ inline]
1491
+ private predicate fwdFlowOut (
1492
+ NodeEx out , FlowState state , CcNoCall outercc , ParamNodeOption summaryCtx , TypOption argT ,
1493
+ ApOption argAp , Typ t , Ap ap , ApApprox apa
1494
+ ) {
1495
+ exists (
1496
+ DataFlowCall call , RetNodeEx ret , boolean allowsFieldFlow , CcNoCall innercc ,
1497
+ DataFlowCallable inner
1498
+ |
1499
+ fwdFlowOutCallContextReduced ( call , ret , state , innercc , summaryCtx , argT , argAp , t , ap ,
1500
+ apa , inner )
1501
+ or
1502
+ fwdFlowOutNotCallContextReduced ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ,
1503
+ apa , inner )
1504
+ |
1505
+ flowOutOfCallApa ( call , ret , inner , _, out , allowsFieldFlow , apa ) and
1506
+ outercc = getCallContextReturn ( inner , call ) and
1420
1507
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1421
1508
)
1422
1509
}
@@ -1518,7 +1605,7 @@ module MakeImpl<InputSig Lang> {
1518
1605
DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Ap argAp , Ap ap
1519
1606
) {
1520
1607
exists ( ApApprox argApa , Typ argT |
1521
- flowIntoCallApa ( call , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) ,
1608
+ flowIntoCallApa ( call , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) , _ ,
1522
1609
allowsFieldFlow , argApa ) and
1523
1610
fwdFlow ( arg , _, _, _, _, _, pragma [ only_bind_into ] ( argT ) , pragma [ only_bind_into ] ( argAp ) ,
1524
1611
argApa ) and
@@ -1529,24 +1616,23 @@ module MakeImpl<InputSig Lang> {
1529
1616
}
1530
1617
1531
1618
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 )
1619
+ private predicate flowIntoCallAp ( DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , Ap ap ) {
1620
+ exists ( ApApprox apa , boolean allowsFieldFlow |
1621
+ flowIntoCallApa ( call , arg , p , _, allowsFieldFlow , apa ) and
1622
+ fwdFlow ( arg , _, _, _, _, _, _, ap , apa ) and
1623
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1538
1624
)
1539
1625
}
1540
1626
1541
1627
pragma [ nomagic]
1542
1628
private predicate flowOutOfCallAp (
1543
- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1544
- Ap ap
1629
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , Ap ap
1545
1630
) {
1546
- exists ( ApApprox apa |
1547
- flowOutOfCallApa ( call , ret , _, out , allowsFieldFlow , apa ) and
1631
+ exists ( ApApprox apa , boolean allowsFieldFlow |
1632
+ flowOutOfCallApa ( call , ret , _, _ , out , allowsFieldFlow , apa ) and
1548
1633
fwdFlow ( ret , _, _, _, _, _, _, ap , apa ) and
1549
- pos = ret .getReturnPosition ( )
1634
+ pos = ret .getReturnPosition ( ) and
1635
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1550
1636
)
1551
1637
}
1552
1638
@@ -1627,10 +1713,9 @@ module MakeImpl<InputSig Lang> {
1627
1713
)
1628
1714
or
1629
1715
// flow into a callable
1630
- exists ( ParamNodeEx p , boolean allowsFieldFlow |
1716
+ exists ( ParamNodeEx p |
1631
1717
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
1718
+ flowIntoCallAp ( _, node , p , ap ) and
1634
1719
returnCtx = TReturnCtxNone ( )
1635
1720
)
1636
1721
or
@@ -1680,10 +1765,9 @@ module MakeImpl<InputSig Lang> {
1680
1765
DataFlowCall call , RetNodeEx ret , ReturnPosition pos , FlowState state ,
1681
1766
ReturnCtx returnCtx , ApOption returnAp , Ap ap
1682
1767
) {
1683
- exists ( NodeEx out , boolean allowsFieldFlow |
1768
+ exists ( NodeEx out |
1684
1769
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 ( )
1770
+ flowOutOfCallAp ( call , ret , pos , out , ap )
1687
1771
)
1688
1772
}
1689
1773
@@ -1872,11 +1956,23 @@ module MakeImpl<InputSig Lang> {
1872
1956
bindingset [ node, cc]
1873
1957
LocalCc getLocalCc ( NodeEx node , Cc cc ) { any ( ) }
1874
1958
1875
- bindingset [ call, c, outercc]
1876
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) { any ( ) }
1959
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) { none ( ) }
1960
+
1961
+ bindingset [ call, ctx]
1962
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) { any ( ) }
1963
+
1964
+ bindingset [ call, c]
1965
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) { any ( ) }
1966
+
1967
+ DataFlowCallable viableImplCallContextReducedReverse ( DataFlowCall call , CcNoCall ctx ) {
1968
+ none ( )
1969
+ }
1877
1970
1878
- bindingset [ call, c, innercc]
1879
- CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call , Cc innercc ) { any ( ) }
1971
+ bindingset [ ctx]
1972
+ predicate viableImplNotCallContextReducedReverse ( CcNoCall ctx ) { any ( ) }
1973
+
1974
+ bindingset [ call, c]
1975
+ CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) { any ( ) }
1880
1976
}
1881
1977
1882
1978
private module Level1CallContext {
@@ -1899,9 +1995,17 @@ module MakeImpl<InputSig Lang> {
1899
1995
bindingset [ node, cc]
1900
1996
LocalCc getLocalCc ( NodeEx node , Cc cc ) { any ( ) }
1901
1997
1902
- bindingset [ call, c, outercc]
1903
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) {
1904
- checkCallContextCall ( outercc , call , c ) and
1998
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) {
1999
+ result = prunedViableImplInCallContext ( call , ctx )
2000
+ }
2001
+
2002
+ bindingset [ call, ctx]
2003
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) {
2004
+ noPrunedViableImplInCallContext ( call , ctx )
2005
+ }
2006
+
2007
+ bindingset [ call, c]
2008
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) {
1905
2009
if recordDataFlowCallSiteDispatch ( call , c )
1906
2010
then result = TSpecificCall ( call )
1907
2011
else result = TSomeCall ( )
@@ -1918,18 +2022,34 @@ module MakeImpl<InputSig Lang> {
1918
2022
node .getEnclosingCallable ( ) )
1919
2023
}
1920
2024
1921
- bindingset [ call, c, outercc]
1922
- CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c , Cc outercc ) {
1923
- checkCallContextCall ( outercc , call , c ) and
2025
+ DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) {
2026
+ result = prunedViableImplInCallContext ( call , ctx )
2027
+ }
2028
+
2029
+ bindingset [ call, ctx]
2030
+ predicate viableImplNotCallContextReduced ( DataFlowCall call , Cc ctx ) {
2031
+ noPrunedViableImplInCallContext ( call , ctx )
2032
+ }
2033
+
2034
+ bindingset [ call, c]
2035
+ CcCall getCallContextCall ( DataFlowCall call , DataFlowCallable c ) {
1924
2036
if recordDataFlowCallSite ( call , c )
1925
2037
then result = TSpecificCall ( call )
1926
2038
else result = TSomeCall ( )
1927
2039
}
1928
2040
}
1929
2041
1930
- bindingset [ call, c, innercc]
1931
- CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call , Cc innercc ) {
1932
- checkCallContextReturn ( innercc , c , call ) and
2042
+ DataFlowCallable viableImplCallContextReducedReverse ( DataFlowCall call , CcNoCall ctx ) {
2043
+ result = prunedViableImplInCallContextReverse ( call , ctx )
2044
+ }
2045
+
2046
+ bindingset [ ctx]
2047
+ predicate viableImplNotCallContextReducedReverse ( CcNoCall ctx ) {
2048
+ ctx instanceof CallContextAny
2049
+ }
2050
+
2051
+ bindingset [ call, c]
2052
+ CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) {
1933
2053
if reducedViableImplInReturn ( c , call ) then result = TReturn ( c , call ) else result = ccNone ( )
1934
2054
}
1935
2055
}
0 commit comments