@@ -1467,10 +1467,11 @@ module MakeImpl<InputSig Lang> {
1467
1467
pragma [ nomagic]
1468
1468
private predicate fwdFlowIntoArg (
1469
1469
ArgNodeEx arg , FlowState state , Cc outercc , ParamNodeOption summaryCtx , TypOption argT ,
1470
- ApOption argAp , Typ t , Ap ap , ApApprox apa , boolean cc
1470
+ ApOption argAp , Typ t , Ap ap , boolean emptyAp , ApApprox apa , boolean cc
1471
1471
) {
1472
1472
fwdFlow ( arg , state , outercc , summaryCtx , argT , argAp , t , ap , apa ) and
1473
- if outercc instanceof CcCall then cc = true else cc = false
1473
+ ( if outercc instanceof CcCall then cc = true else cc = false ) and
1474
+ if ap instanceof ApNil then emptyAp = true else emptyAp = false
1474
1475
}
1475
1476
1476
1477
private signature module FwdFlowInInputSig {
@@ -1552,26 +1553,59 @@ module MakeImpl<InputSig Lang> {
1552
1553
viableImplNotCallContextReducedInlineLate ( call , outercc )
1553
1554
}
1554
1555
1555
- pragma [ nomagic ]
1556
+ pragma [ inline ]
1556
1557
private predicate fwdFlowInCand (
1558
+ DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
1559
+ ParamNodeEx p , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap ,
1560
+ boolean emptyAp , ApApprox apa , boolean cc
1561
+ ) {
1562
+ exists ( boolean allowsFieldFlow |
1563
+ fwdFlowIntoArg ( arg , state , outercc , summaryCtx , argT , argAp , t , ap , emptyAp , apa , cc ) and
1564
+ (
1565
+ inner = viableImplCallContextReducedInlineLate ( call , arg , outercc )
1566
+ or
1567
+ viableImplArgNotCallContextReduced ( call , arg , outercc )
1568
+ ) and
1569
+ callEdgeArgParamRestrictedInlineLate ( call , inner , arg , p , allowsFieldFlow , apa ) and
1570
+ if allowsFieldFlow = false then emptyAp = true else any ( )
1571
+ )
1572
+ }
1573
+
1574
+ pragma [ inline]
1575
+ private predicate fwdFlowInCandTypeFlowDisabled (
1576
+ DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
1577
+ ParamNodeEx p , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap ,
1578
+ ApApprox apa , boolean cc
1579
+ ) {
1580
+ not enableTypeFlow ( ) and
1581
+ fwdFlowInCand ( call , arg , state , outercc , inner , p , summaryCtx , argT , argAp , t , ap , _,
1582
+ apa , cc )
1583
+ }
1584
+
1585
+ pragma [ nomagic]
1586
+ private predicate fwdFlowInCandTypeFlowEnabled (
1557
1587
DataFlowCall call , ArgNodeEx arg , Cc outercc , DataFlowCallable inner , ParamNodeEx p ,
1558
- ApApprox apa , boolean allowsFieldFlow , boolean cc
1588
+ boolean emptyAp , ApApprox apa , boolean cc
1559
1589
) {
1560
- fwdFlowIntoArg ( arg , _, outercc , _, _, _, _, _, apa , cc ) and
1561
- (
1562
- inner = viableImplCallContextReducedInlineLate ( call , arg , outercc )
1563
- or
1564
- viableImplArgNotCallContextReduced ( call , arg , outercc )
1565
- ) and
1566
- callEdgeArgParamRestrictedInlineLate ( call , inner , arg , p , allowsFieldFlow , apa )
1590
+ enableTypeFlow ( ) and
1591
+ fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, _, _, emptyAp , apa , cc )
1592
+ }
1593
+
1594
+ pragma [ nomagic]
1595
+ private predicate fwdFlowInValidEdgeTypeFlowDisabled (
1596
+ DataFlowCall call , DataFlowCallable inner , CcCall innercc , boolean cc
1597
+ ) {
1598
+ not enableTypeFlow ( ) and
1599
+ FwdTypeFlow:: typeFlowValidEdgeIn ( call , inner , cc ) and
1600
+ innercc = getCallContextCall ( call , inner )
1567
1601
}
1568
1602
1569
1603
pragma [ nomagic]
1570
- private predicate fwdFlowInValidEdge (
1604
+ private predicate fwdFlowInValidEdgeTypeFlowEnabled (
1571
1605
DataFlowCall call , ArgNodeEx arg , Cc outercc , DataFlowCallable inner , ParamNodeEx p ,
1572
- CcCall innercc , ApApprox apa , boolean allowsFieldFlow , boolean cc
1606
+ CcCall innercc , boolean emptyAp , ApApprox apa , boolean cc
1573
1607
) {
1574
- fwdFlowInCand ( call , arg , outercc , inner , p , apa , allowsFieldFlow , cc ) and
1608
+ fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ) and
1575
1609
FwdTypeFlow:: typeFlowValidEdgeIn ( call , inner , cc ) and
1576
1610
innercc = getCallContextCall ( call , inner )
1577
1611
}
@@ -1582,10 +1616,18 @@ module MakeImpl<InputSig Lang> {
1582
1616
CcCall innercc , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t ,
1583
1617
Ap ap , ApApprox apa , boolean cc
1584
1618
) {
1585
- exists ( ArgNodeEx arg , boolean allowsFieldFlow |
1586
- fwdFlowIntoArg ( arg , state , outercc , summaryCtx , argT , argAp , t , ap , apa , cc ) and
1587
- fwdFlowInValidEdge ( call , arg , outercc , inner , p , innercc , apa , allowsFieldFlow , cc ) and
1588
- if allowsFieldFlow = false then ap instanceof ApNil else any ( )
1619
+ exists ( ArgNodeEx arg |
1620
+ // type flow disabled: linear recursion
1621
+ fwdFlowInCandTypeFlowDisabled ( call , arg , state , outercc , inner , p , summaryCtx , argT ,
1622
+ argAp , t , ap , apa , cc ) and
1623
+ fwdFlowInValidEdgeTypeFlowDisabled ( call , inner , innercc , cc )
1624
+ or
1625
+ // type flow enabled: non-linear recursion
1626
+ exists ( boolean emptyAp |
1627
+ fwdFlowIntoArg ( arg , state , outercc , summaryCtx , argT , argAp , t , ap , emptyAp , apa , cc ) and
1628
+ fwdFlowInValidEdgeTypeFlowEnabled ( call , arg , outercc , inner , p , innercc , emptyAp ,
1629
+ apa , cc )
1630
+ )
1589
1631
)
1590
1632
}
1591
1633
}
0 commit comments