@@ -1022,9 +1022,9 @@ private module Stage1 implements StageSig {
10221022 }
10231023
10241024 pragma [ nomagic]
1025- predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1025+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind , Configuration config ) {
10261026 throughFlowNodeCand ( ret , config ) and
1027- pos = ret .getReturnPosition ( )
1027+ kind = ret .getKind ( )
10281028 }
10291029
10301030 pragma [ nomagic]
@@ -1083,13 +1083,16 @@ private predicate viableReturnPosOutNodeCand1(
10831083 */
10841084pragma [ nomagic]
10851085private predicate flowOutOfCallNodeCand1 (
1086- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , Configuration config
1086+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , Configuration config
10871087) {
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+ )
10931096}
10941097
10951098pragma [ nomagic]
@@ -1149,10 +1152,10 @@ private int join(NodeEx n2, Configuration conf) {
11491152 */
11501153pragma [ nomagic]
11511154private predicate flowOutOfCallNodeCand1 (
1152- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1155+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
11531156 Configuration config
11541157) {
1155- flowOutOfCallNodeCand1 ( call , ret , pos , out , pragma [ only_bind_into ] ( config ) ) and
1158+ flowOutOfCallNodeCand1 ( call , ret , kind , out , pragma [ only_bind_into ] ( config ) ) and
11561159 exists ( int b , int j |
11571160 b = branch ( ret , pragma [ only_bind_into ] ( config ) ) and
11581161 j = join ( out , pragma [ only_bind_into ] ( config ) ) and
@@ -1193,7 +1196,7 @@ private signature module StageSig {
11931196
11941197 predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) ;
11951198
1196- predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) ;
1199+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind , Configuration config ) ;
11971200
11981201 predicate storeStepCand (
11991202 NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType ,
@@ -1259,7 +1262,7 @@ private module MkStage<StageSig PrevStage> {
12591262 ) ;
12601263
12611264 predicate flowOutOfCall (
1262- DataFlowCall call , RetNodeEx ret , ReturnPosition pos , NodeEx out , boolean allowsFieldFlow ,
1265+ DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow ,
12631266 Configuration config
12641267 ) ;
12651268
@@ -1288,14 +1291,11 @@ private module MkStage<StageSig PrevStage> {
12881291 DataFlowCall call , DataFlowCallable c , CcCall ccc , RetNodeEx ret , ReturnKindExt kind ,
12891292 NodeEx out , boolean allowsFieldFlow , Configuration config
12901293 ) {
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 ( )
12991299 }
13001300
13011301 /**
@@ -1507,27 +1507,26 @@ private module MkStage<StageSig PrevStage> {
15071507
15081508 pragma [ nomagic]
15091509 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
15121512 ) {
15131513 exists ( boolean allowsFieldFlow |
15141514 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 ,
15161516 pragma [ only_bind_into ] ( config ) ) and
15171517 if allowsFieldFlow = false then ap instanceof ApNil else any ( )
15181518 )
15191519 }
15201520
15211521 pragma [ nomagic]
15221522 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 ,
15241524 Ap ap , Configuration config
15251525 ) {
15261526 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
15281528 p .isParameterOf ( c , ppos ) and
1529- pos = ret .getReturnPosition ( ) and
1530- parameterFlowThroughAllowed ( p , pos .getKind ( ) )
1529+ parameterFlowThroughAllowed ( p , kind )
15311530 )
15321531 }
15331532
@@ -1631,17 +1630,17 @@ private module MkStage<StageSig PrevStage> {
16311630 returnCtx = TReturnCtxNone ( )
16321631 or
16331632 // 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 )
16371636 )
16381637 or
16391638 // 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 )
16431642 then (
1644- returnCtx = TReturnCtxMaybeFlowThrough ( pos ) and
1643+ returnCtx = TReturnCtxMaybeFlowThrough ( kind ) and
16451644 returnAp = apSome ( ap )
16461645 ) else (
16471646 returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
@@ -1674,12 +1673,12 @@ private module MkStage<StageSig PrevStage> {
16741673
16751674 pragma [ nomagic]
16761675 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 ,
16781677 ApOption returnAp , Ap ap , Configuration config
16791678 ) {
16801679 exists ( NodeEx out , boolean allowsFieldFlow |
16811680 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
16831682 if allowsFieldFlow = false then ap instanceof ApNil else any ( )
16841683 )
16851684 }
@@ -1697,14 +1696,15 @@ private module MkStage<StageSig PrevStage> {
16971696
16981697 pragma [ nomagic]
16991698 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
17021701 ) {
17031702 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
17051705 flowThroughIntoCall ( call , arg , p , allowsFieldFlow , config ) and
17061706 ( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1707- parameterFlowThroughAllowed ( p , returnPos . getKind ( ) )
1707+ parameterFlowThroughAllowed ( p , kind )
17081708 )
17091709 }
17101710
@@ -1715,12 +1715,12 @@ private module MkStage<StageSig PrevStage> {
17151715 */
17161716 pragma [ nomagic]
17171717 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 ,
17191719 Configuration config
17201720 ) {
17211721 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
17241724 matchesCall ( ccc , call )
17251725 )
17261726 }
@@ -1793,37 +1793,37 @@ private module MkStage<StageSig PrevStage> {
17931793
17941794 pragma [ nomagic]
17951795 private predicate parameterFlowsThroughRev (
1796- ParamNodeEx p , Ap ap , ReturnPosition returnPos , Configuration config
1796+ ParamNodeEx p , Ap ap , ReturnKindExt kind , Configuration config
17971797 ) {
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 )
18001800 }
18011801
18021802 pragma [ nomagic]
18031803 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 )
18071807 )
18081808 }
18091809
18101810 pragma [ nomagic]
1811- predicate returnMayFlowThrough ( RetNodeEx ret , ReturnPosition pos , Configuration config ) {
1811+ predicate returnMayFlowThrough ( RetNodeEx ret , ReturnKindExt kind , Configuration config ) {
18121812 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 )
18151815 )
18161816 }
18171817
18181818 pragma [ nomagic]
18191819 predicate callMayFlowThroughRev ( DataFlowCall call , Configuration config ) {
18201820 exists (
1821- ReturnPosition returnPos0 , Ap returnAp0 , ArgNodeEx arg , FlowState state ,
1821+ ReturnKindExt returnKind0 , Ap returnAp0 , ArgNodeEx arg , FlowState state ,
18221822 ReturnCtx returnCtx , ApOption returnAp , Ap ap
18231823 |
18241824 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 )
18271827 )
18281828 }
18291829
@@ -2027,10 +2027,10 @@ private module Stage2 implements StageSig {
20272027
20282028pragma [ nomagic]
20292029private predicate flowOutOfCallNodeCand2 (
2030- DataFlowCall call , RetNodeEx node1 , ReturnPosition pos , NodeEx node2 , boolean allowsFieldFlow ,
2030+ DataFlowCall call , RetNodeEx node1 , ReturnKindExt kind , NodeEx node2 , boolean allowsFieldFlow ,
20312031 Configuration config
20322032) {
2033- flowOutOfCallNodeCand1 ( call , node1 , pos , node2 , allowsFieldFlow , config ) and
2033+ flowOutOfCallNodeCand1 ( call , node1 , kind , node2 , allowsFieldFlow , config ) and
20342034 Stage2:: revFlow ( node2 , pragma [ only_bind_into ] ( config ) ) and
20352035 Stage2:: revFlowAlias ( node1 , pragma [ only_bind_into ] ( config ) )
20362036}
@@ -2546,11 +2546,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
25462546
25472547 pragma [ nomagic]
25482548 predicate flowOutOfCall (
2549- DataFlowCall call , RetNodeEx node1 , ReturnPosition pos , NodeEx node2 , boolean allowsFieldFlow ,
2549+ DataFlowCall call , RetNodeEx node1 , ReturnKindExt kind , NodeEx node2 , boolean allowsFieldFlow ,
25502550 Configuration config
25512551 ) {
25522552 exists ( FlowState state |
2553- flowOutOfCallNodeCand2 ( call , node1 , pos , node2 , allowsFieldFlow , config ) and
2553+ flowOutOfCallNodeCand2 ( call , node1 , kind , node2 , allowsFieldFlow , config ) and
25542554 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _, pragma [ only_bind_into ] ( config ) ) and
25552555 PrevStage:: revFlowAlias ( node1 , pragma [ only_bind_into ] ( state ) , _,
25562556 pragma [ only_bind_into ] ( config ) )
0 commit comments