@@ -531,6 +531,79 @@ module Make<LocationSig Location, InputSig<Location> Input> {
531531 input = getABasicBlockPredecessor ( bbPhi ) and
532532 1 = refRank ( bbPhi , - 1 , v , _)
533533 }
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+ )
534607 }
535608
536609 private module SsaDefReaches {
0 commit comments