@@ -531,6 +531,79 @@ module Make<LocationSig Location, InputSig<Location> Input> {
531
531
input = getABasicBlockPredecessor ( bbPhi ) and
532
532
1 = refRank ( bbPhi , - 1 , v , _)
533
533
}
534
+
535
+ private predicate adjacentRefs ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SourceVariable v ) {
536
+ adjacentRefRead ( bb1 , i1 , bb2 , i2 , v )
537
+ or
538
+ adjacentRefPhi ( bb1 , i1 , _, bb2 , v ) and i2 = - 1
539
+ }
540
+
541
+ /**
542
+ * Holds if the reference to `v` at index `i1` in basic block `bb1` reaches
543
+ * the certain read at index `i2` in basic block `bb2` without going
544
+ * through any other certain read. The boolean `samevar` indicates whether
545
+ * the two references are to the same SSA variable.
546
+ *
547
+ * Note that since this relation skips over phi nodes and phi reads, it may
548
+ * be quadratic in the number of variable references for certain access
549
+ * patterns.
550
+ */
551
+ predicate firstUseAfterRef (
552
+ BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SourceVariable v , boolean samevar
553
+ ) {
554
+ adjacentRefs ( bb1 , i1 , bb2 , i2 , v ) and
555
+ variableRead ( bb2 , i2 , v , _) and
556
+ samevar = true
557
+ or
558
+ exists ( BasicBlock bb0 , int i0 , boolean samevar0 |
559
+ firstUseAfterRef ( bb0 , i0 , bb2 , i2 , v , samevar0 ) and
560
+ adjacentRefs ( bb1 , i1 , bb0 , i0 , v ) and
561
+ not variableWrite ( bb0 , i0 , v , true ) and
562
+ if any ( Definition def ) .definesAt ( v , bb0 , i0 )
563
+ then samevar = false
564
+ else (
565
+ samevar = samevar0 and synthPhiRead ( bb0 , v ) and i0 = - 1
566
+ )
567
+ )
568
+ }
569
+ }
570
+
571
+ /**
572
+ * Holds if `def` reaches the certain read at index `i` in basic block `bb`
573
+ * without going through any other certain read. The boolean `samevar`
574
+ * indicates whether the read is a use of `def` or whether some number of phi
575
+ * nodes and/or uncertain reads occur between `def` and the read.
576
+ *
577
+ * Note that since this relation skips over phi nodes and phi reads, it may
578
+ * be quadratic in the number of variable references for certain access
579
+ * patterns.
580
+ */
581
+ predicate firstUse ( Definition def , BasicBlock bb , int i , boolean samevar ) {
582
+ exists ( BasicBlock bb1 , int i1 , SourceVariable v |
583
+ def .definesAt ( v , bb1 , i1 ) and
584
+ AdjacentSsaRefs:: firstUseAfterRef ( bb1 , i1 , bb , i , v , samevar )
585
+ )
586
+ }
587
+
588
+ /**
589
+ * Holds if the certain read at index `i1` in basic block `bb1` reaches the
590
+ * certain read at index `i2` in basic block `bb2` without going through any
591
+ * other certain read. The boolean `samevar` indicates whether the two reads
592
+ * are of the same SSA variable.
593
+ *
594
+ * Note that since this relation skips over phi nodes and phi reads, it may
595
+ * be quadratic in the number of variable references for certain access
596
+ * patterns.
597
+ */
598
+ predicate adjacentUseUse (
599
+ BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SourceVariable v , boolean samevar
600
+ ) {
601
+ exists ( boolean samevar0 |
602
+ variableRead ( bb1 , i1 , v , true ) and
603
+ not variableWrite ( bb1 , i1 , v , true ) and
604
+ AdjacentSsaRefs:: firstUseAfterRef ( bb1 , i1 , bb2 , i2 , v , samevar0 ) and
605
+ if any ( Definition def ) .definesAt ( v , bb1 , i1 ) then samevar = false else samevar = samevar0
606
+ )
534
607
}
535
608
536
609
private module SsaDefReaches {
0 commit comments