@@ -535,6 +535,7 @@ private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _
535535
536536private predicate throughFlowNodeCand1 ( Node node , Configuration config ) {
537537 nodeCand1 ( node , true , config ) and
538+ nodeCandFwd1 ( node , true , config ) and
538539 not fullBarrier ( node , config ) and
539540 not inBarrier ( node , config ) and
540541 not outBarrier ( node , config )
@@ -1523,11 +1524,50 @@ private predicate flowCandIsReturned(
15231524 )
15241525}
15251526
1527+ /**
1528+ * Holds if `argApf` is recorded as the summary context for flow reaching `node`
1529+ * and remains relevant for the following pruning stage.
1530+ */
1531+ private predicate flowCandSummaryCtx ( Node node , AccessPathFront argApf , Configuration config ) {
1532+ exists ( AccessPathFront apf |
1533+ flowCand ( node , true , _, apf , config ) and
1534+ flowCandFwd ( node , true , TAccessPathFrontSome ( argApf ) , apf , config )
1535+ )
1536+ }
1537+
1538+ /**
1539+ * Holds if a length 2 access path approximation with the head `tc` is expected
1540+ * to be expensive.
1541+ */
1542+ private predicate expensiveLen2unfolding ( TypedContent tc , Configuration config ) {
1543+ exists ( int tails , int nodes , int apLimit , int tupleLimit |
1544+ tails = strictcount ( AccessPathFront apf | flowCandConsCand ( tc , apf , config ) ) and
1545+ nodes =
1546+ strictcount ( Node n |
1547+ flowCand ( n , _, _, any ( AccessPathFrontHead apf | apf .headUsesContent ( tc ) ) , config )
1548+ or
1549+ flowCandSummaryCtx ( n , any ( AccessPathFrontHead apf | apf .headUsesContent ( tc ) ) , config )
1550+ ) and
1551+ accessPathApproxCostLimits ( apLimit , tupleLimit ) and
1552+ apLimit < tails and
1553+ tupleLimit < ( tails - 1 ) * nodes
1554+ )
1555+ }
1556+
15261557private newtype TAccessPathApprox =
15271558 TNil ( DataFlowType t ) or
1528- TConsNil ( TypedContent tc , DataFlowType t ) { flowCandConsCand ( tc , TFrontNil ( t ) , _) } or
1559+ TConsNil ( TypedContent tc , DataFlowType t ) {
1560+ flowCandConsCand ( tc , TFrontNil ( t ) , _) and
1561+ not expensiveLen2unfolding ( tc , _)
1562+ } or
15291563 TConsCons ( TypedContent tc1 , TypedContent tc2 , int len ) {
1530- flowCandConsCand ( tc1 , TFrontHead ( tc2 ) , _) and len in [ 2 .. accessPathLimit ( ) ]
1564+ flowCandConsCand ( tc1 , TFrontHead ( tc2 ) , _) and
1565+ len in [ 2 .. accessPathLimit ( ) ] and
1566+ not expensiveLen2unfolding ( tc1 , _)
1567+ } or
1568+ TCons1 ( TypedContent tc , int len ) {
1569+ len in [ 1 .. accessPathLimit ( ) ] and
1570+ expensiveLen2unfolding ( tc , _)
15311571 }
15321572
15331573/**
@@ -1622,6 +1662,49 @@ private class AccessPathApproxConsCons extends AccessPathApproxCons, TConsCons {
16221662 or
16231663 len = 2 and
16241664 result = TConsNil ( tc2 , _)
1665+ or
1666+ result = TCons1 ( tc2 , len - 1 )
1667+ )
1668+ }
1669+ }
1670+
1671+ private class AccessPathApproxCons1 extends AccessPathApproxCons , TCons1 {
1672+ private TypedContent tc ;
1673+ private int len ;
1674+
1675+ AccessPathApproxCons1 ( ) { this = TCons1 ( tc , len ) }
1676+
1677+ override string toString ( ) {
1678+ if len = 1
1679+ then result = "[" + tc .toString ( ) + "]"
1680+ else result = "[" + tc .toString ( ) + ", ... (" + len .toString ( ) + ")]"
1681+ }
1682+
1683+ override TypedContent getHead ( ) { result = tc }
1684+
1685+ override int len ( ) { result = len }
1686+
1687+ override DataFlowType getType ( ) { result = tc .getContainerType ( ) }
1688+
1689+ override AccessPathFront getFront ( ) { result = TFrontHead ( tc ) }
1690+
1691+ override AccessPathApprox pop ( TypedContent head ) {
1692+ head = tc and
1693+ (
1694+ exists ( TypedContent tc2 | flowCandConsCand ( tc , TFrontHead ( tc2 ) , _) |
1695+ result = TConsCons ( tc2 , _, len - 1 )
1696+ or
1697+ len = 2 and
1698+ result = TConsNil ( tc2 , _)
1699+ or
1700+ result = TCons1 ( tc2 , len - 1 )
1701+ )
1702+ or
1703+ exists ( DataFlowType t |
1704+ len = 1 and
1705+ flowCandConsCand ( tc , TFrontNil ( t ) , _) and
1706+ result = TNil ( t )
1707+ )
16251708 )
16261709 }
16271710}
@@ -2045,23 +2128,34 @@ private predicate flow(Node n, Configuration config) { flow(n, _, _, _, config)
20452128
20462129pragma [ noinline]
20472130private predicate parameterFlow (
2048- ParameterNode p , AccessPathApprox apa , DataFlowCallable c , Configuration config
2131+ ParameterNode p , AccessPathApprox apa , AccessPathApprox apa0 , DataFlowCallable c ,
2132+ Configuration config
20492133) {
2050- flow ( p , true , _ , apa , config ) and
2134+ flow ( p , true , TAccessPathApproxSome ( apa0 ) , apa , config ) and
20512135 c = p .getEnclosingCallable ( )
20522136}
20532137
2054- private predicate parameterMayFlowThrough ( ParameterNode p , AccessPathApprox apa ) {
2138+ private predicate parameterMayFlowThrough ( ParameterNode p , DataFlowCallable c , AccessPathApprox apa ) {
20552139 exists ( ReturnNodeExt ret , Configuration config , AccessPathApprox apa0 |
2056- parameterFlow ( p , apa , ret .getEnclosingCallable ( ) , config ) and
2140+ parameterFlow ( p , apa , apa0 , c , config ) and
2141+ c = ret .getEnclosingCallable ( ) and
20572142 flow ( ret , true , TAccessPathApproxSome ( _) , apa0 , config ) and
20582143 flowFwd ( ret , any ( CallContextCall ccc ) , TAccessPathApproxSome ( apa ) , _, apa0 , config )
20592144 )
20602145}
20612146
2147+ private predicate nodeMayUseSummary ( Node n , AccessPathApprox apa , Configuration config ) {
2148+ exists ( DataFlowCallable c , AccessPathApprox apa0 |
2149+ parameterMayFlowThrough ( _, c , apa ) and
2150+ flow ( n , true , _, apa0 , config ) and
2151+ flowFwd ( n , any ( CallContextCall ccc ) , TAccessPathApproxSome ( apa ) , _, apa0 , config ) and
2152+ n .getEnclosingCallable ( ) = c
2153+ )
2154+ }
2155+
20622156private newtype TSummaryCtx =
20632157 TSummaryCtxNone ( ) or
2064- TSummaryCtxSome ( ParameterNode p , AccessPath ap ) { parameterMayFlowThrough ( p , ap .getApprox ( ) ) }
2158+ TSummaryCtxSome ( ParameterNode p , AccessPath ap ) { parameterMayFlowThrough ( p , _ , ap .getApprox ( ) ) }
20652159
20662160/**
20672161 * A context for generating flow summaries. This represents flow entry through
@@ -2096,9 +2190,112 @@ private class SummaryCtxSome extends SummaryCtx, TSummaryCtxSome {
20962190 }
20972191}
20982192
2193+ /**
2194+ * Gets the number of length 2 access path approximations that correspond to `apa`.
2195+ */
2196+ private int count1to2unfold ( AccessPathApproxCons1 apa , Configuration config ) {
2197+ exists ( TypedContent tc , int len |
2198+ tc = apa .getHead ( ) and
2199+ len = apa .len ( ) and
2200+ result =
2201+ strictcount ( AccessPathFront apf |
2202+ flowConsCand ( tc , any ( AccessPathApprox ap | ap .getFront ( ) = apf and ap .len ( ) = len - 1 ) ,
2203+ config )
2204+ )
2205+ )
2206+ }
2207+
2208+ private int countNodesUsingAccessPath ( AccessPathApprox apa , Configuration config ) {
2209+ result = strictcount ( Node n | flow ( n , _, _, apa , config ) or nodeMayUseSummary ( n , apa , config ) )
2210+ }
2211+
2212+ /**
2213+ * Holds if a length 2 access path approximation matching `apa` is expected
2214+ * to be expensive.
2215+ */
2216+ private predicate expensiveLen1to2unfolding ( AccessPathApproxCons1 apa , Configuration config ) {
2217+ exists ( int aps , int nodes , int apLimit , int tupleLimit |
2218+ aps = count1to2unfold ( apa , config ) and
2219+ nodes = countNodesUsingAccessPath ( apa , config ) and
2220+ accessPathCostLimits ( apLimit , tupleLimit ) and
2221+ apLimit < aps and
2222+ tupleLimit < ( aps - 1 ) * nodes
2223+ )
2224+ }
2225+
2226+ private AccessPathApprox getATail ( AccessPathApprox apa , Configuration config ) {
2227+ exists ( TypedContent head |
2228+ apa .pop ( head ) = result and
2229+ flowConsCand ( head , result , config )
2230+ )
2231+ }
2232+
2233+ /**
2234+ * Holds with `unfold = false` if a precise head-tail representation of `apa` is
2235+ * expected to be expensive. Holds with `unfold = true` otherwise.
2236+ */
2237+ private predicate evalUnfold ( AccessPathApprox apa , boolean unfold , Configuration config ) {
2238+ exists ( int aps , int nodes , int apLimit , int tupleLimit |
2239+ aps = countPotentialAps ( apa , config ) and
2240+ nodes = countNodesUsingAccessPath ( apa , config ) and
2241+ accessPathCostLimits ( apLimit , tupleLimit ) and
2242+ if apLimit < aps and tupleLimit < ( aps - 1 ) * nodes then unfold = false else unfold = true
2243+ )
2244+ }
2245+
2246+ /**
2247+ * Gets the number of `AccessPath`s that correspond to `apa`.
2248+ */
2249+ private int countAps ( AccessPathApprox apa , Configuration config ) {
2250+ evalUnfold ( apa , false , config ) and
2251+ result = 1 and
2252+ ( not apa instanceof AccessPathApproxCons1 or expensiveLen1to2unfolding ( apa , config ) )
2253+ or
2254+ evalUnfold ( apa , false , config ) and
2255+ result = count1to2unfold ( apa , config ) and
2256+ not expensiveLen1to2unfolding ( apa , config )
2257+ or
2258+ evalUnfold ( apa , true , config ) and
2259+ result = countPotentialAps ( apa , config )
2260+ }
2261+
2262+ /**
2263+ * Gets the number of `AccessPath`s that would correspond to `apa` assuming
2264+ * that it is expanded to a precise head-tail representation.
2265+ */
2266+ language [ monotonicAggregates]
2267+ private int countPotentialAps ( AccessPathApprox apa , Configuration config ) {
2268+ apa instanceof AccessPathApproxNil and result = 1
2269+ or
2270+ result = strictsum ( AccessPathApprox tail | tail = getATail ( apa , config ) | countAps ( tail , config ) )
2271+ }
2272+
20992273private newtype TAccessPath =
21002274 TAccessPathNil ( DataFlowType t ) or
2101- TAccessPathCons ( TypedContent head , AccessPath tail ) { flowConsCand ( head , tail .getApprox ( ) , _) }
2275+ TAccessPathCons ( TypedContent head , AccessPath tail ) {
2276+ exists ( AccessPathApproxCons apa |
2277+ not evalUnfold ( apa , false , _) and
2278+ head = apa .getHead ( ) and
2279+ tail .getApprox ( ) = getATail ( apa , _)
2280+ )
2281+ } or
2282+ TAccessPathCons2 ( TypedContent head1 , TypedContent head2 , int len ) {
2283+ exists ( AccessPathApproxCons apa |
2284+ evalUnfold ( apa , false , _) and
2285+ not expensiveLen1to2unfolding ( apa , _) and
2286+ apa .len ( ) = len and
2287+ head1 = apa .getHead ( ) and
2288+ head2 = getATail ( apa , _) .getHead ( )
2289+ )
2290+ } or
2291+ TAccessPathCons1 ( TypedContent head , int len ) {
2292+ exists ( AccessPathApproxCons apa |
2293+ evalUnfold ( apa , false , _) and
2294+ expensiveLen1to2unfolding ( apa , _) and
2295+ apa .len ( ) = len and
2296+ head = apa .getHead ( )
2297+ )
2298+ }
21022299
21032300private newtype TPathNode =
21042301 TPathNodeMid ( Node node , CallContext cc , SummaryCtx sc , AccessPath ap , Configuration config ) {
@@ -2202,20 +2399,96 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
22022399 result = TConsNil ( head , tail .( AccessPathNil ) .getType ( ) )
22032400 or
22042401 result = TConsCons ( head , tail .getHead ( ) , this .length ( ) )
2402+ or
2403+ result = TCons1 ( head , this .length ( ) )
22052404 }
22062405
22072406 override int length ( ) { result = 1 + tail .length ( ) }
22082407
2209- private string toStringImpl ( ) {
2408+ private string toStringImpl ( boolean needsSuffix ) {
22102409 exists ( DataFlowType t |
22112410 tail = TAccessPathNil ( t ) and
2411+ needsSuffix = false and
22122412 result = head .toString ( ) + "]" + concat ( " : " + ppReprType ( t ) )
22132413 )
22142414 or
2215- result = head + ", " + tail .( AccessPathCons ) .toStringImpl ( )
2415+ result = head + ", " + tail .( AccessPathCons ) .toStringImpl ( needsSuffix )
2416+ or
2417+ exists ( TypedContent tc2 , TypedContent tc3 , int len | tail = TAccessPathCons2 ( tc2 , tc3 , len ) |
2418+ result = head + ", " + tc2 + ", " + tc3 + ", ... (" and len > 2 and needsSuffix = true
2419+ or
2420+ result = head + ", " + tc2 + ", " + tc3 + "]" and len = 2 and needsSuffix = false
2421+ )
2422+ or
2423+ exists ( TypedContent tc2 , int len | tail = TAccessPathCons1 ( tc2 , len ) |
2424+ result = head + ", " + tc2 + ", ... (" and len > 1 and needsSuffix = true
2425+ or
2426+ result = head + ", " + tc2 + "]" and len = 1 and needsSuffix = false
2427+ )
2428+ }
2429+
2430+ override string toString ( ) {
2431+ result = "[" + this .toStringImpl ( true ) + length ( ) .toString ( ) + ")]"
2432+ or
2433+ result = "[" + this .toStringImpl ( false )
22162434 }
2435+ }
2436+
2437+ private class AccessPathCons2 extends AccessPath , TAccessPathCons2 {
2438+ private TypedContent head1 ;
2439+ private TypedContent head2 ;
2440+ private int len ;
2441+
2442+ AccessPathCons2 ( ) { this = TAccessPathCons2 ( head1 , head2 , len ) }
2443+
2444+ override TypedContent getHead ( ) { result = head1 }
2445+
2446+ override AccessPath getTail ( ) {
2447+ flowConsCand ( head1 , result .getApprox ( ) , _) and
2448+ result .getHead ( ) = head2 and
2449+ result .length ( ) = len - 1
2450+ }
2451+
2452+ override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head1 ) }
22172453
2218- override string toString ( ) { result = "[" + this .toStringImpl ( ) }
2454+ override AccessPathApproxCons getApprox ( ) {
2455+ result = TConsCons ( head1 , head2 , len ) or
2456+ result = TCons1 ( head1 , len )
2457+ }
2458+
2459+ override int length ( ) { result = len }
2460+
2461+ override string toString ( ) {
2462+ if len = 2
2463+ then result = "[" + head1 .toString ( ) + ", " + head2 .toString ( ) + "]"
2464+ else
2465+ result = "[" + head1 .toString ( ) + ", " + head2 .toString ( ) + ", ... (" + len .toString ( ) + ")]"
2466+ }
2467+ }
2468+
2469+ private class AccessPathCons1 extends AccessPath , TAccessPathCons1 {
2470+ private TypedContent head ;
2471+ private int len ;
2472+
2473+ AccessPathCons1 ( ) { this = TAccessPathCons1 ( head , len ) }
2474+
2475+ override TypedContent getHead ( ) { result = head }
2476+
2477+ override AccessPath getTail ( ) {
2478+ flowConsCand ( head , result .getApprox ( ) , _) and result .length ( ) = len - 1
2479+ }
2480+
2481+ override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head ) }
2482+
2483+ override AccessPathApproxCons getApprox ( ) { result = TCons1 ( head , len ) }
2484+
2485+ override int length ( ) { result = len }
2486+
2487+ override string toString ( ) {
2488+ if len = 1
2489+ then result = "[" + head .toString ( ) + "]"
2490+ else result = "[" + head .toString ( ) + ", ... (" + len .toString ( ) + ")]"
2491+ }
22192492}
22202493
22212494/**
0 commit comments