@@ -942,11 +942,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
942
942
}
943
943
944
944
pragma [ nomagic]
945
- predicate returnMayFlowThrough ( RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind ) {
945
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind ) {
946
946
throughFlowNodeCand ( ret ) and
947
- kind = ret .getKind ( ) and
948
- exists ( argAp ) and
949
- exists ( ap )
947
+ kind = ret .getKind ( )
950
948
}
951
949
952
950
pragma [ nomagic]
@@ -969,19 +967,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
969
967
970
968
predicate callEdgeReturn (
971
969
DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
972
- boolean allowsFieldFlow , Ap ap
970
+ boolean allowsFieldFlow
973
971
) {
974
972
flowOutOfCallNodeCand1 ( call , ret , kind , out , allowsFieldFlow ) and
975
- c = ret .getEnclosingCallable ( ) and
976
- exists ( ap )
973
+ c = ret .getEnclosingCallable ( )
977
974
}
978
975
979
976
predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
980
977
callEdgeArgParam ( call , c , _, _, _, _)
981
978
}
982
979
983
980
predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
984
- callEdgeReturn ( call , c , _, _, _, _, _ )
981
+ callEdgeReturn ( call , c , _, _, _, _)
985
982
}
986
983
987
984
additional predicate stats (
@@ -1004,7 +1001,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1004
1001
calledges =
1005
1002
count ( DataFlowCall call , DataFlowCallable c |
1006
1003
callEdgeArgParam ( call , c , _, _, _, _) or
1007
- callEdgeReturn ( call , c , _, _, _, _, _ )
1004
+ callEdgeReturn ( call , c , _, _, _, _)
1008
1005
)
1009
1006
}
1010
1007
/* End: Stage 1 logic. */
@@ -1287,7 +1284,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1287
1284
1288
1285
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap ) ;
1289
1286
1290
- predicate returnMayFlowThrough ( RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind ) ;
1287
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind ) ;
1291
1288
1292
1289
predicate storeStepCand (
1293
1290
NodeEx node1 , Ap ap1 , Content c , NodeEx node2 , DataFlowType contentType ,
@@ -1303,7 +1300,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1303
1300
1304
1301
predicate callEdgeReturn (
1305
1302
DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1306
- boolean allowsFieldFlow , Ap ap
1303
+ boolean allowsFieldFlow
1307
1304
) ;
1308
1305
1309
1306
predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) ;
@@ -1437,13 +1434,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1437
1434
1438
1435
pragma [ nomagic]
1439
1436
private predicate flowThroughOutOfCall (
1440
- DataFlowCall call , CcCall ccc , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1441
- ApApprox argApa , ApApprox apa
1437
+ DataFlowCall call , CcCall ccc , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow
1442
1438
) {
1443
1439
exists ( ReturnKindExt kind |
1444
- PrevStage:: callEdgeReturn ( call , _, ret , kind , out , allowsFieldFlow , apa ) and
1440
+ PrevStage:: callEdgeReturn ( call , _, ret , kind , out , allowsFieldFlow ) and
1445
1441
PrevStage:: callMayFlowThroughRev ( call ) and
1446
- PrevStage:: returnMayFlowThrough ( ret , argApa , apa , kind ) and
1442
+ PrevStage:: returnMayFlowThrough ( ret , kind ) and
1447
1443
matchesCall ( ccc , call )
1448
1444
)
1449
1445
}
@@ -1560,12 +1556,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1560
1556
fwdFlowOut ( _, _, node , state , cc , summaryCtx , t , ap , apa , stored )
1561
1557
or
1562
1558
// flow through a callable
1563
- exists (
1564
- DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow ,
1565
- ApApprox innerArgApa
1566
- |
1567
- fwdFlowThrough ( call , cc , state , ccc , summaryCtx , t , ap , apa , stored , ret , innerArgApa ) and
1568
- flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow , innerArgApa , apa ) and
1559
+ exists ( DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow |
1560
+ fwdFlowThrough ( call , cc , state , ccc , summaryCtx , t , ap , apa , stored , ret , _) and
1561
+ flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow ) and
1569
1562
not inBarrier ( node , state ) and
1570
1563
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1571
1564
)
@@ -1925,7 +1918,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1925
1918
DataFlowCallable c , CcNoCall ctx
1926
1919
) {
1927
1920
result = viableImplCallContextReducedReverse ( c , ctx ) and
1928
- PrevStage:: callEdgeReturn ( result , c , _, _, _, _, _ )
1921
+ PrevStage:: callEdgeReturn ( result , c , _, _, _, _)
1929
1922
}
1930
1923
1931
1924
bindingset [ c, ctx]
@@ -1939,21 +1932,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1939
1932
bindingset [ call]
1940
1933
pragma [ inline_late]
1941
1934
private predicate flowOutOfCallApaInlineLate (
1942
- DataFlowCall call , DataFlowCallable c , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1943
- ApApprox apa
1935
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow
1944
1936
) {
1945
- PrevStage:: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow , apa )
1937
+ PrevStage:: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow )
1946
1938
}
1947
1939
1948
- bindingset [ c, ret, apa , innercc]
1940
+ bindingset [ c, ret, innercc]
1949
1941
pragma [ inline_late]
1950
1942
pragma [ noopt]
1951
1943
private predicate flowOutOfCallApaNotCallContextReduced (
1952
1944
DataFlowCall call , DataFlowCallable c , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1953
- ApApprox apa , CcNoCall innercc
1945
+ CcNoCall innercc
1954
1946
) {
1955
1947
viableImplNotCallContextReducedReverse ( innercc ) and
1956
- PrevStage:: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow , apa )
1948
+ PrevStage:: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow )
1957
1949
}
1958
1950
1959
1951
pragma [ nomagic]
@@ -1975,10 +1967,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1975
1967
inner = ret .getEnclosingCallable ( ) and
1976
1968
(
1977
1969
call = viableImplCallContextReducedReverseInlineLate ( inner , innercc ) and
1978
- flowOutOfCallApaInlineLate ( call , inner , ret , out , allowsFieldFlow , apa )
1970
+ flowOutOfCallApaInlineLate ( call , inner , ret , out , allowsFieldFlow )
1979
1971
or
1980
- flowOutOfCallApaNotCallContextReduced ( call , inner , ret , out , allowsFieldFlow , apa ,
1981
- innercc )
1972
+ flowOutOfCallApaNotCallContextReduced ( call , inner , ret , out , allowsFieldFlow , innercc )
1982
1973
)
1983
1974
}
1984
1975
@@ -2050,10 +2041,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2050
2041
private predicate fwdFlow1Out (
2051
2042
NodeEx node , FlowState state , Cc cc , Typ t0 , Ap ap , TypOption stored
2052
2043
) {
2053
- exists ( ApApprox apa |
2054
- fwdFlow1 ( node , state , cc , _, t0 , _, ap , apa , stored ) and
2055
- PrevStage:: callEdgeReturn ( _, _, _, _, node , _, apa )
2056
- )
2044
+ fwdFlow1 ( node , state , cc , _, t0 , _, ap , _, stored ) and
2045
+ PrevStage:: callEdgeReturn ( _, _, _, _, node , _)
2057
2046
}
2058
2047
2059
2048
pragma [ nomagic]
@@ -2097,15 +2086,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2097
2086
) {
2098
2087
exists ( ReturnKindExt kind , ParamNodeEx p , Ap argAp |
2099
2088
instanceofCcCall ( ccc ) and
2100
- fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc , summaryCtx , t , ap ,
2101
- pragma [ only_bind_into ] ( apa ) , stored ) and
2089
+ fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc , summaryCtx , t , ap , apa , stored ) and
2102
2090
summaryCtx =
2103
2091
TSummaryCtxSome ( pragma [ only_bind_into ] ( p ) , _, _, pragma [ only_bind_into ] ( argAp ) , _) and
2104
2092
not outBarrier ( ret , state ) and
2105
2093
kind = ret .getKind ( ) and
2106
2094
parameterFlowThroughAllowed ( p , kind ) and
2107
2095
argApa = getApprox ( argAp ) and
2108
- PrevStage:: returnMayFlowThrough ( ret , pragma [ only_bind_into ] ( argApa ) , apa , kind )
2096
+ PrevStage:: returnMayFlowThrough ( ret , kind )
2109
2097
)
2110
2098
}
2111
2099
@@ -2178,10 +2166,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2178
2166
RetNodeEx ret , ReturnPosition pos , FlowState state , CcCall ccc , ParamNodeEx p , Typ argT ,
2179
2167
Ap argAp , ApApprox argApa , TypOption argStored , Ap ap
2180
2168
) {
2181
- exists ( DataFlowCall call , ApApprox apa , boolean allowsFieldFlow |
2182
- returnFlowsThrough0 ( call , state , ccc , ap , apa , ret ,
2169
+ exists ( DataFlowCall call , boolean allowsFieldFlow |
2170
+ returnFlowsThrough0 ( call , state , ccc , ap , _ , ret ,
2183
2171
TSummaryCtxSome ( p , _, argT , argAp , argStored ) , argApa ) and
2184
- flowThroughOutOfCall ( call , ccc , ret , _, allowsFieldFlow , argApa , apa ) and
2172
+ flowThroughOutOfCall ( call , ccc , ret , _, allowsFieldFlow ) and
2185
2173
pos = ret .getReturnPosition ( ) and
2186
2174
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2187
2175
)
@@ -2216,14 +2204,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2216
2204
pragma [ nomagic]
2217
2205
private predicate flowOutOfCallAp (
2218
2206
DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnPosition pos , NodeEx out ,
2219
- Ap ap
2207
+ Ap ap , boolean allowsFieldFlow
2220
2208
) {
2221
- exists ( ApApprox apa , boolean allowsFieldFlow |
2222
- PrevStage:: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow , apa ) and
2223
- fwdFlow ( ret , _, _, _, _, ap , apa , _) and
2224
- pos = ret .getReturnPosition ( ) and
2225
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2226
- |
2209
+ PrevStage:: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow ) and
2210
+ fwdFlow ( ret , _, _, _, _, ap , _, _) and
2211
+ pos = ret .getReturnPosition ( ) and
2212
+ ( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
2213
+ (
2227
2214
// both directions are needed for flow-through
2228
2215
FwdTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _) or
2229
2216
FwdTypeFlowInput:: dataFlowTakenCallEdgeOut ( call , c )
@@ -2356,7 +2343,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2356
2343
predicate enableTypeFlow = Param:: enableTypeFlow / 0 ;
2357
2344
2358
2345
predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
2359
- flowOutOfCallAp ( call , c , _, _, _, _)
2346
+ flowOutOfCallAp ( call , c , _, _, _, _, _ )
2360
2347
}
2361
2348
2362
2349
predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
@@ -2407,7 +2394,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2407
2394
DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , Ap ap , boolean cc
2408
2395
) {
2409
2396
exists ( DataFlowCallable c |
2410
- flowOutOfCallAp ( call , c , ret , pos , out , ap ) and
2397
+ flowOutOfCallAp ( call , c , ret , pos , out , ap , _ ) and
2411
2398
RevTypeFlow:: typeFlowValidEdgeIn ( call , c , cc )
2412
2399
)
2413
2400
}
@@ -2559,8 +2546,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2559
2546
}
2560
2547
2561
2548
pragma [ nomagic]
2562
- predicate returnMayFlowThrough ( RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind ) {
2563
- exists ( ParamNodeEx p , ReturnPosition pos |
2549
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind ) {
2550
+ exists ( ParamNodeEx p , ReturnPosition pos , Ap argAp , Ap ap |
2564
2551
returnFlowsThrough ( ret , pos , _, _, p , _, argAp , _, _, ap ) and
2565
2552
parameterFlowsThroughRev ( p , argAp , pos , ap ) and
2566
2553
kind = pos .getKind ( )
@@ -2607,14 +2594,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2607
2594
2608
2595
predicate callEdgeReturn (
2609
2596
DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
2610
- boolean allowsFieldFlow , Ap ap
2597
+ boolean allowsFieldFlow
2611
2598
) {
2612
- exists ( FlowState state , ReturnPosition pos |
2613
- flowOutOfCallAp ( call , c , ret , pos , out , ap ) and
2599
+ exists ( FlowState state , ReturnPosition pos , Ap ap |
2600
+ flowOutOfCallAp ( call , c , ret , pos , out , ap , allowsFieldFlow ) and
2614
2601
revFlow ( ret , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2615
2602
revFlow ( out , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2616
2603
kind = pos .getKind ( ) and
2617
- allowsFieldFlow = true and
2618
2604
RevTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _)
2619
2605
)
2620
2606
}
@@ -2624,7 +2610,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2624
2610
}
2625
2611
2626
2612
predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
2627
- callEdgeReturn ( call , c , _, _, _, _, _ )
2613
+ callEdgeReturn ( call , c , _, _, _, _)
2628
2614
}
2629
2615
2630
2616
/** Holds if `node1` can step to `node2` in one or more local steps. */
@@ -2719,7 +2705,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2719
2705
callEdgeArgParam ( _, _, node , next , _, ap ) and
2720
2706
apNext = ap
2721
2707
or
2722
- callEdgeReturn ( _, _, node , _, next , _, ap ) and
2708
+ callEdgeReturn ( _, _, node , _, next , _) and
2723
2709
apNext = ap
2724
2710
or
2725
2711
storeStepCand ( node , _, _, next , _, _)
@@ -3206,13 +3192,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3206
3192
PathNodeImpl pn1 , PathNodeImpl pn2 , PathNodeImpl pn3 , NodeEx node , Cc cc ,
3207
3193
FlowState state , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored
3208
3194
) {
3209
- exists (
3210
- DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow ,
3211
- ApApprox innerArgApa , ApApprox apa
3212
- |
3213
- fwdFlowThroughStep1 ( pn1 , pn2 , pn3 , call , cc , state , ccc , summaryCtx , t , ap , apa ,
3214
- stored , ret , innerArgApa ) and
3215
- flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow , innerArgApa , apa ) and
3195
+ exists ( DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow |
3196
+ fwdFlowThroughStep1 ( pn1 , pn2 , pn3 , call , cc , state , ccc , summaryCtx , t , ap , _, stored ,
3197
+ ret , _) and
3198
+ flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow ) and
3216
3199
not inBarrier ( node , state ) and
3217
3200
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
3218
3201
)
0 commit comments