@@ -448,6 +448,91 @@ module Make<LocationSig Location, InputSig<Location> Input> {
448
448
}
449
449
}
450
450
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
+
451
536
private module SsaDefReaches {
452
537
newtype TSsaRefKind =
453
538
SsaActualRead ( ) or
0 commit comments