@@ -1560,20 +1560,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1560
1560
apa = getApprox ( ap )
1561
1561
)
1562
1562
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
- )
1563
+ // flow into a callable without summary context
1564
+ fwdFlowInNoFlowThrough ( node , apa , state , cc , t , ap ) and
1565
+ summaryCtx = TSummaryCtxNone ( ) and
1566
+ // When the call contexts of source and sink needs to match then there's
1567
+ // never any reason to enter a callable except to find a summary. See also
1568
+ // the comment in `PathNodeMid::isAtSink`.
1569
+ not Config:: getAFeature ( ) instanceof FeatureEqualSourceSinkCallContext
1570
+ or
1571
+ // flow into a callable with summary context (non-linear recursion)
1572
+ fwdFlowInFlowThrough ( node , apa , state , cc , t , ap ) and
1573
+ summaryCtx = TSummaryCtxSome ( node , state , t , ap )
1577
1574
or
1578
1575
// flow out of a callable
1579
1576
fwdFlowOut ( _, _, node , state , cc , summaryCtx , t , ap , apa )
@@ -1593,7 +1590,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1593
1590
private newtype TSummaryCtx =
1594
1591
TSummaryCtxNone ( ) or
1595
1592
TSummaryCtxSome ( ParamNodeEx p , FlowState state , Typ t , Ap ap ) {
1596
- fwdFlowIn ( p , _, state , _, t , ap , true )
1593
+ fwdFlowInFlowThrough ( p , _, state , _, t , ap )
1597
1594
}
1598
1595
1599
1596
/**
@@ -1721,12 +1718,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1721
1718
if ap instanceof ApNil then emptyAp = true else emptyAp = false
1722
1719
}
1723
1720
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
- }
1721
+ bindingset [ call, c, p, apa]
1722
+ private signature predicate callRestrictionSig (
1723
+ DataFlowCall call , DataFlowCallable c , ParamNodeEx p , ApApprox apa , boolean emptyAp
1724
+ ) ;
1730
1725
1731
1726
/**
1732
1727
* Exposes the inlined predicate `fwdFlowIn`, which is used to calculate both
@@ -1736,19 +1731,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1736
1731
* need to record the argument that flows into the parameter.
1737
1732
*
1738
1733
* 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.
1734
+ * this to arguments that may actually flow through, using `callRestrictionSig`,
1735
+ * which reduces the argument-to-parameter fan-in significantly.
1742
1736
*/
1743
- private module FwdFlowIn< FwdFlowInInputSig I > {
1737
+ private module FwdFlowIn< callRestrictionSig / 5 callRestriction > {
1744
1738
pragma [ nomagic]
1745
1739
private predicate callEdgeArgParamRestricted (
1746
- DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1747
- boolean allowsFieldFlow , ApApprox apa
1740
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p , boolean emptyAp ,
1741
+ ApApprox apa
1748
1742
) {
1749
- PrevStage:: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa ) and
1750
- I:: callRestriction ( call ) and
1751
- I:: parameterRestriction ( p , apa )
1743
+ exists ( boolean allowsFieldFlow |
1744
+ PrevStage:: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa ) and
1745
+ callRestriction ( call , c , p , apa , emptyAp )
1746
+ |
1747
+ allowsFieldFlow = true
1748
+ or
1749
+ emptyAp = true
1750
+ )
1752
1751
}
1753
1752
1754
1753
pragma [ nomagic]
@@ -1780,10 +1779,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1780
1779
bindingset [ call]
1781
1780
pragma [ inline_late]
1782
1781
private predicate callEdgeArgParamRestrictedInlineLate (
1783
- DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1784
- boolean allowsFieldFlow , ApApprox apa
1782
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p , boolean emptyAp ,
1783
+ ApApprox apa
1785
1784
) {
1786
- callEdgeArgParamRestricted ( call , c , arg , p , allowsFieldFlow , apa )
1785
+ callEdgeArgParamRestricted ( call , c , arg , p , emptyAp , apa )
1787
1786
}
1788
1787
1789
1788
bindingset [ call, ctx]
@@ -1807,44 +1806,35 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1807
1806
private predicate fwdFlowInCand (
1808
1807
DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
1809
1808
ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , boolean emptyAp , ApApprox apa ,
1810
- boolean cc , boolean allowsFlowThrough
1809
+ boolean cc
1811
1810
) {
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
- )
1811
+ fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
1812
+ (
1813
+ inner = viableImplCallContextReducedInlineLate ( call , arg , outercc )
1814
+ or
1815
+ viableImplArgNotCallContextReduced ( call , arg , outercc )
1816
+ ) and
1817
+ not outBarrier ( arg , state ) and
1818
+ not inBarrier ( p , state ) and
1819
+ callEdgeArgParamRestrictedInlineLate ( call , inner , arg , p , emptyAp , apa )
1827
1820
}
1828
1821
1829
1822
pragma [ inline]
1830
1823
private predicate fwdFlowInCandTypeFlowDisabled (
1831
1824
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
1825
+ ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , ApApprox apa , boolean cc
1834
1826
) {
1835
1827
not enableTypeFlow ( ) and
1836
- fwdFlowInCand ( call , arg , state , outercc , inner , p , summaryCtx , t , ap , _, apa , cc ,
1837
- allowsFlowThrough )
1828
+ fwdFlowInCand ( call , arg , state , outercc , inner , p , summaryCtx , t , ap , _, apa , cc )
1838
1829
}
1839
1830
1840
1831
pragma [ nomagic]
1841
1832
private predicate fwdFlowInCandTypeFlowEnabled (
1842
1833
DataFlowCall call , ArgNodeEx arg , Cc outercc , DataFlowCallable inner , ParamNodeEx p ,
1843
- boolean emptyAp , ApApprox apa , boolean cc , boolean allowsFlowThrough
1834
+ boolean emptyAp , ApApprox apa , boolean cc
1844
1835
) {
1845
1836
enableTypeFlow ( ) and
1846
- fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc ,
1847
- allowsFlowThrough )
1837
+ fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc )
1848
1838
}
1849
1839
1850
1840
pragma [ nomagic]
@@ -1859,10 +1849,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1859
1849
pragma [ nomagic]
1860
1850
private predicate fwdFlowInValidEdgeTypeFlowEnabled (
1861
1851
DataFlowCall call , ArgNodeEx arg , Cc outercc , DataFlowCallable inner , ParamNodeEx p ,
1862
- CcCall innercc , boolean emptyAp , ApApprox apa , boolean cc , boolean allowsFlowThrough
1852
+ CcCall innercc , boolean emptyAp , ApApprox apa , boolean cc
1863
1853
) {
1864
- fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ,
1865
- allowsFlowThrough ) and
1854
+ fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ) and
1866
1855
FwdTypeFlow:: typeFlowValidEdgeIn ( call , inner , cc ) and
1867
1856
innercc = getCallContextCall ( call , inner )
1868
1857
}
@@ -1871,38 +1860,68 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1871
1860
predicate fwdFlowIn (
1872
1861
DataFlowCall call , ArgNodeEx arg , DataFlowCallable inner , ParamNodeEx p ,
1873
1862
FlowState state , Cc outercc , CcCall innercc , SummaryCtx summaryCtx , Typ t , Ap ap ,
1874
- ApApprox apa , boolean cc , boolean allowsFlowThrough
1863
+ ApApprox apa , boolean cc
1875
1864
) {
1876
1865
// type flow disabled: linear recursion
1877
1866
fwdFlowInCandTypeFlowDisabled ( call , arg , state , outercc , inner , p , summaryCtx , t , ap ,
1878
- apa , cc , allowsFlowThrough ) and
1867
+ apa , cc ) and
1879
1868
fwdFlowInValidEdgeTypeFlowDisabled ( call , inner , innercc , pragma [ only_bind_into ] ( cc ) )
1880
1869
or
1881
1870
// type flow enabled: non-linear recursion
1882
1871
exists ( boolean emptyAp |
1883
1872
fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
1884
1873
fwdFlowInValidEdgeTypeFlowEnabled ( call , arg , outercc , inner , p , innercc , emptyAp , apa ,
1885
- cc , allowsFlowThrough )
1874
+ cc )
1886
1875
)
1887
1876
}
1888
1877
}
1889
1878
1890
- private module FwdFlowInNoRestriction implements FwdFlowInInputSig { }
1879
+ bindingset [ call, c, p, apa]
1880
+ private predicate callRestrictionNoFlowThrough (
1881
+ DataFlowCall call , DataFlowCallable c , ParamNodeEx p , ApApprox apa , boolean emptyAp
1882
+ ) {
1883
+ (
1884
+ if
1885
+ PrevStage:: callMayFlowThroughRev ( call ) and
1886
+ PrevStage:: parameterMayFlowThrough ( p , apa )
1887
+ then not allowsFieldFlowThrough ( call , c ) and emptyAp = false
1888
+ else emptyAp = [ false , true ]
1889
+ ) and
1890
+ exists ( c )
1891
+ }
1892
+
1893
+ private module FwdFlowInNoThrough = FwdFlowIn< callRestrictionNoFlowThrough / 5 > ;
1891
1894
1892
1895
pragma [ nomagic]
1893
- private predicate fwdFlowIn (
1894
- ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , Ap ap ,
1895
- boolean allowsFlowThrough
1896
+ private predicate fwdFlowInNoFlowThrough (
1897
+ ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , Ap ap
1898
+ ) {
1899
+ FwdFlowInNoThrough:: fwdFlowIn ( _, _, _, p , state , _, innercc , _, t , ap , apa , _)
1900
+ }
1901
+
1902
+ bindingset [ call, c, p, apa]
1903
+ private predicate callRestrictionFlowThrough (
1904
+ DataFlowCall call , DataFlowCallable c , ParamNodeEx p , ApApprox apa , boolean emptyAp
1896
1905
) {
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
1906
+ PrevStage:: callMayFlowThroughRev ( call ) and
1907
+ PrevStage:: parameterMayFlowThrough ( p , apa ) and
1908
+ (
1909
+ emptyAp = true
1910
+ or
1911
+ allowsFieldFlowThrough ( call , c ) and
1912
+ emptyAp = false
1903
1913
)
1904
1914
}
1905
1915
1916
+ private module FwdFlowInThrough = FwdFlowIn< callRestrictionFlowThrough / 5 > ;
1917
+
1918
+ pragma [ nomagic]
1919
+ private predicate fwdFlowInFlowThrough (
1920
+ ParamNodeEx p , ApApprox apa , FlowState state , CcCall innercc , Typ t , Ap ap
1921
+ ) {
1922
+ FwdFlowInThrough:: fwdFlowIn ( _, _, _, p , state , _, innercc , _, t , ap , apa , _)
1923
+ }
1924
+
1906
1925
pragma [ nomagic]
1907
1926
private DataFlowCall viableImplCallContextReducedReverseRestricted (
1908
1927
DataFlowCallable c , CcNoCall ctx
@@ -2000,8 +2019,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2000
2019
DataFlowCall call , DataFlowCallable c , ParamNodeEx p , FlowState state , CcCall innercc ,
2001
2020
Typ t , Ap ap , boolean cc
2002
2021
) {
2003
- FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( call , _, c , p , state , _, innercc , _, t , ap ,
2004
- _, cc , _)
2022
+ FwdFlowInNoThrough:: fwdFlowIn ( call , _, c , p , state , _, innercc , _, t , ap , _, cc )
2023
+ or
2024
+ FwdFlowInThrough:: fwdFlowIn ( call , _, c , p , state , _, innercc , _, t , ap , _, cc )
2005
2025
}
2006
2026
2007
2027
pragma [ nomagic]
@@ -2104,19 +2124,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2104
2124
fwdFlowThrough0 ( call , _, cc , state , ccc , summaryCtx , t , ap , apa , ret , _, innerArgApa )
2105
2125
}
2106
2126
2107
- private module FwdFlowThroughRestriction implements FwdFlowInInputSig {
2108
- predicate callRestriction = PrevStage:: callMayFlowThroughRev / 1 ;
2109
-
2110
- predicate parameterRestriction = PrevStage:: parameterMayFlowThrough / 2 ;
2111
- }
2112
-
2113
2127
pragma [ nomagic]
2114
2128
private predicate fwdFlowIsEntered0 (
2115
2129
DataFlowCall call , ArgNodeEx arg , Cc cc , CcCall innerCc , SummaryCtx summaryCtx ,
2116
2130
ParamNodeEx p , FlowState state , Typ t , Ap ap
2117
2131
) {
2118
- FwdFlowIn< FwdFlowThroughRestriction > :: fwdFlowIn ( call , arg , _, p , state , cc , innerCc ,
2119
- summaryCtx , t , ap , _, _, true )
2132
+ FwdFlowInThrough:: fwdFlowIn ( call , arg , _, p , state , cc , innerCc , summaryCtx , t , ap , _, _)
2120
2133
}
2121
2134
2122
2135
/**
@@ -3067,15 +3080,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3067
3080
pragma [ nomagic]
3068
3081
private predicate fwdFlowInStep (
3069
3082
ArgNodeEx arg , ParamNodeEx p , FlowState state , Cc outercc , CcCall innercc ,
3070
- SummaryCtx summaryCtx , Typ t , Ap ap , boolean allowsFlowThrough
3083
+ SummaryCtx outerSummaryCtx , SummaryCtx innerSummaryCtx , Typ t , Ap ap
3071
3084
) {
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
- )
3085
+ FwdFlowInNoThrough :: fwdFlowIn ( _ , arg , _ , p , state , outercc , innercc , outerSummaryCtx , t ,
3086
+ ap , _ , _) and
3087
+ innerSummaryCtx = TSummaryCtxNone ( )
3088
+ or
3089
+ FwdFlowInThrough :: fwdFlowIn ( _ , arg , _ , p , state , outercc , innercc , outerSummaryCtx , t ,
3090
+ ap , _ , _ ) and
3091
+ innerSummaryCtx = TSummaryCtxSome ( p , state , t , ap )
3079
3092
}
3080
3093
3081
3094
pragma [ nomagic]
@@ -3239,15 +3252,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3239
3252
)
3240
3253
or
3241
3254
// flow into a callable
3242
- exists (
3243
- ArgNodeEx arg , boolean allowsFlowThrough , Cc outercc , SummaryCtx outerSummaryCtx
3244
- |
3255
+ exists ( ArgNodeEx arg , Cc outercc , SummaryCtx outerSummaryCtx |
3245
3256
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 ( )
3257
+ fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , summaryCtx , t , ap ) and
3258
+ label = ""
3251
3259
)
3252
3260
or
3253
3261
// flow out of a callable
0 commit comments