@@ -813,6 +813,7 @@ private predicate viableParamArgCand(
813813 not inBarrier ( p , config )
814814}
815815
816+ pragma [ nomagic]
816817private predicate parameterFlowReturn (
817818 ParameterNode p , ReturnNodeExt ret , ReturnKindExt kind , DataFlowType t1 , DataFlowType t2 ,
818819 Summary summary , Configuration config
@@ -1006,6 +1007,12 @@ private class TaintStoreNode extends NodeExt, TTaintStoreNode {
10061007 }
10071008}
10081009
1010+ private predicate additionalLocalFlowStepExt ( NodeExt node1 , NodeExt node2 , Configuration config ) {
1011+ node1 = TReadTaintNode ( _, node2 .getNode ( ) , _, _, config )
1012+ or
1013+ node2 = TTaintStoreNode ( node1 .getNode ( ) , _, _, _, config )
1014+ }
1015+
10091016pragma [ nomagic]
10101017private predicate localFlowBigStepExt (
10111018 NodeExt node1 , NodeExt node2 , boolean preservesValue , Configuration config
@@ -1048,12 +1055,6 @@ private predicate additionalJumpStepExt(NodeExt node1, NodeExt node2, Configurat
10481055 additionalJumpStep ( node1 .getNode ( ) , node2 .getNode ( ) , config )
10491056}
10501057
1051- private predicate additionalLocalFlowStepExt ( NodeExt node1 , NodeExt node2 , Configuration config ) {
1052- node1 = TReadTaintNode ( _, node2 .getNode ( ) , _, _, config )
1053- or
1054- node2 = TTaintStoreNode ( node1 .getNode ( ) , _, _, _, config )
1055- }
1056-
10571058private predicate argumentValueFlowsThrough ( NodeExt node1 , NodeExt node2 ) {
10581059 argumentValueFlowsThrough ( _, node1 .getNode ( ) , TContentNone ( ) , TContentNone ( ) , node2 .getNode ( ) )
10591060}
@@ -1341,7 +1342,7 @@ private predicate readCand2(Content f, boolean read, Configuration config) {
13411342 useFieldFlow ( config ) and
13421343 nodeCandFwd2 ( node , _, true , unbind ( config ) ) and
13431344 readExt ( node , f , mid , config ) and
1344- storeCandFwd2 ( f , _ , unbind ( config ) ) and
1345+ storeCandFwd2 ( f , unbindBool ( read ) , unbind ( config ) ) and
13451346 nodeCand2 ( mid , _, read , config )
13461347 )
13471348}
@@ -1358,10 +1359,10 @@ private predicate nodeCand2Store(
13581359}
13591360
13601361pragma [ nomagic]
1361- private predicate storeCand ( Content f , boolean stored , Configuration conf ) {
1362+ private predicate storeCand2 ( Content f , boolean stored , Configuration conf ) {
13621363 exists ( NodeExt node |
13631364 nodeCand2Store ( f , node , _, stored , conf ) and
1364- nodeCand2 ( node , _, _ , conf )
1365+ nodeCand2 ( node , _, stored , conf )
13651366 )
13661367}
13671368
@@ -1372,17 +1373,19 @@ private predicate storeCand(Content f, boolean stored, Configuration conf) {
13721373 */
13731374pragma [ noinline]
13741375private predicate readStoreCand ( Content f , boolean nonEmpty , Configuration conf ) {
1375- storeCand ( f , nonEmpty , conf ) and
1376+ storeCand2 ( f , nonEmpty , conf ) and
13761377 readCand2 ( f , nonEmpty , conf )
13771378}
13781379
1380+ private predicate nodeCand2 ( NodeExt node , Configuration config ) { nodeCand2 ( node , _, _, config ) }
1381+
13791382pragma [ nomagic]
13801383private predicate flowOutOfCallableNodeCand2 (
13811384 NodeExt node1 , NodeExt node2 , boolean allowsFieldFlow , boolean apfEmpty , Configuration config
13821385) {
13831386 flowOutOfCallableNodeCand1 ( node1 , node2 , allowsFieldFlow , config ) and
13841387 nodeCand2 ( node2 , _, apfEmpty .booleanNot ( ) , config ) and
1385- nodeCand2 ( node1 , _ , _ , unbind ( config ) )
1388+ nodeCand2 ( node1 , unbind ( config ) )
13861389}
13871390
13881391pragma [ nomagic]
@@ -1391,7 +1394,23 @@ private predicate flowIntoCallableNodeCand2(
13911394) {
13921395 flowIntoCallableNodeCand1 ( node1 , node2 , allowsFieldFlow , config ) and
13931396 nodeCand2 ( node2 , _, apfEmpty .booleanNot ( ) , config ) and
1394- nodeCand2 ( node1 , _, _, unbind ( config ) )
1397+ nodeCand2 ( node1 , unbind ( config ) )
1398+ }
1399+
1400+ pragma [ nomagic]
1401+ private predicate readExtCand (
1402+ NodeExt node1 , Content f , NodeExt node2 , boolean apfEmpty , Configuration config
1403+ ) {
1404+ readExt ( node1 , f , node2 , config ) and
1405+ readStoreCand ( f , apfEmpty , config )
1406+ }
1407+
1408+ pragma [ nomagic]
1409+ private predicate storeExtCand (
1410+ NodeExt node1 , Content f , NodeExt node2 , boolean apfEmpty , Configuration config
1411+ ) {
1412+ storeExt ( node1 , f , node2 , config ) and
1413+ readStoreCand ( f , apfEmpty , config )
13951414}
13961415
13971416private newtype TAccessPathFront =
@@ -1446,7 +1465,7 @@ private predicate flowCandFwd(
14461465 */
14471466private class AccessPathFrontNilNode extends TNodeExt {
14481467 AccessPathFrontNilNode ( ) {
1449- nodeCand2 ( this , _, _ , _ ) and
1468+ nodeCand2 ( this , _) and
14501469 (
14511470 any ( Configuration c ) .isSource ( this .( NodeExt ) .getNode ( ) )
14521471 or
@@ -1476,7 +1495,7 @@ private predicate flowCandFwd0(
14761495 apf = node .( AccessPathFrontNilNode ) .getApf ( ) and
14771496 apfEmpty = true
14781497 or
1479- nodeCand2 ( node , _ , _ , _ ) and
1498+ nodeCand2 ( node , unbind ( config ) ) and
14801499 (
14811500 exists ( NodeExt mid |
14821501 flowCandFwd ( mid , fromArg , apf , apfEmpty , config ) and
@@ -1531,9 +1550,10 @@ private predicate flowCandFwd0(
15311550 ( apfEmpty = true or allowsFieldFlow = true )
15321551 )
15331552 or
1534- exists ( Content f , AccessPathFront apf0 , boolean apf0Empty |
1535- flowCandFwdStore ( f , node , fromArg , apf0 , apf0Empty , config ) and
1536- readStoreCand ( f , unbindBool ( apf0Empty .booleanNot ( ) ) , unbind ( config ) ) and
1553+ exists ( NodeExt mid , Content f , boolean apf0Empty |
1554+ flowCandFwd ( mid , fromArg , _, apf0Empty , config ) and
1555+ storeExtCand ( mid , f , node , _/*apf0Empty*/ , config ) and
1556+ nodeCand2 ( node , _, true , unbind ( config ) ) and
15371557 apf .headUsesContent ( f ) and
15381558 apfEmpty = false
15391559 )
@@ -1544,34 +1564,23 @@ private predicate flowCandFwd0(
15441564 )
15451565}
15461566
1547- pragma [ nomagic]
1548- private predicate flowCandFwdStore (
1549- Content f , NodeExt node , boolean fromArg , AccessPathFront apf , boolean apfEmpty ,
1550- Configuration config
1551- ) {
1552- exists ( NodeExt mid |
1553- flowCandFwd ( mid , fromArg , apf , apfEmpty , config ) and
1554- storeExt ( mid , f , node , config ) and
1555- nodeCand2 ( node , _, true , unbind ( config ) ) and
1556- compatibleTypes ( apf .getType ( ) , f .getType ( ) )
1557- )
1558- }
1559-
15601567pragma [ nomagic]
15611568private predicate consCandFwd ( Content f , AccessPathFront apf , boolean apfEmpty , Configuration config ) {
1562- exists ( NodeExt n |
1563- flowCandFwdStore ( f , n , _, apf , apfEmpty , config ) and
1564- readStoreCand ( f , unbindBool ( apfEmpty .booleanNot ( ) ) , unbind ( config ) )
1569+ exists ( NodeExt mid , NodeExt n |
1570+ flowCandFwd ( mid , _, apf , apfEmpty , config ) and
1571+ storeExtCand ( mid , f , n , _ /*apfEmpty*/ , config ) and
1572+ nodeCand2 ( n , _, true , unbind ( config ) ) and
1573+ compatibleTypes ( apf .getType ( ) , f .getType ( ) )
15651574 )
15661575}
15671576
15681577pragma [ nomagic]
15691578private predicate flowCandFwdRead ( Content f , NodeExt node , boolean fromArg , Configuration config ) {
1570- exists ( NodeExt mid , AccessPathFront apf |
1579+ exists ( NodeExt mid , AccessPathFrontHead apf |
15711580 flowCandFwd ( mid , fromArg , apf , false , config ) and
1572- readExt ( mid , f , node , config ) and
1581+ readExtCand ( mid , f , node , _ , config ) and
15731582 apf .headUsesContent ( f ) and
1574- nodeCand2 ( node , _ , _ , unbind ( config ) )
1583+ nodeCand2 ( node , unbind ( config ) )
15751584 )
15761585}
15771586
@@ -1662,7 +1671,7 @@ private predicate flowCandRead(
16621671 NodeExt node , Content f , boolean toReturn , AccessPathFront apf0 , Configuration config
16631672) {
16641673 exists ( NodeExt mid |
1665- readExt ( node , f , mid , config ) and
1674+ readExtCand ( node , f , mid , _ , config ) and
16661675 flowCand ( mid , toReturn , apf0 , _, config )
16671676 )
16681677}
@@ -1672,7 +1681,7 @@ private predicate flowCandStore(
16721681 NodeExt node , Content f , boolean toReturn , AccessPathFront apf0 , Configuration config
16731682) {
16741683 exists ( NodeExt mid |
1675- storeExt ( node , f , mid , config ) and
1684+ storeExtCand ( node , f , mid , _ , config ) and
16761685 flowCand ( mid , toReturn , apf0 , _, config )
16771686 )
16781687}
@@ -1911,7 +1920,7 @@ pragma[nomagic]
19111920private predicate flowFwdStore0 (
19121921 NodeExt mid , Content f , NodeExt node , AccessPathFront apf0 , Configuration config
19131922) {
1914- storeExt ( mid , f , node , config ) and
1923+ storeExtCand ( mid , f , node , _ , config ) and
19151924 flowCand ( mid , _, apf0 , _, config )
19161925}
19171926
@@ -1931,7 +1940,7 @@ private predicate flowFwdRead(
19311940) {
19321941 exists ( NodeExt mid , AccessPathFrontHead apf0 |
19331942 flowFwd ( mid , fromArg , apf0 , false , ap0 , config ) and
1934- readExt ( mid , f , node , config ) and
1943+ readExtCand ( mid , f , node , _ , config ) and
19351944 apf0 .headUsesContent ( f ) and
19361945 flowCand ( node , _, _, _, unbind ( config ) )
19371946 )
@@ -2027,7 +2036,7 @@ pragma[nomagic]
20272036private predicate storeFwd (
20282037 NodeExt node1 , Content f , NodeExt node2 , AccessPath ap , AccessPath ap0 , Configuration config
20292038) {
2030- storeExt ( node1 , f , node2 , config ) and
2039+ storeExtCand ( node1 , f , node2 , _ , config ) and
20312040 flowFwdStore ( node2 , f , ap , _, _, config ) and
20322041 ap0 = push ( f , ap )
20332042}
@@ -2046,7 +2055,7 @@ pragma[nomagic]
20462055private predicate readFwd (
20472056 NodeExt node1 , Content f , NodeExt node2 , AccessPath ap , AccessPath ap0 , Configuration config
20482057) {
2049- readExt ( node1 , f , node2 , config ) and
2058+ readExtCand ( node1 , f , node2 , _ , config ) and
20502059 flowFwdRead ( node2 , f , ap , _, config ) and
20512060 ap0 = pop ( f , ap )
20522061}
0 commit comments