@@ -39,7 +39,7 @@ private module Liveness {
39
39
/**
40
40
* Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
41
41
*/
42
- private predicate ref ( BasicBlock bb , int i , SourceVariable v , RefKind k ) {
42
+ predicate ref ( BasicBlock bb , int i , SourceVariable v , RefKind k ) {
43
43
exists ( boolean certain | variableRead ( bb , i , v , certain ) | k = Read ( certain ) )
44
44
or
45
45
exists ( boolean certain | variableWrite ( bb , i , v , certain ) | k = Write ( certain ) )
@@ -76,6 +76,10 @@ private module Liveness {
76
76
not result + 1 = refRank ( bb , _, v , _)
77
77
}
78
78
79
+ predicate lastRefIsRead ( BasicBlock bb , SourceVariable v ) {
80
+ maxRefRank ( bb , v ) = refRank ( bb , _, v , Read ( _) )
81
+ }
82
+
79
83
/**
80
84
* Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
81
85
* that is either a read or a certain write.
@@ -185,42 +189,127 @@ newtype TDefinition =
185
189
186
190
private module SsaDefReaches {
187
191
newtype TSsaRefKind =
188
- SsaRead ( ) or
192
+ SsaActualRead ( ) or
193
+ SsaPhiRead ( ) or
189
194
SsaDef ( )
190
195
196
+ class SsaRead = SsaActualRead or SsaPhiRead ;
197
+
191
198
/**
192
199
* A classification of SSA variable references into reads and definitions.
193
200
*/
194
201
class SsaRefKind extends TSsaRefKind {
195
202
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"
198
208
or
199
209
this = SsaDef ( ) and
200
210
result = "SsaDef"
201
211
}
202
212
203
213
int getOrder ( ) {
204
- this = SsaRead ( ) and
214
+ this instanceof SsaRead and
205
215
result = 0
206
216
or
207
217
this = SsaDef ( ) and
208
218
result = 1
209
219
}
210
220
}
211
221
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
+
212
296
/**
213
297
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
214
298
* either a read (when `k` is `SsaRead()`) or an SSA definition (when `k`
215
299
* is `SsaDef()`).
216
300
*
217
301
* Unlike `Liveness::ref`, this includes `phi` nodes.
218
302
*/
303
+ pragma [ nomagic]
219
304
predicate ssaRef ( BasicBlock bb , int i , SourceVariable v , SsaRefKind k ) {
220
305
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 ( )
222
311
or
223
- exists ( Definition def | def .definesAt ( v , bb , i ) ) and
312
+ any ( Definition def ) .definesAt ( v , bb , i ) and
224
313
k = SsaDef ( )
225
314
}
226
315
@@ -273,7 +362,7 @@ private module SsaDefReaches {
273
362
)
274
363
or
275
364
ssaDefReachesRank ( bb , def , rnk - 1 , v ) and
276
- rnk = ssaRefRank ( bb , _, v , SsaRead ( ) )
365
+ rnk = ssaRefRank ( bb , _, v , any ( SsaRead k ) )
277
366
}
278
367
279
368
/**
@@ -283,7 +372,7 @@ private module SsaDefReaches {
283
372
predicate ssaDefReachesReadWithinBlock ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
284
373
exists ( int rnk |
285
374
ssaDefReachesRank ( bb , def , rnk , v ) and
286
- rnk = ssaRefRank ( bb , i , v , SsaRead ( ) )
375
+ rnk = ssaRefRank ( bb , i , v , any ( SsaRead k ) )
287
376
)
288
377
}
289
378
@@ -309,45 +398,94 @@ private module SsaDefReaches {
309
398
ssaDefRank ( def , v , bb , i , _) = maxSsaRefRank ( bb , v )
310
399
}
311
400
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 ) )
314
403
}
315
404
316
405
pragma [ noinline]
317
406
private predicate ssaDefReachesThroughBlock ( Definition def , BasicBlock bb ) {
318
407
ssaDefReachesEndOfBlock ( bb , def , _) and
319
- not defOccursInBlock ( _, bb , def .getSourceVariable ( ) )
408
+ not defOccursInBlock ( _, bb , def .getSourceVariable ( ) , _ )
320
409
}
321
410
322
411
/**
323
412
* 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.
327
418
*/
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
330
422
bb2 = getABasicBlockSuccessor ( bb1 )
331
423
or
332
424
exists ( BasicBlock mid |
333
- varBlockReaches ( def , bb1 , mid ) and
425
+ varBlockReachesInclPhiRead ( def , bb1 , mid ) and
334
426
ssaDefReachesThroughBlock ( def , mid ) and
335
427
bb2 = getABasicBlockSuccessor ( mid )
336
428
)
337
429
}
338
430
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
+
339
448
/**
340
449
* 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`.
344
454
*/
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]
345
462
predicate defAdjacentRead ( Definition def , BasicBlock bb1 , BasicBlock bb2 , int i2 ) {
346
463
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
+ )
348
484
}
349
485
}
350
486
487
+ predicate phiReadExposedForTesting = phiRead / 2 ;
488
+
351
489
private import SsaDefReaches
352
490
353
491
pragma [ nomagic]
@@ -365,7 +503,8 @@ predicate liveThrough(BasicBlock bb, SourceVariable v) {
365
503
*/
366
504
pragma [ nomagic]
367
505
predicate 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
369
508
ssaDefReachesRank ( bb , def , last , v ) and
370
509
liveAtExit ( bb , v )
371
510
)
@@ -405,7 +544,7 @@ pragma[nomagic]
405
544
predicate ssaDefReachesRead ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
406
545
ssaDefReachesReadWithinBlock ( v , def , bb , i )
407
546
or
408
- variableRead ( bb , i , v , _ ) and
547
+ ssaRef ( bb , i , v , any ( SsaRead k ) ) and
409
548
ssaDefReachesEndOfBlock ( getABasicBlockPredecessor ( bb ) , def , v ) and
410
549
not ssaDefReachesReadWithinBlock ( v , _, bb , i )
411
550
}
@@ -421,7 +560,7 @@ pragma[nomagic]
421
560
predicate adjacentDefRead ( Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 ) {
422
561
exists ( int rnk |
423
562
rnk = ssaDefRank ( def , _, bb1 , i1 , _) and
424
- rnk + 1 = ssaDefRank ( def , _, bb1 , i2 , SsaRead ( ) ) and
563
+ rnk + 1 = ssaDefRank ( def , _, bb1 , i2 , SsaActualRead ( ) ) and
425
564
variableRead ( bb1 , i2 , _, _) and
426
565
bb2 = bb1
427
566
)
@@ -538,18 +677,15 @@ predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Def
538
677
*/
539
678
pragma [ nomagic]
540
679
predicate lastRef ( Definition def , BasicBlock bb , int i ) {
680
+ // Can reach another definition
541
681
lastRefRedef ( def , bb , i , _)
542
682
or
543
- lastSsaRef ( def , _, bb , i ) and
544
- (
683
+ exists ( SourceVariable v | lastSsaRef ( def , v , bb , i ) |
545
684
// Can reach exit directly
546
685
bb instanceof ExitBasicBlock
547
686
or
548
687
// 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 )
553
689
)
554
690
}
555
691
0 commit comments