@@ -1433,9 +1433,12 @@ private module MkStage<StageSig PrevStage> {
1433
1433
)
1434
1434
or
1435
1435
// flow through a callable
1436
- exists ( DataFlowCall call , ParamNodeEx summaryCtx0 , Ap argAp0 |
1437
- fwdFlowOutFromArg ( call , node , state , summaryCtx0 , argAp0 , ap , apa , config ) and
1438
- fwdFlowIsEntered ( call , cc , summaryCtx , argAp , summaryCtx0 , argAp0 , config )
1436
+ exists (
1437
+ DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow , ApApprox innerArgApa
1438
+ |
1439
+ fwdFlowThrough ( call , cc , state , ccc , summaryCtx , argAp , ap , apa , ret , innerArgApa , config ) and
1440
+ flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow , innerArgApa , apa , config ) and
1441
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1439
1442
)
1440
1443
}
1441
1444
@@ -1505,62 +1508,40 @@ private module MkStage<StageSig PrevStage> {
1505
1508
1506
1509
pragma [ nomagic]
1507
1510
private predicate fwdFlowRetFromArg (
1508
- RetNodeEx ret , FlowState state , CcCall ccc , ParamNodeEx summaryCtx , Ap argAp , ApApprox argApa ,
1509
- Ap ap , ApApprox apa , Configuration config
1511
+ RetNodeEx ret , ReturnKindExt kind , FlowState state , CcCall ccc , ParamNodeEx summaryCtx ,
1512
+ Ap argAp , ApApprox argApa , Ap ap , ApApprox apa , Configuration config
1510
1513
) {
1511
- exists ( ReturnKindExt kind |
1512
- fwdFlow ( pragma [ only_bind_into ] ( ret ) , state , ccc ,
1513
- TParamNodeSome ( pragma [ only_bind_into ] ( summaryCtx . asNode ( ) ) ) , apSome ( argAp ) , ap , apa ,
1514
- config ) and
1515
- getApprox ( argAp ) = argApa and
1516
- kind = ret . getKind ( ) and
1517
- parameterFlowThroughAllowed ( summaryCtx , kind )
1518
- )
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 ) )
1519
1522
}
1520
1523
1521
1524
pragma [ inline]
1522
- private predicate fwdFlowInMayFlowThrough (
1523
- DataFlowCall call , Cc cc , CcCall innerCc , ParamNodeOption summaryCtx , ApOption argAp ,
1524
- ParamNodeEx param , Ap ap , ApApprox apa , Configuration config
1525
- ) {
1526
- fwdFlowIn ( call , pragma [ only_bind_into ] ( param ) , _, cc , innerCc , summaryCtx , argAp , ap ,
1527
- pragma [ only_bind_into ] ( apa ) , pragma [ only_bind_into ] ( config ) ) and
1528
- PrevStage:: parameterMayFlowThrough ( param , apa , config )
1529
- }
1530
-
1531
- // dedup before joining with `flowThroughOutOfCall`
1532
- pragma [ nomagic]
1533
- private predicate fwdFlowInMayFlowThroughProj (
1534
- DataFlowCall call , CcCall innerCc , ApApprox apa , Configuration config
1535
- ) {
1536
- fwdFlowInMayFlowThrough ( call , _, innerCc , _, _, _, _, apa , config )
1537
- }
1538
-
1539
- /**
1540
- * Same as `flowThroughOutOfCall`, but restricted to calls that are reached
1541
- * in the flow covered by `fwdFlow`, where data might flow through the target
1542
- * callable and back out at `call`.
1543
- */
1544
- pragma [ nomagic]
1545
- private predicate fwdFlowThroughOutOfCall (
1546
- DataFlowCall call , CcCall ccc , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1547
- ApApprox argApa , ApApprox apa , Configuration config
1525
+ private predicate fwdFlowThrough0 (
1526
+ 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
1548
1529
) {
1549
- fwdFlowInMayFlowThroughProj ( call , ccc , argApa , config ) and
1550
- flowThroughOutOfCall ( call , ccc , ret , out , allowsFieldFlow , argApa , apa , config )
1530
+ fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , kind , state , pragma [ only_bind_into ] ( ccc ) ,
1531
+ innerSummaryCtx , innerArgAp , innerArgApa , ap , pragma [ only_bind_into ] ( apa ) ,
1532
+ pragma [ only_bind_into ] ( config ) ) and
1533
+ fwdFlowIsEntered ( call , cc , ccc , summaryCtx , argAp , innerSummaryCtx , innerArgAp ,
1534
+ pragma [ only_bind_into ] ( config ) ) and
1535
+ matchesCall ( ccc , call )
1551
1536
}
1552
1537
1553
1538
pragma [ nomagic]
1554
- private predicate fwdFlowOutFromArg (
1555
- DataFlowCall call , NodeEx out , FlowState state , ParamNodeEx summaryCtx , Ap argAp , Ap ap ,
1556
- ApApprox apa , Configuration config
1539
+ private predicate fwdFlowThrough (
1540
+ DataFlowCall call , Cc cc , FlowState state , CcCall ccc , ParamNodeOption summaryCtx ,
1541
+ ApOption argAp , Ap ap , ApApprox apa , RetNodeEx ret , ApApprox innerArgApa , Configuration config
1557
1542
) {
1558
- exists ( RetNodeEx ret , boolean allowsFieldFlow , CcCall ccc , ApApprox argApa |
1559
- fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) ,
1560
- summaryCtx , argAp , pragma [ only_bind_into ] ( argApa ) , ap , pragma [ only_bind_into ] ( apa ) , config ) and
1561
- fwdFlowThroughOutOfCall ( call , ccc , ret , out , allowsFieldFlow , argApa , apa , config ) and
1562
- ( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) )
1563
- )
1543
+ fwdFlowThrough0 ( call , cc , state , ccc , summaryCtx , argAp , ap , apa , ret , _, _, _, innerArgApa ,
1544
+ config )
1564
1545
}
1565
1546
1566
1547
/**
@@ -1569,10 +1550,15 @@ private module MkStage<StageSig PrevStage> {
1569
1550
*/
1570
1551
pragma [ nomagic]
1571
1552
private predicate fwdFlowIsEntered (
1572
- DataFlowCall call , Cc cc , ParamNodeOption summaryCtx , ApOption argAp , ParamNodeEx p , Ap ap ,
1573
- Configuration config
1553
+ DataFlowCall call , Cc cc , CcCall innerCc , ParamNodeOption summaryCtx , ApOption argAp ,
1554
+ ParamNodeEx p , Ap ap , Configuration config
1574
1555
) {
1575
- fwdFlowInMayFlowThrough ( call , cc , _, summaryCtx , argAp , p , ap , _, config )
1556
+ exists ( ApApprox apa |
1557
+ fwdFlowIn ( call , pragma [ only_bind_into ] ( p ) , _, cc , innerCc , summaryCtx , argAp , ap ,
1558
+ pragma [ only_bind_into ] ( apa ) , pragma [ only_bind_into ] ( config ) ) and
1559
+ PrevStage:: parameterMayFlowThrough ( p , apa , config ) and
1560
+ PrevStage:: callMayFlowThroughRev ( call , pragma [ only_bind_into ] ( config ) )
1561
+ )
1576
1562
}
1577
1563
1578
1564
pragma [ nomagic]
@@ -1591,17 +1577,25 @@ private module MkStage<StageSig PrevStage> {
1591
1577
fwdFlowConsCand ( ap1 , c , ap2 , config )
1592
1578
}
1593
1579
1580
+ pragma [ nomagic]
1581
+ private predicate returnFlowsThrough0 (
1582
+ 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
+ ) {
1586
+ fwdFlowThrough0 ( call , _, state , ccc , _, _, ap , apa , ret , kind , innerSummaryCtx , innerArgAp ,
1587
+ innerArgApa , config )
1588
+ }
1589
+
1594
1590
pragma [ nomagic]
1595
1591
private predicate returnFlowsThrough (
1596
1592
RetNodeEx ret , ReturnKindExt kind , FlowState state , CcCall ccc , ParamNodeEx p , Ap argAp ,
1597
1593
Ap ap , Configuration config
1598
1594
) {
1599
- exists ( boolean allowsFieldFlow , ApApprox argApa , ApApprox apa |
1600
- fwdFlowRetFromArg ( pragma [ only_bind_into ] ( ret ) , state , pragma [ only_bind_into ] ( ccc ) , p , argAp ,
1601
- pragma [ only_bind_into ] ( argApa ) , ap , pragma [ only_bind_into ] ( apa ) , config ) and
1602
- kind = ret .getKind ( ) and
1603
- fwdFlowThroughOutOfCall ( _, ccc , ret , _, allowsFieldFlow , argApa , apa , config ) and
1604
- ( if allowsFieldFlow = false then ap instanceof ApNil else any ( ) )
1595
+ exists ( DataFlowCall call , ApApprox apa , boolean allowsFieldFlow , ApApprox innerArgApa |
1596
+ returnFlowsThrough0 ( call , state , ccc , ap , apa , ret , kind , p , argAp , innerArgApa , config ) and
1597
+ flowThroughOutOfCall ( call , ccc , ret , _, allowsFieldFlow , innerArgApa , apa , config ) and
1598
+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1605
1599
)
1606
1600
}
1607
1601
0 commit comments