@@ -649,15 +649,25 @@ module RangeStage<
649
649
or
650
650
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
651
651
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
652
- exists (
653
- Sem:: SsaVariable v2 , Sem:: Guard guardEq , boolean eqIsTrue , D:: Delta d1 , D:: Delta d2 ,
654
- D:: Delta oldDelta
655
- |
656
- guardEq = semEqFlowCond ( v , semSsaRead ( pragma [ only_bind_into ] ( v2 ) , d1 ) , d2 , true , eqIsTrue ) and
652
+ exists ( Sem:: SsaVariable v2 , D:: Delta oldDelta , float d |
653
+ // equality needs to control guard
654
+ result .getBasicBlock ( ) = eqSsaCondDirectlyControls ( v , v2 , d ) and
657
655
result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
658
- // guardEq needs to control guard
659
- guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue ) and
660
- delta = D:: fromFloat ( D:: toFloat ( oldDelta ) - D:: toFloat ( d1 ) + D:: toFloat ( d2 ) )
656
+ delta = D:: fromFloat ( D:: toFloat ( oldDelta ) + d )
657
+ )
658
+ }
659
+
660
+ /**
661
+ * Gets a basic block in which `v1` equals `v2 + delta`.
662
+ */
663
+ pragma [ nomagic]
664
+ private Sem:: BasicBlock eqSsaCondDirectlyControls (
665
+ Sem:: SsaVariable v1 , Sem:: SsaVariable v2 , float delta
666
+ ) {
667
+ exists ( Sem:: Guard guardEq , D:: Delta d1 , D:: Delta d2 , boolean eqIsTrue |
668
+ guardEq = semEqFlowCond ( v1 , semSsaRead ( v2 , d1 ) , d2 , true , eqIsTrue ) and
669
+ delta = D:: toFloat ( d2 ) - D:: toFloat ( d1 ) and
670
+ guardEq .directlyControls ( result , eqIsTrue )
661
671
)
662
672
}
663
673
0 commit comments