@@ -1489,10 +1489,6 @@ private module MkStage<StageSig PrevStage> {
1489
1489
parameterFlowThroughAllowed ( p , ret .getKind ( ) )
1490
1490
}
1491
1491
1492
- predicate returnMayFlowThrough ( RetNodeEx ret , Configuration config ) {
1493
- returnFlowsThrough ( ret , _, _, _, _, _, config )
1494
- }
1495
-
1496
1492
pragma [ nomagic]
1497
1493
private predicate flowThroughIntoCall (
1498
1494
DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow , Configuration config
@@ -1507,52 +1503,58 @@ private module MkStage<StageSig PrevStage> {
1507
1503
* Holds if `node` with access path `ap` is part of a path from a source to a
1508
1504
* sink in the configuration `config`.
1509
1505
*
1510
- * The Boolean `toReturn ` records whether the node must be returned from the
1511
- * enclosing callable in order to reach a sink, and if so, `returnAp` records
1512
- * the access path of the returned value.
1506
+ * The parameter `returnCtx ` records whether (and how) the node must be returned
1507
+ * from the enclosing callable in order to reach a sink, and if so, `returnAp`
1508
+ * records the access path of the returned value.
1513
1509
*/
1514
1510
pragma [ nomagic]
1515
1511
additional predicate revFlow (
1516
- NodeEx node , FlowState state , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
1512
+ NodeEx node , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap ,
1513
+ Configuration config
1517
1514
) {
1518
- revFlow0 ( node , state , toReturn , returnAp , ap , config ) and
1515
+ revFlow0 ( node , state , returnCtx , returnAp , ap , config ) and
1519
1516
fwdFlow ( node , state , _, _, _, ap , config )
1520
1517
}
1521
1518
1522
1519
pragma [ nomagic]
1523
1520
private predicate revFlow0 (
1524
- NodeEx node , FlowState state , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
1521
+ NodeEx node , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap ,
1522
+ Configuration config
1525
1523
) {
1526
1524
fwdFlow ( node , state , _, _, _, ap , config ) and
1527
1525
sinkNode ( node , state , config ) and
1528
- ( if hasSinkCallCtx ( config ) then toReturn = true else toReturn = false ) and
1526
+ (
1527
+ if hasSinkCallCtx ( config )
1528
+ then returnCtx = TReturnCtxNoFlowThrough ( )
1529
+ else returnCtx = TReturnCtxNone ( )
1530
+ ) and
1529
1531
returnAp = apNone ( ) and
1530
1532
ap instanceof ApNil
1531
1533
or
1532
1534
exists ( NodeEx mid , FlowState state0 |
1533
1535
localStep ( node , state , mid , state0 , true , _, config , _) and
1534
- revFlow ( mid , state0 , toReturn , returnAp , ap , config )
1536
+ revFlow ( mid , state0 , returnCtx , returnAp , ap , config )
1535
1537
)
1536
1538
or
1537
1539
exists ( NodeEx mid , FlowState state0 , ApNil nil |
1538
1540
fwdFlow ( node , pragma [ only_bind_into ] ( state ) , _, _, _, ap , pragma [ only_bind_into ] ( config ) ) and
1539
1541
localStep ( node , pragma [ only_bind_into ] ( state ) , mid , state0 , false , _, config , _) and
1540
- revFlow ( mid , state0 , toReturn , returnAp , nil , pragma [ only_bind_into ] ( config ) ) and
1542
+ revFlow ( mid , state0 , returnCtx , returnAp , nil , pragma [ only_bind_into ] ( config ) ) and
1541
1543
ap instanceof ApNil
1542
1544
)
1543
1545
or
1544
1546
exists ( NodeEx mid |
1545
1547
jumpStep ( node , mid , config ) and
1546
1548
revFlow ( mid , state , _, _, ap , config ) and
1547
- toReturn = false and
1549
+ returnCtx = TReturnCtxNone ( ) and
1548
1550
returnAp = apNone ( )
1549
1551
)
1550
1552
or
1551
1553
exists ( NodeEx mid , ApNil nil |
1552
1554
fwdFlow ( node , _, _, _, _, ap , pragma [ only_bind_into ] ( config ) ) and
1553
1555
additionalJumpStep ( node , mid , config ) and
1554
1556
revFlow ( pragma [ only_bind_into ] ( mid ) , state , _, _, nil , pragma [ only_bind_into ] ( config ) ) and
1555
- toReturn = false and
1557
+ returnCtx = TReturnCtxNone ( ) and
1556
1558
returnAp = apNone ( ) and
1557
1559
ap instanceof ApNil
1558
1560
)
@@ -1562,47 +1564,50 @@ private module MkStage<StageSig PrevStage> {
1562
1564
additionalJumpStateStep ( node , state , mid , state0 , config ) and
1563
1565
revFlow ( pragma [ only_bind_into ] ( mid ) , pragma [ only_bind_into ] ( state0 ) , _, _, nil ,
1564
1566
pragma [ only_bind_into ] ( config ) ) and
1565
- toReturn = false and
1567
+ returnCtx = TReturnCtxNone ( ) and
1566
1568
returnAp = apNone ( ) and
1567
1569
ap instanceof ApNil
1568
1570
)
1569
1571
or
1570
1572
// store
1571
1573
exists ( Ap ap0 , Content c |
1572
- revFlowStore ( ap0 , c , ap , node , state , _, _, toReturn , returnAp , config ) and
1574
+ revFlowStore ( ap0 , c , ap , node , state , _, _, returnCtx , returnAp , config ) and
1573
1575
revFlowConsCand ( ap0 , c , ap , config )
1574
1576
)
1575
1577
or
1576
1578
// read
1577
1579
exists ( NodeEx mid , Ap ap0 |
1578
- revFlow ( mid , state , toReturn , returnAp , ap0 , config ) and
1580
+ revFlow ( mid , state , returnCtx , returnAp , ap0 , config ) and
1579
1581
readStepFwd ( node , ap , _, mid , ap0 , config )
1580
1582
)
1581
1583
or
1582
1584
// flow into a callable
1583
1585
revFlowInNotToReturn ( node , state , returnAp , ap , config ) and
1584
- toReturn = false
1586
+ returnCtx = TReturnCtxNone ( )
1585
1587
or
1586
1588
// flow through a callable
1587
- exists ( DataFlowCall call , Ap returnAp0 |
1588
- revFlowInToReturn ( call , node , state , returnAp0 , ap , config ) and
1589
- revFlowIsReturned ( call , toReturn , returnAp , returnAp0 , config )
1589
+ exists ( DataFlowCall call , ReturnPosition returnPos0 , Ap returnAp0 |
1590
+ revFlowInToReturn ( call , node , state , returnPos0 , returnAp0 , ap , config ) and
1591
+ revFlowIsReturned ( call , returnCtx , returnAp , returnPos0 , returnAp0 , config )
1590
1592
)
1591
1593
or
1592
1594
// flow out of a callable
1593
1595
revFlowOut ( _, node , state , _, _, ap , config ) and
1594
- toReturn = true and
1595
1596
if returnFlowsThrough ( node , state , _, _, _, ap , config )
1596
- then returnAp = apSome ( ap )
1597
- else returnAp = apNone ( )
1597
+ then (
1598
+ returnCtx = TReturnCtxMaybeFlowThrough ( node .( RetNodeEx ) .getReturnPosition ( ) ) and
1599
+ returnAp = apSome ( ap )
1600
+ ) else (
1601
+ returnCtx = TReturnCtxNoFlowThrough ( ) and returnAp = apNone ( )
1602
+ )
1598
1603
}
1599
1604
1600
1605
pragma [ nomagic]
1601
1606
private predicate revFlowStore (
1602
1607
Ap ap0 , Content c , Ap ap , NodeEx node , FlowState state , TypedContent tc , NodeEx mid ,
1603
- boolean toReturn , ApOption returnAp , Configuration config
1608
+ ReturnCtx returnCtx , ApOption returnAp , Configuration config
1604
1609
) {
1605
- revFlow ( mid , state , toReturn , returnAp , ap0 , config ) and
1610
+ revFlow ( mid , state , returnCtx , returnAp , ap0 , config ) and
1606
1611
storeStepFwd ( node , ap , tc , mid , ap0 , config ) and
1607
1612
tc .getContent ( ) = c
1608
1613
}
@@ -1622,11 +1627,11 @@ private module MkStage<StageSig PrevStage> {
1622
1627
1623
1628
pragma [ nomagic]
1624
1629
private predicate revFlowOut (
1625
- DataFlowCall call , RetNodeEx ret , FlowState state , boolean toReturn , ApOption returnAp , Ap ap ,
1626
- Configuration config
1630
+ DataFlowCall call , RetNodeEx ret , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
1631
+ Ap ap , Configuration config
1627
1632
) {
1628
1633
exists ( NodeEx out , boolean allowsFieldFlow |
1629
- revFlow ( out , state , toReturn , returnAp , ap , config ) and
1634
+ revFlow ( out , state , returnCtx , returnAp , ap , config ) and
1630
1635
flowOutOfCall ( call , ret , out , allowsFieldFlow , config ) and
1631
1636
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1632
1637
)
@@ -1637,20 +1642,22 @@ private module MkStage<StageSig PrevStage> {
1637
1642
ArgNodeEx arg , FlowState state , ApOption returnAp , Ap ap , Configuration config
1638
1643
) {
1639
1644
exists ( ParamNodeEx p , boolean allowsFieldFlow |
1640
- revFlow ( p , state , false , returnAp , ap , config ) and
1645
+ revFlow ( p , state , TReturnCtxNone ( ) , returnAp , ap , config ) and
1641
1646
flowIntoCall ( _, arg , p , allowsFieldFlow , config ) and
1642
1647
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1643
1648
)
1644
1649
}
1645
1650
1646
1651
pragma [ nomagic]
1647
1652
private predicate revFlowInToReturn (
1648
- DataFlowCall call , ArgNodeEx arg , FlowState state , Ap returnAp , Ap ap , Configuration config
1653
+ DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnPosition returnPos , Ap returnAp ,
1654
+ Ap ap , Configuration config
1649
1655
) {
1650
1656
exists ( ParamNodeEx p , boolean allowsFieldFlow |
1651
- revFlow ( p , state , true , apSome ( returnAp ) , ap , config ) and
1657
+ revFlow ( p , state , TReturnCtxMaybeFlowThrough ( returnPos ) , apSome ( returnAp ) , ap , config ) and
1652
1658
flowThroughIntoCall ( call , arg , p , allowsFieldFlow , config ) and
1653
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1659
+ ( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) ) and
1660
+ parameterFlowThroughAllowed ( p .asNode ( ) , returnPos .getKind ( ) )
1654
1661
)
1655
1662
}
1656
1663
@@ -1661,11 +1668,13 @@ private module MkStage<StageSig PrevStage> {
1661
1668
*/
1662
1669
pragma [ nomagic]
1663
1670
private predicate revFlowIsReturned (
1664
- DataFlowCall call , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
1671
+ DataFlowCall call , ReturnCtx returnCtx , ApOption returnAp , ReturnPosition pos , Ap ap ,
1672
+ Configuration config
1665
1673
) {
1666
1674
exists ( RetNodeEx ret , FlowState state , CcCall ccc |
1667
- revFlowOut ( call , ret , state , toReturn , returnAp , ap , config ) and
1675
+ revFlowOut ( call , ret , state , returnCtx , returnAp , ap , config ) and
1668
1676
returnFlowsThrough ( ret , state , ccc , _, _, ap , config ) and
1677
+ pos = ret .getReturnPosition ( ) and
1669
1678
matchesCall ( ccc , call )
1670
1679
)
1671
1680
}
@@ -1736,34 +1745,39 @@ private module MkStage<StageSig PrevStage> {
1736
1745
validAp ( ap , config )
1737
1746
}
1738
1747
1739
- pragma [ noinline ]
1740
- private predicate parameterFlow (
1741
- ParamNodeEx p , Ap ap , Ap ap0 , DataFlowCallable c , Configuration config
1748
+ pragma [ nomagic ]
1749
+ private predicate parameterFlowsThroughRev (
1750
+ ParamNodeEx p , Ap ap , ReturnPosition returnPos , Configuration config
1742
1751
) {
1743
- revFlow ( p , _, true , apSome ( ap0 ) , ap , config ) and
1744
- c = p . getEnclosingCallable ( )
1752
+ revFlow ( p , _, TReturnCtxMaybeFlowThrough ( returnPos ) , apSome ( _ ) , ap , config ) and
1753
+ parameterFlowThroughAllowed ( p . asNode ( ) , returnPos . getKind ( ) )
1745
1754
}
1746
1755
1756
+ pragma [ nomagic]
1747
1757
predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) {
1748
- exists ( DataFlowCallable c , RetNodeEx ret , FlowState state , Ap ap0 , ParameterPosition pos |
1749
- parameterFlow ( p , ap , ap0 , c , config ) and
1750
- c = ret .getEnclosingCallable ( ) and
1751
- revFlow ( pragma [ only_bind_into ] ( ret ) , pragma [ only_bind_into ] ( state ) , true , apSome ( _) ,
1752
- pragma [ only_bind_into ] ( ap0 ) , pragma [ only_bind_into ] ( config ) ) and
1753
- returnFlowsThrough ( ret , state , _, p .asNode ( ) , ap , ap0 , config ) and
1754
- p .getPosition ( ) = pos and
1755
- parameterFlowThroughAllowed ( p .asNode ( ) , ret .getKind ( ) )
1758
+ exists ( RetNodeEx ret |
1759
+ returnFlowsThrough ( ret , _, _, p .asNode ( ) , ap , _, config ) and
1760
+ parameterFlowsThroughRev ( p , ap , ret .getReturnPosition ( ) , config )
1761
+ )
1762
+ }
1763
+
1764
+ pragma [ nomagic]
1765
+ predicate returnMayFlowThrough ( RetNodeEx ret , Configuration config ) {
1766
+ exists ( ParamNodeEx p , Ap ap |
1767
+ returnFlowsThrough ( ret , _, _, p .asNode ( ) , ap , _, config ) and
1768
+ parameterFlowsThroughRev ( p , ap , ret .getReturnPosition ( ) , config )
1756
1769
)
1757
1770
}
1758
1771
1759
1772
pragma [ nomagic]
1760
1773
predicate callMayFlowThroughRev ( DataFlowCall call , Configuration config ) {
1761
1774
exists (
1762
- Ap returnAp0 , ArgNodeEx arg , FlowState state , boolean toReturn , ApOption returnAp , Ap ap
1775
+ ReturnPosition returnPos0 , Ap returnAp0 , ArgNodeEx arg , FlowState state ,
1776
+ ReturnCtx returnCtx , ApOption returnAp , Ap ap
1763
1777
|
1764
- revFlow ( arg , state , toReturn , returnAp , ap , config ) and
1765
- revFlowInToReturn ( call , arg , state , returnAp0 , ap , config ) and
1766
- revFlowIsReturned ( call , toReturn , returnAp , returnAp0 , config )
1778
+ revFlow ( arg , state , returnCtx , returnAp , ap , config ) and
1779
+ revFlowInToReturn ( call , arg , state , returnPos0 , returnAp0 , ap , config ) and
1780
+ revFlowIsReturned ( call , returnCtx , returnAp , returnPos0 , returnAp0 , config )
1767
1781
)
1768
1782
}
1769
1783
@@ -1786,8 +1800,8 @@ private module MkStage<StageSig PrevStage> {
1786
1800
conscand = count ( TypedContent f0 , Ap ap | consCand ( f0 , ap , config ) ) and
1787
1801
states = count ( FlowState state | revFlow ( _, state , _, _, _, config ) ) and
1788
1802
tuples =
1789
- count ( NodeEx n , FlowState state , boolean b , ApOption retAp , Ap ap |
1790
- revFlow ( n , state , b , retAp , ap , config )
1803
+ count ( NodeEx n , FlowState state , ReturnCtx returnCtx , ApOption retAp , Ap ap |
1804
+ revFlow ( n , state , returnCtx , retAp , ap , config )
1791
1805
)
1792
1806
}
1793
1807
/* End: Stage logic. */
@@ -2250,7 +2264,7 @@ private predicate flowCandSummaryCtx(
2250
2264
NodeEx node , FlowState state , AccessPathFront argApf , Configuration config
2251
2265
) {
2252
2266
exists ( AccessPathFront apf |
2253
- Stage3:: revFlow ( node , state , true , _, apf , config ) and
2267
+ Stage3:: revFlow ( node , state , TReturnCtxMaybeFlowThrough ( _ ) , _, apf , config ) and
2254
2268
Stage3:: fwdFlow ( node , state , any ( Stage3:: CcCall ccc ) , _, TAccessPathFrontSome ( argApf ) , apf ,
2255
2269
config )
2256
2270
)
@@ -2530,7 +2544,7 @@ private predicate nodeMayUseSummary0(
2530
2544
) {
2531
2545
exists ( AccessPathApprox apa0 |
2532
2546
Stage4:: parameterMayFlowThrough ( p , _, _) and
2533
- Stage4:: revFlow ( n , state , true , _, apa0 , config ) and
2547
+ Stage4:: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _ ) , _, apa0 , config ) and
2534
2548
Stage4:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParamNodeSome ( p .asNode ( ) ) ,
2535
2549
TAccessPathApproxSome ( apa ) , apa0 , config )
2536
2550
)
0 commit comments