@@ -545,6 +545,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
545
545
private module Stage1 implements StageSig {
546
546
class Ap = Unit ;
547
547
548
+ class ApNil = Ap ;
549
+
548
550
private class Cc = boolean ;
549
551
550
552
/* Begin: Stage 1 logic. */
@@ -1297,6 +1299,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1297
1299
private signature module StageSig {
1298
1300
class Ap ;
1299
1301
1302
+ class ApNil extends Ap ;
1303
+
1300
1304
predicate revFlow ( NodeEx node ) ;
1301
1305
1302
1306
predicate revFlowAp ( NodeEx node , Ap ap ) ;
@@ -1560,20 +1564,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1560
1564
apa = getApprox ( ap )
1561
1565
)
1562
1566
or
1563
- // flow into a callable
1564
- exists ( boolean allowsFlowThrough |
1565
- fwdFlowIn ( node , apa , state , cc , t , ap , allowsFlowThrough ) and
1566
- if allowsFlowThrough = true
1567
- then (
1568
- summaryCtx = TSummaryCtxSome ( node , state , t , ap )
1569
- ) else (
1570
- summaryCtx = TSummaryCtxNone ( ) and
1571
- // When the call contexts of source and sink needs to match then there's
1572
- // never any reason to enter a callable except to find a summary. See also
1573
- // the comment in `PathNodeMid::isAtSink`.
1574
- not Config:: getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
1575
- )
1576
- )
1567
+ // flow into a callable without summary context
1568
+ fwdFlowInNoFlowThrough ( node , apa , state , cc , t , ap ) and
1569
+ summaryCtx = TSummaryCtxNone ( ) and
1570
+ // When the call contexts of source and sink needs to match then there's
1571
+ // never any reason to enter a callable except to find a summary. See also
1572
+ // the comment in `PathNodeMid::isAtSink`.
1573
+ not Config:: getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
1574
+ or
1575
+ // flow into a callable with summary context (non-linear recursion)
1576
+ fwdFlowInFlowThrough ( node , apa , state , cc , t , ap ) and
1577
+ summaryCtx = TSummaryCtxSome ( node , state , t , ap )
1577
1578
or
1578
1579
// flow out of a callable
1579
1580
fwdFlowOut ( _, _, node , state , cc , summaryCtx , t , ap , apa )
@@ -1593,7 +1594,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1593
1594
private newtype TSummaryCtx =
1594
1595
TSummaryCtxNone ( ) or
1595
1596
TSummaryCtxSome ( ParamNodeEx p , FlowState state , Typ t , Ap ap ) {
1596
- fwdFlowIn ( p , _, state , _, t , ap , true )
1597
+ fwdFlowInFlowThrough ( p , _, state , _, t , ap )
1597
1598
}
1598
1599
1599
1600
/**
@@ -1721,12 +1722,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1721
1722
if ap instanceof ApNil then emptyAp = true else emptyAp = false
1722
1723
}
1723
1724
1724
- private signature module FwdFlowInInputSig {
1725
- default predicate callRestriction ( DataFlowCall call ) { any ( ) }
1726
-
1727
- bindingset [ p, apa]
1728
- default predicate parameterRestriction ( ParamNodeEx p , ApApprox apa ) { any ( ) }
1729
- }
1725
+ private signature predicate flowThroughSig ( ) ;
1730
1726
1731
1727
/**
1732
1728
* Exposes the inlined predicate `fwdFlowIn`, which is used to calculate both
@@ -1736,19 +1732,40 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1736
1732
* need to record the argument that flows into the parameter.
1737
1733
*
1738
1734
* For flow through, we do need to record the argument, however, we can restrict
1739
- * this to arguments that may actually flow through, using `callRestriction` and
1740
- * `parameterRestriction`, which reduces the argument-to-parameter fan-in
1741
- * significantly.
1735
+ * this to arguments that may actually flow through, which reduces the
1736
+ * argument-to-parameter fan-in significantly.
1742
1737
*/
1743
- private module FwdFlowIn< FwdFlowInInputSig I > {
1738
+ private module FwdFlowIn< flowThroughSig / 0 flowThrough > {
1744
1739
pragma [ nomagic]
1745
1740
private predicate callEdgeArgParamRestricted (
1746
- DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1747
- boolean allowsFieldFlow , ApApprox apa
1741
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p , boolean emptyAp ,
1742
+ ApApprox apa
1748
1743
) {
1749
- PrevStage:: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa ) and
1750
- I:: callRestriction ( call ) and
1751
- I:: parameterRestriction ( p , apa )
1744
+ exists ( boolean allowsFieldFlow |
1745
+ PrevStage:: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa )
1746
+ |
1747
+ if
1748
+ PrevStage:: callMayFlowThroughRev ( call ) and
1749
+ PrevStage:: parameterMayFlowThrough ( p , apa )
1750
+ then
1751
+ emptyAp = true and
1752
+ apa instanceof PrevStage:: ApNil and
1753
+ flowThrough ( )
1754
+ or
1755
+ emptyAp = false and
1756
+ allowsFieldFlow = true and
1757
+ if allowsFieldFlowThrough ( call , c ) then flowThrough ( ) else not flowThrough ( )
1758
+ else (
1759
+ not flowThrough ( ) and
1760
+ (
1761
+ emptyAp = true and
1762
+ apa instanceof PrevStage:: ApNil
1763
+ or
1764
+ emptyAp = false and
1765
+ allowsFieldFlow = true
1766
+ )
1767
+ )
1768
+ )
1752
1769
}
1753
1770
1754
1771
pragma [ nomagic]
@@ -1780,10 +1797,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1780
1797
bindingset [ call]
1781
1798
pragma [ inline_late]
1782
1799
private predicate callEdgeArgParamRestrictedInlineLate (
1783
- DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1784
- boolean allowsFieldFlow , ApApprox apa
1800
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p , boolean emptyAp ,
1801
+ ApApprox apa
1785
1802
) {
1786
- callEdgeArgParamRestricted ( call , c , arg , p , allowsFieldFlow , apa )
1803
+ callEdgeArgParamRestricted ( call , c , arg , p , emptyAp , apa )
1787
1804
}
1788
1805
1789
1806
bindingset [ call, ctx]
@@ -1807,44 +1824,35 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1807
1824
private predicate fwdFlowInCand (
1808
1825
DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
1809
1826
ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , boolean emptyAp , ApApprox apa ,
1810
- boolean cc , boolean allowsFlowThrough
1827
+ boolean cc
1811
1828
) {
1812
- exists ( boolean allowsFieldFlow |
1813
- fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
1814
- (
1815
- inner = viableImplCallContextReducedInlineLate ( call , arg , outercc )
1816
- or
1817
- viableImplArgNotCallContextReduced ( call , arg , outercc )
1818
- ) and
1819
- not outBarrier ( arg , state ) and
1820
- not inBarrier ( p , state ) and
1821
- callEdgeArgParamRestrictedInlineLate ( call , inner , arg , p , allowsFieldFlow , apa ) and
1822
- ( if allowsFieldFlow = false then emptyAp = true else any ( ) ) and
1823
- if allowsFieldFlowThrough ( call , inner )
1824
- then allowsFlowThrough = true
1825
- else allowsFlowThrough = emptyAp
1826
- )
1829
+ fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
1830
+ (
1831
+ inner = viableImplCallContextReducedInlineLate ( call , arg , outercc )
1832
+ or
1833
+ viableImplArgNotCallContextReduced ( call , arg , outercc )
1834
+ ) and
1835
+ not outBarrier ( arg , state ) and
1836
+ not inBarrier ( p , state ) and
1837
+ callEdgeArgParamRestrictedInlineLate ( call , inner , arg , p , emptyAp , apa )
1827
1838
}
1828
1839
1829
1840
pragma [ inline]
1830
1841
private predicate fwdFlowInCandTypeFlowDisabled (
1831
1842
DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
1832
- ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , ApApprox apa , boolean cc ,
1833
- boolean allowsFlowThrough
1843
+ ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , ApApprox apa , boolean cc
1834
1844
) {
1835
1845
not enableTypeFlow ( ) and
1836
- fwdFlowInCand ( call , arg , state , outercc , inner , p , summaryCtx , t , ap , _, apa , cc ,
1837
- allowsFlowThrough )
1846
+ fwdFlowInCand ( call , arg , state , outercc , inner , p , summaryCtx , t , ap , _, apa , cc )
1838
1847
}
1839
1848
1840
1849
pragma [ nomagic]
1841
1850
private predicate fwdFlowInCandTypeFlowEnabled (
1842
1851
DataFlowCall call , ArgNodeEx arg , Cc outercc , DataFlowCallable inner , ParamNodeEx p ,
1843
- boolean emptyAp , ApApprox apa , boolean cc , boolean allowsFlowThrough
1852
+ boolean emptyAp , ApApprox apa , boolean cc
1844
1853
) {
1845
1854
enableTypeFlow ( ) and
1846
- fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc ,
1847
- allowsFlowThrough )
1855
+ fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc )
1848
1856
}
1849
1857
1850
1858
pragma [ nomagic]
@@ -1859,10 +1867,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1859
1867
pragma [ nomagic]
1860
1868
private predicate fwdFlowInValidEdgeTypeFlowEnabled (
1861
1869
DataFlowCall call , ArgNodeEx arg , Cc outercc , DataFlowCallable inner , ParamNodeEx p ,
1862
- CcCall innercc , boolean emptyAp , ApApprox apa , boolean cc , boolean allowsFlowThrough
1870
+ CcCall innercc , boolean emptyAp , ApApprox apa , boolean cc
1863
1871
) {
1864
- fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ,
1865
- allowsFlowThrough ) and
1872
+ fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ) and
1866
1873
FwdTypeFlow:: typeFlowValidEdgeIn ( call , inner , cc ) and
1867
1874
innercc = getCallContextCall ( call , inner )
1868
1875
}
@@ -1871,36 +1878,42 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1871
1878
predicate fwdFlowIn (
1872
1879
DataFlowCall call , ArgNodeEx arg , DataFlowCallable inner , ParamNodeEx p ,
1873
1880
FlowState state , Cc outercc , CcCall innercc , SummaryCtx summaryCtx , Typ t , Ap ap ,
1874
- ApApprox apa , boolean cc , boolean allowsFlowThrough
1881
+ ApApprox apa , boolean cc
1875
1882
) {
1876
1883
// type flow disabled: linear recursion
1877
1884
fwdFlowInCandTypeFlowDisabled ( call , arg , state , outercc , inner , p , summaryCtx , t , ap ,
1878
- apa , cc , allowsFlowThrough ) and
1885
+ apa , cc ) and
1879
1886
fwdFlowInValidEdgeTypeFlowDisabled ( call , inner , innercc , pragma [ only_bind_into ] ( cc ) )
1880
1887
or
1881
1888
// type flow enabled: non-linear recursion
1882
1889
exists ( boolean emptyAp |
1883
1890
fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
1884
1891
fwdFlowInValidEdgeTypeFlowEnabled ( call , arg , outercc , inner , p , innercc , emptyAp , apa ,
1885
- cc , allowsFlowThrough )
1892
+ cc )
1886
1893
)
1887
1894
}
1888
1895
}
1889
1896
1890
- private module FwdFlowInNoRestriction implements FwdFlowInInputSig { }
1897
+ private predicate bottom ( ) { none ( ) }
1898
+
1899
+ private module FwdFlowInNoThrough = FwdFlowIn< bottom / 0 > ;
1891
1900
1892
1901
pragma [ nomagic]
1893
- private predicate fwdFlowIn (
1894
- ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , Ap ap ,
1895
- boolean allowsFlowThrough
1902
+ private predicate fwdFlowInNoFlowThrough (
1903
+ ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , Ap ap
1896
1904
) {
1897
- exists ( boolean allowsFlowThrough0 |
1898
- FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( _, _, _, p , state , _, innercc , _, t , ap ,
1899
- apa , _, allowsFlowThrough0 ) and
1900
- if PrevStage:: parameterMayFlowThrough ( p , apa )
1901
- then allowsFlowThrough = allowsFlowThrough0
1902
- else allowsFlowThrough = false
1903
- )
1905
+ FwdFlowInNoThrough:: fwdFlowIn ( _, _, _, p , state , _, innercc , _, t , ap , apa , _)
1906
+ }
1907
+
1908
+ private predicate top ( ) { any ( ) }
1909
+
1910
+ private module FwdFlowInThrough = FwdFlowIn< top / 0 > ;
1911
+
1912
+ pragma [ nomagic]
1913
+ private predicate fwdFlowInFlowThrough (
1914
+ ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , Ap ap
1915
+ ) {
1916
+ FwdFlowInThrough:: fwdFlowIn ( _, _, _, p , state , _, innercc , _, t , ap , apa , _)
1904
1917
}
1905
1918
1906
1919
pragma [ nomagic]
@@ -2000,8 +2013,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2000
2013
DataFlowCall call , DataFlowCallable c , ParamNodeEx p , FlowState state , CcCall innercc ,
2001
2014
Typ t , Ap ap , boolean cc
2002
2015
) {
2003
- FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( call , _, c , p , state , _, innercc , _, t , ap ,
2004
- _, cc , _)
2016
+ FwdFlowInNoThrough:: fwdFlowIn ( call , _, c , p , state , _, innercc , _, t , ap , _, cc )
2017
+ or
2018
+ FwdFlowInThrough:: fwdFlowIn ( call , _, c , p , state , _, innercc , _, t , ap , _, cc )
2005
2019
}
2006
2020
2007
2021
pragma [ nomagic]
@@ -2104,19 +2118,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2104
2118
fwdFlowThrough0 ( call , _, cc , state , ccc , summaryCtx , t , ap , apa , ret , _, innerArgApa )
2105
2119
}
2106
2120
2107
- private module FwdFlowThroughRestriction implements FwdFlowInInputSig {
2108
- predicate callRestriction = PrevStage:: callMayFlowThroughRev / 1 ;
2109
-
2110
- predicate parameterRestriction = PrevStage:: parameterMayFlowThrough / 2 ;
2111
- }
2112
-
2113
2121
pragma [ nomagic]
2114
2122
private predicate fwdFlowIsEntered0 (
2115
2123
DataFlowCall call , ArgNodeEx arg , Cc cc , CcCall innerCc , SummaryCtx summaryCtx ,
2116
2124
ParamNodeEx p , FlowState state , Typ t , Ap ap
2117
2125
) {
2118
- FwdFlowIn< FwdFlowThroughRestriction > :: fwdFlowIn ( call , arg , _, p , state , cc , innerCc ,
2119
- summaryCtx , t , ap , _, _, true )
2126
+ FwdFlowInThrough:: fwdFlowIn ( call , arg , _, p , state , cc , innerCc , summaryCtx , t , ap , _, _)
2120
2127
}
2121
2128
2122
2129
/**
@@ -3067,15 +3074,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3067
3074
pragma [ nomagic]
3068
3075
private predicate fwdFlowInStep (
3069
3076
ArgNodeEx arg , ParamNodeEx p , FlowState state , Cc outercc , CcCall innercc ,
3070
- SummaryCtx summaryCtx , Typ t , Ap ap , boolean allowsFlowThrough
3077
+ SummaryCtx outerSummaryCtx , SummaryCtx innerSummaryCtx , Typ t , Ap ap
3071
3078
) {
3072
- exists ( ApApprox apa , boolean allowsFlowThrough0 |
3073
- FwdFlowIn < FwdFlowInNoRestriction > :: fwdFlowIn ( _ , arg , _, p , state , outercc , innercc ,
3074
- summaryCtx , t , ap , apa , _ , allowsFlowThrough0 ) and
3075
- if PrevStage :: parameterMayFlowThrough ( p , apa )
3076
- then allowsFlowThrough = allowsFlowThrough0
3077
- else allowsFlowThrough = false
3078
- )
3079
+ FwdFlowInNoThrough :: fwdFlowIn ( _ , arg , _ , p , state , outercc , innercc , outerSummaryCtx , t ,
3080
+ ap , _ , _) and
3081
+ innerSummaryCtx = TSummaryCtxNone ( )
3082
+ or
3083
+ FwdFlowInThrough :: fwdFlowIn ( _ , arg , _ , p , state , outercc , innercc , outerSummaryCtx , t ,
3084
+ ap , _ , _ ) and
3085
+ innerSummaryCtx = TSummaryCtxSome ( p , state , t , ap )
3079
3086
}
3080
3087
3081
3088
pragma [ nomagic]
@@ -3239,15 +3246,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3239
3246
)
3240
3247
or
3241
3248
// flow into a callable
3242
- exists (
3243
- ArgNodeEx arg , boolean allowsFlowThrough , Cc outercc , SummaryCtx outerSummaryCtx
3244
- |
3249
+ exists ( ArgNodeEx arg , Cc outercc , SummaryCtx outerSummaryCtx |
3245
3250
pn1 = TPathNodeMid ( arg , state , outercc , outerSummaryCtx , t , ap ) and
3246
- fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , t , ap , allowsFlowThrough ) and
3247
- label = "" and
3248
- if allowsFlowThrough = true
3249
- then summaryCtx = TSummaryCtxSome ( node , state , t , ap )
3250
- else summaryCtx = TSummaryCtxNone ( )
3251
+ fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , summaryCtx , t , ap ) and
3252
+ label = ""
3251
3253
)
3252
3254
or
3253
3255
// flow out of a callable
0 commit comments