mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix mutexes hanging due to access to free'd memory
Thanks to Kevin de Vos for reporting the bug & testing the fix
This commit is contained in:
parent
cb75326686
commit
87a96d7bd4
|
@ -575,11 +575,12 @@ void gparams::display_parameter(std::ostream & out, char const * name) {
|
|||
|
||||
void gparams::init() {
|
||||
TRACE("gparams", tout << "gparams::init()\n";);
|
||||
ALLOC_MUTEX(gparams_mux);
|
||||
g_imp = alloc(imp);
|
||||
}
|
||||
|
||||
void gparams::finalize() {
|
||||
TRACE("gparams", tout << "gparams::finalize()\n";);
|
||||
dealloc(g_imp);
|
||||
delete gparams_mux;
|
||||
DEALLOC_MUTEX(gparams_mux);
|
||||
}
|
||||
|
|
|
@ -35,7 +35,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
|
|||
}
|
||||
|
||||
|
||||
static DECLARE_MUTEX(g_memory_mux);
|
||||
static DECLARE_INIT_MUTEX(g_memory_mux);
|
||||
static atomic<bool> g_memory_out_of_memory(false);
|
||||
static bool g_memory_initialized = false;
|
||||
static long long g_memory_alloc_size = 0;
|
||||
|
@ -134,7 +134,9 @@ void memory::finalize() {
|
|||
if (g_memory_initialized) {
|
||||
g_finalizing = true;
|
||||
mem_finalize();
|
||||
delete g_memory_mux;
|
||||
// we leak the mutex since we need it to be always live since memory may
|
||||
// be reinitialized again
|
||||
//delete g_memory_mux;
|
||||
g_memory_initialized = false;
|
||||
g_finalizing = false;
|
||||
}
|
||||
|
|
|
@ -26,6 +26,9 @@ struct lock_guard {
|
|||
};
|
||||
|
||||
#define DECLARE_MUTEX(name) mutex *name = nullptr
|
||||
#define DECLARE_INIT_MUTEX(name) mutex *name = nullptr
|
||||
#define ALLOC_MUTEX(name) (void)
|
||||
#define DEALLOC_MUTEX(name) (void)
|
||||
|
||||
#else
|
||||
#include <atomic>
|
||||
|
@ -35,5 +38,9 @@ template<typename T> using atomic = std::atomic<T>;
|
|||
typedef std::mutex mutex;
|
||||
typedef std::lock_guard<std::mutex> lock_guard;
|
||||
|
||||
#define DECLARE_MUTEX(name) mutex *name = new mutex
|
||||
#define DECLARE_MUTEX(name) mutex *name = nullptr
|
||||
#define DECLARE_INIT_MUTEX(name) mutex *name = new mutex
|
||||
#define ALLOC_MUTEX(name) name = alloc(mutex)
|
||||
#define DEALLOC_MUTEX(name) dealloc(name)
|
||||
|
||||
#endif
|
||||
|
|
|
@ -129,10 +129,11 @@ uint64_t prime_iterator::next() {
|
|||
}
|
||||
|
||||
void prime_iterator::initialize() {
|
||||
ALLOC_MUTEX(g_prime_iterator);
|
||||
g_prime_generator.initialize();
|
||||
}
|
||||
|
||||
void prime_iterator::finalize() {
|
||||
g_prime_generator.finalize();
|
||||
delete g_prime_iterator;
|
||||
DEALLOC_MUTEX(g_prime_iterator);
|
||||
}
|
||||
|
|
|
@ -63,6 +63,7 @@ void finalize_inf_int_rational();
|
|||
|
||||
void rational::initialize() {
|
||||
if (!g_mpq_manager) {
|
||||
ALLOC_MUTEX(g_powers_of_two);
|
||||
g_mpq_manager = alloc(synch_mpq_manager);
|
||||
m().set(m_zero.m_val, 0);
|
||||
m().set(m_one.m_val, 1);
|
||||
|
@ -81,6 +82,6 @@ void rational::finalize() {
|
|||
m_minus_one.~rational();
|
||||
dealloc(g_mpq_manager);
|
||||
g_mpq_manager = nullptr;
|
||||
delete g_powers_of_two;
|
||||
DEALLOC_MUTEX(g_powers_of_two);
|
||||
}
|
||||
|
||||
|
|
|
@ -23,8 +23,12 @@ Revision History:
|
|||
|
||||
static DECLARE_MUTEX(g_rlimit_mux);
|
||||
|
||||
void initialize_rlimit() {
|
||||
ALLOC_MUTEX(g_rlimit_mux);
|
||||
}
|
||||
|
||||
void finalize_rlimit() {
|
||||
delete g_rlimit_mux;
|
||||
DEALLOC_MUTEX(g_rlimit_mux);
|
||||
}
|
||||
|
||||
reslimit::reslimit():
|
||||
|
|
|
@ -20,8 +20,10 @@ Revision History:
|
|||
|
||||
#include "util/vector.h"
|
||||
|
||||
void initialize_rlimit();
|
||||
void finalize_rlimit();
|
||||
/*
|
||||
ADD_INITIALIZER('initialize_rlimit();')
|
||||
ADD_FINALIZER('finalize_rlimit();')
|
||||
*/
|
||||
|
||||
|
|
|
@ -64,12 +64,13 @@ static internal_symbol_table* g_symbol_table = nullptr;
|
|||
|
||||
void initialize_symbols() {
|
||||
if (!g_symbol_table) {
|
||||
ALLOC_MUTEX(g_symbol_lock);
|
||||
g_symbol_table = alloc(internal_symbol_table);
|
||||
}
|
||||
}
|
||||
|
||||
void finalize_symbols() {
|
||||
delete g_symbol_lock;
|
||||
DEALLOC_MUTEX(g_symbol_lock);
|
||||
dealloc(g_symbol_table);
|
||||
g_symbol_table = nullptr;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue