@@ -1560,20 +1560,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
15601560 apa = getApprox ( ap )
15611561 )
15621562 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 )
15771574 or
15781575 // flow out of a callable
15791576 fwdFlowOut ( _, _, node , state , cc , summaryCtx , t , ap , apa )
@@ -1593,7 +1590,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
15931590 private newtype TSummaryCtx =
15941591 TSummaryCtxNone ( ) or
15951592 TSummaryCtxSome ( ParamNodeEx p , FlowState state , Typ t , Ap ap ) {
1596- fwdFlowIn ( p , _, state , _, t , ap , true )
1593+ fwdFlowInFlowThrough ( p , _, state , _, t , ap )
15971594 }
15981595
15991596 /**
@@ -1721,12 +1718,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17211718 if ap instanceof ApNil then emptyAp = true else emptyAp = false
17221719 }
17231720
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+ ) ;
17301725
17311726 /**
17321727 * Exposes the inlined predicate `fwdFlowIn`, which is used to calculate both
@@ -1736,19 +1731,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17361731 * need to record the argument that flows into the parameter.
17371732 *
17381733 * 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.
17421736 */
1743- private module FwdFlowIn< FwdFlowInInputSig I > {
1737+ private module FwdFlowIn< callRestrictionSig / 5 callRestriction > {
17441738 pragma [ nomagic]
17451739 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
17481742 ) {
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+ )
17521751 }
17531752
17541753 pragma [ nomagic]
@@ -1780,10 +1779,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17801779 bindingset [ call]
17811780 pragma [ inline_late]
17821781 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
17851784 ) {
1786- callEdgeArgParamRestricted ( call , c , arg , p , allowsFieldFlow , apa )
1785+ callEdgeArgParamRestricted ( call , c , arg , p , emptyAp , apa )
17871786 }
17881787
17891788 bindingset [ call, ctx]
@@ -1807,44 +1806,35 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
18071806 private predicate fwdFlowInCand (
18081807 DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
18091808 ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , boolean emptyAp , ApApprox apa ,
1810- boolean cc , boolean allowsFlowThrough
1809+ boolean cc
18111810 ) {
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 )
18271820 }
18281821
18291822 pragma [ inline]
18301823 private predicate fwdFlowInCandTypeFlowDisabled (
18311824 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
18341826 ) {
18351827 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 )
18381829 }
18391830
18401831 pragma [ nomagic]
18411832 private predicate fwdFlowInCandTypeFlowEnabled (
18421833 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
18441835 ) {
18451836 enableTypeFlow ( ) and
1846- fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc ,
1847- allowsFlowThrough )
1837+ fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc )
18481838 }
18491839
18501840 pragma [ nomagic]
@@ -1859,10 +1849,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
18591849 pragma [ nomagic]
18601850 private predicate fwdFlowInValidEdgeTypeFlowEnabled (
18611851 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
18631853 ) {
1864- fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ,
1865- allowsFlowThrough ) and
1854+ fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ) and
18661855 FwdTypeFlow:: typeFlowValidEdgeIn ( call , inner , cc ) and
18671856 innercc = getCallContextCall ( call , inner )
18681857 }
@@ -1871,38 +1860,68 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
18711860 predicate fwdFlowIn (
18721861 DataFlowCall call , ArgNodeEx arg , DataFlowCallable inner , ParamNodeEx p ,
18731862 FlowState state , Cc outercc , CcCall innercc , SummaryCtx summaryCtx , Typ t , Ap ap ,
1874- ApApprox apa , boolean cc , boolean allowsFlowThrough
1863+ ApApprox apa , boolean cc
18751864 ) {
18761865 // type flow disabled: linear recursion
18771866 fwdFlowInCandTypeFlowDisabled ( call , arg , state , outercc , inner , p , summaryCtx , t , ap ,
1878- apa , cc , allowsFlowThrough ) and
1867+ apa , cc ) and
18791868 fwdFlowInValidEdgeTypeFlowDisabled ( call , inner , innercc , pragma [ only_bind_into ] ( cc ) )
18801869 or
18811870 // type flow enabled: non-linear recursion
18821871 exists ( boolean emptyAp |
18831872 fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
18841873 fwdFlowInValidEdgeTypeFlowEnabled ( call , arg , outercc , inner , p , innercc , emptyAp , apa ,
1885- cc , allowsFlowThrough )
1874+ cc )
18861875 )
18871876 }
18881877 }
18891878
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 > ;
18911894
18921895 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
18961905 ) {
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
19031913 )
19041914 }
19051915
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+
19061925 pragma [ nomagic]
19071926 private DataFlowCall viableImplCallContextReducedReverseRestricted (
19081927 DataFlowCallable c , CcNoCall ctx
@@ -2000,8 +2019,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
20002019 DataFlowCall call , DataFlowCallable c , ParamNodeEx p , FlowState state , CcCall innercc ,
20012020 Typ t , Ap ap , boolean cc
20022021 ) {
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 )
20052025 }
20062026
20072027 pragma [ nomagic]
@@ -2104,19 +2124,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
21042124 fwdFlowThrough0 ( call , _, cc , state , ccc , summaryCtx , t , ap , apa , ret , _, innerArgApa )
21052125 }
21062126
2107- private module FwdFlowThroughRestriction implements FwdFlowInInputSig {
2108- predicate callRestriction = PrevStage:: callMayFlowThroughRev / 1 ;
2109-
2110- predicate parameterRestriction = PrevStage:: parameterMayFlowThrough / 2 ;
2111- }
2112-
21132127 pragma [ nomagic]
21142128 private predicate fwdFlowIsEntered0 (
21152129 DataFlowCall call , ArgNodeEx arg , Cc cc , CcCall innerCc , SummaryCtx summaryCtx ,
21162130 ParamNodeEx p , FlowState state , Typ t , Ap ap
21172131 ) {
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 , _, _)
21202133 }
21212134
21222135 /**
@@ -3067,15 +3080,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30673080 pragma [ nomagic]
30683081 private predicate fwdFlowInStep (
30693082 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
30713084 ) {
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 )
30793092 }
30803093
30813094 pragma [ nomagic]
@@ -3239,15 +3252,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32393252 )
32403253 or
32413254 // flow into a callable
3242- exists (
3243- ArgNodeEx arg , boolean allowsFlowThrough , Cc outercc , SummaryCtx outerSummaryCtx
3244- |
3255+ exists ( ArgNodeEx arg , Cc outercc , SummaryCtx outerSummaryCtx |
32453256 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 = ""
32513259 )
32523260 or
32533261 // flow out of a callable
0 commit comments