@@ -1508,26 +1508,28 @@ private module MkStage<StageSig PrevStage> {
1508
1508
1509
1509
pragma [ nomagic]
1510
1510
private predicate fwdFlowRetFromArg (
1511
- RetNodeEx ret , ReturnKindExt kind , FlowState state , CcCall ccc , ParamNodeEx summaryCtx ,
1512
- Ap argAp , ApApprox argApa , Ap ap , ApApprox apa , Configuration config
1511
+ RetNodeEx ret , FlowState state , CcCall ccc , ParamNodeEx summaryCtx , Ap argAp , ApApprox argApa ,
1512
+ Ap ap , ApApprox apa , Configuration config
1513
1513
) {
1514
- fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc ,
1515
- TParamNodeSome ( pragma [ only_bind_into ] ( summaryCtx .asNode ( ) ) ) ,
1516
- pragma [ only_bind_into ] ( apSome ( argAp ) ) , ap , pragma [ only_bind_into ] ( apa ) ,
1517
- pragma [ only_bind_into ] ( config ) ) and
1518
- kind = ret .getKind ( ) and
1519
- parameterFlowThroughAllowed ( summaryCtx , kind ) and
1520
- argApa = getApprox ( argAp ) and
1521
- PrevStage:: returnMayFlowThrough ( ret , argApa , apa , kind , pragma [ only_bind_into ] ( config ) )
1514
+ exists ( ReturnKindExt kind |
1515
+ fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc ,
1516
+ TParamNodeSome ( pragma [ only_bind_into ] ( summaryCtx .asNode ( ) ) ) ,
1517
+ pragma [ only_bind_into ] ( apSome ( argAp ) ) , ap , pragma [ only_bind_into ] ( apa ) ,
1518
+ pragma [ only_bind_into ] ( config ) ) and
1519
+ kind = ret .getKind ( ) and
1520
+ parameterFlowThroughAllowed ( summaryCtx , kind ) and
1521
+ argApa = getApprox ( argAp ) and
1522
+ PrevStage:: returnMayFlowThrough ( ret , argApa , apa , kind , pragma [ only_bind_into ] ( config ) )
1523
+ )
1522
1524
}
1523
1525
1524
1526
pragma [ inline]
1525
1527
private predicate fwdFlowThrough0 (
1526
1528
DataFlowCall call , Cc cc , FlowState state , CcCall ccc , ParamNodeOption summaryCtx ,
1527
- ApOption argAp , Ap ap , ApApprox apa , RetNodeEx ret , ReturnKindExt kind ,
1528
- ParamNodeEx innerSummaryCtx , Ap innerArgAp , ApApprox innerArgApa , Configuration config
1529
+ ApOption argAp , Ap ap , ApApprox apa , RetNodeEx ret , ParamNodeEx innerSummaryCtx ,
1530
+ Ap innerArgAp , ApApprox innerArgApa , Configuration config
1529
1531
) {
1530
- fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , kind , state , pragma [ only_bind_into ] ( ccc ) ,
1532
+ fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) ,
1531
1533
innerSummaryCtx , innerArgAp , innerArgApa , ap , pragma [ only_bind_into ] ( apa ) ,
1532
1534
pragma [ only_bind_into ] ( config ) ) and
1533
1535
fwdFlowIsEntered ( call , cc , ccc , summaryCtx , argAp , innerSummaryCtx , innerArgAp ,
@@ -1540,7 +1542,7 @@ private module MkStage<StageSig PrevStage> {
1540
1542
DataFlowCall call , Cc cc , FlowState state , CcCall ccc , ParamNodeOption summaryCtx ,
1541
1543
ApOption argAp , Ap ap , ApApprox apa , RetNodeEx ret , ApApprox innerArgApa , Configuration config
1542
1544
) {
1543
- fwdFlowThrough0 ( call , cc , state , ccc , summaryCtx , argAp , ap , apa , ret , _, _, _ , innerArgApa ,
1545
+ fwdFlowThrough0 ( call , cc , state , ccc , summaryCtx , argAp , ap , apa , ret , _, _, innerArgApa ,
1544
1546
config )
1545
1547
}
1546
1548
@@ -1580,21 +1582,21 @@ private module MkStage<StageSig PrevStage> {
1580
1582
pragma [ nomagic]
1581
1583
private predicate returnFlowsThrough0 (
1582
1584
DataFlowCall call , FlowState state , CcCall ccc , Ap ap , ApApprox apa , RetNodeEx ret ,
1583
- ReturnKindExt kind , ParamNodeEx innerSummaryCtx , Ap innerArgAp , ApApprox innerArgApa ,
1584
- Configuration config
1585
+ ParamNodeEx innerSummaryCtx , Ap innerArgAp , ApApprox innerArgApa , Configuration config
1585
1586
) {
1586
- fwdFlowThrough0 ( call , _, state , ccc , _, _, ap , apa , ret , kind , innerSummaryCtx , innerArgAp ,
1587
+ fwdFlowThrough0 ( call , _, state , ccc , _, _, ap , apa , ret , innerSummaryCtx , innerArgAp ,
1587
1588
innerArgApa , config )
1588
1589
}
1589
1590
1590
1591
pragma [ nomagic]
1591
1592
private predicate returnFlowsThrough (
1592
- RetNodeEx ret , ReturnKindExt kind , FlowState state , CcCall ccc , ParamNodeEx p , Ap argAp ,
1593
+ RetNodeEx ret , ReturnPosition pos , FlowState state , CcCall ccc , ParamNodeEx p , Ap argAp ,
1593
1594
Ap ap , Configuration config
1594
1595
) {
1595
1596
exists ( DataFlowCall call , ApApprox apa , boolean allowsFieldFlow , ApApprox innerArgApa |
1596
- returnFlowsThrough0 ( call , state , ccc , ap , apa , ret , kind , p , argAp , innerArgApa , config ) and
1597
+ returnFlowsThrough0 ( call , state , ccc , ap , apa , ret , p , argAp , innerArgApa , config ) and
1597
1598
flowThroughOutOfCall ( call , ccc , ret , _, allowsFieldFlow , innerArgApa , apa , config ) and
1599
+ pos = ret .getReturnPosition ( ) and
1598
1600
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1599
1601
)
1600
1602
}
@@ -1628,12 +1630,13 @@ private module MkStage<StageSig PrevStage> {
1628
1630
1629
1631
pragma [ nomagic]
1630
1632
private predicate flowOutOfCallAp (
1631
- DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
1633
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1632
1634
Ap ap , Configuration config
1633
1635
) {
1634
1636
exists ( ApApprox apa |
1635
- flowOutOfCallApa ( call , ret , kind , out , allowsFieldFlow , apa , config ) and
1636
- fwdFlow ( ret , _, _, _, _, ap , apa , config )
1637
+ flowOutOfCallApa ( call , ret , _, out , allowsFieldFlow , apa , config ) and
1638
+ fwdFlow ( ret , _, _, _, _, ap , apa , config ) and
1639
+ pos = ret .getReturnPosition ( )
1637
1640
)
1638
1641
}
1639
1642
@@ -1728,17 +1731,17 @@ private module MkStage<StageSig PrevStage> {
1728
1731
)
1729
1732
or
1730
1733
// flow through a callable
1731
- exists ( DataFlowCall call , ReturnKindExt returnKind0 , Ap returnAp0 |
1732
- revFlowInToReturn ( call , node , state , returnKind0 , returnAp0 , ap , config ) and
1733
- revFlowIsReturned ( call , returnCtx , returnAp , returnKind0 , returnAp0 , config )
1734
+ exists ( DataFlowCall call , ReturnPosition pos , Ap returnAp0 |
1735
+ revFlowInToReturn ( call , node , state , pos , returnAp0 , ap , config ) and
1736
+ revFlowIsReturned ( call , returnCtx , returnAp , pos , returnAp0 , config )
1734
1737
)
1735
1738
or
1736
1739
// flow out of a callable
1737
- exists ( ReturnKindExt kind |
1738
- revFlowOut ( _, node , kind , state , _, _, ap , config ) and
1739
- if returnFlowsThrough ( node , kind , state , _, _, _, ap , config )
1740
+ exists ( ReturnPosition pos |
1741
+ revFlowOut ( _, node , pos , state , _, _, ap , config ) and
1742
+ if returnFlowsThrough ( node , pos , state , _, _, _, ap , config )
1740
1743
then (
1741
- returnCtx = TReturnCtxMaybeFlowThrough ( kind ) and
1744
+ returnCtx = TReturnCtxMaybeFlowThrough ( pos ) and
1742
1745
returnAp = apSome ( ap )
1743
1746
) else (
1744
1747
returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
@@ -1771,12 +1774,12 @@ private module MkStage<StageSig PrevStage> {
1771
1774
1772
1775
pragma [ nomagic]
1773
1776
private predicate revFlowOut (
1774
- DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , FlowState state , ReturnCtx returnCtx ,
1777
+ DataFlowCall call , RetNodeEx ret , ReturnPosition pos , FlowState state , ReturnCtx returnCtx ,
1775
1778
ApOption returnAp , Ap ap , Configuration config
1776
1779
) {
1777
1780
exists ( NodeEx out , boolean allowsFieldFlow |
1778
1781
revFlow ( out , state , returnCtx , returnAp , ap , config ) and
1779
- flowOutOfCallAp ( call , ret , kind , out , allowsFieldFlow , ap , config ) and
1782
+ flowOutOfCallAp ( call , ret , pos , out , allowsFieldFlow , ap , config ) and
1780
1783
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1781
1784
)
1782
1785
}
@@ -1797,19 +1800,19 @@ private module MkStage<StageSig PrevStage> {
1797
1800
1798
1801
pragma [ nomagic]
1799
1802
private predicate revFlowParamToReturn (
1800
- ParamNodeEx p , FlowState state , ReturnKindExt kind , Ap returnAp , Ap ap , Configuration config
1803
+ ParamNodeEx p , FlowState state , ReturnPosition pos , Ap returnAp , Ap ap , Configuration config
1801
1804
) {
1802
- revFlow ( p , state , TReturnCtxMaybeFlowThrough ( kind ) , apSome ( returnAp ) , ap , config ) and
1803
- parameterFlowThroughAllowed ( p , kind )
1805
+ revFlow ( p , state , TReturnCtxMaybeFlowThrough ( pos ) , apSome ( returnAp ) , ap , config ) and
1806
+ parameterFlowThroughAllowed ( p , pos . getKind ( ) )
1804
1807
}
1805
1808
1806
1809
pragma [ nomagic]
1807
1810
private predicate revFlowInToReturn (
1808
- DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnKindExt kind , Ap returnAp , Ap ap ,
1811
+ DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnPosition pos , Ap returnAp , Ap ap ,
1809
1812
Configuration config
1810
1813
) {
1811
1814
exists ( ParamNodeEx p , boolean allowsFieldFlow |
1812
- revFlowParamToReturn ( p , state , kind , returnAp , ap , config ) and
1815
+ revFlowParamToReturn ( p , state , pos , returnAp , ap , config ) and
1813
1816
revFlowThroughIntoCall ( call , arg , p , allowsFieldFlow , ap , config )
1814
1817
)
1815
1818
}
@@ -1821,12 +1824,12 @@ private module MkStage<StageSig PrevStage> {
1821
1824
*/
1822
1825
pragma [ nomagic]
1823
1826
private predicate revFlowIsReturned (
1824
- DataFlowCall call , ReturnCtx returnCtx , ApOption returnAp , ReturnKindExt kind , Ap ap ,
1827
+ DataFlowCall call , ReturnCtx returnCtx , ApOption returnAp , ReturnPosition pos , Ap ap ,
1825
1828
Configuration config
1826
1829
) {
1827
1830
exists ( RetNodeEx ret , FlowState state , CcCall ccc |
1828
- revFlowOut ( call , ret , kind , state , returnCtx , returnAp , ap , config ) and
1829
- returnFlowsThrough ( ret , kind , state , ccc , _, _, ap , config ) and
1831
+ revFlowOut ( call , ret , pos , state , returnCtx , returnAp , ap , config ) and
1832
+ returnFlowsThrough ( ret , pos , state , ccc , _, _, ap , config ) and
1830
1833
matchesCall ( ccc , call )
1831
1834
)
1832
1835
}
@@ -1904,27 +1907,28 @@ private module MkStage<StageSig PrevStage> {
1904
1907
1905
1908
pragma [ nomagic]
1906
1909
private predicate parameterFlowsThroughRev (
1907
- ParamNodeEx p , Ap ap , ReturnKindExt kind , Ap returnAp , Configuration config
1910
+ ParamNodeEx p , Ap ap , ReturnPosition pos , Ap returnAp , Configuration config
1908
1911
) {
1909
- revFlow ( p , _, TReturnCtxMaybeFlowThrough ( kind ) , apSome ( returnAp ) , ap , config ) and
1910
- parameterFlowThroughAllowed ( p , kind )
1912
+ revFlow ( p , _, TReturnCtxMaybeFlowThrough ( pos ) , apSome ( returnAp ) , ap , config ) and
1913
+ parameterFlowThroughAllowed ( p , pos . getKind ( ) )
1911
1914
}
1912
1915
1913
1916
pragma [ nomagic]
1914
1917
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) {
1915
- exists ( RetNodeEx ret , ReturnKindExt kind |
1916
- returnFlowsThrough ( ret , kind , _, _, p , ap , _, config ) and
1917
- parameterFlowsThroughRev ( p , ap , kind , _, config )
1918
+ exists ( RetNodeEx ret , ReturnPosition pos |
1919
+ returnFlowsThrough ( ret , pos , _, _, p , ap , _, config ) and
1920
+ parameterFlowsThroughRev ( p , ap , pos , _, config )
1918
1921
)
1919
1922
}
1920
1923
1921
1924
pragma [ nomagic]
1922
1925
predicate returnMayFlowThrough (
1923
1926
RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind , Configuration config
1924
1927
) {
1925
- exists ( ParamNodeEx p |
1926
- returnFlowsThrough ( ret , kind , _, _, p , argAp , ap , config ) and
1927
- parameterFlowsThroughRev ( p , argAp , kind , ap , config )
1928
+ exists ( ParamNodeEx p , ReturnPosition pos |
1929
+ returnFlowsThrough ( ret , pos , _, _, p , argAp , ap , config ) and
1930
+ parameterFlowsThroughRev ( p , argAp , pos , ap , config ) and
1931
+ kind = pos .getKind ( )
1928
1932
)
1929
1933
}
1930
1934
@@ -1933,9 +1937,9 @@ private module MkStage<StageSig PrevStage> {
1933
1937
DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
1934
1938
Ap ap , Configuration config
1935
1939
) {
1936
- exists ( ReturnKindExt returnKind0 , Ap returnAp0 |
1937
- revFlowInToReturn ( call , arg , state , returnKind0 , returnAp0 , ap , config ) and
1938
- revFlowIsReturned ( call , returnCtx , returnAp , returnKind0 , returnAp0 , config )
1940
+ exists ( ReturnPosition pos , Ap returnAp0 |
1941
+ revFlowInToReturn ( call , arg , state , pos , returnAp0 , ap , config ) and
1942
+ revFlowIsReturned ( call , returnCtx , returnAp , pos , returnAp0 , config )
1939
1943
)
1940
1944
}
1941
1945
0 commit comments