@@ -1022,9 +1022,9 @@ private module Stage1 implements StageSig {
1022
1022
}
1023
1023
1024
1024
pragma [ nomagic]
1025
- predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1025
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind , Configuration config ) {
1026
1026
throughFlowNodeCand ( ret , config ) and
1027
- pos = ret .getReturnPosition ( )
1027
+ kind = ret .getKind ( )
1028
1028
}
1029
1029
1030
1030
pragma [ nomagic]
@@ -1083,13 +1083,16 @@ private predicate viableReturnPosOutNodeCand1(
1083
1083
*/
1084
1084
pragma [ nomagic]
1085
1085
private predicate flowOutOfCallNodeCand1 (
1086
- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , Configuration config
1086
+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , Configuration config
1087
1087
) {
1088
- viableReturnPosOutNodeCand1 ( call , pos , out , config ) and
1089
- pos = ret .getReturnPosition ( ) and
1090
- Stage1:: revFlow ( ret , config ) and
1091
- not outBarrier ( ret , config ) and
1092
- not inBarrier ( out , config )
1088
+ exists ( ReturnPosition pos |
1089
+ viableReturnPosOutNodeCand1 ( call , pos , out , config ) and
1090
+ pos = ret .getReturnPosition ( ) and
1091
+ kind = pos .getKind ( ) and
1092
+ Stage1:: revFlow ( ret , config ) and
1093
+ not outBarrier ( ret , config ) and
1094
+ not inBarrier ( out , config )
1095
+ )
1093
1096
}
1094
1097
1095
1098
pragma [ nomagic]
@@ -1149,10 +1152,10 @@ private int join(NodeEx n2, Configuration conf) {
1149
1152
*/
1150
1153
pragma [ nomagic]
1151
1154
private predicate flowOutOfCallNodeCand1 (
1152
- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1155
+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
1153
1156
Configuration config
1154
1157
) {
1155
- flowOutOfCallNodeCand1 ( call , ret , pos , out , pragma [ only_bind_into ] ( config ) ) and
1158
+ flowOutOfCallNodeCand1 ( call , ret , kind , out , pragma [ only_bind_into ] ( config ) ) and
1156
1159
exists ( int b , int j |
1157
1160
b = branch ( ret , pragma [ only_bind_into ] ( config ) ) and
1158
1161
j = join ( out , pragma [ only_bind_into ] ( config ) ) and
@@ -1193,7 +1196,7 @@ private signature module StageSig {
1193
1196
1194
1197
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) ;
1195
1198
1196
- predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) ;
1199
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind , Configuration config ) ;
1197
1200
1198
1201
predicate storeStepCand (
1199
1202
NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType ,
@@ -1259,7 +1262,7 @@ private module MkStage<StageSig PrevStage> {
1259
1262
) ;
1260
1263
1261
1264
predicate flowOutOfCall (
1262
- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1265
+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
1263
1266
Configuration config
1264
1267
) ;
1265
1268
@@ -1288,14 +1291,11 @@ private module MkStage<StageSig PrevStage> {
1288
1291
DataFlowCall call , DataFlowCallable c , CcCall ccc , RetNodeEx ret , ReturnKindExt kind ,
1289
1292
NodeEx out , boolean allowsFieldFlow , Configuration config
1290
1293
) {
1291
- exists ( ReturnPosition pos |
1292
- flowOutOfCall ( call , ret , pos , out , allowsFieldFlow , pragma [ only_bind_into ] ( config ) ) and
1293
- kind = pos .getKind ( ) and
1294
- PrevStage:: callMayFlowThroughRev ( call , pragma [ only_bind_into ] ( config ) ) and
1295
- PrevStage:: returnMayFlowThrough ( ret , pos , pragma [ only_bind_into ] ( config ) ) and
1296
- matchesCall ( ccc , call ) and
1297
- c = ret .getEnclosingCallable ( )
1298
- )
1294
+ flowOutOfCall ( call , ret , kind , out , allowsFieldFlow , pragma [ only_bind_into ] ( config ) ) and
1295
+ PrevStage:: callMayFlowThroughRev ( call , pragma [ only_bind_into ] ( config ) ) and
1296
+ PrevStage:: returnMayFlowThrough ( ret , kind , pragma [ only_bind_into ] ( config ) ) and
1297
+ matchesCall ( ccc , call ) and
1298
+ c = ret .getEnclosingCallable ( )
1299
1299
}
1300
1300
1301
1301
/**
@@ -1507,27 +1507,26 @@ private module MkStage<StageSig PrevStage> {
1507
1507
1508
1508
pragma [ nomagic]
1509
1509
private predicate returnFlowsThrough0 (
1510
- RetNodeEx ret , FlowState state , CcCall ccc , DataFlowCallable c , ParameterPosition ppos ,
1511
- Ap argAp , Ap ap , Configuration config
1510
+ RetNodeEx ret , ReturnKindExt kind , FlowState state , CcCall ccc , DataFlowCallable c ,
1511
+ ParameterPosition ppos , Ap argAp , Ap ap , Configuration config
1512
1512
) {
1513
1513
exists ( boolean allowsFieldFlow |
1514
1514
fwdFlow ( ret , state , ccc , TParameterPositionSome ( ppos ) , apSome ( argAp ) , ap , config ) and
1515
- flowThroughOutOfCall ( _, c , _, pragma [ only_bind_into ] ( ret ) , _ , _, allowsFieldFlow ,
1515
+ flowThroughOutOfCall ( _, c , _, pragma [ only_bind_into ] ( ret ) , kind , _, allowsFieldFlow ,
1516
1516
pragma [ only_bind_into ] ( config ) ) and
1517
1517
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1518
1518
)
1519
1519
}
1520
1520
1521
1521
pragma [ nomagic]
1522
1522
private predicate returnFlowsThrough (
1523
- RetNodeEx ret , ReturnPosition pos , FlowState state , CcCall ccc , ParamNodeEx p , Ap argAp ,
1523
+ RetNodeEx ret , ReturnKindExt kind , FlowState state , CcCall ccc , ParamNodeEx p , Ap argAp ,
1524
1524
Ap ap , Configuration config
1525
1525
) {
1526
1526
exists ( DataFlowCallable c , ParameterPosition ppos |
1527
- returnFlowsThrough0 ( ret , state , ccc , c , ppos , argAp , ap , config ) and
1527
+ returnFlowsThrough0 ( ret , kind , state , ccc , c , ppos , argAp , ap , config ) and
1528
1528
p .isParameterOf ( c , ppos ) and
1529
- pos = ret .getReturnPosition ( ) and
1530
- parameterFlowThroughAllowed ( p , pos .getKind ( ) )
1529
+ parameterFlowThroughAllowed ( p , kind )
1531
1530
)
1532
1531
}
1533
1532
@@ -1631,17 +1630,17 @@ private module MkStage<StageSig PrevStage> {
1631
1630
returnCtx = TReturnCtxNone ( )
1632
1631
or
1633
1632
// flow through a callable
1634
- exists ( DataFlowCall call , ReturnPosition returnPos0 , Ap returnAp0 |
1635
- revFlowInToReturn ( call , node , state , returnPos0 , returnAp0 , ap , config ) and
1636
- revFlowIsReturned ( call , returnCtx , returnAp , returnPos0 , returnAp0 , config )
1633
+ exists ( DataFlowCall call , ReturnKindExt returnKind0 , Ap returnAp0 |
1634
+ revFlowInToReturn ( call , node , state , returnKind0 , returnAp0 , ap , config ) and
1635
+ revFlowIsReturned ( call , returnCtx , returnAp , returnKind0 , returnAp0 , config )
1637
1636
)
1638
1637
or
1639
1638
// flow out of a callable
1640
- exists ( ReturnPosition pos |
1641
- revFlowOut ( _, node , pos , state , _, _, ap , config ) and
1642
- if returnFlowsThrough ( node , pos , state , _, _, _, ap , config )
1639
+ exists ( ReturnKindExt kind |
1640
+ revFlowOut ( _, node , kind , state , _, _, ap , config ) and
1641
+ if returnFlowsThrough ( node , kind , state , _, _, _, ap , config )
1643
1642
then (
1644
- returnCtx = TReturnCtxMaybeFlowThrough ( pos ) and
1643
+ returnCtx = TReturnCtxMaybeFlowThrough ( kind ) and
1645
1644
returnAp = apSome ( ap )
1646
1645
) else (
1647
1646
returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
@@ -1674,12 +1673,12 @@ private module MkStage<StageSig PrevStage> {
1674
1673
1675
1674
pragma [ nomagic]
1676
1675
private predicate revFlowOut (
1677
- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , FlowState state , ReturnCtx returnCtx ,
1676
+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , FlowState state , ReturnCtx returnCtx ,
1678
1677
ApOption returnAp , Ap ap , Configuration config
1679
1678
) {
1680
1679
exists ( NodeEx out , boolean allowsFieldFlow |
1681
1680
revFlow ( out , state , returnCtx , returnAp , ap , config ) and
1682
- flowOutOfCall ( call , ret , pos , out , allowsFieldFlow , config ) and
1681
+ flowOutOfCall ( call , ret , kind , out , allowsFieldFlow , config ) and
1683
1682
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1684
1683
)
1685
1684
}
@@ -1697,14 +1696,15 @@ private module MkStage<StageSig PrevStage> {
1697
1696
1698
1697
pragma [ nomagic]
1699
1698
private predicate revFlowInToReturn (
1700
- DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnPosition returnPos , Ap returnAp ,
1701
- Ap ap , Configuration config
1699
+ DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnKindExt kind , Ap returnAp , Ap ap ,
1700
+ Configuration config
1702
1701
) {
1703
1702
exists ( ParamNodeEx p , boolean allowsFieldFlow |
1704
- revFlow ( p , state , TReturnCtxMaybeFlowThrough ( returnPos ) , apSome ( returnAp ) , ap , config ) and
1703
+ revFlow ( pragma [ only_bind_into ] ( p ) , state ,
1704
+ TReturnCtxMaybeFlowThrough ( pragma [ only_bind_into ] ( kind ) ) , apSome ( returnAp ) , ap , config ) and
1705
1705
flowThroughIntoCall ( call , arg , p , allowsFieldFlow , config ) and
1706
1706
( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1707
- parameterFlowThroughAllowed ( p , returnPos . getKind ( ) )
1707
+ parameterFlowThroughAllowed ( p , kind )
1708
1708
)
1709
1709
}
1710
1710
@@ -1715,12 +1715,12 @@ private module MkStage<StageSig PrevStage> {
1715
1715
*/
1716
1716
pragma [ nomagic]
1717
1717
private predicate revFlowIsReturned (
1718
- DataFlowCall call , ReturnCtx returnCtx , ApOption returnAp , ReturnPosition pos , Ap ap ,
1718
+ DataFlowCall call , ReturnCtx returnCtx , ApOption returnAp , ReturnKindExt kind , Ap ap ,
1719
1719
Configuration config
1720
1720
) {
1721
1721
exists ( RetNodeEx ret , FlowState state , CcCall ccc |
1722
- revFlowOut ( call , ret , pos , state , returnCtx , returnAp , ap , config ) and
1723
- returnFlowsThrough ( ret , pos , state , ccc , _, _, ap , config ) and
1722
+ revFlowOut ( call , ret , kind , state , returnCtx , returnAp , ap , config ) and
1723
+ returnFlowsThrough ( ret , kind , state , ccc , _, _, ap , config ) and
1724
1724
matchesCall ( ccc , call )
1725
1725
)
1726
1726
}
@@ -1793,37 +1793,37 @@ private module MkStage<StageSig PrevStage> {
1793
1793
1794
1794
pragma [ nomagic]
1795
1795
private predicate parameterFlowsThroughRev (
1796
- ParamNodeEx p , Ap ap , ReturnPosition returnPos , Configuration config
1796
+ ParamNodeEx p , Ap ap , ReturnKindExt kind , Configuration config
1797
1797
) {
1798
- revFlow ( p , _, TReturnCtxMaybeFlowThrough ( returnPos ) , apSome ( _) , ap , config ) and
1799
- parameterFlowThroughAllowed ( p , returnPos . getKind ( ) )
1798
+ revFlow ( p , _, TReturnCtxMaybeFlowThrough ( kind ) , apSome ( _) , ap , config ) and
1799
+ parameterFlowThroughAllowed ( p , kind )
1800
1800
}
1801
1801
1802
1802
pragma [ nomagic]
1803
1803
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) {
1804
- exists ( RetNodeEx ret , ReturnPosition pos |
1805
- returnFlowsThrough ( ret , pos , _, _, p , ap , _, config ) and
1806
- parameterFlowsThroughRev ( p , ap , pos , config )
1804
+ exists ( RetNodeEx ret , ReturnKindExt kind |
1805
+ returnFlowsThrough ( ret , kind , _, _, p , ap , _, config ) and
1806
+ parameterFlowsThroughRev ( p , ap , kind , config )
1807
1807
)
1808
1808
}
1809
1809
1810
1810
pragma [ nomagic]
1811
- predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1811
+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind , Configuration config ) {
1812
1812
exists ( ParamNodeEx p , Ap ap |
1813
- returnFlowsThrough ( ret , pos , _, _, p , ap , _, config ) and
1814
- parameterFlowsThroughRev ( p , ap , pos , config )
1813
+ returnFlowsThrough ( ret , kind , _, _, p , ap , _, config ) and
1814
+ parameterFlowsThroughRev ( p , ap , kind , config )
1815
1815
)
1816
1816
}
1817
1817
1818
1818
pragma [ nomagic]
1819
1819
predicate callMayFlowThroughRev ( DataFlowCall call , Configuration config ) {
1820
1820
exists (
1821
- ReturnPosition returnPos0 , Ap returnAp0 , ArgNodeEx arg , FlowState state ,
1821
+ ReturnKindExt returnKind0 , Ap returnAp0 , ArgNodeEx arg , FlowState state ,
1822
1822
ReturnCtx returnCtx , ApOption returnAp , Ap ap
1823
1823
|
1824
1824
revFlow ( arg , state , returnCtx , returnAp , ap , config ) and
1825
- revFlowInToReturn ( call , arg , state , returnPos0 , returnAp0 , ap , config ) and
1826
- revFlowIsReturned ( call , returnCtx , returnAp , returnPos0 , returnAp0 , config )
1825
+ revFlowInToReturn ( call , arg , state , returnKind0 , returnAp0 , ap , config ) and
1826
+ revFlowIsReturned ( call , returnCtx , returnAp , returnKind0 , returnAp0 , config )
1827
1827
)
1828
1828
}
1829
1829
@@ -2027,10 +2027,10 @@ private module Stage2 implements StageSig {
2027
2027
2028
2028
pragma [ nomagic]
2029
2029
private predicate flowOutOfCallNodeCand2 (
2030
- DataFlowCall call , RetNodeEx node1 , ReturnPosition pos , NodeEx node2 , boolean allowsFieldFlow ,
2030
+ DataFlowCall call , RetNodeEx node1 , ReturnKindExt kind , NodeEx node2 , boolean allowsFieldFlow ,
2031
2031
Configuration config
2032
2032
) {
2033
- flowOutOfCallNodeCand1 ( call , node1 , pos , node2 , allowsFieldFlow , config ) and
2033
+ flowOutOfCallNodeCand1 ( call , node1 , kind , node2 , allowsFieldFlow , config ) and
2034
2034
Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( config ) ) and
2035
2035
Stage2:: revFlowAlias ( node1 , pragma [ only_bind_into ] ( config ) )
2036
2036
}
@@ -2546,11 +2546,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
2546
2546
2547
2547
pragma [ nomagic]
2548
2548
predicate flowOutOfCall (
2549
- DataFlowCall call , RetNodeEx node1 , ReturnPosition pos , NodeEx node2 , boolean allowsFieldFlow ,
2549
+ DataFlowCall call , RetNodeEx node1 , ReturnKindExt kind , NodeEx node2 , boolean allowsFieldFlow ,
2550
2550
Configuration config
2551
2551
) {
2552
2552
exists ( FlowState state |
2553
- flowOutOfCallNodeCand2 ( call , node1 , pos , node2 , allowsFieldFlow , config ) and
2553
+ flowOutOfCallNodeCand2 ( call , node1 , kind , node2 , allowsFieldFlow , config ) and
2554
2554
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _, pragma [ only_bind_into ] ( config ) ) and
2555
2555
PrevStage:: revFlowAlias ( node1 , pragma [ only_bind_into ] ( state ) , _,
2556
2556
pragma [ only_bind_into ] ( config ) )
0 commit comments