@@ -331,15 +331,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
331
331
private module SsaDefReachesNew {
332
332
newtype TSsaRefKind =
333
333
SsaActualRead ( ) or
334
- SsaPhiRead ( ) or
335
334
SsaDef ( )
336
335
337
- class SsaRead = SsaActualRead or SsaPhiRead ;
338
-
339
- class SsaDefExt = SsaDef or SsaPhiRead ;
340
-
341
- SsaDefExt ssaDefExt ( ) { any ( ) }
342
-
343
336
/**
344
337
* A classification of SSA variable references into reads and definitions.
345
338
*/
@@ -348,15 +341,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
348
341
this = SsaActualRead ( ) and
349
342
result = "SsaActualRead"
350
343
or
351
- this = SsaPhiRead ( ) and
352
- result = "SsaPhiRead"
353
- or
354
344
this = SsaDef ( ) and
355
345
result = "SsaDef"
356
346
}
357
347
358
348
int getOrder ( ) {
359
- this instanceof SsaRead and
349
+ this = SsaActualRead ( ) and
360
350
result = 0
361
351
or
362
352
this = SsaDef ( ) and
@@ -366,10 +356,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
366
356
367
357
/**
368
358
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
369
- * either a read (when `k` is `SsaActualRead()`), an SSA definition (when `k`
370
- * is `SsaDef()`), or a phi-read (when ` k` is `SsaPhiRead ()`).
359
+ * either a read (when `k` is `SsaActualRead()`) or an SSA definition (when
360
+ * ` k` is `SsaDef ()`).
371
361
*
372
- * Unlike `Liveness::ref`, this includes `phi` (read) nodes.
362
+ * Unlike `Liveness::ref`, this includes `phi` nodes.
373
363
*/
374
364
pragma [ nomagic]
375
365
predicate ssaRef ( BasicBlock bb , int i , SourceVariable v , SsaRefKind k ) {
@@ -378,8 +368,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
378
368
or
379
369
any ( Definition def ) .definesAt ( v , bb , i ) and
380
370
k = SsaDef ( )
381
- or
382
- synthPhiRead ( bb , v ) and i = - 1 and k = SsaPhiRead ( )
383
371
}
384
372
385
373
private newtype OrderedSsaRefIndex =
@@ -426,31 +414,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
426
414
* Holds if the SSA definition `def` reaches rank index `rnk` in its own
427
415
* basic block `bb`.
428
416
*/
429
- predicate ssaDefReachesRank ( BasicBlock bb , DefinitionExt def , int rnk , SourceVariable v ) {
417
+ predicate ssaDefReachesRank ( BasicBlock bb , Definition def , int rnk , SourceVariable v ) {
430
418
exists ( int i |
431
- rnk = ssaRefRank ( bb , i , v , ssaDefExt ( ) ) and
432
- def .definesAt ( v , bb , i , _ )
419
+ rnk = ssaRefRank ( bb , i , v , SsaDef ( ) ) and
420
+ def .definesAt ( v , bb , i )
433
421
)
434
422
or
435
423
ssaDefReachesRank ( bb , def , rnk - 1 , v ) and
436
424
rnk = ssaRefRank ( bb , _, v , SsaActualRead ( ) )
437
425
}
438
426
439
427
pragma [ nomagic]
440
- predicate liveThroughExt ( BasicBlock bb , SourceVariable v ) {
428
+ private predicate liveThrough ( BasicBlock bb , SourceVariable v ) {
441
429
liveAtExit ( bb , v ) and
442
- not ssaRef ( bb , _, v , ssaDefExt ( ) )
430
+ not ssaRef ( bb , _, v , SsaDef ( ) )
443
431
}
444
432
445
433
/**
446
- * NB: If this predicate is exposed, it should be cached.
447
- *
448
434
* Holds if the SSA definition of `v` at `def` reaches the end of basic
449
435
* block `bb`, at which point it is still live, without crossing another
450
436
* SSA definition of `v`.
451
437
*/
452
438
pragma [ nomagic]
453
- predicate ssaDefReachesEndOfBlockExt ( BasicBlock bb , DefinitionExt def , SourceVariable v ) {
439
+ predicate ssaDefReachesEndOfBlock ( BasicBlock bb , Definition def , SourceVariable v ) {
454
440
exists ( int last |
455
441
last = maxSsaRefRank ( pragma [ only_bind_into ] ( bb ) , pragma [ only_bind_into ] ( v ) ) and
456
442
ssaDefReachesRank ( bb , def , last , v ) and
@@ -463,33 +449,31 @@ module Make<LocationSig Location, InputSig<Location> Input> {
463
449
// the node. If two definitions dominate a node then one must dominate the
464
450
// other, so therefore the definition of _closest_ is given by the dominator
465
451
// tree. Thus, reaching definitions can be calculated in terms of dominance.
466
- ssaDefReachesEndOfBlockExt ( getImmediateBasicBlockDominator ( bb ) , def , pragma [ only_bind_into ] ( v ) ) and
467
- liveThroughExt ( bb , pragma [ only_bind_into ] ( v ) )
452
+ ssaDefReachesEndOfBlock ( getImmediateBasicBlockDominator ( bb ) , def , pragma [ only_bind_into ] ( v ) ) and
453
+ liveThrough ( bb , pragma [ only_bind_into ] ( v ) )
468
454
}
469
455
470
456
/**
471
- * Holds if the SSA definition of `v` at `def` reaches index `i` in the same
457
+ * Holds if the SSA definition of `v` at `def` reaches index `i` in its own
472
458
* basic block `bb`, without crossing another SSA definition of `v`.
473
459
*/
474
- predicate ssaDefReachesReadWithinBlock ( SourceVariable v , DefinitionExt def , BasicBlock bb , int i ) {
460
+ predicate ssaDefReachesReadWithinBlock ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
475
461
exists ( int rnk |
476
462
ssaDefReachesRank ( bb , def , rnk , v ) and
477
463
rnk = ssaRefRank ( bb , i , v , SsaActualRead ( ) )
478
464
)
479
465
}
480
466
481
467
/**
482
- * NB: If this predicate is exposed, it should be cached.
483
- *
484
468
* Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
485
469
* basic block `bb`, without crossing another SSA definition of `v`.
486
470
*/
487
471
pragma [ nomagic]
488
- predicate ssaDefReachesReadExt ( SourceVariable v , DefinitionExt def , BasicBlock bb , int i ) {
472
+ predicate ssaDefReachesRead ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
489
473
ssaDefReachesReadWithinBlock ( v , def , bb , i )
490
474
or
491
475
ssaRef ( bb , i , v , SsaActualRead ( ) ) and
492
- ssaDefReachesEndOfBlockExt ( getABasicBlockPredecessor ( bb ) , def , v ) and
476
+ ssaDefReachesEndOfBlock ( getABasicBlockPredecessor ( bb ) , def , v ) and
493
477
not ssaDefReachesReadWithinBlock ( v , _, bb , i )
494
478
}
495
479
}
0 commit comments