fix mutexes hanging due to access to free'd memory

Thanks to Kevin de Vos for reporting the bug & testing the fix

src/util/gparams.cpp

@@ -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);
 }

src/util/memory_manager.cpp

@@ -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;
     }

src/util/mutex.h

@@ -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

src/util/prime_generator.cpp

@@ -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);
 }

src/util/rational.cpp

@@ -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);
 }
 

src/util/rlimit.cpp

@@ -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():

src/util/rlimit.h

@@ -20,8 +20,10 @@ Revision History:
 
 #include "util/vector.h"
 
+void initialize_rlimit();
 void finalize_rlimit();
 /*
+  ADD_INITIALIZER('initialize_rlimit();')
   ADD_FINALIZER('finalize_rlimit();')
 */
 

src/util/symbol.cpp

@@ -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;
 }