@@ -331,15 +331,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
331331 private module SsaDefReachesNew {
332332 newtype TSsaRefKind =
333333 SsaActualRead ( ) or
334- SsaPhiRead ( ) or
335334 SsaDef ( )
336335
337- class SsaRead = SsaActualRead or SsaPhiRead ;
338-
339- class SsaDefExt = SsaDef or SsaPhiRead ;
340-
341- SsaDefExt ssaDefExt ( ) { any ( ) }
342-
343336 /**
344337 * A classification of SSA variable references into reads and definitions.
345338 */
@@ -348,15 +341,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
348341 this = SsaActualRead ( ) and
349342 result = "SsaActualRead"
350343 or
351- this = SsaPhiRead ( ) and
352- result = "SsaPhiRead"
353- or
354344 this = SsaDef ( ) and
355345 result = "SsaDef"
356346 }
357347
358348 int getOrder ( ) {
359- this instanceof SsaRead and
349+ this = SsaActualRead ( ) and
360350 result = 0
361351 or
362352 this = SsaDef ( ) and
@@ -366,10 +356,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
366356
367357 /**
368358 * 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 ()`).
371361 *
372- * Unlike `Liveness::ref`, this includes `phi` (read) nodes.
362+ * Unlike `Liveness::ref`, this includes `phi` nodes.
373363 */
374364 pragma [ nomagic]
375365 predicate ssaRef ( BasicBlock bb , int i , SourceVariable v , SsaRefKind k ) {
@@ -378,8 +368,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
378368 or
379369 any ( Definition def ) .definesAt ( v , bb , i ) and
380370 k = SsaDef ( )
381- or
382- synthPhiRead ( bb , v ) and i = - 1 and k = SsaPhiRead ( )
383371 }
384372
385373 private newtype OrderedSsaRefIndex =
@@ -426,31 +414,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
426414 * Holds if the SSA definition `def` reaches rank index `rnk` in its own
427415 * basic block `bb`.
428416 */
429- predicate ssaDefReachesRank ( BasicBlock bb , DefinitionExt def , int rnk , SourceVariable v ) {
417+ predicate ssaDefReachesRank ( BasicBlock bb , Definition def , int rnk , SourceVariable v ) {
430418 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 )
433421 )
434422 or
435423 ssaDefReachesRank ( bb , def , rnk - 1 , v ) and
436424 rnk = ssaRefRank ( bb , _, v , SsaActualRead ( ) )
437425 }
438426
439427 pragma [ nomagic]
440- predicate liveThroughExt ( BasicBlock bb , SourceVariable v ) {
428+ private predicate liveThrough ( BasicBlock bb , SourceVariable v ) {
441429 liveAtExit ( bb , v ) and
442- not ssaRef ( bb , _, v , ssaDefExt ( ) )
430+ not ssaRef ( bb , _, v , SsaDef ( ) )
443431 }
444432
445433 /**
446- * NB: If this predicate is exposed, it should be cached.
447- *
448434 * Holds if the SSA definition of `v` at `def` reaches the end of basic
449435 * block `bb`, at which point it is still live, without crossing another
450436 * SSA definition of `v`.
451437 */
452438 pragma [ nomagic]
453- predicate ssaDefReachesEndOfBlockExt ( BasicBlock bb , DefinitionExt def , SourceVariable v ) {
439+ predicate ssaDefReachesEndOfBlock ( BasicBlock bb , Definition def , SourceVariable v ) {
454440 exists ( int last |
455441 last = maxSsaRefRank ( pragma [ only_bind_into ] ( bb ) , pragma [ only_bind_into ] ( v ) ) and
456442 ssaDefReachesRank ( bb , def , last , v ) and
@@ -463,33 +449,31 @@ module Make<LocationSig Location, InputSig<Location> Input> {
463449 // the node. If two definitions dominate a node then one must dominate the
464450 // other, so therefore the definition of _closest_ is given by the dominator
465451 // 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 ) )
468454 }
469455
470456 /**
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
472458 * basic block `bb`, without crossing another SSA definition of `v`.
473459 */
474- predicate ssaDefReachesReadWithinBlock ( SourceVariable v , DefinitionExt def , BasicBlock bb , int i ) {
460+ predicate ssaDefReachesReadWithinBlock ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
475461 exists ( int rnk |
476462 ssaDefReachesRank ( bb , def , rnk , v ) and
477463 rnk = ssaRefRank ( bb , i , v , SsaActualRead ( ) )
478464 )
479465 }
480466
481467 /**
482- * NB: If this predicate is exposed, it should be cached.
483- *
484468 * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
485469 * basic block `bb`, without crossing another SSA definition of `v`.
486470 */
487471 pragma [ nomagic]
488- predicate ssaDefReachesReadExt ( SourceVariable v , DefinitionExt def , BasicBlock bb , int i ) {
472+ predicate ssaDefReachesRead ( SourceVariable v , Definition def , BasicBlock bb , int i ) {
489473 ssaDefReachesReadWithinBlock ( v , def , bb , i )
490474 or
491475 ssaRef ( bb , i , v , SsaActualRead ( ) ) and
492- ssaDefReachesEndOfBlockExt ( getABasicBlockPredecessor ( bb ) , def , v ) and
476+ ssaDefReachesEndOfBlock ( getABasicBlockPredecessor ( bb ) , def , v ) and
493477 not ssaDefReachesReadWithinBlock ( v , _, bb , i )
494478 }
495479 }
0 commit comments