@@ -39,7 +39,7 @@ private module Liveness {
3939 /**
4040 * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
4141 */
42- private predicate ref ( BasicBlock bb , int i , SourceVariable v , RefKind k ) {
42+ predicate ref ( BasicBlock bb , int i , SourceVariable v , RefKind k ) {
4343 exists ( boolean certain | variableRead ( bb , i , v , certain ) | k = Read ( certain ) )
4444 or
4545 exists ( boolean certain | variableWrite ( bb , i , v , certain ) | k = Write ( certain ) )
@@ -76,6 +76,10 @@ private module Liveness {
7676 not result + 1 = refRank ( bb , _, v , _)
7777 }
7878
79+ predicate lastRefIsRead ( BasicBlock bb , SourceVariable v ) {
80+ maxRefRank ( bb , v ) = refRank ( bb , _, v , Read ( _) )
81+ }
82+
7983 /**
8084 * Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
8185 * that is either a read or a certain write.
@@ -185,42 +189,127 @@ newtype TDefinition =
185189
186190private module SsaDefReaches {
187191 newtype TSsaRefKind =
188- SsaRead ( ) or
192+ SsaActualRead ( ) or
193+ SsaPhiRead ( ) or
189194 SsaDef ( )
190195
196+ class SsaRead = SsaActualRead or SsaPhiRead ;
197+
191198 /**
192199 * A classification of SSA variable references into reads and definitions.
193200 */
194201 class SsaRefKind extends TSsaRefKind {
195202 string toString ( ) {
196- this = SsaRead ( ) and
197- result = "SsaRead"
203+ this = SsaActualRead ( ) and
204+ result = "SsaActualRead"
205+ or
206+ this = SsaPhiRead ( ) and
207+ result = "SsaPhiRead"
198208 or
199209 this = SsaDef ( ) and
200210 result = "SsaDef"
201211 }
202212
203213 int getOrder ( ) {
204- this = SsaRead ( ) and
214+ this instanceof SsaRead and
205215 result = 0
206216 or
207217 this = SsaDef ( ) and
208218 result = 1
209219 }
210220 }
211221
222+ /**
223+ * Holds if `bb` is in the dominance frontier of a block containing a
224+ * read of `v`.
225+ */
226+ pragma [ nomagic]
227+ private predicate inReadDominanceFrontier ( BasicBlock bb , SourceVariable v ) {
228+ exists ( BasicBlock readbb | inDominanceFrontier ( readbb , bb ) |
229+ lastRefIsRead ( readbb , v )
230+ or
231+ phiRead ( readbb , v )
232+ )
233+ }
234+
235+ /**
236+ * Holds if a phi-read node should be inserted for variable `v` at the beginning
237+ * of basic block `bb`.
238+ *
239+ * Phi-read nodes are like normal phi nodes, but they are inserted based on reads
240+ * instead of writes, and only if the dominance-frontier block does not already
241+ * contain a reference (read or write) to `v`. Unlike normal phi nodes, this is
242+ * an internal implementation detail that is not exposed.
243+ *
244+ * The motivation for adding phi-reads is to improve performance of the use-use
245+ * calculation in cases where there is a large number of reads that can reach the
246+ * same join-point, and from there reach a large number of basic blocks. Example:
247+ *
248+ * ```cs
249+ * if (a)
250+ * use(x);
251+ * else if (b)
252+ * use(x);
253+ * else if (c)
254+ * use(x);
255+ * else if (d)
256+ * use(x);
257+ * // many more ifs ...
258+ *
259+ * // phi-read for `x` inserted here
260+ *
261+ * // program not mentioning `x`, with large basic block graph
262+ *
263+ * use(x);
264+ * ```
265+ *
266+ * Without phi-reads, the analysis has to replicate reachability for each of
267+ * the guarded uses of `x`. However, with phi-reads, the analysis will limit
268+ * each conditional use of `x` to reach the basic block containing the phi-read
269+ * node for `x`, and only that basic block will have to compute reachability
270+ * through the remainder of the large program.
271+ *
272+ * Like normal reads, each phi-read node `phi-read` can be reached from exactly
273+ * one SSA definition (without passing through another definition): Assume, for
274+ * the sake of contradiction, that there are two reaching definitions `def1` and
275+ * `def2`. Now, if both `def1` and `def2` dominate `phi-read`, then the nearest
276+ * dominating definition will prevent the other from reaching `phi-read`. So, at
277+ * least one of `def1` and `def2` cannot dominate `phi-read`; assume it is `def1`.
278+ * Then `def1` must go through one of its dominance-frontier blocks in order to
279+ * reach `phi-read`. However, such a block will always start with a (normal) phi
280+ * node, which contradicts reachability.
281+ *
282+ * Also, like normal reads, the unique SSA definition `def` that reaches `phi-read`,
283+ * will dominate `phi-read`. Assuming it doesn't means that the path from `def`
284+ * to `phi-read` goes through a dominance-frontier block, and hence a phi node,
285+ * which contradicts reachability.
286+ */
287+ pragma [ nomagic]
288+ predicate phiRead ( BasicBlock bb , SourceVariable v ) {
289+ inReadDominanceFrontier ( bb , v ) and
290+ liveAtEntry ( bb , v ) and
291+ // only if there are no other references to `v` inside `bb`
292+ not ref ( bb , _, v , _) and
293+ not exists ( Definition def | def .definesAt ( v , bb , _) )
294+ }
295+
212296 /**
213297 * Holds if the `i`th node of basic block `bb` is a reference to `v`,
214298 * either a read (when `k` is `SsaRead()`) or an SSA definition (when `k`
215299 * is `SsaDef()`).
216300 *
217301 * Unlike `Liveness::ref`, this includes `phi` nodes.
218302 */
303+ pragma [ nomagic]
219304 predicate ssaRef ( BasicBlock bb , int i , SourceVariable v , SsaRefKind k ) {
220305 variableRead ( bb , i , v , _) and
221- k = SsaRead ( )
306+ k = SsaActualRead ( )
307+ or
308+ phiRead ( bb , v ) and
309+ i = - 1 and
310+ k = SsaPhiRead ( )
222311 or
223- exists ( Definition def | def .definesAt ( v , bb , i ) ) and
312+ any ( Definition def ) .definesAt ( v , bb , i ) and
224313 k = SsaDef ( )
225314 }
226315
@@ -273,7 +362,7 @@ private module SsaDefReaches {
273362 )
274363 or
275364 ssaDefReachesRank ( bb , def , rnk - 1 , v ) and
276- rnk = ssaRefRank ( bb , _, v , SsaRead ( ) )
365+ rnk = ssaRefRank ( bb , _, v , any ( SsaRead k ) )
277366 }
278367
279368 /**
@@ -283,7 +372,7 @@ private module SsaDefReaches {
283372 predicate ssaDefReachesReadWithinBlock ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
284373 exists ( int rnk |
285374 ssaDefReachesRank ( bb , def , rnk , v ) and
286- rnk = ssaRefRank ( bb , i , v , SsaRead ( ) )
375+ rnk = ssaRefRank ( bb , i , v , any ( SsaRead k ) )
287376 )
288377 }
289378
@@ -309,45 +398,94 @@ private module SsaDefReaches {
309398 ssaDefRank ( def , v , bb , i , _) = maxSsaRefRank ( bb , v )
310399 }
311400
312- predicate defOccursInBlock ( Definition def , BasicBlock bb , SourceVariable v ) {
313- exists ( ssaDefRank ( def , v , bb , _, _ ) )
401+ predicate defOccursInBlock ( Definition def , BasicBlock bb , SourceVariable v , SsaRefKind k ) {
402+ exists ( ssaDefRank ( def , v , bb , _, k ) )
314403 }
315404
316405 pragma [ noinline]
317406 private predicate ssaDefReachesThroughBlock ( Definition def , BasicBlock bb ) {
318407 ssaDefReachesEndOfBlock ( bb , def , _) and
319- not defOccursInBlock ( _, bb , def .getSourceVariable ( ) )
408+ not defOccursInBlock ( _, bb , def .getSourceVariable ( ) , _ )
320409 }
321410
322411 /**
323412 * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
324- * `bb2` is a transitive successor of `bb1`, `def` is live at the end of `bb1`,
325- * and the underlying variable for `def` is neither read nor written in any block
326- * on the path between `bb1` and `bb2`.
413+ * `bb2` is a transitive successor of `bb1`, `def` is live at the end of _some_
414+ * predecessor of `bb2`, and the underlying variable for `def` is neither read
415+ * nor written in any block on the path between `bb1` and `bb2`.
416+ *
417+ * Phi reads are considered as normal reads for this predicate.
327418 */
328- predicate varBlockReaches ( Definition def , BasicBlock bb1 , BasicBlock bb2 ) {
329- defOccursInBlock ( def , bb1 , _) and
419+ pragma [ nomagic]
420+ private predicate varBlockReachesInclPhiRead ( Definition def , BasicBlock bb1 , BasicBlock bb2 ) {
421+ defOccursInBlock ( def , bb1 , _, _) and
330422 bb2 = getABasicBlockSuccessor ( bb1 )
331423 or
332424 exists ( BasicBlock mid |
333- varBlockReaches ( def , bb1 , mid ) and
425+ varBlockReachesInclPhiRead ( def , bb1 , mid ) and
334426 ssaDefReachesThroughBlock ( def , mid ) and
335427 bb2 = getABasicBlockSuccessor ( mid )
336428 )
337429 }
338430
431+ pragma [ nomagic]
432+ private predicate phiReadStep ( Definition def , SourceVariable v , BasicBlock bb1 , BasicBlock bb2 ) {
433+ varBlockReachesInclPhiRead ( def , bb1 , bb2 ) and
434+ defOccursInBlock ( def , bb2 , v , SsaPhiRead ( ) )
435+ }
436+
437+ pragma [ nomagic]
438+ private predicate varBlockReachesExclPhiRead ( Definition def , BasicBlock bb1 , BasicBlock bb2 ) {
439+ varBlockReachesInclPhiRead ( pragma [ only_bind_into ] ( def ) , bb1 , pragma [ only_bind_into ] ( bb2 ) ) and
440+ ssaRef ( bb2 , _, def .getSourceVariable ( ) , [ SsaActualRead ( ) .( TSsaRefKind ) , SsaDef ( ) ] )
441+ or
442+ exists ( BasicBlock mid |
443+ varBlockReachesExclPhiRead ( def , mid , bb2 ) and
444+ phiReadStep ( def , _, bb1 , mid )
445+ )
446+ }
447+
339448 /**
340449 * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
341- * `def` is read at index `i2` in basic block `bb2`, `bb2` is in a transitive
342- * successor block of `bb1`, and `def` is neither read nor written in any block
343- * on a path between `bb1` and `bb2`.
450+ * the underlying variable `v` of `def` is accessed in basic block `bb2`
451+ * (either a read or a write), `bb2` is a transitive successor of `bb1`, and
452+ * `v` is neither read nor written in any block on the path between `bb1`
453+ * and `bb2`.
344454 */
455+ pragma [ nomagic]
456+ predicate varBlockReaches ( Definition def , BasicBlock bb1 , BasicBlock bb2 ) {
457+ varBlockReachesExclPhiRead ( def , bb1 , bb2 ) and
458+ not defOccursInBlock ( def , bb1 , _, SsaPhiRead ( ) )
459+ }
460+
461+ pragma [ nomagic]
345462 predicate defAdjacentRead ( Definition def , BasicBlock bb1 , BasicBlock bb2 , int i2 ) {
346463 varBlockReaches ( def , bb1 , bb2 ) and
347- ssaRefRank ( bb2 , i2 , def .getSourceVariable ( ) , SsaRead ( ) ) = 1
464+ ssaRefRank ( bb2 , i2 , def .getSourceVariable ( ) , SsaActualRead ( ) ) = 1
465+ }
466+
467+ /**
468+ * Holds if `def` is accessed in basic block `bb` (either a read or a write),
469+ * `bb1` can reach a transitive successor `bb2` where `def` is no longer live,
470+ * and `v` is neither read nor written in any block on the path between `bb`
471+ * and `bb2`.
472+ */
473+ pragma [ nomagic]
474+ predicate varBlockReachesExit ( Definition def , BasicBlock bb ) {
475+ exists ( BasicBlock bb2 | varBlockReachesInclPhiRead ( def , bb , bb2 ) |
476+ not defOccursInBlock ( def , bb2 , _, _) and
477+ not ssaDefReachesEndOfBlock ( bb2 , def , _)
478+ )
479+ or
480+ exists ( BasicBlock mid |
481+ varBlockReachesExit ( def , mid ) and
482+ phiReadStep ( def , _, bb , mid )
483+ )
348484 }
349485}
350486
487+ predicate phiReadExposedForTesting = phiRead / 2 ;
488+
351489private import SsaDefReaches
352490
353491pragma [ nomagic]
@@ -365,7 +503,8 @@ predicate liveThrough(BasicBlock bb, SourceVariable v) {
365503 */
366504pragma [ nomagic]
367505predicate ssaDefReachesEndOfBlock ( BasicBlock bb , Definition def , SourceVariable v ) {
368- exists ( int last | last = maxSsaRefRank ( bb , v ) |
506+ exists ( int last |
507+ last = maxSsaRefRank ( pragma [ only_bind_into ] ( bb ) , pragma [ only_bind_into ] ( v ) ) and
369508 ssaDefReachesRank ( bb , def , last , v ) and
370509 liveAtExit ( bb , v )
371510 )
@@ -405,7 +544,7 @@ pragma[nomagic]
405544predicate ssaDefReachesRead ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
406545 ssaDefReachesReadWithinBlock ( v , def , bb , i )
407546 or
408- variableRead ( bb , i , v , _ ) and
547+ ssaRef ( bb , i , v , any ( SsaRead k ) ) and
409548 ssaDefReachesEndOfBlock ( getABasicBlockPredecessor ( bb ) , def , v ) and
410549 not ssaDefReachesReadWithinBlock ( v , _, bb , i )
411550}
@@ -421,7 +560,7 @@ pragma[nomagic]
421560predicate adjacentDefRead ( Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 ) {
422561 exists ( int rnk |
423562 rnk = ssaDefRank ( def , _, bb1 , i1 , _) and
424- rnk + 1 = ssaDefRank ( def , _, bb1 , i2 , SsaRead ( ) ) and
563+ rnk + 1 = ssaDefRank ( def , _, bb1 , i2 , SsaActualRead ( ) ) and
425564 variableRead ( bb1 , i2 , _, _) and
426565 bb2 = bb1
427566 )
@@ -538,18 +677,15 @@ predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Def
538677 */
539678pragma [ nomagic]
540679predicate lastRef ( Definition def , BasicBlock bb , int i ) {
680+ // Can reach another definition
541681 lastRefRedef ( def , bb , i , _)
542682 or
543- lastSsaRef ( def , _, bb , i ) and
544- (
683+ exists ( SourceVariable v | lastSsaRef ( def , v , bb , i ) |
545684 // Can reach exit directly
546685 bb instanceof ExitBasicBlock
547686 or
548687 // Can reach a block using one or more steps, where `def` is no longer live
549- exists ( BasicBlock bb2 | varBlockReaches ( def , bb , bb2 ) |
550- not defOccursInBlock ( def , bb2 , _) and
551- not ssaDefReachesEndOfBlock ( bb2 , def , _)
552- )
688+ varBlockReachesExit ( def , bb )
553689 )
554690}
555691
0 commit comments