restore most global muxes as heap-allocated to avoid crashes with hard-kills like ctrl-c

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 <module-name>.<parameter-name>=value\n";
+            out << "Example:  pp.decimal=true\n";
             out << "\n";
-            if (!smt2_style) {
-                out << "To set a module parameter, use <module-name>.<parameter-name>=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;
 }
 
 

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

src/util/mutex.h

@@ -25,6 +25,8 @@ struct lock_guard {
   lock_guard(mutex &) {}
 };
 
+#define DECLARE_MUTEX(name) mutex *name = nullptr
+
 #else
 #include <atomic>
 #include <mutex>
@@ -32,4 +34,6 @@ struct lock_guard {
 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
 #endif

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

src/util/rational.cpp

@@ -40,11 +40,11 @@ static void mk_power_up_to(vector<rational> & 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;
 }
 

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

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;

src/util/symbol.cpp

@@ -23,7 +23,7 @@ Revision History:
 #include "util/string_buffer.h"
 #include <cstring>
 
-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;
 }