@@ -2081,6 +2081,41 @@ 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+ private BasicBlock getGuardEquivalentImmediateDominator ( BasicBlock bb ) {
2099+ result = bb .getImmediateDominator ( ) and
2100+ not guardControlledBranchTarget ( bb )
2101+ }
2102+
2103+ /**
2104+ * Holds if the immediately preceding reference to the input to `phi` from
2105+ * the block `input` is guard-equivalent with `input` in the sense that the
2106+ * set of guards controlling the preceding reference is the same as the set
2107+ * of guards controlling `input`.
2108+ *
2109+ * This is restricted to phi inputs that are actually read.
2110+ */
2111+ private predicate phiInputIsGuardEquivalentWithPreviousRef ( SsaPhiExt phi , BasicBlock input ) {
2112+ exists ( BasicBlock prev |
2113+ phiInputHasRead ( phi , input ) and
2114+ AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) , phi .getSourceVariable ( ) ) and
2115+ prev = getGuardEquivalentImmediateDominator * ( input )
2116+ )
2117+ }
2118+
20842119 /**
20852120 * Holds if the input to `phi` from the block `input` might be relevant for
20862121 * barrier guards as a separately synthesized `TSsaInputNode`.
@@ -2095,7 +2130,7 @@ module Make<
20952130 or
20962131 DfInput:: supportBarrierGuardsOnPhiEdges ( ) and
20972132 // If the input isn't explicitly read then a guard cannot check it.
2098- exists ( DfInput :: getARead ( getAPhiInputDef ( phi , input ) ) ) and
2133+ phiInputHasRead ( phi , input ) and
20992134 (
21002135 // The input node is relevant either if it sits directly on a branch
21012136 // edge for a guard,
@@ -2114,15 +2149,19 @@ module Make<
21142149 // }
21152150 // // phi-read node for `x`
21162151 // ```
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- )
2152+ not phiInputIsGuardEquivalentWithPreviousRef ( phi , input )
2153+ // An equivalent, but less performant, way to express this is as follows:
2154+ // ```
2155+ // exists(BasicBlock prev |
2156+ // AdjacentSsaRefs::adjacentRefPhi(prev, _, input, phi.getBasicBlock(),
2157+ // phi.getSourceVariable()) and
2158+ // prev != input and
2159+ // exists(DfInput::Guard g, DfInput::GuardValue val |
2160+ // DfInput::guardDirectlyControlsBlock(g, input, val) and
2161+ // not DfInput::guardDirectlyControlsBlock(g, prev, val)
2162+ // )
2163+ // )
2164+ // ```
21262165 )
21272166 }
21282167
0 commit comments