@@ -257,11 +257,21 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo
257257 or
258258 // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
259259 // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
260- exists ( SsaVariable v2 , Guard guardEq , boolean eqIsTrue , int d1 , int d2 |
261- guardEq = eqFlowCond ( v , ssaRead ( v2 , d1 ) , d2 , true , eqIsTrue ) and
262- result = boundFlowCond ( v2 , e , delta + d1 - d2 , upper , testIsTrue ) and
263- // guardEq needs to control guard
264- guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue )
260+ exists ( SsaVariable v2 , int d |
261+ // equality needs to control guard
262+ result .getBasicBlock ( ) = eqSsaCondDirectlyControls ( v , v2 , d ) and
263+ result = boundFlowCond ( v2 , e , delta - d , upper , testIsTrue )
264+ )
265+ }
266+
267+ /**
268+ * Gets a basic block in which `v1` equals `v2 + delta`.
269+ */
270+ private BasicBlock eqSsaCondDirectlyControls ( SsaVariable v1 , SsaVariable v2 , int delta ) {
271+ exists ( Guard guardEq , int d1 , int d2 , boolean eqIsTrue |
272+ guardEq = eqFlowCond ( v1 , ssaRead ( v2 , d1 ) , d2 , true , eqIsTrue ) and
273+ delta = d2 - d1 and
274+ guardEq .directlyControls ( result , eqIsTrue )
265275 )
266276}
267277
0 commit comments