@@ -1310,7 +1310,7 @@ module MakeImpl<InputSig Lang> {
1310
1310
PrevStage:: revFlow ( node ) and result = getTyp ( node .getDataFlowType ( ) )
1311
1311
}
1312
1312
1313
- pragma [ inline ]
1313
+ pragma [ nomagic ]
1314
1314
private predicate flowThroughOutOfCall (
1315
1315
DataFlowCall call , CcCall ccc , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1316
1316
boolean allowsFieldFlow , ApApprox argApa , ApApprox apa
@@ -1321,14 +1321,13 @@ module MakeImpl<InputSig Lang> {
1321
1321
matchesCall ( ccc , call )
1322
1322
}
1323
1323
1324
- pragma [ nomagic]
1325
- private predicate flowThroughOutOfCall (
1326
- DataFlowCall call , CcCall ccc , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
1327
- ApApprox argApa , ApApprox apa
1328
- ) {
1329
- flowThroughOutOfCall ( call , ccc , _, kind , out , allowsFieldFlow , argApa , apa )
1330
- }
1331
-
1324
+ // pragma[nomagic]
1325
+ // private predicate flowThroughOutOfCall(
1326
+ // DataFlowCall call, CcCall ccc, ReturnKindExt kind, NodeEx out, boolean allowsFieldFlow,
1327
+ // ApApprox argApa, ApApprox apa
1328
+ // ) {
1329
+ // flowThroughOutOfCall(call, ccc, _, kind, out, allowsFieldFlow, argApa, apa)
1330
+ // }
1332
1331
/**
1333
1332
* Holds if `node` is reachable with access path `ap` from a source.
1334
1333
*
@@ -1441,10 +1440,10 @@ module MakeImpl<InputSig Lang> {
1441
1440
)
1442
1441
or
1443
1442
// flow into a callable
1444
- exists ( boolean inSummaryCtx |
1445
- fwdFlowIn ( node , apa , state , cc , t , origT , ap , inSummaryCtx )
1443
+ exists ( boolean inSummaryCtx , boolean allowsFlowThrough |
1444
+ fwdFlowIn ( node , apa , state , cc , t , origT , ap , inSummaryCtx , allowsFlowThrough )
1446
1445
|
1447
- PrevStage :: parameterMayFlowThrough ( node , apa ) and
1446
+ allowsFlowThrough = true and
1448
1447
summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
1449
1448
argT = ArgTypOption:: some ( toArgTyp ( t ) ) and
1450
1449
argAp = apSome ( ap )
@@ -1468,9 +1467,8 @@ module MakeImpl<InputSig Lang> {
1468
1467
ApApprox innerArgApa
1469
1468
|
1470
1469
fwdFlowThrough ( call , cc , state , ccc , summaryCtx , argT , argAp , t , origT , ap , apa , ret ,
1471
- innerArgApa ) and
1472
- flowThroughOutOfCall ( call , ccc , ret , _, node , allowsFieldFlow , innerArgApa , apa ) and
1473
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1470
+ innerArgApa , allowsFieldFlow ) and
1471
+ flowThroughOutOfCall ( call , ccc , ret , _, node , allowsFieldFlow , innerArgApa , apa )
1474
1472
)
1475
1473
}
1476
1474
@@ -1606,10 +1604,14 @@ module MakeImpl<InputSig Lang> {
1606
1604
}
1607
1605
1608
1606
private signature module FwdFlowInInputSig {
1609
- default predicate callRestriction ( DataFlowCall call ) { any ( ) }
1610
-
1611
- bindingset [ p, apa]
1612
- default predicate parameterRestriction ( ParamNodeEx p , ApApprox apa ) { any ( ) }
1607
+ // default predicate callRestriction(DataFlowCall call) { any() }
1608
+ // bindingset[p, apa]
1609
+ // default predicate parameterRestriction(ParamNodeEx p, ApApprox apa) { any() }
1610
+ default predicate restriction (
1611
+ DataFlowCall call , ParamNodeEx p , ApApprox apa , boolean allowsFieldFlow
1612
+ ) {
1613
+ PrevStage:: callEdgeArgParam ( call , _, _, p , allowsFieldFlow , apa )
1614
+ }
1613
1615
}
1614
1616
1615
1617
/**
@@ -1630,9 +1632,13 @@ module MakeImpl<InputSig Lang> {
1630
1632
DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1631
1633
boolean allowsFieldFlow , ApApprox apa
1632
1634
) {
1633
- PrevStage:: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa ) and
1634
- I:: callRestriction ( call ) and
1635
- I:: parameterRestriction ( p , apa )
1635
+ exists ( boolean allowsFieldFlow1 , boolean allowsFieldFlow2 |
1636
+ PrevStage:: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow1 , apa ) and
1637
+ I:: restriction ( call , p , apa , allowsFieldFlow2 ) and
1638
+ allowsFieldFlow = allowsFieldFlow1 .booleanAnd ( allowsFieldFlow2 )
1639
+ )
1640
+ // I::callRestriction(call) and
1641
+ // I::parameterRestriction(p, apa)
1636
1642
}
1637
1643
1638
1644
pragma [ nomagic]
@@ -1767,15 +1773,40 @@ module MakeImpl<InputSig Lang> {
1767
1773
1768
1774
private module FwdFlowInNoRestriction implements FwdFlowInInputSig { }
1769
1775
1776
+ pragma [ nomagic]
1777
+ private predicate flowThroughOutOfCall (
1778
+ DataFlowCall call , ParamNodeEx p , ApApprox apa , boolean allowsFieldFlow
1779
+ ) {
1780
+ PrevStage:: parameterMayFlowThrough ( p , apa ) and
1781
+ flowThroughOutOfCall ( call , _, _, _, _, allowsFieldFlow , apa , _) and
1782
+ PrevStage:: callEdgeArgParam ( call , _, _, p , _, apa )
1783
+ }
1784
+
1785
+ bindingset [ call, p, ap, apa]
1786
+ pragma [ inline_late]
1787
+ private predicate fwdFlowInFlowThroughAllowed (
1788
+ DataFlowCall call , ParamNodeEx p , Ap ap , ApApprox apa
1789
+ ) {
1790
+ exists ( boolean allowsFieldFlow |
1791
+ flowThroughOutOfCall ( call , p , apa , allowsFieldFlow ) and
1792
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1793
+ )
1794
+ }
1795
+
1770
1796
pragma [ nomagic]
1771
1797
private predicate fwdFlowIn (
1772
1798
ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , TypOption origT ,
1773
- Ap ap , boolean inSummaryCtx
1799
+ Ap ap , boolean inSummaryCtx , boolean allowsFlowThrough
1774
1800
) {
1775
- exists ( ParamNodeOption summaryCtx |
1776
- FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( _ , _, p , state , _, innercc , summaryCtx , _ ,
1777
- _, t , origT , ap , apa , _) and
1801
+ exists ( DataFlowCall call , ParamNodeOption summaryCtx |
1802
+ FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( call , _, p , state , _, innercc , summaryCtx ,
1803
+ _, _ , t , origT , ap , apa , _) and
1778
1804
if summaryCtx = TParamNodeNone ( ) then inSummaryCtx = false else inSummaryCtx = true
1805
+ |
1806
+ allowsFlowThrough = false
1807
+ or
1808
+ allowsFlowThrough = true and
1809
+ fwdFlowInFlowThroughAllowed ( call , p , ap , apa )
1779
1810
)
1780
1811
}
1781
1812
@@ -1947,16 +1978,18 @@ module MakeImpl<InputSig Lang> {
1947
1978
pragma [ nomagic]
1948
1979
private predicate fwdFlowRetFromArg (
1949
1980
RetNodeEx ret , FlowState state , CcCall ccc , ParamNodeEx summaryCtx , ArgTyp argT , Ap argAp ,
1950
- ApApprox argApa , Typ t , TypOption origT , Ap ap , ApApprox apa
1981
+ ApApprox argApa , Typ t , TypOption origT , Ap ap , ApApprox apa , boolean allowsFieldFlow
1951
1982
) {
1952
- exists ( DataFlowCall call , ReturnKindExt kind , boolean allowsFieldFlow |
1983
+ exists ( DataFlowCall call , ReturnKindExt kind |
1953
1984
fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc ,
1954
1985
TParamNodeSome ( pragma [ only_bind_into ] ( summaryCtx .asNode ( ) ) ) , ArgTypOption:: some ( argT ) ,
1955
1986
pragma [ only_bind_into ] ( apSome ( argAp ) ) , t , origT , ap , pragma [ only_bind_into ] ( apa ) ) and
1956
1987
parameterFlowThroughAllowed ( summaryCtx , kind ) and
1957
1988
argApa = getApprox ( argAp ) and
1958
1989
flowThroughOutOfCall ( call , ccc , ret , kind , _, allowsFieldFlow , argApa , apa ) and
1959
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1990
+ if allowsFieldFlow = false
1991
+ then ap instanceof ApNil and argAp instanceof ApNil
1992
+ else any ( )
1960
1993
)
1961
1994
}
1962
1995
@@ -1965,10 +1998,10 @@ module MakeImpl<InputSig Lang> {
1965
1998
DataFlowCall call , Cc cc , FlowState state , CcCall ccc , ParamNodeOption summaryCtx ,
1966
1999
ArgTypOption argT , ApOption argAp , Typ t , TypOption origT , Ap ap , ApApprox apa ,
1967
2000
RetNodeEx ret , ParamNodeEx innerSummaryCtx , ArgTyp innerArgT , Ap innerArgAp ,
1968
- ApApprox innerArgApa
2001
+ ApApprox innerArgApa , boolean allowsFieldFlow
1969
2002
) {
1970
2003
fwdFlowRetFromArg ( ret , state , ccc , innerSummaryCtx , innerArgT , innerArgAp , innerArgApa , t ,
1971
- origT , ap , apa ) and
2004
+ origT , ap , apa , allowsFieldFlow ) and
1972
2005
fwdFlowIsEntered ( call , cc , ccc , summaryCtx , argT , argAp , innerSummaryCtx , innerArgT ,
1973
2006
innerArgAp )
1974
2007
}
@@ -1977,16 +2010,14 @@ module MakeImpl<InputSig Lang> {
1977
2010
private predicate fwdFlowThrough (
1978
2011
DataFlowCall call , Cc cc , FlowState state , CcCall ccc , ParamNodeOption summaryCtx ,
1979
2012
ArgTypOption argT , ApOption argAp , Typ t , TypOption origT , Ap ap , ApApprox apa ,
1980
- RetNodeEx ret , ApApprox innerArgApa
2013
+ RetNodeEx ret , ApApprox innerArgApa , boolean allowsFieldFlow
1981
2014
) {
1982
2015
fwdFlowThrough0 ( call , cc , state , ccc , summaryCtx , argT , argAp , t , origT , ap , apa , ret , _,
1983
- _, _, innerArgApa )
2016
+ _, _, innerArgApa , allowsFieldFlow )
1984
2017
}
1985
2018
1986
2019
private module FwdFlowThroughRestriction implements FwdFlowInInputSig {
1987
- predicate callRestriction = PrevStage:: callMayFlowThroughRev / 1 ;
1988
-
1989
- predicate parameterRestriction = PrevStage:: parameterMayFlowThrough / 2 ;
2020
+ predicate restriction = flowThroughOutOfCall / 4 ;
1990
2021
}
1991
2022
1992
2023
/**
@@ -2000,7 +2031,8 @@ module MakeImpl<InputSig Lang> {
2000
2031
) {
2001
2032
exists ( ApApprox apa |
2002
2033
FwdFlowIn< FwdFlowThroughRestriction > :: fwdFlowIn ( call , _, p , _, cc , innerCc , summaryCtx ,
2003
- argT , argAp , any ( Typ t0 | t = toArgTyp ( t0 ) ) , _, ap , apa , _)
2034
+ argT , argAp , any ( Typ t0 | t = toArgTyp ( t0 ) ) , _, ap , apa , _) and
2035
+ fwdFlowInFlowThroughAllowed ( call , p , ap , apa )
2004
2036
)
2005
2037
}
2006
2038
@@ -2024,10 +2056,11 @@ module MakeImpl<InputSig Lang> {
2024
2056
pragma [ nomagic]
2025
2057
private predicate returnFlowsThrough0 (
2026
2058
DataFlowCall call , FlowState state , CcCall ccc , Ap ap , ApApprox apa , RetNodeEx ret ,
2027
- ParamNodeEx innerSummaryCtx , ArgTyp innerArgT , Ap innerArgAp , ApApprox innerArgApa
2059
+ ParamNodeEx innerSummaryCtx , ArgTyp innerArgT , Ap innerArgAp , ApApprox innerArgApa ,
2060
+ boolean allowsFieldFlow
2028
2061
) {
2029
2062
fwdFlowThrough0 ( call , _, state , ccc , _, _, _, _, _, ap , apa , ret , innerSummaryCtx ,
2030
- innerArgT , innerArgAp , innerArgApa )
2063
+ innerArgT , innerArgAp , innerArgApa , allowsFieldFlow )
2031
2064
}
2032
2065
2033
2066
pragma [ nomagic]
@@ -2036,10 +2069,10 @@ module MakeImpl<InputSig Lang> {
2036
2069
ArgTyp argT , Ap argAp , Ap ap
2037
2070
) {
2038
2071
exists ( DataFlowCall call , ApApprox apa , boolean allowsFieldFlow , ApApprox innerArgApa |
2039
- returnFlowsThrough0 ( call , state , ccc , ap , apa , ret , p , argT , argAp , innerArgApa ) and
2072
+ returnFlowsThrough0 ( call , state , ccc , ap , apa , ret , p , argT , argAp , innerArgApa ,
2073
+ allowsFieldFlow ) and
2040
2074
flowThroughOutOfCall ( call , ccc , ret , _, _, allowsFieldFlow , innerArgApa , apa ) and
2041
- pos = ret .getReturnPosition ( ) and
2042
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2075
+ pos = ret .getReturnPosition ( )
2043
2076
)
2044
2077
}
2045
2078
@@ -2053,7 +2086,9 @@ module MakeImpl<InputSig Lang> {
2053
2086
flowIntoCallApaTaken ( call , _, pragma [ only_bind_into ] ( arg ) , p , allowsFieldFlow , argApa ) and
2054
2087
fwdFlow ( arg , _, _, _, _, _, pragma [ only_bind_into ] ( argT ) , _,
2055
2088
pragma [ only_bind_into ] ( argAp ) , argApa ) and
2056
- if allowsFieldFlow = false then argAp instanceof ApNil else any ( )
2089
+ if allowsFieldFlow = false
2090
+ then argAp instanceof ApNil and ap instanceof ApNil
2091
+ else any ( )
2057
2092
)
2058
2093
}
2059
2094
@@ -3255,12 +3290,12 @@ module MakeImpl<InputSig Lang> {
3255
3290
then t = nt
3256
3291
else (
3257
3292
compatibleTypes ( nt , t0 ) and
3258
- // t = t0
3259
- if inSummaryCtx = true and node instanceof ParamNodeEx
3260
- then
3261
- t = nt and
3262
- compatibleTypes ( origT , t )
3263
- else t = t0
3293
+ t = t0
3294
+ // if inSummaryCtx = true and node instanceof ParamNodeEx
3295
+ // then
3296
+ // t = nt and
3297
+ // compatibleTypes(origT, t)
3298
+ // else t = t0
3264
3299
)
3265
3300
)
3266
3301
else t = t0
0 commit comments