From d8b6767e4e5285fef3cf4450b9cba04431e40727 Mon Sep 17 00:00:00 2001 From: Martin Date: Tue, 26 May 2020 19:49:01 +0100 Subject: [PATCH] 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. --- src/util/floatingpoint.cpp | 17 ++++++++++++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/issue3619.smt2 | 7 +++++++ 3 files changed, 22 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/fp/issue3619.smt2 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 +#include #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::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); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5a59f2f54..fbf249e7f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -503,6 +503,7 @@ set(regress_0_tests regress0/fp/down-cast-RNA.smt2 regress0/fp/ext-rew-test.smt2 regress0/fp/issue3536.smt2 + regress0/fp/issue3619.smt2 regress0/fp/issue4277-assign-func.smt2 regress0/fp/rti_3_5_bug.smt2 regress0/fp/rti_3_5_bug_report.smt2 diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2 new file mode 100644 index 000000000..9d6e0a36d --- /dev/null +++ b/test/regress/regress0/fp/issue3619.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: symfpu +(set-logic QF_FPLRA) +(set-info :status sat) +(declare-fun a () (_ FloatingPoint 11 53)) +(assert (= (fp.to_real a) 0.0)) +(check-sat) + -- 2.30.2