C++: Fix floating point imprecision.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-03-08 13:19:56 +00:00
parent ce0f2b1788
commit 619266d04b
2 changed files with 11 additions and 2 deletions

View File

@@ -936,6 +936,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
bounded(cast.getOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
}
/**
* Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
* needed on the lesser side of a floating-point comparison or on both sides of
* a floating point equality because QL does not follow IEEE in floating-point
* comparisons but instead defines -0.0 to be less than and distinct from 0.0.
*/
bindingset[x]
private float normalizeFloatUp(float x) { result = x + 0.0 }
/**
* Holds if `b + delta` is a valid bound for `e`.
* - `upper = true` : `e <= b + delta`
@@ -1025,7 +1034,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
e.(SemNegateExpr).getOperand() = mid and
b instanceof SemZeroBound and
bounded(mid, b, d, upper.booleanNot(), fromBackEdge, origdelta, reason) and
f = -D::toFloat(d) and
f = normalizeFloatUp(-D::toFloat(d)) and
delta = D::fromFloat(f) and
if semPositive(e) then f >= 0 else any()
)

View File

@@ -271,7 +271,7 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=0 range=>=-7
int c = -a;
range(c); // $ range=<=7 MISSING: range=>=0
range(c); // $ range=<=7 range=>=0
range(b+c); // $ range="<=- ...+0" range=">=+ ...:a+0" range=>=-7 range=<=7
total += b+c;
range(total);