@@ -1529,12 +1529,8 @@ private module MkStage<StageSig PrevStage> {
1529
1529
ApOption argAp , Ap ap , ApApprox apa , RetNodeEx ret , ParamNodeEx innerSummaryCtx ,
1530
1530
Ap innerArgAp , ApApprox innerArgApa , Configuration config
1531
1531
) {
1532
- fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) ,
1533
- innerSummaryCtx , innerArgAp , innerArgApa , ap , pragma [ only_bind_into ] ( apa ) ,
1534
- pragma [ only_bind_into ] ( config ) ) and
1535
- fwdFlowIsEntered ( call , cc , ccc , summaryCtx , argAp , innerSummaryCtx , innerArgAp ,
1536
- pragma [ only_bind_into ] ( config ) ) and
1537
- matchesCall ( ccc , call )
1532
+ fwdFlowRetFromArg ( ret , state , ccc , innerSummaryCtx , innerArgAp , innerArgApa , ap , apa , config ) and
1533
+ fwdFlowIsEntered ( call , cc , ccc , summaryCtx , argAp , innerSummaryCtx , innerArgAp , config )
1538
1534
}
1539
1535
1540
1536
pragma [ nomagic]
@@ -1603,15 +1599,15 @@ private module MkStage<StageSig PrevStage> {
1603
1599
1604
1600
pragma [ nomagic]
1605
1601
private predicate flowThroughIntoCall (
1606
- DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Ap argAp ,
1602
+ DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Ap argAp , Ap ap ,
1607
1603
Configuration config
1608
1604
) {
1609
1605
exists ( ApApprox argApa |
1610
1606
flowIntoCallApa ( call , pragma [ only_bind_into ] ( arg ) , pragma [ only_bind_into ] ( p ) ,
1611
1607
allowsFieldFlow , argApa , pragma [ only_bind_into ] ( config ) ) and
1612
1608
fwdFlow ( arg , _, _, _, _, pragma [ only_bind_into ] ( argAp ) , argApa ,
1613
1609
pragma [ only_bind_into ] ( config ) ) and
1614
- returnFlowsThrough ( _, _, _, _, p , pragma [ only_bind_into ] ( argAp ) , _ ,
1610
+ returnFlowsThrough ( _, _, _, _, p , pragma [ only_bind_into ] ( argAp ) , ap ,
1615
1611
pragma [ only_bind_into ] ( config ) ) and
1616
1612
if allowsFieldFlow = false then argAp instanceof ApNil else any ( )
1617
1613
)
@@ -1731,9 +1727,9 @@ private module MkStage<StageSig PrevStage> {
1731
1727
)
1732
1728
or
1733
1729
// flow through a callable
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 )
1730
+ exists ( DataFlowCall call , ParamNodeEx p , ReturnPosition pos , Ap innerReturnAp |
1731
+ revFlowThrough ( call , returnCtx , p , state , pos , returnAp , ap , innerReturnAp , config ) and
1732
+ flowThroughIntoCall ( call , node , p , _ , ap , innerReturnAp , config )
1737
1733
)
1738
1734
or
1739
1735
// flow out of a callable
@@ -1784,37 +1780,23 @@ private module MkStage<StageSig PrevStage> {
1784
1780
)
1785
1781
}
1786
1782
1787
- /**
1788
- * Same as `flowThroughIntoCall`, but restricted to calls that are reached
1789
- * in the flow covered by `revFlow`, where data might flow through the target
1790
- * callable and back out at `call`.
1791
- */
1792
- pragma [ nomagic]
1793
- private predicate revFlowThroughIntoCall (
1794
- DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Ap argAp ,
1795
- Configuration config
1796
- ) {
1797
- flowThroughIntoCall ( call , arg , p , allowsFieldFlow , argAp , config ) and
1798
- revFlowIsReturned ( call , _, _, _, _, config )
1799
- }
1800
-
1801
1783
pragma [ nomagic]
1802
1784
private predicate revFlowParamToReturn (
1803
1785
ParamNodeEx p , FlowState state , ReturnPosition pos , Ap returnAp , Ap ap , Configuration config
1804
1786
) {
1805
- revFlow ( p , state , TReturnCtxMaybeFlowThrough ( pos ) , apSome ( returnAp ) , ap , config ) and
1806
- parameterFlowThroughAllowed ( p , pos .getKind ( ) )
1787
+ revFlow ( pragma [ only_bind_into ] ( p ) , state , TReturnCtxMaybeFlowThrough ( pos ) , apSome ( returnAp ) ,
1788
+ pragma [ only_bind_into ] ( ap ) , pragma [ only_bind_into ] ( config ) ) and
1789
+ parameterFlowThroughAllowed ( p , pos .getKind ( ) ) and
1790
+ PrevStage:: parameterMayFlowThrough ( p , getApprox ( ap ) , config )
1807
1791
}
1808
1792
1809
1793
pragma [ nomagic]
1810
- private predicate revFlowInToReturn (
1811
- DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnPosition pos , Ap returnAp , Ap ap ,
1812
- Configuration config
1794
+ private predicate revFlowThrough (
1795
+ DataFlowCall call , ReturnCtx returnCtx , ParamNodeEx p , FlowState state , ReturnPosition pos ,
1796
+ ApOption returnAp , Ap ap , Ap innerReturnAp , Configuration config
1813
1797
) {
1814
- exists ( ParamNodeEx p , boolean allowsFieldFlow |
1815
- revFlowParamToReturn ( p , state , pos , returnAp , ap , config ) and
1816
- revFlowThroughIntoCall ( call , arg , p , allowsFieldFlow , ap , config )
1817
- )
1798
+ revFlowParamToReturn ( p , state , pos , innerReturnAp , ap , config ) and
1799
+ revFlowIsReturned ( call , returnCtx , returnAp , pos , innerReturnAp , config )
1818
1800
}
1819
1801
1820
1802
/**
@@ -1933,21 +1915,21 @@ private module MkStage<StageSig PrevStage> {
1933
1915
}
1934
1916
1935
1917
pragma [ nomagic]
1936
- predicate revFlowInToReturnIsReturned (
1918
+ private predicate revFlowThroughArg (
1937
1919
DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
1938
1920
Ap ap , Configuration config
1939
1921
) {
1940
- exists ( ReturnPosition pos , Ap returnAp0 |
1941
- revFlowInToReturn ( call , arg , state , pos , returnAp0 , ap , config ) and
1942
- revFlowIsReturned ( call , returnCtx , returnAp , pos , returnAp0 , config )
1922
+ exists ( ParamNodeEx p , ReturnPosition pos , Ap innerReturnAp |
1923
+ revFlowThrough ( call , returnCtx , p , state , pos , returnAp , ap , innerReturnAp , config ) and
1924
+ flowThroughIntoCall ( call , arg , p , _ , ap , innerReturnAp , config )
1943
1925
)
1944
1926
}
1945
1927
1946
1928
pragma [ nomagic]
1947
1929
predicate callMayFlowThroughRev ( DataFlowCall call , Configuration config ) {
1948
1930
exists ( ArgNodeEx arg , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap |
1949
1931
revFlow ( arg , state , returnCtx , returnAp , ap , config ) and
1950
- revFlowInToReturnIsReturned ( call , arg , state , returnCtx , returnAp , ap , config )
1932
+ revFlowThroughArg ( call , arg , state , returnCtx , returnAp , ap , config )
1951
1933
)
1952
1934
}
1953
1935
0 commit comments