@@ -2081,6 +2081,54 @@ module Make<
20812081 )
20822082 }
20832083
2084+ pragma [ nomagic]
2085+ private predicate phiInputHasRead ( SsaPhiExt phi , BasicBlock input ) {
2086+ exists ( DfInput:: getARead ( getAPhiInputDef ( phi , input ) ) )
2087+ }
2088+
2089+ /** Holds if `bb` is the target end of a branch edge of a guard and the guard controls `bb`. */
2090+ pragma [ nomagic]
2091+ private predicate guardControlledBranchTarget ( BasicBlock bb ) {
2092+ exists ( BasicBlock guard |
2093+ any ( DfInput:: Guard g ) .hasValueBranchEdge ( guard , bb , _) and
2094+ dominatingEdge ( guard , bb )
2095+ )
2096+ }
2097+
2098+ /**
2099+ * Holds if `prev` is the block containing the unique predecessor of `phi`
2100+ * that reaches `phi` through the input block `input`, and that `mid` is a
2101+ * block in the dominator tree between `prev` and `input` that is
2102+ * guard-equivalent with `input` in the sense that the set of guards
2103+ * controlling `mid` is the same as the set of guards controlling `input`.
2104+ *
2105+ * This is restricted to phi inputs that are actually read.
2106+ */
2107+ private predicate phiInputGuardEquivalenceReaches (
2108+ BasicBlock prev , BasicBlock mid , SsaPhiExt phi , BasicBlock input
2109+ ) {
2110+ phiInputHasRead ( phi , input ) and
2111+ AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) , phi .getSourceVariable ( ) ) and
2112+ mid = input
2113+ or
2114+ exists ( BasicBlock mid0 |
2115+ phiInputGuardEquivalenceReaches ( prev , mid0 , phi , input ) and
2116+ not guardControlledBranchTarget ( mid0 ) and
2117+ mid0 != prev and
2118+ mid = mid0 .getImmediateDominator ( )
2119+ )
2120+ }
2121+
2122+ /**
2123+ * Holds if the immediately preceding reference to the input to `phi` from
2124+ * the block `input` is guard-equivalent with `input`.
2125+ *
2126+ * This is restricted to phi inputs that are actually read.
2127+ */
2128+ private predicate phiInputIsGuardEquivalentWithPreviousRef ( SsaPhiExt phi , BasicBlock input ) {
2129+ exists ( BasicBlock prev | phiInputGuardEquivalenceReaches ( prev , prev , phi , input ) )
2130+ }
2131+
20842132 /**
20852133 * Holds if the input to `phi` from the block `input` might be relevant for
20862134 * barrier guards as a separately synthesized `TSsaInputNode`.
@@ -2095,7 +2143,7 @@ module Make<
20952143 or
20962144 DfInput:: supportBarrierGuardsOnPhiEdges ( ) and
20972145 // If the input isn't explicitly read then a guard cannot check it.
2098- exists ( DfInput :: getARead ( getAPhiInputDef ( phi , input ) ) ) and
2146+ phiInputHasRead ( phi , input ) and
20992147 (
21002148 // The input node is relevant either if it sits directly on a branch
21012149 // edge for a guard,
@@ -2114,15 +2162,19 @@ module Make<
21142162 // }
21152163 // // phi-read node for `x`
21162164 // ```
2117- exists ( BasicBlock prev |
2118- AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) ,
2119- phi .getSourceVariable ( ) ) and
2120- prev != input and
2121- exists ( DfInput:: Guard g , DfInput:: GuardValue val |
2122- DfInput:: guardDirectlyControlsBlock ( g , input , val ) and
2123- not DfInput:: guardDirectlyControlsBlock ( g , prev , val )
2124- )
2125- )
2165+ not phiInputIsGuardEquivalentWithPreviousRef ( phi , input )
2166+ // An equivalent, but less performant, way to express this is as follows:
2167+ // ```
2168+ // exists(BasicBlock prev |
2169+ // AdjacentSsaRefs::adjacentRefPhi(prev, _, input, phi.getBasicBlock(),
2170+ // phi.getSourceVariable()) and
2171+ // prev != input and
2172+ // exists(DfInput::Guard g, DfInput::GuardValue val |
2173+ // DfInput::guardDirectlyControlsBlock(g, input, val) and
2174+ // not DfInput::guardDirectlyControlsBlock(g, prev, val)
2175+ // )
2176+ // )
2177+ // ```
21262178 )
21272179 }
21282180
0 commit comments