@@ -545,6 +545,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
545545 private module Stage1 implements StageSig {
546546 class Ap = Unit ;
547547
548+ class ApNil = Ap ;
549+
548550 private class Cc = boolean ;
549551
550552 /* Begin: Stage 1 logic. */
@@ -1297,6 +1299,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
12971299 private signature module StageSig {
12981300 class Ap ;
12991301
1302+ class ApNil extends Ap ;
1303+
13001304 predicate revFlow ( NodeEx node ) ;
13011305
13021306 predicate revFlowAp ( NodeEx node , Ap ap ) ;
@@ -1560,20 +1564,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
15601564 apa = getApprox ( ap )
15611565 )
15621566 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 )
15771578 or
15781579 // flow out of a callable
15791580 fwdFlowOut ( _, _, node , state , cc , summaryCtx , t , ap , apa )
@@ -1593,7 +1594,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
15931594 private newtype TSummaryCtx =
15941595 TSummaryCtxNone ( ) or
15951596 TSummaryCtxSome ( ParamNodeEx p , FlowState state , Typ t , Ap ap ) {
1596- fwdFlowIn ( p , _, state , _, t , ap , true )
1597+ fwdFlowInFlowThrough ( p , _, state , _, t , ap )
15971598 }
15981599
15991600 /**
@@ -1721,12 +1722,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17211722 if ap instanceof ApNil then emptyAp = true else emptyAp = false
17221723 }
17231724
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 ( ) ;
17301726
17311727 /**
17321728 * Exposes the inlined predicate `fwdFlowIn`, which is used to calculate both
@@ -1736,19 +1732,40 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17361732 * need to record the argument that flows into the parameter.
17371733 *
17381734 * 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.
17421737 */
1743- private module FwdFlowIn< FwdFlowInInputSig I > {
1738+ private module FwdFlowIn< flowThroughSig / 0 flowThrough > {
17441739 pragma [ nomagic]
17451740 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
17481743 ) {
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+ )
17521769 }
17531770
17541771 pragma [ nomagic]
@@ -1780,10 +1797,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17801797 bindingset [ call]
17811798 pragma [ inline_late]
17821799 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
17851802 ) {
1786- callEdgeArgParamRestricted ( call , c , arg , p , allowsFieldFlow , apa )
1803+ callEdgeArgParamRestricted ( call , c , arg , p , emptyAp , apa )
17871804 }
17881805
17891806 bindingset [ call, ctx]
@@ -1807,44 +1824,35 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
18071824 private predicate fwdFlowInCand (
18081825 DataFlowCall call , ArgNodeEx arg , FlowState state , Cc outercc , DataFlowCallable inner ,
18091826 ParamNodeEx p , SummaryCtx summaryCtx , Typ t , Ap ap , boolean emptyAp , ApApprox apa ,
1810- boolean cc , boolean allowsFlowThrough
1827+ boolean cc
18111828 ) {
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 )
18271838 }
18281839
18291840 pragma [ inline]
18301841 private predicate fwdFlowInCandTypeFlowDisabled (
18311842 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
18341844 ) {
18351845 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 )
18381847 }
18391848
18401849 pragma [ nomagic]
18411850 private predicate fwdFlowInCandTypeFlowEnabled (
18421851 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
18441853 ) {
18451854 enableTypeFlow ( ) and
1846- fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc ,
1847- allowsFlowThrough )
1855+ fwdFlowInCand ( call , arg , _, outercc , inner , p , _, _, _, emptyAp , apa , cc )
18481856 }
18491857
18501858 pragma [ nomagic]
@@ -1859,10 +1867,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
18591867 pragma [ nomagic]
18601868 private predicate fwdFlowInValidEdgeTypeFlowEnabled (
18611869 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
18631871 ) {
1864- fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ,
1865- allowsFlowThrough ) and
1872+ fwdFlowInCandTypeFlowEnabled ( call , arg , outercc , inner , p , emptyAp , apa , cc ) and
18661873 FwdTypeFlow:: typeFlowValidEdgeIn ( call , inner , cc ) and
18671874 innercc = getCallContextCall ( call , inner )
18681875 }
@@ -1871,36 +1878,42 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
18711878 predicate fwdFlowIn (
18721879 DataFlowCall call , ArgNodeEx arg , DataFlowCallable inner , ParamNodeEx p ,
18731880 FlowState state , Cc outercc , CcCall innercc , SummaryCtx summaryCtx , Typ t , Ap ap ,
1874- ApApprox apa , boolean cc , boolean allowsFlowThrough
1881+ ApApprox apa , boolean cc
18751882 ) {
18761883 // type flow disabled: linear recursion
18771884 fwdFlowInCandTypeFlowDisabled ( call , arg , state , outercc , inner , p , summaryCtx , t , ap ,
1878- apa , cc , allowsFlowThrough ) and
1885+ apa , cc ) and
18791886 fwdFlowInValidEdgeTypeFlowDisabled ( call , inner , innercc , pragma [ only_bind_into ] ( cc ) )
18801887 or
18811888 // type flow enabled: non-linear recursion
18821889 exists ( boolean emptyAp |
18831890 fwdFlowIntoArg ( arg , state , outercc , summaryCtx , t , ap , emptyAp , apa , cc ) and
18841891 fwdFlowInValidEdgeTypeFlowEnabled ( call , arg , outercc , inner , p , innercc , emptyAp , apa ,
1885- cc , allowsFlowThrough )
1892+ cc )
18861893 )
18871894 }
18881895 }
18891896
1890- private module FwdFlowInNoRestriction implements FwdFlowInInputSig { }
1897+ private predicate bottom ( ) { none ( ) }
1898+
1899+ private module FwdFlowInNoThrough = FwdFlowIn< bottom / 0 > ;
18911900
18921901 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
18961904 ) {
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 , _)
19041917 }
19051918
19061919 pragma [ nomagic]
@@ -2000,8 +2013,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
20002013 DataFlowCall call , DataFlowCallable c , ParamNodeEx p , FlowState state , CcCall innercc ,
20012014 Typ t , Ap ap , boolean cc
20022015 ) {
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 )
20052019 }
20062020
20072021 pragma [ nomagic]
@@ -2104,19 +2118,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
21042118 fwdFlowThrough0 ( call , _, cc , state , ccc , summaryCtx , t , ap , apa , ret , _, innerArgApa )
21052119 }
21062120
2107- private module FwdFlowThroughRestriction implements FwdFlowInInputSig {
2108- predicate callRestriction = PrevStage:: callMayFlowThroughRev / 1 ;
2109-
2110- predicate parameterRestriction = PrevStage:: parameterMayFlowThrough / 2 ;
2111- }
2112-
21132121 pragma [ nomagic]
21142122 private predicate fwdFlowIsEntered0 (
21152123 DataFlowCall call , ArgNodeEx arg , Cc cc , CcCall innerCc , SummaryCtx summaryCtx ,
21162124 ParamNodeEx p , FlowState state , Typ t , Ap ap
21172125 ) {
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 , _, _)
21202127 }
21212128
21222129 /**
@@ -3067,15 +3074,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30673074 pragma [ nomagic]
30683075 private predicate fwdFlowInStep (
30693076 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
30713078 ) {
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 )
30793086 }
30803087
30813088 pragma [ nomagic]
@@ -3239,15 +3246,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32393246 )
32403247 or
32413248 // flow into a callable
3242- exists (
3243- ArgNodeEx arg , boolean allowsFlowThrough , Cc outercc , SummaryCtx outerSummaryCtx
3244- |
3249+ exists ( ArgNodeEx arg , Cc outercc , SummaryCtx outerSummaryCtx |
32453250 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 = ""
32513253 )
32523254 or
32533255 // flow out of a callable
0 commit comments