@@ -584,6 +584,43 @@ private module Stage1 {
584584 revFlow ( node , toReturn , config ) and exists ( returnAp ) and exists ( ap )
585585 }
586586
587+ private predicate throughFlowNodeCand1 ( Node node , Configuration config ) {
588+ revFlow ( node , true , config ) and
589+ fwdFlow ( node , true , config ) and
590+ not fullBarrier ( node , config ) and
591+ not inBarrier ( node , config ) and
592+ not outBarrier ( node , config )
593+ }
594+
595+ /** Holds if flow may return from `callable`. */
596+ pragma [ nomagic]
597+ private predicate returnFlowCallableNodeCand1 (
598+ DataFlowCallable callable , ReturnKindExt kind , Configuration config
599+ ) {
600+ exists ( ReturnNodeExt ret |
601+ throughFlowNodeCand1 ( ret , config ) and
602+ callable = ret .getEnclosingCallable ( ) and
603+ kind = ret .getKind ( )
604+ )
605+ }
606+
607+ /**
608+ * Holds if flow may enter through `p` and reach a return node making `p` a
609+ * candidate for the origin of a summary.
610+ */
611+ predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , Ap ap , Configuration config ) {
612+ exists ( ReturnKindExt kind |
613+ throughFlowNodeCand1 ( p , config ) and
614+ returnFlowCallableNodeCand1 ( c , kind , config ) and
615+ p .getEnclosingCallable ( ) = c and
616+ exists ( ap ) and
617+ // we don't expect a parameter to return stored in itself
618+ not exists ( int pos |
619+ kind .( ParamUpdateReturnKind ) .getPosition ( ) = pos and p .isParameterOf ( _, pos )
620+ )
621+ )
622+ }
623+
587624 predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
588625 fwd = true and
589626 nodes = count ( Node node | fwdFlow ( node , config ) ) and
@@ -603,41 +640,6 @@ private module Stage1 {
603640bindingset [ result , b]
604641private boolean unbindBool ( boolean b ) { result != b .booleanNot ( ) }
605642
606- private predicate throughFlowNodeCand1 ( Node node , Configuration config ) {
607- Stage1:: revFlow ( node , true , config ) and
608- Stage1:: fwdFlow ( node , true , config ) and
609- not fullBarrier ( node , config ) and
610- not inBarrier ( node , config ) and
611- not outBarrier ( node , config )
612- }
613-
614- /** Holds if flow may return from `callable`. */
615- pragma [ nomagic]
616- private predicate returnFlowCallableNodeCand1 (
617- DataFlowCallable callable , ReturnKindExt kind , Configuration config
618- ) {
619- exists ( ReturnNodeExt ret |
620- throughFlowNodeCand1 ( ret , config ) and
621- callable = ret .getEnclosingCallable ( ) and
622- kind = ret .getKind ( )
623- )
624- }
625-
626- /**
627- * Holds if flow may enter through `p` and reach a return node making `p` a
628- * candidate for the origin of a summary.
629- */
630- private predicate parameterThroughFlowNodeCand1 ( ParameterNode p , Configuration config ) {
631- exists ( ReturnKindExt kind |
632- throughFlowNodeCand1 ( p , config ) and
633- returnFlowCallableNodeCand1 ( p .getEnclosingCallable ( ) , kind , config ) and
634- // we don't expect a parameter to return stored in itself
635- not exists ( int pos |
636- kind .( ParamUpdateReturnKind ) .getPosition ( ) = pos and p .isParameterOf ( _, pos )
637- )
638- )
639- }
640-
641643pragma [ noinline]
642644private predicate localFlowStepNodeCand1 ( Node node1 , Node node2 , Configuration config ) {
643645 Stage1:: revFlow ( node2 , config ) and
@@ -889,8 +891,13 @@ private module Stage2 {
889891 )
890892 or
891893 // flow into a callable
892- fwdFlowIn ( _, node , _, cc , _, ap , config ) and
893- if parameterThroughFlowNodeCand1 ( node , config ) then argAp = apSome ( ap ) else argAp = apNone ( )
894+ exists ( ApApprox apa |
895+ fwdFlowIn ( _, node , _, cc , _, ap , config ) and
896+ apa = getApprox ( ap ) and
897+ if PrevStage:: parameterMayFlowThrough ( node , _, apa , config )
898+ then argAp = apSome ( ap )
899+ else argAp = apNone ( )
900+ )
894901 or
895902 // flow out of a callable
896903 exists ( DataFlowCall call |
@@ -979,7 +986,7 @@ private module Stage2 {
979986 ) {
980987 exists ( ParameterNode p |
981988 fwdFlowIn ( call , p , cc , _, argAp , ap , config ) and
982- parameterThroughFlowNodeCand1 ( p , config )
989+ PrevStage :: parameterMayFlowThrough ( p , _ , getApprox ( ap ) , config )
983990 )
984991 }
985992
@@ -1075,7 +1082,7 @@ private module Stage2 {
10751082 // flow out of a callable
10761083 revFlowOut ( _, node , _, _, ap , config ) and
10771084 toReturn = true and
1078- if fwdFlow ( node , true , apSome ( _) , unbindBool ( ap ) , config )
1085+ if fwdFlow ( node , any ( CcCall ccc ) , apSome ( _) , ap , config )
10791086 then returnAp = apSome ( ap )
10801087 else returnAp = apNone ( )
10811088 }
@@ -1176,6 +1183,27 @@ private module Stage2 {
11761183 storeStepCand ( _, ap , tc , _, _, config )
11771184 }
11781185
1186+ pragma [ noinline]
1187+ private predicate parameterFlow (
1188+ ParameterNode p , Ap ap , Ap ap0 , DataFlowCallable c , Configuration config
1189+ ) {
1190+ revFlow ( p , true , apSome ( ap0 ) , ap , config ) and
1191+ c = p .getEnclosingCallable ( )
1192+ }
1193+
1194+ predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , Ap ap , Configuration config ) {
1195+ exists ( ReturnNodeExt ret , Ap ap0 , ReturnKindExt kind , int pos |
1196+ parameterFlow ( p , ap , ap0 , c , config ) and
1197+ c = ret .getEnclosingCallable ( ) and
1198+ revFlow ( ret , true , apSome ( _) , ap0 , config ) and
1199+ fwdFlow ( ret , any ( CcCall ccc ) , apSome ( ap ) , ap0 , config ) and
1200+ kind = ret .getKind ( ) and
1201+ p .isParameterOf ( _, pos ) and
1202+ // we don't expect a parameter to return stored in itself
1203+ not kind .( ParamUpdateReturnKind ) .getPosition ( ) = pos
1204+ )
1205+ }
1206+
11791207 predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
11801208 fwd = true and
11811209 nodes = count ( Node node | fwdFlow ( node , _, _, _, config ) ) and
@@ -1339,8 +1367,7 @@ private module Stage3 {
13391367
13401368 class ApNil = AccessPathFrontNil ;
13411369
1342- bindingset [ result , ap]
1343- ApApprox getApprox ( Ap ap ) { result = unbindBool ( ap .toBoolNonEmpty ( ) ) }
1370+ ApApprox getApprox ( Ap ap ) { result = ap .toBoolNonEmpty ( ) }
13441371
13451372 ApNil getApNil ( Node node ) { result = TFrontNil ( getNodeType ( node ) ) }
13461373
@@ -1404,7 +1431,7 @@ private module Stage3 {
14041431 pragma [ nomagic]
14051432 predicate fwdFlow ( Node node , Cc cc , ApOption argAp , Ap ap , Configuration config ) {
14061433 fwdFlow0 ( node , cc , argAp , ap , config ) and
1407- flowCand ( node , getApprox ( ap ) , config ) and
1434+ flowCand ( node , unbindBool ( getApprox ( ap ) ) , config ) and
14081435 not ap .isClearedAt ( node ) and
14091436 if node instanceof CastingNode then compatibleTypes ( getNodeType ( node ) , ap .getType ( ) ) else any ( )
14101437 }
@@ -1458,10 +1485,13 @@ private module Stage3 {
14581485 )
14591486 or
14601487 // flow into a callable
1461- fwdFlowIn ( _, node , _, cc , _, ap , config ) and
1462- if PrevStage:: revFlow ( node , true , _, unbindBool ( ap .toBoolNonEmpty ( ) ) , config )
1463- then argAp = apSome ( ap )
1464- else argAp = apNone ( )
1488+ exists ( ApApprox apa |
1489+ fwdFlowIn ( _, node , _, cc , _, ap , config ) and
1490+ apa = getApprox ( ap ) and
1491+ if PrevStage:: parameterMayFlowThrough ( node , _, apa , config )
1492+ then argAp = apSome ( ap )
1493+ else argAp = apNone ( )
1494+ )
14651495 or
14661496 // flow out of a callable
14671497 exists ( DataFlowCall call |
@@ -1550,7 +1580,7 @@ private module Stage3 {
15501580 ) {
15511581 exists ( ParameterNode p |
15521582 fwdFlowIn ( call , p , cc , _, argAp , ap , config ) and
1553- PrevStage:: revFlow ( p , true , TBooleanSome ( _ ) , unbindBool ( ap . toBoolNonEmpty ( ) ) , config )
1583+ PrevStage:: parameterMayFlowThrough ( p , _ , unbindBool ( getApprox ( ap ) ) , config )
15541584 )
15551585 }
15561586
@@ -1646,7 +1676,9 @@ private module Stage3 {
16461676 // flow out of a callable
16471677 revFlowOut ( _, node , _, _, ap , config ) and
16481678 toReturn = true and
1649- if fwdFlow ( node , true , _, ap , config ) then returnAp = apSome ( ap ) else returnAp = apNone ( )
1679+ if fwdFlow ( node , any ( CcCall ccc ) , apSome ( _) , ap , config )
1680+ then returnAp = apSome ( ap )
1681+ else returnAp = apNone ( )
16501682 }
16511683
16521684 pragma [ nomagic]
@@ -1740,6 +1772,27 @@ private module Stage3 {
17401772 storeStepCand ( _, ap , tc , _, _, config )
17411773 }
17421774
1775+ pragma [ noinline]
1776+ private predicate parameterFlow (
1777+ ParameterNode p , Ap ap , Ap ap0 , DataFlowCallable c , Configuration config
1778+ ) {
1779+ revFlow ( p , true , apSome ( ap0 ) , ap , config ) and
1780+ c = p .getEnclosingCallable ( )
1781+ }
1782+
1783+ predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , Ap ap , Configuration config ) {
1784+ exists ( ReturnNodeExt ret , Ap ap0 , ReturnKindExt kind , int pos |
1785+ parameterFlow ( p , ap , ap0 , c , config ) and
1786+ c = ret .getEnclosingCallable ( ) and
1787+ revFlow ( ret , true , apSome ( _) , ap0 , config ) and
1788+ fwdFlow ( ret , any ( CcCall ccc ) , apSome ( ap ) , ap0 , config ) and
1789+ kind = ret .getKind ( ) and
1790+ p .isParameterOf ( _, pos ) and
1791+ // we don't expect a parameter to return stored in itself
1792+ not kind .( ParamUpdateReturnKind ) .getPosition ( ) = pos
1793+ )
1794+ }
1795+
17431796 predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
17441797 fwd = true and
17451798 nodes = count ( Node node | fwdFlow ( node , _, _, _, config ) ) and
@@ -2092,8 +2145,8 @@ private module Stage4 {
20922145 // flow into a callable
20932146 exists ( ApApprox apa |
20942147 fwdFlowIn ( _, node , _, cc , _, ap , config ) and
2095- apa = ap . getFront ( ) and
2096- if PrevStage:: revFlow ( node , true , _, apa , config )
2148+ apa = getApprox ( ap ) and
2149+ if PrevStage:: parameterMayFlowThrough ( node , _, apa , config )
20972150 then argAp = apSome ( ap )
20982151 else argAp = apNone ( )
20992152 )
@@ -2184,7 +2237,7 @@ private module Stage4 {
21842237 ) {
21852238 exists ( ParameterNode p |
21862239 fwdFlowIn ( call , p , cc , _, argAp , ap , config ) and
2187- PrevStage:: revFlow ( p , true , TAccessPathFrontSome ( _ ) , ap . getFront ( ) , config )
2240+ PrevStage:: parameterMayFlowThrough ( p , _ , getApprox ( ap ) , config )
21882241 )
21892242 }
21902243
@@ -2280,7 +2333,7 @@ private module Stage4 {
22802333 // flow out of a callable
22812334 revFlowOut ( _, node , _, _, ap , config ) and
22822335 toReturn = true and
2283- if fwdFlow ( node , any ( CallContextCall ccc ) , apSome ( _) , ap , config )
2336+ if fwdFlow ( node , any ( CcCall ccc ) , apSome ( _) , ap , config )
22842337 then returnAp = apSome ( ap )
22852338 else returnAp = apNone ( )
22862339 }
@@ -2343,7 +2396,7 @@ private module Stage4 {
23432396 private predicate revFlowIsReturned (
23442397 DataFlowCall call , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
23452398 ) {
2346- exists ( ReturnNodeExt ret , CallContextCall ccc |
2399+ exists ( ReturnNodeExt ret , CcCall ccc |
23472400 revFlowOut ( call , ret , toReturn , returnAp , ap , config ) and
23482401 fwdFlow ( ret , ccc , apSome ( _) , ap , config ) and
23492402 ccc .matchesCall ( call )
@@ -2379,6 +2432,27 @@ private module Stage4 {
23792432 storeStepCand ( _, ap , tc , _, _, config )
23802433 }
23812434
2435+ pragma [ noinline]
2436+ private predicate parameterFlow (
2437+ ParameterNode p , Ap ap , Ap ap0 , DataFlowCallable c , Configuration config
2438+ ) {
2439+ revFlow ( p , true , apSome ( ap0 ) , ap , config ) and
2440+ c = p .getEnclosingCallable ( )
2441+ }
2442+
2443+ predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , Ap ap , Configuration config ) {
2444+ exists ( ReturnNodeExt ret , Ap ap0 , ReturnKindExt kind , int pos |
2445+ parameterFlow ( p , ap , ap0 , c , config ) and
2446+ c = ret .getEnclosingCallable ( ) and
2447+ revFlow ( ret , true , apSome ( _) , ap0 , config ) and
2448+ fwdFlow ( ret , any ( CcCall ccc ) , apSome ( ap ) , ap0 , config ) and
2449+ kind = ret .getKind ( ) and
2450+ p .isParameterOf ( _, pos ) and
2451+ // we don't expect a parameter to return stored in itself
2452+ not kind .( ParamUpdateReturnKind ) .getPosition ( ) = pos
2453+ )
2454+ }
2455+
23822456 predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
23832457 fwd = true and
23842458 nodes = count ( Node node | fwdFlow ( node , _, _, _, config ) ) and
@@ -2398,27 +2472,9 @@ private module Stage4 {
23982472bindingset [ conf, result ]
23992473private Configuration unbind ( Configuration conf ) { result >= conf and result <= conf }
24002474
2401- pragma [ noinline]
2402- private predicate parameterFlow (
2403- ParameterNode p , AccessPathApprox apa , AccessPathApprox apa0 , DataFlowCallable c ,
2404- Configuration config
2405- ) {
2406- Stage4:: revFlow ( p , true , TAccessPathApproxSome ( apa0 ) , apa , config ) and
2407- c = p .getEnclosingCallable ( )
2408- }
2409-
2410- private predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , AccessPathApprox apa ) {
2411- exists ( ReturnNodeExt ret , Configuration config , AccessPathApprox apa0 |
2412- parameterFlow ( p , apa , apa0 , c , config ) and
2413- c = ret .getEnclosingCallable ( ) and
2414- Stage4:: revFlow ( ret , true , TAccessPathApproxSome ( _) , apa0 , config ) and
2415- Stage4:: fwdFlow ( ret , any ( CallContextCall ccc ) , TAccessPathApproxSome ( apa ) , apa0 , config )
2416- )
2417- }
2418-
24192475private predicate nodeMayUseSummary ( Node n , AccessPathApprox apa , Configuration config ) {
24202476 exists ( DataFlowCallable c , AccessPathApprox apa0 |
2421- parameterMayFlowThrough ( _, c , apa ) and
2477+ Stage4 :: parameterMayFlowThrough ( _, c , apa , _ ) and
24222478 Stage4:: revFlow ( n , true , _, apa0 , config ) and
24232479 Stage4:: fwdFlow ( n , any ( CallContextCall ccc ) , TAccessPathApproxSome ( apa ) , apa0 , config ) and
24242480 n .getEnclosingCallable ( ) = c
@@ -2427,7 +2483,9 @@ private predicate nodeMayUseSummary(Node n, AccessPathApprox apa, Configuration
24272483
24282484private newtype TSummaryCtx =
24292485 TSummaryCtxNone ( ) or
2430- TSummaryCtxSome ( ParameterNode p , AccessPath ap ) { parameterMayFlowThrough ( p , _, ap .getApprox ( ) ) }
2486+ TSummaryCtxSome ( ParameterNode p , AccessPath ap ) {
2487+ Stage4:: parameterMayFlowThrough ( p , _, ap .getApprox ( ) , _)
2488+ }
24312489
24322490/**
24332491 * A context for generating flow summaries. This represents flow entry through
0 commit comments