@@ -1005,8 +1005,9 @@ private module Stage1 implements StageSig {
1005
1005
}
1006
1006
1007
1007
pragma [ nomagic]
1008
- predicate returnMayFlowThrough ( RetNodeEx ret , Configuration config ) {
1009
- throughFlowNodeCand ( ret , config )
1008
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1009
+ throughFlowNodeCand ( ret , config ) and
1010
+ pos = ret .getReturnPosition ( )
1010
1011
}
1011
1012
1012
1013
pragma [ nomagic]
@@ -1065,9 +1066,10 @@ private predicate viableReturnPosOutNodeCand1(
1065
1066
*/
1066
1067
pragma [ nomagic]
1067
1068
private predicate flowOutOfCallNodeCand1 (
1068
- DataFlowCall call , RetNodeEx ret , NodeEx out , Configuration config
1069
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , Configuration config
1069
1070
) {
1070
- viableReturnPosOutNodeCand1 ( call , ret .getReturnPosition ( ) , out , config ) and
1071
+ viableReturnPosOutNodeCand1 ( call , pos , out , config ) and
1072
+ pos = ret .getReturnPosition ( ) and
1071
1073
Stage1:: revFlow ( ret , config ) and
1072
1074
not outBarrier ( ret , config ) and
1073
1075
not inBarrier ( out , config )
@@ -1103,7 +1105,7 @@ private predicate flowIntoCallNodeCand1(
1103
1105
private int branch ( NodeEx n1 , Configuration conf ) {
1104
1106
result =
1105
1107
strictcount ( NodeEx n |
1106
- flowOutOfCallNodeCand1 ( _, n1 , n , conf ) or flowIntoCallNodeCand1 ( _, n1 , n , conf )
1108
+ flowOutOfCallNodeCand1 ( _, n1 , _ , n , conf ) or flowIntoCallNodeCand1 ( _, n1 , n , conf )
1107
1109
)
1108
1110
}
1109
1111
@@ -1115,7 +1117,7 @@ private int branch(NodeEx n1, Configuration conf) {
1115
1117
private int join ( NodeEx n2 , Configuration conf ) {
1116
1118
result =
1117
1119
strictcount ( NodeEx n |
1118
- flowOutOfCallNodeCand1 ( _, n , n2 , conf ) or flowIntoCallNodeCand1 ( _, n , n2 , conf )
1120
+ flowOutOfCallNodeCand1 ( _, n , _ , n2 , conf ) or flowIntoCallNodeCand1 ( _, n , n2 , conf )
1119
1121
)
1120
1122
}
1121
1123
@@ -1128,12 +1130,13 @@ private int join(NodeEx n2, Configuration conf) {
1128
1130
*/
1129
1131
pragma [ nomagic]
1130
1132
private predicate flowOutOfCallNodeCand1 (
1131
- DataFlowCall call , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow , Configuration config
1133
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1134
+ Configuration config
1132
1135
) {
1133
- flowOutOfCallNodeCand1 ( call , ret , out , config ) and
1136
+ flowOutOfCallNodeCand1 ( call , ret , pos , out , pragma [ only_bind_into ] ( config ) ) and
1134
1137
exists ( int b , int j |
1135
- b = branch ( ret , config ) and
1136
- j = join ( out , config ) and
1138
+ b = branch ( ret , pragma [ only_bind_into ] ( config ) ) and
1139
+ j = join ( out , pragma [ only_bind_into ] ( config ) ) and
1137
1140
if b .minimum ( j ) <= config .fieldFlowBranchLimit ( )
1138
1141
then allowsFieldFlow = true
1139
1142
else allowsFieldFlow = false
@@ -1171,7 +1174,7 @@ private signature module StageSig {
1171
1174
1172
1175
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) ;
1173
1176
1174
- predicate returnMayFlowThrough ( RetNodeEx ret , Configuration config ) ;
1177
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) ;
1175
1178
1176
1179
predicate storeStepCand (
1177
1180
NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType ,
@@ -1237,7 +1240,8 @@ private module MkStage<StageSig PrevStage> {
1237
1240
) ;
1238
1241
1239
1242
predicate flowOutOfCall (
1240
- DataFlowCall call , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow , Configuration config
1243
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1244
+ Configuration config
1241
1245
) ;
1242
1246
1243
1247
predicate flowIntoCall (
@@ -1262,13 +1266,16 @@ private module MkStage<StageSig PrevStage> {
1262
1266
1263
1267
pragma [ nomagic]
1264
1268
private predicate flowThroughOutOfCall (
1265
- DataFlowCall call , CcCall ccc , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1266
- Configuration config
1269
+ DataFlowCall call , CcCall ccc , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1270
+ boolean allowsFieldFlow , Configuration config
1267
1271
) {
1268
- flowOutOfCall ( call , ret , out , allowsFieldFlow , pragma [ only_bind_into ] ( config ) ) and
1269
- PrevStage:: callMayFlowThroughRev ( call , pragma [ only_bind_into ] ( config ) ) and
1270
- PrevStage:: returnMayFlowThrough ( ret , pragma [ only_bind_into ] ( config ) ) and
1271
- matchesCall ( ccc , call )
1272
+ exists ( ReturnPosition pos |
1273
+ flowOutOfCall ( call , ret , pos , out , allowsFieldFlow , pragma [ only_bind_into ] ( config ) ) and
1274
+ kind = pos .getKind ( ) and
1275
+ PrevStage:: callMayFlowThroughRev ( call , pragma [ only_bind_into ] ( config ) ) and
1276
+ PrevStage:: returnMayFlowThrough ( ret , pos , pragma [ only_bind_into ] ( config ) ) and
1277
+ matchesCall ( ccc , call )
1278
+ )
1272
1279
}
1273
1280
1274
1281
/**
@@ -1429,7 +1436,7 @@ private module MkStage<StageSig PrevStage> {
1429
1436
DataFlowCallable inner
1430
1437
|
1431
1438
fwdFlow ( ret , state , innercc , summaryCtx , argAp , ap , config ) and
1432
- flowOutOfCall ( call , ret , out , allowsFieldFlow , config ) and
1439
+ flowOutOfCall ( call , ret , _ , out , allowsFieldFlow , config ) and
1433
1440
inner = ret .getEnclosingCallable ( ) and
1434
1441
ccOut = getCallContextReturn ( inner , call , innercc ) and
1435
1442
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
@@ -1441,11 +1448,11 @@ private module MkStage<StageSig PrevStage> {
1441
1448
DataFlowCall call , NodeEx out , FlowState state , ParamNode summaryCtx , Ap argAp , Ap ap ,
1442
1449
Configuration config
1443
1450
) {
1444
- exists ( RetNodeEx ret , boolean allowsFieldFlow , CcCall ccc |
1451
+ exists ( RetNodeEx ret , ReturnKindExt kind , boolean allowsFieldFlow , CcCall ccc |
1445
1452
fwdFlow ( ret , state , ccc , TParamNodeSome ( summaryCtx ) , apSome ( argAp ) , ap , config ) and
1446
- flowThroughOutOfCall ( call , ccc , ret , out , allowsFieldFlow , config ) and
1453
+ flowThroughOutOfCall ( call , ccc , ret , kind , out , allowsFieldFlow , config ) and
1447
1454
( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1448
- parameterFlowThroughAllowed ( summaryCtx , ret . getKind ( ) )
1455
+ parameterFlowThroughAllowed ( summaryCtx , kind )
1449
1456
)
1450
1457
}
1451
1458
@@ -1483,10 +1490,12 @@ private module MkStage<StageSig PrevStage> {
1483
1490
1484
1491
pragma [ nomagic]
1485
1492
private predicate returnFlowsThrough (
1486
- RetNodeEx ret , FlowState state , CcCall ccc , ParamNode p , Ap argAp , Ap ap , Configuration config
1493
+ RetNodeEx ret , ReturnPosition pos , FlowState state , CcCall ccc , ParamNode p , Ap argAp , Ap ap ,
1494
+ Configuration config
1487
1495
) {
1488
1496
fwdFlow ( ret , state , ccc , TParamNodeSome ( p ) , apSome ( argAp ) , ap , config ) and
1489
- parameterFlowThroughAllowed ( p , ret .getKind ( ) )
1497
+ pos = ret .getReturnPosition ( ) and
1498
+ parameterFlowThroughAllowed ( p , pos .getKind ( ) )
1490
1499
}
1491
1500
1492
1501
pragma [ nomagic]
@@ -1496,7 +1505,7 @@ private module MkStage<StageSig PrevStage> {
1496
1505
flowIntoCall ( call , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) , allowsFieldFlow ,
1497
1506
pragma [ only_bind_into ] ( config ) ) and
1498
1507
fwdFlow ( arg , _, _, _, _, _, pragma [ only_bind_into ] ( config ) ) and
1499
- returnFlowsThrough ( _, _, _, p .asNode ( ) , _, _, pragma [ only_bind_into ] ( config ) )
1508
+ returnFlowsThrough ( _, _, _, _ , p .asNode ( ) , _, _, pragma [ only_bind_into ] ( config ) )
1500
1509
}
1501
1510
1502
1511
/**
@@ -1592,13 +1601,15 @@ private module MkStage<StageSig PrevStage> {
1592
1601
)
1593
1602
or
1594
1603
// flow out of a callable
1595
- revFlowOut ( _, node , state , _, _, ap , config ) and
1596
- if returnFlowsThrough ( node , state , _, _, _, ap , config )
1597
- then (
1598
- returnCtx = TReturnCtxMaybeFlowThrough ( node .( RetNodeEx ) .getReturnPosition ( ) ) and
1599
- returnAp = apSome ( ap )
1600
- ) else (
1601
- returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
1604
+ exists ( ReturnPosition pos |
1605
+ revFlowOut ( _, node , pos , state , _, _, ap , config ) and
1606
+ if returnFlowsThrough ( node , pos , state , _, _, _, ap , config )
1607
+ then (
1608
+ returnCtx = TReturnCtxMaybeFlowThrough ( pos ) and
1609
+ returnAp = apSome ( ap )
1610
+ ) else (
1611
+ returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
1612
+ )
1602
1613
)
1603
1614
}
1604
1615
@@ -1627,12 +1638,12 @@ private module MkStage<StageSig PrevStage> {
1627
1638
1628
1639
pragma [ nomagic]
1629
1640
private predicate revFlowOut (
1630
- DataFlowCall call , RetNodeEx ret , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
1631
- Ap ap , Configuration config
1641
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , FlowState state , ReturnCtx returnCtx ,
1642
+ ApOption returnAp , Ap ap , Configuration config
1632
1643
) {
1633
1644
exists ( NodeEx out , boolean allowsFieldFlow |
1634
1645
revFlow ( out , state , returnCtx , returnAp , ap , config ) and
1635
- flowOutOfCall ( call , ret , out , allowsFieldFlow , config ) and
1646
+ flowOutOfCall ( call , ret , pos , out , allowsFieldFlow , config ) and
1636
1647
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1637
1648
)
1638
1649
}
@@ -1672,9 +1683,8 @@ private module MkStage<StageSig PrevStage> {
1672
1683
Configuration config
1673
1684
) {
1674
1685
exists ( RetNodeEx ret , FlowState state , CcCall ccc |
1675
- revFlowOut ( call , ret , state , returnCtx , returnAp , ap , config ) and
1676
- returnFlowsThrough ( ret , state , ccc , _, _, ap , config ) and
1677
- pos = ret .getReturnPosition ( ) and
1686
+ revFlowOut ( call , ret , pos , state , returnCtx , returnAp , ap , config ) and
1687
+ returnFlowsThrough ( ret , pos , state , ccc , _, _, ap , config ) and
1678
1688
matchesCall ( ccc , call )
1679
1689
)
1680
1690
}
@@ -1755,17 +1765,17 @@ private module MkStage<StageSig PrevStage> {
1755
1765
1756
1766
pragma [ nomagic]
1757
1767
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) {
1758
- exists ( RetNodeEx ret |
1759
- returnFlowsThrough ( ret , _, _, p .asNode ( ) , ap , _, config ) and
1760
- parameterFlowsThroughRev ( p , ap , ret . getReturnPosition ( ) , config )
1768
+ exists ( RetNodeEx ret , ReturnPosition pos |
1769
+ returnFlowsThrough ( ret , pos , _, _, p .asNode ( ) , ap , _, config ) and
1770
+ parameterFlowsThroughRev ( p , ap , pos , config )
1761
1771
)
1762
1772
}
1763
1773
1764
1774
pragma [ nomagic]
1765
- predicate returnMayFlowThrough ( RetNodeEx ret , Configuration config ) {
1775
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1766
1776
exists ( ParamNodeEx p , Ap ap |
1767
- returnFlowsThrough ( ret , _, _, p .asNode ( ) , ap , _, config ) and
1768
- parameterFlowsThroughRev ( p , ap , ret . getReturnPosition ( ) , config )
1777
+ returnFlowsThrough ( ret , pos , _, _, p .asNode ( ) , ap , _, config ) and
1778
+ parameterFlowsThroughRev ( p , ap , pos , config )
1769
1779
)
1770
1780
}
1771
1781
@@ -1946,7 +1956,7 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
1946
1956
exists ( lcc )
1947
1957
}
1948
1958
1949
- predicate flowOutOfCall = flowOutOfCallNodeCand1 / 5 ;
1959
+ predicate flowOutOfCall = flowOutOfCallNodeCand1 / 6 ;
1950
1960
1951
1961
predicate flowIntoCall = flowIntoCallNodeCand1 / 5 ;
1952
1962
@@ -1982,9 +1992,10 @@ private module Stage2 implements StageSig {
1982
1992
1983
1993
pragma [ nomagic]
1984
1994
private predicate flowOutOfCallNodeCand2 (
1985
- DataFlowCall call , RetNodeEx node1 , NodeEx node2 , boolean allowsFieldFlow , Configuration config
1995
+ DataFlowCall call , RetNodeEx node1 , ReturnPosition pos , NodeEx node2 , boolean allowsFieldFlow ,
1996
+ Configuration config
1986
1997
) {
1987
- flowOutOfCallNodeCand1 ( call , node1 , node2 , allowsFieldFlow , config ) and
1998
+ flowOutOfCallNodeCand1 ( call , node1 , pos , node2 , allowsFieldFlow , config ) and
1988
1999
Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( config ) ) and
1989
2000
Stage2:: revFlowAlias ( node1 , pragma [ only_bind_into ] ( config ) )
1990
2001
}
@@ -2053,7 +2064,7 @@ private module LocalFlowBigStep {
2053
2064
jumpStep ( node , next , config ) or
2054
2065
additionalJumpStep ( node , next , config ) or
2055
2066
flowIntoCallNodeCand2 ( _, node , next , _, config ) or
2056
- flowOutOfCallNodeCand2 ( _, node , next , _, config ) or
2067
+ flowOutOfCallNodeCand2 ( _, node , _ , next , _, config ) or
2057
2068
Stage2:: storeStepCand ( node , _, _, next , _, config ) or
2058
2069
Stage2:: readStepCand ( node , _, next , config )
2059
2070
)
@@ -2194,7 +2205,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
2194
2205
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , ap , config , _) and exists ( lcc )
2195
2206
}
2196
2207
2197
- predicate flowOutOfCall = flowOutOfCallNodeCand2 / 5 ;
2208
+ predicate flowOutOfCall = flowOutOfCallNodeCand2 / 6 ;
2198
2209
2199
2210
predicate flowIntoCall = flowIntoCallNodeCand2 / 5 ;
2200
2211
@@ -2500,10 +2511,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
2500
2511
2501
2512
pragma [ nomagic]
2502
2513
predicate flowOutOfCall (
2503
- DataFlowCall call , RetNodeEx node1 , NodeEx node2 , boolean allowsFieldFlow , Configuration config
2514
+ DataFlowCall call , RetNodeEx node1 , ReturnPosition pos , NodeEx node2 , boolean allowsFieldFlow ,
2515
+ Configuration config
2504
2516
) {
2505
2517
exists ( FlowState state |
2506
- flowOutOfCallNodeCand2 ( call , node1 , node2 , allowsFieldFlow , config ) and
2518
+ flowOutOfCallNodeCand2 ( call , node1 , pos , node2 , allowsFieldFlow , config ) and
2507
2519
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _, pragma [ only_bind_into ] ( config ) ) and
2508
2520
PrevStage:: revFlowAlias ( node1 , pragma [ only_bind_into ] ( state ) , _,
2509
2521
pragma [ only_bind_into ] ( config ) )
0 commit comments