From a5ecf87ab82c86b01eef01646b70fdcbb30b1f5d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:32:38 +0100 Subject: [PATCH 01/12] fix #1288 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/tbv.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 7475750db..69cc4819a 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,8 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = num_tbits(); bit > 0;) { - --bit; + for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { From 6f7f957a266d8a22f628aaee29303ac650529f73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:38:02 +0100 Subject: [PATCH 02/12] likely fix for #1287 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8938fb1b5..41f3f0e06 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -140,7 +140,7 @@ namespace z3 { class context { bool m_enable_exceptions; Z3_context m_ctx; - static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } + static void __cdecl error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } void init(config & c) { m_ctx = Z3_mk_context_rc(c); m_enable_exceptions = true; From c72b3356c16778fe21223f374f7679c1c0664e65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:41:02 +0100 Subject: [PATCH 03/12] fix #1286 Signed-off-by: Nikolaj Bjorner --- src/interp/iz3mgr.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 6ca8fae34..e4c294059 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -96,7 +96,7 @@ class ast_r : public ast_i { ast_r(const ast_r &other) : ast_i(other) { _m = other._m; - _m->inc_ref(_ast); + if (_m) _m->inc_ref(_ast); } ast_r &operator=(const ast_r &other) { @@ -104,7 +104,7 @@ class ast_r : public ast_i { _m->dec_ref(_ast); _ast = other._ast; _m = other._m; - _m->inc_ref(_ast); + if (_m) _m->inc_ref(_ast); return *this; } From 52217f0600aaa2b2961f971d8648b8e3c7bf4f2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:56:05 +0100 Subject: [PATCH 04/12] fix #1290 Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index f94558097..4290700d4 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -86,18 +86,18 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); m_const_decls.erase(d); + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); m_finterp.remove(d); m_func_decls.erase(d); + m_manager.dec_ref(ef->get_data().m_key); + dealloc(ef->get_data().m_value); } } From 1371caace28097b8d86ba4cd47be22492d419784 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 11:05:57 +0100 Subject: [PATCH 05/12] fix #1287, again Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 41f3f0e06..2200874d3 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -140,7 +140,7 @@ namespace z3 { class context { bool m_enable_exceptions; Z3_context m_ctx; - static void __cdecl error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } + static void Z3_API error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } void init(config & c) { m_ctx = Z3_mk_context_rc(c); m_enable_exceptions = true; From 22fa108ffd91834eb5b4a98a3e14434750b7b8f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 11:07:22 +0100 Subject: [PATCH 06/12] fix #1288, again Signed-off-by: Nikolaj Bjorner --- src/muz/rel/tbv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 69cc4819a..5ef15303e 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,7 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { + for (unsigned bit = std::min(63u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { From 06d75a616f6246eaa717ca34bb2719726d6858d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 11:40:17 +0100 Subject: [PATCH 07/12] fix #1288, again Signed-off-by: Nikolaj Bjorner --- src/muz/rel/tbv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 5ef15303e..69cc4819a 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,7 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = std::min(63u, num_tbits()); bit-- > 0;) { + for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { From d2ec927844120a4c26236e80b9bd8ae302de51f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 12:34:08 +0100 Subject: [PATCH 08/12] fix build break Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 4290700d4..833c254c3 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -86,18 +86,22 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { + auto k = ec->get_data().m_key; + auto v = ec->get_data().m_value; m_interp.remove(d); m_const_decls.erase(d); - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); + m_manager.dec_ref(k); + m_manager.dec_ref(v); return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { + auto k = ef->get_data().m_key; + auto v = ef->get_data().m_value; m_finterp.remove(d); m_func_decls.erase(d); - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); + m_manager.dec_ref(k); + dealloc(v); } } From f359f238851d8c1a5db11a95d4ded3639813db9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 15:47:06 -0700 Subject: [PATCH 09/12] another fix for #1288 Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 9569ac280..7cf87b24b 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -558,14 +558,13 @@ void mpz_manager::big_rem(mpz const & a, mpz const & b, mpz & c) { template void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { - if (is_small(a) && is_small(b)) { + COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int)); + if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) { int _a = a.m_val; int _b = b.m_val; if (_a < 0) _a = -_a; if (_b < 0) _b = -_b; unsigned r = u_gcd(_a, _b); - // Remark: r is (INT_MAX + 1) - // If a == b == INT_MIN set(c, r); } else { From cae414e575299d976899b764041195ff36f484e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Oct 2017 13:59:44 -0700 Subject: [PATCH 10/12] fixes for #1296, removing COMPILE_TIME_ASSERT Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/maximize_ac_sharing.cpp | 5 +++-- src/sat/sat_watched.h | 8 ++++---- src/smt/smt_theory_var_list.h | 4 ++-- src/util/approx_set.h | 4 ++-- src/util/bit_vector.h | 2 +- src/util/debug.h | 1 - src/util/double_manager.h | 2 +- src/util/mpf.cpp | 6 +++--- src/util/mpff.cpp | 4 ++-- src/util/mpn.cpp | 2 +- src/util/mpz.cpp | 10 +++++----- src/util/uint_set.h | 1 - src/util/util.h | 6 +++--- 13 files changed, 27 insertions(+), 28 deletions(-) diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp index d7e8df7a2..a838f59fa 100644 --- a/src/ast/rewriter/maximize_ac_sharing.cpp +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -54,13 +54,13 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";); try_to_reuse: if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) { - for (unsigned i = 0; i < num_args - 1; i++) { + for (unsigned i = 0; i + 1 < num_args; i++) { for (unsigned j = i + 1; j < num_args; j++) { if (contains(f, _args[i], _args[j])) { TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";); _args[i] = m.mk_app(f, _args[i], _args[j]); SASSERT(num_args > 1); - for (unsigned w = j; w < num_args - 1; w++) { + for (unsigned w = j; w + 1 < num_args; w++) { _args[w] = _args[w+1]; } num_args--; @@ -144,6 +144,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) { while (i != old_lim) { --i; entry * e = m_entries[i]; + m_cache.remove(e); m.dec_ref(e->m_arg1); m.dec_ref(e->m_arg2); } diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index e5a02953b..639d3e6a8 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -109,10 +109,10 @@ namespace sat { bool operator!=(watched const & w) const { return !operator==(w); } }; - COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3); - COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3); - COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3); - COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3); + static_assert(0 <= watched::BINARY && watched::BINARY <= 3, ""); + static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, ""); + static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, ""); + static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, ""); struct watched_lt { bool operator()(watched const & w1, watched const & w2) const { diff --git a/src/smt/smt_theory_var_list.h b/src/smt/smt_theory_var_list.h index d7e246824..aa2816786 100644 --- a/src/smt/smt_theory_var_list.h +++ b/src/smt/smt_theory_var_list.h @@ -67,9 +67,9 @@ namespace smt { }; // 32 bit machine - COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int)); + static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit"); // 64 bit machine - COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int)); + static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit"); }; #endif /* SMT_THEORY_VAR_LIST_H_ */ diff --git a/src/util/approx_set.h b/src/util/approx_set.h index e696d52ee..1cb7ae9f2 100644 --- a/src/util/approx_set.h +++ b/src/util/approx_set.h @@ -29,7 +29,7 @@ public: static const unsigned long long zero = 0ull; static const unsigned long long one = 1ull; }; -COMPILE_TIME_ASSERT(sizeof(unsigned long long) == 8); +static_assert(sizeof(unsigned long long) == 8, ""); template <> class approx_set_traits { public: @@ -37,7 +37,7 @@ public: static const unsigned zero = 0; static const unsigned one = 1; }; -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes"); template class approx_set_tpl : private T2U_Proc { diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 6a254e399..2d42e35a2 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -24,7 +24,7 @@ Revision History: #include "util/vector.h" #include "util/memory_manager.h" -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes"); #define BV_DEFAULT_CAPACITY 2 class bit_vector { diff --git a/src/util/debug.h b/src/util/debug.h index e0ceb9a64..536df4588 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -90,7 +90,6 @@ bool is_debug_enabled(const char * tag); exit(-1); \ } -#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "") void finalize_debug(); /* diff --git a/src/util/double_manager.h b/src/util/double_manager.h index 33cccf2af..7532a3b8b 100644 --- a/src/util/double_manager.h +++ b/src/util/double_manager.h @@ -97,7 +97,7 @@ public: } }; -COMPILE_TIME_ASSERT(sizeof(uint64) == sizeof(double)); +static_assert(sizeof(uint64) == sizeof(double), ""); #endif /* DOUBLE_MANAGER_H_ */ diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5e7233110..3218419a9 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -73,7 +73,7 @@ mpf_manager::~mpf_manager() { } void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, int value) { - COMPILE_TIME_ASSERT(sizeof(int) == 4); + static_assert(sizeof(int) == 4, "assume integers are 4 bytes"); o.sign = false; o.ebits = ebits; @@ -119,7 +119,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { // double === mpf(11, 53) - COMPILE_TIME_ASSERT(sizeof(double) == 8); + static_assert(sizeof(double) == 8, "doubles are 8 bytes"); uint64 raw; memcpy(&raw, &value, sizeof(double)); @@ -155,7 +155,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) { // single === mpf(8, 24) - COMPILE_TIME_ASSERT(sizeof(float) == 4); + static_assert(sizeof(float) == 4, "floats are 4 bytes"); unsigned int raw; memcpy(&raw, &value, sizeof(float)); diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 459b0691c..eac9cc80c 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -27,8 +27,8 @@ Revision History: #include "util/bit_util.h" #include "util/trace.h" -COMPILE_TIME_ASSERT(sizeof(mpn_digit) == sizeof(unsigned)); -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(mpn_digit) == sizeof(unsigned), ""); +static_assert(sizeof(unsigned) == 4, "unsigned haven't changed size for a while"); // MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word. #define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1)) diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 65223133f..2059ea6fd 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -24,7 +24,7 @@ Revision History: #define max(a,b) (((a) > (b)) ? (a) : (b)) typedef uint64 mpn_double_digit; -COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit)); +static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment"); const mpn_digit mpn_manager::zero = 0; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 7cf87b24b..7ad472ef1 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -558,7 +558,7 @@ void mpz_manager::big_rem(mpz const & a, mpz const & b, mpz & c) { template void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { - COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int)); + static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch"); if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) { int _a = a.m_val; int _b = b.m_val; @@ -724,7 +724,7 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { #ifdef LEHMER_GCD // For now, it only works if sizeof(digit_t) == sizeof(unsigned) - COMPILE_TIME_ASSERT(sizeof(digit_t) == sizeof(unsigned)); + static_assert(sizeof(digit_t) == sizeof(unsigned), ""); int64 a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz; mpz a1, b1, t, r, tmp; @@ -1754,7 +1754,7 @@ void mpz_manager::mul2k(mpz & a, unsigned k) { } #ifndef _MP_GMP -COMPILE_TIME_ASSERT(sizeof(digit_t) == 4 || sizeof(digit_t) == 8); +static_assert(sizeof(digit_t) == 4 || sizeof(digit_t) == 8, ""); #endif template @@ -1821,7 +1821,7 @@ unsigned mpz_manager::log2(mpz const & a) { if (is_small(a)) return ::log2((unsigned)a.m_val); #ifndef _MP_GMP - COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); + static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, ""); mpz_cell * c = a.m_ptr; unsigned sz = c->m_size; digit_t * ds = c->m_digits; @@ -1843,7 +1843,7 @@ unsigned mpz_manager::mlog2(mpz const & a) { if (is_small(a)) return ::log2((unsigned)-a.m_val); #ifndef _MP_GMP - COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); + static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, ""); mpz_cell * c = a.m_ptr; unsigned sz = c->m_size; digit_t * ds = c->m_digits; diff --git a/src/util/uint_set.h b/src/util/uint_set.h index 33c39eeb2..352189ef1 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -22,7 +22,6 @@ Revision History: #include "util/util.h" #include "util/vector.h" -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); class uint_set : unsigned_vector { diff --git a/src/util/util.h b/src/util/util.h index 23c2c1657..1f753099c 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -33,13 +33,13 @@ Revision History: typedef unsigned long long uint64; #endif -COMPILE_TIME_ASSERT(sizeof(uint64) == 8); +static_assert(sizeof(uint64) == 8, "64 bits please"); #ifndef int64 typedef long long int64; #endif -COMPILE_TIME_ASSERT(sizeof(int64) == 8); +static_assert(sizeof(int64) == 8, "64 bits"); #ifndef INT64_MIN #define INT64_MIN static_cast(0x8000000000000000ull) @@ -111,7 +111,7 @@ inline unsigned next_power_of_two(unsigned v) { unsigned log2(unsigned v); unsigned uint64_log2(uint64 v); -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits"); // Return the number of 1 bits in v. static inline unsigned get_num_1bits(unsigned v) { From 7f693186a0c0ca9cc0d15ff3fd8fbc1734e95ee1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Oct 2017 07:10:04 -0700 Subject: [PATCH 11/12] trying to address leak reported in #1297 Signed-off-by: Nikolaj Bjorner --- src/api/api_parsers.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index bef31e9f1..7a68efbd8 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -69,6 +69,7 @@ extern "C" { ok = false; } mk_c(c)->m_smtlib_error_buffer = outs.str(); + outs.clear(); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); @@ -98,6 +99,7 @@ extern "C" { ok = false; } mk_c(c)->m_smtlib_error_buffer = outs.str(); + outs.clear(); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); From 09ea370ea33f64e54f9cd837cd4e9f66ebe933df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Oct 2017 12:06:19 -0700 Subject: [PATCH 12/12] update C-example that fails to not use longjumps. Issue #1297 Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 35 ++++++++++++++++++++++++----------- src/api/api_parsers.cpp | 16 ++++++++-------- 2 files changed, 32 insertions(+), 19 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 88fdaa1cf..6327ad40f 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -65,6 +65,15 @@ void throw_z3_error(Z3_context c, Z3_error_code e) longjmp(g_catch_buffer, e); } +/** + \brief Error handling that depends on checking an error code on the context. + +*/ + +void nothrow_z3_error(Z3_context c, Z3_error_code e) { + // no-op +} + /** \brief Create a logical context. @@ -1592,18 +1601,16 @@ void error_code_example1() void error_code_example2() { Z3_config cfg; Z3_context ctx = NULL; - int r; + Z3_error_code e; printf("\nerror_code_example2\n"); LOG_MSG("error_code_example2"); - /* low tech try&catch */ - r = setjmp(g_catch_buffer); - if (r == 0) { + if (1) { Z3_ast x, y, app; cfg = Z3_mk_config(); - ctx = mk_context_custom(cfg, throw_z3_error); + ctx = mk_context_custom(cfg, nothrow_z3_error); Z3_del_config(cfg); x = mk_int_var(ctx, "x"); @@ -1611,11 +1618,14 @@ void error_code_example2() { printf("before Z3_mk_iff\n"); /* the next call will produce an error */ app = Z3_mk_iff(ctx, x, y); + e = Z3_get_error_code(ctx); + if (e != Z3_OK) goto err; unreachable(); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); + err: + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { Z3_del_context(ctx); } @@ -1781,15 +1791,14 @@ void parser_example5() { Z3_config cfg; Z3_context ctx = NULL; Z3_solver s = NULL; - int r; + Z3_error_code e; printf("\nparser_example5\n"); LOG_MSG("parser_example5"); - r = setjmp(g_catch_buffer); - if (r == 0) { + if (1) { cfg = Z3_mk_config(); - ctx = mk_context_custom(cfg, throw_z3_error); + ctx = mk_context_custom(cfg, nothrow_z3_error); s = mk_solver(ctx); Z3_del_config(cfg); @@ -1798,12 +1807,15 @@ void parser_example5() { "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", 0, 0, 0, 0, 0, 0); + e = Z3_get_error_code(ctx); + if (e != Z3_OK) goto err; unreachable(); del_solver(ctx, s); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); + err: + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); del_solver(ctx, s); @@ -2639,6 +2651,7 @@ void smt2parser_example() { ctx = mk_context(); fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () (_ BitVec 8)) (assert (bvuge a #x10)) (assert (bvule a #xf0))", 0, 0, 0, 0, 0, 0); printf("formulas: %s\n", Z3_ast_to_string(ctx, fs)); + Z3_del_context(ctx); } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 7a68efbd8..71fa945d3 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -56,20 +56,20 @@ extern "C" { Z3_func_decl const decls[]) { Z3_TRY; LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - std::ostringstream outs; + std::ostringstream* outs = alloc(std::ostringstream); bool ok = false; RESET_ERROR_CODE(); init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(outs); + mk_c(c)->m_smtlib_parser->set_error_stream(*outs); try { ok = mk_c(c)->m_smtlib_parser->parse_string(str); } catch (...) { ok = false; } - mk_c(c)->m_smtlib_error_buffer = outs.str(); - outs.clear(); + mk_c(c)->m_smtlib_error_buffer = outs->str(); + dealloc(outs); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); @@ -89,17 +89,17 @@ extern "C" { LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls); bool ok = false; RESET_ERROR_CODE(); - std::ostringstream outs; + std::ostringstream* outs = alloc(std::ostringstream); init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(outs); + mk_c(c)->m_smtlib_parser->set_error_stream(*outs); try { ok = mk_c(c)->m_smtlib_parser->parse_file(file_name); } catch(...) { ok = false; } - mk_c(c)->m_smtlib_error_buffer = outs.str(); - outs.clear(); + mk_c(c)->m_smtlib_error_buffer = outs->str(); + dealloc(outs); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR);