mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

address min-int overflow reported in #2565

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-17 18:19:55 -04:00
parent 77ef40a3db
commit 9c74c05854
2 changed files with 28 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/test/mpz.cpp
View file

@ -293,6 +293,19 @@ void tst_int_min_bug() {
m.del(r);
}
void tst_int64_min_bug() {
synch_mpz_manager m;
mpz intmin;
mpz test;
m.set(test, "-9223372036854775808");
m.set(intmin, std::numeric_limits<int64_t>::min());
std::cout << "minint: " << m.to_string(intmin) << "\n";
ENSURE(m.eq(test, intmin));
m.del(intmin);
m.del(test);
}
void tst_scoped() {
synch_mpz_manager m;
scoped_synch_mpz a(m);
@ -504,6 +517,7 @@ void tst_mpz() {
// tst_gcd();
tst_scoped();
tst_int_min_bug();
tst_int64_min_bug();
bug4();
bug3();
bug1();

19
src/util/mpz.cpp
View file

@ -272,7 +272,12 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
c.m_kind = mpz_large;
SASSERT(capacity(c) >= m_init_cell_capacity);
uint64_t _v;
if (v < 0) {
if (v == std::numeric_limits<int64_t>::min()) {
// min-int is even
_v = -(v/2);
c.m_val = -1;
}
else if (v < 0) {
_v = -v;
c.m_val = -1;
}
@ -298,14 +303,15 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
}
c.m_kind = mpz_large;
uint64_t _v;
bool sign;
if (v < 0) {
bool sign = v < 0;
if (v == std::numeric_limits<int64_t>::min()) {
_v = -(v/2);
}
else if (v < 0) {
_v = -v;
sign = true;
}
else {
_v = v;
sign = false;
}
mpz_set_ui(*c.m_ptr, static_cast<unsigned>(_v));
MPZ_BEGIN_CRITICAL();
@ -316,6 +322,9 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
if (sign)
mpz_neg(*c.m_ptr, *c.m_ptr);
#endif
if (v == std::numeric_limits<int64_t>::min()) {
big_add(c, c, c);
}
}
template<bool SYNCH>