@@ -448,6 +448,91 @@ module Make<LocationSig Location, InputSig<Location> Input> {
448448 }
449449 }
450450
451+ private module AdjacentSsaRefs {
452+ /**
453+ * Holds if the `i`th node of basic block `bb` is a reference to `v`,
454+ * either a read (when `k` is `Read()`) or an SSA definition (when
455+ * `k` is `Def()`).
456+ *
457+ * Unlike `Liveness::varRef`, this includes phi nodes, phi reads, and
458+ * pseudo-reads associated with uncertain writes, but excludes uncertain
459+ * reads.
460+ */
461+ pragma [ nomagic]
462+ predicate ssaRef ( BasicBlock bb , int i , SourceVariable v , RefKind k ) {
463+ variableRead ( bb , i , v , true ) and
464+ k = Read ( )
465+ or
466+ variableWrite ( bb , i , v , false ) and
467+ k = Read ( )
468+ or
469+ any ( Definition def ) .definesAt ( v , bb , i ) and
470+ k = Def ( )
471+ or
472+ synthPhiRead ( bb , v ) and i = - 1 and k = Def ( )
473+ }
474+
475+ private import RankRefs< ssaRef / 4 >
476+
477+ /**
478+ * Holds if `v` is live at the end of basic block `bb`, which contains no
479+ * reference to `v`, and `idom` is the immediate dominator of `bb`.
480+ */
481+ pragma [ nomagic]
482+ private predicate liveThrough ( BasicBlock idom , BasicBlock bb , SourceVariable v ) {
483+ idom = getImmediateBasicBlockDominator ( bb ) and
484+ liveAtExit ( bb , v ) and
485+ not ssaRef ( bb , _, v , _)
486+ }
487+
488+ pragma [ nomagic]
489+ private predicate refReachesEndOfBlock ( BasicBlock bbRef , int i , BasicBlock bb , SourceVariable v ) {
490+ maxRefRank ( bb , v ) = refRank ( bb , i , v , _) and
491+ liveAtExit ( bb , v ) and
492+ bbRef = bb
493+ or
494+ exists ( BasicBlock idom |
495+ refReachesEndOfBlock ( bbRef , i , idom , v ) and
496+ liveThrough ( idom , bb , v )
497+ )
498+ }
499+
500+ /**
501+ * Holds if `v` has adjacent references at index `i1` in basic block `bb1`
502+ * and index `i2` in basic block `bb2`, that is, there is a path between
503+ * the first reference to the second without any other reference to `v` in
504+ * between. References include certain reads, SSA definitions, and
505+ * pseudo-reads in the form of phi-reads. The first reference can be any of
506+ * these kinds while the second is restricted to certain reads and
507+ * uncertain writes.
508+ *
509+ * Note that the placement of phi-reads ensures that the first reference is
510+ * uniquely determined by the second and that the first reference dominates
511+ * the second.
512+ */
513+ predicate adjacentRefRead ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SourceVariable v ) {
514+ bb1 = bb2 and
515+ refRank ( bb1 , i1 , v , _) + 1 = refRank ( bb2 , i2 , v , Read ( ) )
516+ or
517+ refReachesEndOfBlock ( bb1 , i1 , getImmediateBasicBlockDominator ( bb2 ) , v ) and
518+ 1 = refRank ( bb2 , i2 , v , Read ( ) )
519+ }
520+
521+ /**
522+ * Holds if the phi node or phi-read for `v` in basic block `bbPhi` takes
523+ * input from basic block `input`, and that the reference to `v` at index
524+ * `i` in basic block `bb` reaches the end of `input` without going through
525+ * any other reference to `v`.
526+ */
527+ predicate adjacentRefPhi (
528+ BasicBlock bb , int i , BasicBlock input , BasicBlock bbPhi , SourceVariable v
529+ ) {
530+ refReachesEndOfBlock ( bb , i , input , v ) and
531+ input = getABasicBlockPredecessor ( bbPhi ) and
532+ 1 = refRank ( bbPhi , - 1 , v , _)
533+ }
534+ }
535+
451536 private module SsaDefReaches {
452537 newtype TSsaRefKind =
453538 SsaActualRead ( ) or
0 commit comments