From c21f0c2f0097aa632c015d762fc3320bf67358b1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 13 Jun 2019 18:42:57 +0100 Subject: [PATCH] restore most global muxes as heap-allocated to avoid crashes with hard-kills like ctrl-c --- src/util/gparams.cpp | 54 +++++++++++++++++------------------- src/util/memory_manager.cpp | 8 +----- src/util/mutex.h | 4 +++ src/util/prime_generator.cpp | 5 ++-- src/util/rational.cpp | 5 ++-- src/util/rlimit.cpp | 18 +++++++----- src/util/rlimit.h | 5 ++++ src/util/symbol.cpp | 5 ++-- 8 files changed, 55 insertions(+), 49 deletions(-) diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 0983189da..eebd751ba 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -21,7 +21,7 @@ Notes: #include "util/trace.h" #include "util/mutex.h" -static mutex gparams_mux; +static DECLARE_MUTEX(gparams_mux); extern void gparams_register_modules(); @@ -113,7 +113,7 @@ public: } void reset() { - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); m_params.reset(); for (auto & kv : m_module_params) { dealloc(kv.m_value); @@ -329,7 +329,7 @@ public: bool error = false; std::string error_msg; { - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -381,7 +381,7 @@ public: bool error = false; std::string error_msg; { - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -428,7 +428,7 @@ public: params_ref result; params_ref * ps = nullptr; { - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); if (m_module_params.find(module_name, ps)) { result.copy(*ps); } @@ -447,30 +447,28 @@ public: // ----------------------------------------------- void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { - { - lock_guard lock(gparams_mux); - out << "Global parameters\n"; - get_param_descrs().display(out, indent + 4, smt2_style, include_descr); + lock_guard lock(*gparams_mux); + out << "Global parameters\n"; + get_param_descrs().display(out, indent + 4, smt2_style, include_descr); + out << "\n"; + if (!smt2_style) { + out << "To set a module parameter, use .=value\n"; + out << "Example: pp.decimal=true\n"; out << "\n"; - if (!smt2_style) { - out << "To set a module parameter, use .=value\n"; - out << "Example: pp.decimal=true\n"; - out << "\n"; - } - for (auto & kv : get_module_param_descrs()) { - out << "[module] " << kv.m_key; - char const * descr = nullptr; - if (get_module_descrs().find(kv.m_key, descr)) { - out << ", description: " << descr; - } - out << "\n"; - kv.m_value->display(out, indent + 4, smt2_style, include_descr); + } + for (auto & kv : get_module_param_descrs()) { + out << "[module] " << kv.m_key; + char const * descr = nullptr; + if (get_module_descrs().find(kv.m_key, descr)) { + out << ", description: " << descr; } + out << "\n"; + kv.m_value->display(out, indent + 4, smt2_style, include_descr); } } void display_modules(std::ostream & out) { - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); for (auto & kv : get_module_param_descrs()) { out << "[module] " << kv.m_key; char const * descr = nullptr; @@ -484,7 +482,7 @@ public: void display_module(std::ostream & out, symbol const & module_name) { bool error = false; std::string error_msg; - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); try { param_descrs * d = nullptr; if (!get_module_param_descrs().find(module_name, d)) { @@ -513,7 +511,7 @@ public: bool error = false; std::string error_msg; { - lock_guard lock(gparams_mux); + lock_guard lock(*gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -636,10 +634,8 @@ void gparams::init() { void gparams::finalize() { TRACE("gparams", tout << "gparams::finalize()\n";); - if (g_imp != nullptr) { - dealloc(g_imp); - g_imp = nullptr; - } + dealloc(g_imp); + delete gparams_mux; } diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 0396439e4..96067fc61 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -35,11 +35,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) { } -#ifndef SINGLE_THREAD -static mutex *g_memory_mux = new mutex; -#else -static mutex *g_memory_mux = nullptr; -#endif +static DECLARE_MUTEX(g_memory_mux); static atomic g_memory_out_of_memory(false); static bool g_memory_initialized = false; static long long g_memory_alloc_size = 0; @@ -138,9 +134,7 @@ void memory::finalize() { if (g_memory_initialized) { g_finalizing = true; mem_finalize(); -#ifndef SINGLE_THREAD delete g_memory_mux; -#endif g_memory_initialized = false; g_finalizing = false; } diff --git a/src/util/mutex.h b/src/util/mutex.h index 36d06f9a2..008284d7d 100644 --- a/src/util/mutex.h +++ b/src/util/mutex.h @@ -25,6 +25,8 @@ struct lock_guard { lock_guard(mutex &) {} }; +#define DECLARE_MUTEX(name) mutex *name = nullptr + #else #include #include @@ -32,4 +34,6 @@ struct lock_guard { template using atomic = std::atomic; typedef std::mutex mutex; typedef std::lock_guard lock_guard; + +#define DECLARE_MUTEX(name) mutex *name = new mutex #endif diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 21f84e71c..3506280f9 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -110,7 +110,7 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { } } -static mutex g_prime_iterator; +static DECLARE_MUTEX(g_prime_iterator); uint64_t prime_iterator::next() { unsigned idx = m_idx; @@ -120,7 +120,7 @@ uint64_t prime_iterator::next() { } else { uint64_t r; - lock_guard lock(g_prime_iterator); + lock_guard lock(*g_prime_iterator); { r = (*m_generator)(idx); } @@ -134,4 +134,5 @@ void prime_iterator::initialize() { void prime_iterator::finalize() { g_prime_generator.finalize(); + delete g_prime_iterator; } diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 5e5ebe9e0..ccad41fbd 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -40,11 +40,11 @@ static void mk_power_up_to(vector & pws, unsigned n) { } } -static mutex g_powers_of_two; +static DECLARE_MUTEX(g_powers_of_two); rational rational::power_of_two(unsigned k) { rational result; - lock_guard lock(g_powers_of_two); + lock_guard lock(*g_powers_of_two); { if (k >= m_powers_of_two.size()) mk_power_up_to(m_powers_of_two, k+1); @@ -81,5 +81,6 @@ void rational::finalize() { m_minus_one.~rational(); dealloc(g_mpq_manager); g_mpq_manager = nullptr; + delete g_powers_of_two; } diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index ac596a118..de3266480 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -21,7 +21,11 @@ Revision History: #include "util/mutex.h" -static mutex g_rlimit_mux; +static DECLARE_MUTEX(g_rlimit_mux); + +void finalize_rlimit() { + delete g_rlimit_mux; +} reslimit::reslimit(): m_cancel(0), @@ -73,32 +77,32 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*g_rlimit_mux); m_children.push_back(r); } void reslimit::pop_child() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*g_rlimit_mux); m_children.pop_back(); } void reslimit::cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*g_rlimit_mux); set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*g_rlimit_mux); set_cancel(0); } void reslimit::inc_cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*g_rlimit_mux); set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - lock_guard lock(g_rlimit_mux); + lock_guard lock(*g_rlimit_mux); if (m_cancel > 0) { set_cancel(m_cancel-1); } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index c118a1093..455bdc740 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -20,6 +20,11 @@ Revision History: #include "util/vector.h" +void finalize_rlimit(); +/* + ADD_FINALIZER('finalize_rlimit();') +*/ + class reslimit { volatile unsigned m_cancel; bool m_suspend; diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 36ea344fa..4d889fca2 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -23,7 +23,7 @@ Revision History: #include "util/string_buffer.h" #include -static mutex g_symbol_lock; +static DECLARE_MUTEX(g_symbol_lock); symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -38,7 +38,7 @@ public: char const * get_str(char const * d) { const char * result; - lock_guard lock(g_symbol_lock); + lock_guard lock(*g_symbol_lock); str_hashtable::entry * e; if (m_table.insert_if_not_there_core(d, e)) { // new entry @@ -69,6 +69,7 @@ void initialize_symbols() { } void finalize_symbols() { + delete g_symbol_lock; dealloc(g_symbol_table); g_symbol_table = nullptr; }