@@ -366,7 +366,7 @@ private module Stage1 {
366
366
exists ( Node mid , Node node , TypedContent tc |
367
367
not fullBarrier ( node , config ) and
368
368
useFieldFlow ( config ) and
369
- fwdFlow ( mid , config ) and
369
+ fwdFlow ( mid , _ , config ) and
370
370
store ( mid , tc , node , _) and
371
371
c = tc .getContent ( )
372
372
)
@@ -389,8 +389,8 @@ private module Stage1 {
389
389
}
390
390
391
391
pragma [ nomagic]
392
- private predicate fwdFlowOutFromArg ( DataFlowCall call , Node node , Configuration config ) {
393
- fwdFlowOut ( call , node , true , config )
392
+ private predicate fwdFlowOutFromArg ( DataFlowCall call , Node out , Configuration config ) {
393
+ fwdFlowOut ( call , out , true , config )
394
394
}
395
395
396
396
/**
@@ -584,21 +584,20 @@ private module Stage1 {
584
584
revFlow ( node , toReturn , config ) and exists ( returnAp ) and exists ( ap )
585
585
}
586
586
587
- private predicate throughFlowNodeCand1 ( Node node , Configuration config ) {
587
+ private predicate throughFlowNodeCand ( Node node , Configuration config ) {
588
588
revFlow ( node , true , config ) and
589
589
fwdFlow ( node , true , config ) and
590
- not fullBarrier ( node , config ) and
591
590
not inBarrier ( node , config ) and
592
591
not outBarrier ( node , config )
593
592
}
594
593
595
594
/** Holds if flow may return from `callable`. */
596
595
pragma [ nomagic]
597
- private predicate returnFlowCallableNodeCand1 (
596
+ private predicate returnFlowCallableNodeCand (
598
597
DataFlowCallable callable , ReturnKindExt kind , Configuration config
599
598
) {
600
599
exists ( ReturnNodeExt ret |
601
- throughFlowNodeCand1 ( ret , config ) and
600
+ throughFlowNodeCand ( ret , config ) and
602
601
callable = ret .getEnclosingCallable ( ) and
603
602
kind = ret .getKind ( )
604
603
)
@@ -610,8 +609,8 @@ private module Stage1 {
610
609
*/
611
610
predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , Ap ap , Configuration config ) {
612
611
exists ( ReturnKindExt kind |
613
- throughFlowNodeCand1 ( p , config ) and
614
- returnFlowCallableNodeCand1 ( c , kind , config ) and
612
+ throughFlowNodeCand ( p , config ) and
613
+ returnFlowCallableNodeCand ( c , kind , config ) and
615
614
p .getEnclosingCallable ( ) = c and
616
615
exists ( ap ) and
617
616
// we don't expect a parameter to return stored in itself
@@ -803,7 +802,7 @@ private module Stage2 {
803
802
CcNoCall ( ) { this = false }
804
803
}
805
804
806
- Cc ccAny ( ) { result = false }
805
+ Cc ccNone ( ) { result = false }
807
806
808
807
private class LocalCc = Unit ;
809
808
@@ -859,7 +858,7 @@ private module Stage2 {
859
858
predicate fwdFlow ( Node node , Cc cc , ApOption argAp , Ap ap , Configuration config ) {
860
859
flowCand ( node , _, config ) and
861
860
config .isSource ( node ) and
862
- cc = ccAny ( ) and
861
+ cc = ccNone ( ) and
863
862
argAp = apNone ( ) and
864
863
ap = getApNil ( node )
865
864
or
@@ -878,15 +877,15 @@ private module Stage2 {
878
877
fwdFlow ( mid , _, _, ap , config ) and
879
878
flowCand ( node , _, unbind ( config ) ) and
880
879
jumpStep ( mid , node , config ) and
881
- cc = ccAny ( ) and
880
+ cc = ccNone ( ) and
882
881
argAp = apNone ( )
883
882
)
884
883
or
885
884
exists ( Node mid , ApNil nil |
886
885
fwdFlow ( mid , _, _, nil , config ) and
887
886
flowCand ( node , _, unbind ( config ) ) and
888
887
additionalJumpStep ( mid , node , config ) and
889
- cc = ccAny ( ) and
888
+ cc = ccNone ( ) and
890
889
argAp = apNone ( ) and
891
890
ap = getApNil ( node )
892
891
)
@@ -970,13 +969,19 @@ private module Stage2 {
970
969
)
971
970
}
972
971
972
+ /**
973
+ * Holds if flow may exit from `call` at `out` with access path `ap`. The
974
+ * inner call context is `innercc`, but `ccOut` is just the call context
975
+ * based on the return step. In the case of through-flow `ccOut` is discarded
976
+ * and replaced by the outer call context as tracked by `fwdFlowIsEntered`.
977
+ */
973
978
pragma [ nomagic]
974
979
private predicate fwdFlowOut (
975
- DataFlowCall call , Node node , Cc innercc , Cc ccOut , ApOption argAp , Ap ap , Configuration config
980
+ DataFlowCall call , Node out , Cc innercc , Cc ccOut , ApOption argAp , Ap ap , Configuration config
976
981
) {
977
982
exists ( ReturnNodeExt ret , boolean allowsFieldFlow , DataFlowCallable inner |
978
983
fwdFlow ( ret , innercc , argAp , ap , config ) and
979
- flowOutOfCall ( call , ret , node , allowsFieldFlow , config ) and
984
+ flowOutOfCall ( call , ret , out , allowsFieldFlow , config ) and
980
985
inner = ret .getEnclosingCallable ( ) and
981
986
checkCallContextReturn ( innercc , inner , call ) and
982
987
ccOut = getCallContextReturn ( inner , call )
@@ -987,9 +992,9 @@ private module Stage2 {
987
992
988
993
pragma [ nomagic]
989
994
private predicate fwdFlowOutFromArg (
990
- DataFlowCall call , Node node , Ap argAp , Ap ap , Configuration config
995
+ DataFlowCall call , Node out , Ap argAp , Ap ap , Configuration config
991
996
) {
992
- fwdFlowOut ( call , node , any ( CcCall ccc ) , _, apSome ( argAp ) , ap , config )
997
+ fwdFlowOut ( call , out , any ( CcCall ccc ) , _, apSome ( argAp ) , ap , config )
993
998
}
994
999
995
1000
/**
@@ -1416,7 +1421,7 @@ private module Stage3 {
1416
1421
CcNoCall ( ) { this = false }
1417
1422
}
1418
1423
1419
- Cc ccAny ( ) { result = false }
1424
+ Cc ccNone ( ) { result = false }
1420
1425
1421
1426
private class LocalCc = Unit ;
1422
1427
@@ -1481,7 +1486,7 @@ private module Stage3 {
1481
1486
private predicate fwdFlow0 ( Node node , Cc cc , ApOption argAp , Ap ap , Configuration config ) {
1482
1487
flowCand ( node , _, config ) and
1483
1488
config .isSource ( node ) and
1484
- cc = ccAny ( ) and
1489
+ cc = ccNone ( ) and
1485
1490
argAp = apNone ( ) and
1486
1491
ap = getApNil ( node )
1487
1492
or
@@ -1500,15 +1505,15 @@ private module Stage3 {
1500
1505
fwdFlow ( mid , _, _, ap , config ) and
1501
1506
flowCand ( node , _, unbind ( config ) ) and
1502
1507
jumpStep ( mid , node , config ) and
1503
- cc = ccAny ( ) and
1508
+ cc = ccNone ( ) and
1504
1509
argAp = apNone ( )
1505
1510
)
1506
1511
or
1507
1512
exists ( Node mid , ApNil nil |
1508
1513
fwdFlow ( mid , _, _, nil , config ) and
1509
1514
flowCand ( node , _, unbind ( config ) ) and
1510
1515
additionalJumpStep ( mid , node , config ) and
1511
- cc = ccAny ( ) and
1516
+ cc = ccNone ( ) and
1512
1517
argAp = apNone ( ) and
1513
1518
ap = getApNil ( node )
1514
1519
)
@@ -1592,13 +1597,19 @@ private module Stage3 {
1592
1597
)
1593
1598
}
1594
1599
1600
+ /**
1601
+ * Holds if flow may exit from `call` at `out` with access path `ap`. The
1602
+ * inner call context is `innercc`, but `ccOut` is just the call context
1603
+ * based on the return step. In the case of through-flow `ccOut` is discarded
1604
+ * and replaced by the outer call context as tracked by `fwdFlowIsEntered`.
1605
+ */
1595
1606
pragma [ nomagic]
1596
1607
private predicate fwdFlowOut (
1597
- DataFlowCall call , Node node , Cc innercc , Cc ccOut , ApOption argAp , Ap ap , Configuration config
1608
+ DataFlowCall call , Node out , Cc innercc , Cc ccOut , ApOption argAp , Ap ap , Configuration config
1598
1609
) {
1599
1610
exists ( ReturnNodeExt ret , boolean allowsFieldFlow , DataFlowCallable inner |
1600
1611
fwdFlow ( ret , innercc , argAp , ap , config ) and
1601
- flowOutOfCall ( call , ret , node , allowsFieldFlow , config ) and
1612
+ flowOutOfCall ( call , ret , out , allowsFieldFlow , config ) and
1602
1613
inner = ret .getEnclosingCallable ( ) and
1603
1614
checkCallContextReturn ( innercc , inner , call ) and
1604
1615
ccOut = getCallContextReturn ( inner , call )
@@ -1609,9 +1620,9 @@ private module Stage3 {
1609
1620
1610
1621
pragma [ nomagic]
1611
1622
private predicate fwdFlowOutFromArg (
1612
- DataFlowCall call , Node node , Ap argAp , Ap ap , Configuration config
1623
+ DataFlowCall call , Node out , Ap argAp , Ap ap , Configuration config
1613
1624
) {
1614
- fwdFlowOut ( call , node , any ( CcCall ccc ) , _, apSome ( argAp ) , ap , config )
1625
+ fwdFlowOut ( call , out , any ( CcCall ccc ) , _, apSome ( argAp ) , ap , config )
1615
1626
}
1616
1627
1617
1628
/**
@@ -2096,7 +2107,7 @@ private module Stage4 {
2096
2107
2097
2108
class CcNoCall = CallContextNoCall ;
2098
2109
2099
- Cc ccAny ( ) { result instanceof CallContextAny }
2110
+ Cc ccNone ( ) { result instanceof CallContextAny }
2100
2111
2101
2112
private class LocalCc = LocalCallContext ;
2102
2113
@@ -2108,7 +2119,7 @@ private module Stage4 {
2108
2119
2109
2120
bindingset [ call, c]
2110
2121
private CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) {
2111
- if reducedViableImplInReturn ( c , call ) then result = TReturn ( c , call ) else result = ccAny ( )
2122
+ if reducedViableImplInReturn ( c , call ) then result = TReturn ( c , call ) else result = ccNone ( )
2112
2123
}
2113
2124
2114
2125
bindingset [ innercc, inner, call]
@@ -2153,6 +2164,7 @@ private module Stage4 {
2153
2164
bindingset [ node, ap]
2154
2165
private predicate filter ( Node node , Ap ap ) { any ( ) }
2155
2166
2167
+ // Type checking is not necessary here as it has already been done in stage 3.
2156
2168
bindingset [ ap, contentType]
2157
2169
private predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
2158
2170
@@ -2180,7 +2192,7 @@ private module Stage4 {
2180
2192
private predicate fwdFlow0 ( Node node , Cc cc , ApOption argAp , Ap ap , Configuration config ) {
2181
2193
flowCand ( node , _, config ) and
2182
2194
config .isSource ( node ) and
2183
- cc = ccAny ( ) and
2195
+ cc = ccNone ( ) and
2184
2196
argAp = apNone ( ) and
2185
2197
ap = getApNil ( node )
2186
2198
or
@@ -2199,15 +2211,15 @@ private module Stage4 {
2199
2211
fwdFlow ( mid , _, _, ap , config ) and
2200
2212
flowCand ( node , _, unbind ( config ) ) and
2201
2213
jumpStep ( mid , node , config ) and
2202
- cc = ccAny ( ) and
2214
+ cc = ccNone ( ) and
2203
2215
argAp = apNone ( )
2204
2216
)
2205
2217
or
2206
2218
exists ( Node mid , ApNil nil |
2207
2219
fwdFlow ( mid , _, _, nil , config ) and
2208
2220
flowCand ( node , _, unbind ( config ) ) and
2209
2221
additionalJumpStep ( mid , node , config ) and
2210
- cc = ccAny ( ) and
2222
+ cc = ccNone ( ) and
2211
2223
argAp = apNone ( ) and
2212
2224
ap = getApNil ( node )
2213
2225
)
@@ -2291,13 +2303,19 @@ private module Stage4 {
2291
2303
)
2292
2304
}
2293
2305
2306
+ /**
2307
+ * Holds if flow may exit from `call` at `out` with access path `ap`. The
2308
+ * inner call context is `innercc`, but `ccOut` is just the call context
2309
+ * based on the return step. In the case of through-flow `ccOut` is discarded
2310
+ * and replaced by the outer call context as tracked by `fwdFlowIsEntered`.
2311
+ */
2294
2312
pragma [ nomagic]
2295
2313
private predicate fwdFlowOut (
2296
- DataFlowCall call , Node node , Cc innercc , Cc ccOut , ApOption argAp , Ap ap , Configuration config
2314
+ DataFlowCall call , Node out , Cc innercc , Cc ccOut , ApOption argAp , Ap ap , Configuration config
2297
2315
) {
2298
2316
exists ( ReturnNodeExt ret , boolean allowsFieldFlow , DataFlowCallable inner |
2299
2317
fwdFlow ( ret , innercc , argAp , ap , config ) and
2300
- flowOutOfCall ( call , ret , node , allowsFieldFlow , config ) and
2318
+ flowOutOfCall ( call , ret , out , allowsFieldFlow , config ) and
2301
2319
inner = ret .getEnclosingCallable ( ) and
2302
2320
checkCallContextReturn ( innercc , inner , call ) and
2303
2321
ccOut = getCallContextReturn ( inner , call )
@@ -2308,9 +2326,9 @@ private module Stage4 {
2308
2326
2309
2327
pragma [ nomagic]
2310
2328
private predicate fwdFlowOutFromArg (
2311
- DataFlowCall call , Node node , Ap argAp , Ap ap , Configuration config
2329
+ DataFlowCall call , Node out , Ap argAp , Ap ap , Configuration config
2312
2330
) {
2313
- fwdFlowOut ( call , node , any ( CcCall ccc ) , _, apSome ( argAp ) , ap , config )
2331
+ fwdFlowOut ( call , out , any ( CcCall ccc ) , _, apSome ( argAp ) , ap , config )
2314
2332
}
2315
2333
2316
2334
/**
0 commit comments