diff options
author | Martin <martin.brain@cs.ox.ac.uk> | 2020-05-26 19:49:01 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-26 13:49:01 -0500 |
commit | d8b6767e4e5285fef3cf4450b9cba04431e40727 (patch) | |
tree | a752140ddb4ae5985aa5f34c1c24f479d4693977 /src/util/floatingpoint.cpp | |
parent | 114a215e9b33effb361c4b000fb23085ce9f079a (diff) |
Fix an incorrect limit in conversion from real to float (#4418)
This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.
Diffstat (limited to 'src/util/floatingpoint.cpp')
-rw-r--r-- | src/util/floatingpoint.cpp | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 1b1bfddc2..3bcf2b0de 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -19,6 +19,7 @@ #include "util/integer.h" #include <math.h> +#include <limits> #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" @@ -920,15 +921,25 @@ static FloatingPointLiteral constructorHelperBitVector( Integer significand(0); #endif Integer signedSignificand(sign * significand); - - // Only have pow(uint32_t) so we should check this. - Assert(this->t.significand() <= 32); + + // We only have multiplyByPow(uint32_t) so we can't convert all numbers. + // As we convert Integer -> unsigned int -> uint32_t we need that + // unsigned int is not smaller than uint32_t + static_assert(sizeof(unsigned int) >= sizeof(uint32_t)); +#ifdef CVC4_ASSERTIONS + // Note that multipling by 2^n requires n bits of space (worst case) + // so, in effect, these tests limit us to cases where the resultant + // number requires up to 2^32 bits = 512 megabyte to represent. + Integer shiftLimit(std::numeric_limits<uint32_t>::max()); +#endif if (!(exp.strictlyNegative())) { + Assert(exp <= shiftLimit); Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt())); return PartialRational(Rational(r), true); } else { Integer one(1U); + Assert((-exp) <= shiftLimit); Integer q(one.multiplyByPow2((-exp).toUnsignedInt())); Rational r(signedSignificand, q); return PartialRational(r, true); |