@@ -1508,26 +1508,28 @@ private module MkStage<StageSig PrevStage> {
15081508
15091509 pragma [ nomagic]
15101510 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
15131513 ) {
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+ )
15221524 }
15231525
15241526 pragma [ inline]
15251527 private predicate fwdFlowThrough0 (
15261528 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
15291531 ) {
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 ) ,
15311533 innerSummaryCtx , innerArgAp , innerArgApa , ap , pragma [ only_bind_into ] ( apa ) ,
15321534 pragma [ only_bind_into ] ( config ) ) and
15331535 fwdFlowIsEntered ( call , cc , ccc , summaryCtx , argAp , innerSummaryCtx , innerArgAp ,
@@ -1540,7 +1542,7 @@ private module MkStage<StageSig PrevStage> {
15401542 DataFlowCall call , Cc cc , FlowState state , CcCall ccc , ParamNodeOption summaryCtx ,
15411543 ApOption argAp , Ap ap , ApApprox apa , RetNodeEx ret , ApApprox innerArgApa , Configuration config
15421544 ) {
1543- fwdFlowThrough0 ( call , cc , state , ccc , summaryCtx , argAp , ap , apa , ret , _, _, _ , innerArgApa ,
1545+ fwdFlowThrough0 ( call , cc , state , ccc , summaryCtx , argAp , ap , apa , ret , _, _, innerArgApa ,
15441546 config )
15451547 }
15461548
@@ -1580,21 +1582,21 @@ private module MkStage<StageSig PrevStage> {
15801582 pragma [ nomagic]
15811583 private predicate returnFlowsThrough0 (
15821584 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
15851586 ) {
1586- fwdFlowThrough0 ( call , _, state , ccc , _, _, ap , apa , ret , kind , innerSummaryCtx , innerArgAp ,
1587+ fwdFlowThrough0 ( call , _, state , ccc , _, _, ap , apa , ret , innerSummaryCtx , innerArgAp ,
15871588 innerArgApa , config )
15881589 }
15891590
15901591 pragma [ nomagic]
15911592 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 ,
15931594 Ap ap , Configuration config
15941595 ) {
15951596 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
15971598 flowThroughOutOfCall ( call , ccc , ret , _, allowsFieldFlow , innerArgApa , apa , config ) and
1599+ pos = ret .getReturnPosition ( ) and
15981600 if allowsFieldFlow = false then ap instanceof ApNil else any ( )
15991601 )
16001602 }
@@ -1628,12 +1630,13 @@ private module MkStage<StageSig PrevStage> {
16281630
16291631 pragma [ nomagic]
16301632 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 ,
16321634 Ap ap , Configuration config
16331635 ) {
16341636 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 ( )
16371640 )
16381641 }
16391642
@@ -1728,17 +1731,17 @@ private module MkStage<StageSig PrevStage> {
17281731 )
17291732 or
17301733 // 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 )
17341737 )
17351738 or
17361739 // 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 )
17401743 then (
1741- returnCtx = TReturnCtxMaybeFlowThrough ( kind ) and
1744+ returnCtx = TReturnCtxMaybeFlowThrough ( pos ) and
17421745 returnAp = apSome ( ap )
17431746 ) else (
17441747 returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
@@ -1771,12 +1774,12 @@ private module MkStage<StageSig PrevStage> {
17711774
17721775 pragma [ nomagic]
17731776 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 ,
17751778 ApOption returnAp , Ap ap , Configuration config
17761779 ) {
17771780 exists ( NodeEx out , boolean allowsFieldFlow |
17781781 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
17801783 if allowsFieldFlow = false then ap instanceof ApNil else any ( )
17811784 )
17821785 }
@@ -1797,19 +1800,19 @@ private module MkStage<StageSig PrevStage> {
17971800
17981801 pragma [ nomagic]
17991802 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
18011804 ) {
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 ( ) )
18041807 }
18051808
18061809 pragma [ nomagic]
18071810 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 ,
18091812 Configuration config
18101813 ) {
18111814 exists ( ParamNodeEx p , boolean allowsFieldFlow |
1812- revFlowParamToReturn ( p , state , kind , returnAp , ap , config ) and
1815+ revFlowParamToReturn ( p , state , pos , returnAp , ap , config ) and
18131816 revFlowThroughIntoCall ( call , arg , p , allowsFieldFlow , ap , config )
18141817 )
18151818 }
@@ -1821,12 +1824,12 @@ private module MkStage<StageSig PrevStage> {
18211824 */
18221825 pragma [ nomagic]
18231826 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 ,
18251828 Configuration config
18261829 ) {
18271830 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
18301833 matchesCall ( ccc , call )
18311834 )
18321835 }
@@ -1904,27 +1907,28 @@ private module MkStage<StageSig PrevStage> {
19041907
19051908 pragma [ nomagic]
19061909 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
19081911 ) {
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 ( ) )
19111914 }
19121915
19131916 pragma [ nomagic]
19141917 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 )
19181921 )
19191922 }
19201923
19211924 pragma [ nomagic]
19221925 predicate returnMayFlowThrough (
19231926 RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind , Configuration config
19241927 ) {
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 ( )
19281932 )
19291933 }
19301934
@@ -1933,9 +1937,9 @@ private module MkStage<StageSig PrevStage> {
19331937 DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
19341938 Ap ap , Configuration config
19351939 ) {
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 )
19391943 )
19401944 }
19411945
0 commit comments