@@ -131,20 +131,12 @@ private class NarrowingCastExpr extends ConvertOrBoxExpr {
131131signature module DeltaSig {
132132 class Delta ;
133133
134- bindingset [ d]
135- bindingset [ result ]
136134 float toFloat ( Delta d ) ;
137135
138- bindingset [ d]
139- bindingset [ result ]
140136 int toInt ( Delta d ) ;
141137
142- bindingset [ n]
143- bindingset [ result ]
144138 Delta fromInt ( int n ) ;
145139
146- bindingset [ f]
147- bindingset [ result ]
148140 Delta fromFloat ( float f ) ;
149141}
150142
@@ -352,13 +344,14 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
352344 or
353345 // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
354346 // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
355- exists ( SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 |
347+ exists ( SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 , float oldDelta |
356348 guardEq =
357349 UtilParam:: semEqFlowCond ( v , UtilParam:: semSsaRead ( v2 , D:: fromFloat ( d1 ) ) , D:: fromFloat ( d2 ) ,
358350 true , eqIsTrue ) and
359- result = boundFlowCond ( v2 , e , delta + d1 - d2 , upper , testIsTrue ) and
351+ result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
360352 // guardEq needs to control guard
361- guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue )
353+ guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue ) and
354+ delta = oldDelta - d1 + d2
362355 )
363356 }
364357
0 commit comments