fix crash on Mac due to different destruction order of globals

the mutex in memory_manager has to be destroyed after all mem deallocations happen

src/shell/lp_frontend.cpp

@@ -16,9 +16,8 @@ Author:
 #include "util/rlimit.h"
 #include "util/gparams.h"
 #include <signal.h>
-#include <mutex>
 
-extern std::mutex* g_stat_mux;
+static std::mutex display_stats_mux;
 
 static lp::lp_solver<double, double>* g_solver = nullptr;
 
@@ -31,14 +30,14 @@ static void display_statistics() {
 static void STD_CALL on_ctrl_c(int) {
     signal (SIGINT, SIG_DFL);
     {
-        std::lock_guard<std::mutex> lock(*g_stat_mux);
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
     }
     raise(SIGINT);
 }
 
 static void on_timeout() {
-    std::lock_guard<std::mutex> lock(*g_stat_mux);
+    std::lock_guard<std::mutex> lock(display_stats_mux);
     display_statistics();
     exit(0);    
 }

src/shell/main.cpp

@@ -18,7 +18,6 @@ Revision History:
 
 --*/
 #include<iostream>
-#include<mutex>
 #include "util/memory_manager.h"
 #include "util/trace.h"
 #include "util/debug.h"
@@ -51,7 +50,6 @@ static char const * g_input_file          = nullptr;
 static bool         g_standard_input      = false;
 static input_kind   g_input_kind          = IN_UNSPECIFIED;
 bool                g_display_statistics  = false;
-std::mutex*         g_stat_mux            = nullptr;
 static bool         g_display_istatistics = false;
 
 static void error(const char * msg) {
@@ -313,7 +311,6 @@ int STD_CALL main(int argc, char ** argv) {
         unsigned return_value = 0;
         memory::initialize(0);
         memory::exit_when_out_of_memory(true, "ERROR: out of memory");
-        g_stat_mux = alloc(std::mutex);
         parse_cmd_line_args(argc, argv);
         env_params::updt_params();
 
@@ -384,7 +381,6 @@ int STD_CALL main(int argc, char ** argv) {
         default:
             UNREACHABLE();
         }
-        dealloc(g_stat_mux);
         memory::finalize();
 #ifdef _WINDOWS
         _CrtDumpMemoryLeaks();

src/shell/opt_frontend.cpp

@@ -7,7 +7,6 @@ Copyright (c) 2015 Microsoft Corporation
 #include<fstream>
 #include<signal.h>
 #include<time.h>
-#include<mutex>
 #include "util/gparams.h"
 #include "util/timeout.h"
 #include "util/cancel_eh.h"
@@ -22,11 +21,11 @@ Copyright (c) 2015 Microsoft Corporation
 #include "opt/opt_parse.h"
 
 extern bool g_display_statistics;
-extern std::mutex* g_stat_mux;
 static bool g_first_interrupt = true;
 static opt::context* g_opt = nullptr;
 static double g_start_time = 0;
 static unsigned_vector g_handles;
+static std::mutex display_stats_mux;
 
 
 
@@ -71,7 +70,7 @@ static void STD_CALL on_ctrl_c(int) {
     else {
         signal (SIGINT, SIG_DFL);
         {
-            std::lock_guard<std::mutex> lock(*g_stat_mux);
+            std::lock_guard<std::mutex> lock(display_stats_mux);
             display_statistics();
         }
         raise(SIGINT);
@@ -80,7 +79,7 @@ static void STD_CALL on_ctrl_c(int) {
 
 static void on_timeout() {
     {
-        std::lock_guard<std::mutex> lock(*g_stat_mux);
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
     }
     exit(0);
@@ -134,7 +133,7 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
         std::cerr << ex.msg() << "\n";
     }
     {
-        std::lock_guard<std::mutex> lock(*g_stat_mux);
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
         register_on_timeout_proc(nullptr);
         g_opt = nullptr;

src/shell/smtlib_frontend.cpp

@@ -21,8 +21,6 @@ Revision History:
 #include<iostream>
 #include<time.h>
 #include<signal.h>
-#include<mutex>
-
 #include "util/timeout.h"
 #include "parsers/smt2/smt2parser.h"
 #include "muz/fp/dl_cmds.h"
@@ -34,7 +32,8 @@ Revision History:
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
 
-extern std::mutex* g_stat_mux;
+static std::mutex display_stats_mux;
+
 extern bool g_display_statistics;
 static clock_t             g_start_time;
 static cmd_context *       g_cmd_context = nullptr;
@@ -52,7 +51,7 @@ static void display_statistics() {
 }
 
 static void on_timeout() {
-    std::lock_guard<std::mutex> lock(*g_stat_mux);
+    std::lock_guard<std::mutex> lock(display_stats_mux);
     display_statistics();
     exit(0);    
 }
@@ -60,7 +59,7 @@ static void on_timeout() {
 static void STD_CALL on_ctrl_c(int) {
     signal (SIGINT, SIG_DFL);
     {
-        std::lock_guard<std::mutex> lock(*g_stat_mux);
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
     }
     raise(SIGINT);
@@ -100,7 +99,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
 
 
     {
-        std::lock_guard<std::mutex> lock(*g_stat_mux);
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
         g_cmd_context = nullptr;
     }

src/util/gparams.cpp

@@ -21,7 +21,7 @@ Notes:
 #include "util/trace.h"
 #include "util/mutex.h"
 
-static mutex* s_mux = nullptr;
+static mutex gparams_mux;
 
 extern void gparams_register_modules();
 
@@ -113,7 +113,7 @@ public:
     }
 
     void reset() {
-        lock_guard lock(*s_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(*s_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(*s_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(*s_mux);
+            lock_guard lock(gparams_mux);
             if (m_module_params.find(module_name, ps)) {
                 result.copy(*ps);
             }
@@ -448,7 +448,7 @@ public:
 
     void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
         {
-            lock_guard lock(*s_mux);
+            lock_guard lock(gparams_mux);
             out << "Global parameters\n";
             get_param_descrs().display(out, indent + 4, smt2_style, include_descr);
             out << "\n";
@@ -470,7 +470,7 @@ public:
     }
 
     void display_modules(std::ostream & out) {
-        lock_guard lock(*s_mux);
+        lock_guard lock(gparams_mux);
         for (auto & kv : get_module_param_descrs()) {
             out << "[module] " << kv.m_key;
             char const * descr = nullptr;
@@ -484,7 +484,7 @@ public:
     void display_module(std::ostream & out, symbol const & module_name) {
         bool error = false;
         std::string error_msg;
-        lock_guard lock(*s_mux);
+        lock_guard lock(gparams_mux);
         try {
             param_descrs * d = nullptr;
             if (!get_module_param_descrs().find(module_name, d)) {
@@ -513,7 +513,7 @@ public:
         bool error = false;
         std::string error_msg;
         {
-            lock_guard lock(*s_mux);
+            lock_guard lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);
@@ -631,16 +631,15 @@ void gparams::display_parameter(std::ostream & out, char const * name) {
 
 void gparams::init() {
     TRACE("gparams", tout << "gparams::init()\n";);
-    s_mux = alloc(mutex);
     g_imp = alloc(imp);
 }
 
 void gparams::finalize() {
     TRACE("gparams", tout << "gparams::finalize()\n";);
-    dealloc(g_imp);
+    if (g_imp != nullptr) {
-    g_imp = nullptr;    
+        dealloc(g_imp);
-    dealloc(s_mux);
+        g_imp = nullptr;
-    s_mux = nullptr;
+    }
 }
 
 

src/util/memory_manager.cpp

@@ -35,7 +35,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
 
 
-static mutex g_memory_mux;
+static 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;
@@ -46,7 +46,6 @@ static long long  g_memory_alloc_count       = 0;
 static long long  g_memory_max_alloc_count   = 0;
 static bool       g_exit_when_out_of_memory  = false;
 static char const * g_out_of_memory_msg      = "ERROR: out of memory";
-static volatile bool g_memory_fully_initialized = false;
 
 void memory::exit_when_out_of_memory(bool flag, char const * msg) {
     g_exit_when_out_of_memory = flag;
@@ -87,29 +86,22 @@ mem_usage_report g_info;
 #endif
 
 void memory::initialize(size_t max_size) {
-    bool initialize = false;
+    static mutex init_mux;
-    {
+    lock_guard lock(init_mux);
-        lock_guard lock(g_memory_mux);
+
-        // only update the maximum size if max_size != UINT_MAX
+    // only update the maximum size if max_size != UINT_MAX
-        if (max_size != UINT_MAX) 
+    if (max_size != UINT_MAX)
-            g_memory_max_size       = max_size;
+        g_memory_max_size = max_size;
-        if (!g_memory_initialized) {
+
-            g_memory_initialized = true;
+    if (g_memory_initialized)
-            initialize = true;
+        return;
-        }
+
-    }
+#ifndef SINGLE_THREAD
-    if (initialize) {
+    g_memory_mux = new mutex;
-        g_memory_out_of_memory = false;
+#endif
-        mem_initialize();
+    g_memory_out_of_memory = false;
-        g_memory_fully_initialized = true;
+    mem_initialize();
-    }
+    g_memory_initialized = true;
-    else {        
-        // Delay the current thread until the DLL is fully initialized
-        // Without this, multiple threads can start to call API functions
-        // before memory::initialize(...) finishes.
-        while (!g_memory_fully_initialized)
-            /* wait */ ;
-    }
 }
 
 bool memory::is_out_of_memory() {
@@ -124,7 +116,7 @@ void memory::set_high_watermark(size_t watermark) {
 bool memory::above_high_watermark() {
     if (g_memory_watermark == 0)
         return false;
-    lock_guard lock(g_memory_mux);
+    lock_guard lock(*g_memory_mux);
     return g_memory_watermark < g_memory_alloc_size;
 }
 
@@ -145,6 +137,9 @@ 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;
     }
@@ -153,7 +148,7 @@ void memory::finalize() {
 unsigned long long memory::get_allocation_size() {
     long long r;
     {
-        lock_guard lock(g_memory_mux);
+        lock_guard lock(*g_memory_mux);
         r = g_memory_alloc_size;
     }
     if (r < 0)
@@ -164,7 +159,7 @@ unsigned long long memory::get_allocation_size() {
 unsigned long long memory::get_max_used_memory() {
     unsigned long long r;
     {
-        lock_guard lock(g_memory_mux);
+        lock_guard lock(*g_memory_mux);
         r = g_memory_max_used_size;
     }
     return r;
@@ -248,7 +243,7 @@ static void synchronize_counters(bool allocating) {
     bool out_of_mem = false;
     bool counts_exceeded = false;
     {
-        lock_guard lock(g_memory_mux);
+        lock_guard lock(*g_memory_mux);
         g_memory_alloc_size += g_memory_thread_alloc_size;
         g_memory_alloc_count += g_memory_thread_alloc_count;
         if (g_memory_alloc_size > g_memory_max_used_size)
@@ -329,7 +324,7 @@ void memory::deallocate(void * p) {
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
     {
-        lock_guard lock(g_memory_mux);
+        lock_guard lock(*g_memory_mux);
         g_memory_alloc_size -= sz;
     }
     free(real_p);
@@ -339,7 +334,7 @@ void * memory::allocate(size_t s) {
     s = s + sizeof(size_t); // we allocate an extra field!
     bool out_of_mem = false, counts_exceeded = false;
     {
-        lock_guard lock(g_memory_mux);
+        lock_guard lock(*g_memory_mux);
         g_memory_alloc_size += s;
         g_memory_alloc_count += 1;
         if (g_memory_alloc_size > g_memory_max_used_size)
@@ -369,7 +364,7 @@ void* memory::reallocate(void *p, size_t s) {
     s = s + sizeof(size_t); // we allocate an extra field!
     bool out_of_mem = false, counts_exceeded = false;
     {
-        lock_guard lock(g_memory_mux);
+        lock_guard lock(*g_memory_mux);
         g_memory_alloc_size += s - sz;
         g_memory_alloc_count += 1;
         if (g_memory_alloc_size > g_memory_max_used_size)

src/util/prime_generator.cpp

@@ -17,21 +17,10 @@ Notes:
 
 --*/
 #include "util/prime_generator.h"
+#include "util/mutex.h"
 
 #define PRIME_LIST_MAX_SIZE 1<<20
 
-prime_generator::prime_generator() {
-    m_primes.push_back(2);
-    m_primes.push_back(3);
-    m_mux = alloc(mutex);
-    process_next_k_numbers(128);
-}
-
-prime_generator::~prime_generator() {
-    dealloc(m_mux);
-    m_mux = nullptr;
-}
-
 void prime_generator::process_next_k_numbers(uint64_t k) {
     svector<uint64_t> todo;
     uint64_t begin = m_primes.back() + 2;
@@ -85,10 +74,14 @@ void prime_generator::process_next_k_numbers(uint64_t k) {
     }
 }
 
+void prime_generator::initialize() {
+    m_primes.push_back(2);
+    m_primes.push_back(3);
+    process_next_k_numbers(128);
+}
+
 void prime_generator::finalize() {
     m_primes.finalize();
-    dealloc(m_mux);
-    m_mux = nullptr;
 }
 
 uint64_t prime_generator::operator()(unsigned idx) {
@@ -117,6 +110,8 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) {
     }
 }
 
+static mutex g_prime_iterator;
+
 uint64_t prime_iterator::next() {
     unsigned idx = m_idx;
     m_idx++;
@@ -125,7 +120,7 @@ uint64_t prime_iterator::next() {
     }
     else {
         uint64_t r;
-        lock_guard lock(*m_generator->m_mux);
+        lock_guard lock(g_prime_iterator);
         {
             r = (*m_generator)(idx);
         }
@@ -133,6 +128,10 @@ uint64_t prime_iterator::next() {
     }
 }
 
+void prime_iterator::initialize() {
+  g_prime_generator.initialize();
+}
+
 void prime_iterator::finalize() {
     g_prime_generator.finalize();
 }

src/util/prime_generator.h

@@ -22,7 +22,6 @@ Notes:
 #include "util/vector.h"
 #include "util/z3_exception.h"
 #include "util/util.h"
-#include "util/mutex.h"
 
 class prime_generator_exception : public default_exception {
 public:
@@ -36,10 +35,8 @@ class prime_generator {
     svector<uint64_t> m_primes;
     void process_next_k_numbers(uint64_t k);
 public:
-    mutex             *m_mux;
-    prime_generator();
-    ~prime_generator();
     uint64_t operator()(unsigned idx);
+    void initialize();
     void finalize();
 };
 
@@ -50,8 +47,10 @@ class prime_iterator {
 public:
     prime_iterator(prime_generator * g = nullptr);
     uint64_t next();
+    static void initialize();
     static void finalize();
     /*
+      ADD_INITIALIZER('prime_iterator::initialize();')
       ADD_FINALIZER('prime_iterator::finalize();')
     */
 };

src/util/rational.cpp

@@ -26,7 +26,6 @@ rational             rational::m_zero;
 rational             rational::m_one;
 rational             rational::m_minus_one;
 vector<rational>     rational::m_powers_of_two;
-static mutex*        s_mux = nullptr;
 
 static void mk_power_up_to(vector<rational> & pws, unsigned n) {
     if (pws.empty()) {
@@ -41,10 +40,11 @@ static void mk_power_up_to(vector<rational> & pws, unsigned n) {
     }
 }
 
+static mutex g_powers_of_two;
 
 rational rational::power_of_two(unsigned k) {
     rational result;
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_powers_of_two);
     {
         if (k >= m_powers_of_two.size())
             mk_power_up_to(m_powers_of_two, k+1);
@@ -64,7 +64,6 @@ void finalize_inf_int_rational();
 void rational::initialize() {
     if (!g_mpq_manager) {
         g_mpq_manager = alloc(synch_mpq_manager);
-        s_mux = alloc(mutex);
         m().set(m_zero.m_val, 0);
         m().set(m_one.m_val, 1);
         m().set(m_minus_one.m_val, -1);
@@ -82,7 +81,5 @@ void rational::finalize() {
     m_minus_one.~rational();
     dealloc(g_mpq_manager);
     g_mpq_manager = nullptr;
-    dealloc(s_mux);
-    s_mux = nullptr;
 }
 

src/util/rlimit.cpp

@@ -21,16 +21,7 @@ Revision History:
 #include "util/mutex.h"
 
 
-static mutex* s_mux = nullptr;
+static mutex g_rlimit_mux;
-
-void initialize_rlimit() {
-    s_mux = new mutex;
-}
-void finalize_rlimit() {
-    delete s_mux;
-    s_mux = nullptr;
-}
-
 
 reslimit::reslimit():
     m_cancel(0),
@@ -82,32 +73,32 @@ char const* reslimit::get_cancel_msg() const {
 }
 
 void reslimit::push_child(reslimit* r) {
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_rlimit_mux);
     m_children.push_back(r);    
 }
 
 void reslimit::pop_child() {
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_rlimit_mux);
     m_children.pop_back();    
 }
 
 void reslimit::cancel() {
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_rlimit_mux);
     set_cancel(m_cancel+1);    
 }
 
 void reslimit::reset_cancel() {
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_rlimit_mux);
     set_cancel(0);    
 }
 
 void reslimit::inc_cancel() {
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_rlimit_mux);
     set_cancel(m_cancel+1);    
 }
 
 void reslimit::dec_cancel() {
-    lock_guard lock(*s_mux);
+    lock_guard lock(g_rlimit_mux);
     if (m_cancel > 0) {
         set_cancel(m_cancel-1);
     }

src/util/rlimit.h

@@ -20,14 +20,6 @@ Revision History:
 
 #include "util/vector.h"
 
-
-void initialize_rlimit();
-void finalize_rlimit();
-/*
-  ADD_INITIALIZER('initialize_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* s_mux = nullptr;
+static 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(*s_mux);
+        lock_guard lock(g_symbol_lock);
         str_hashtable::entry * e;
         if (m_table.insert_if_not_there_core(d, e)) {
             // new entry
@@ -66,16 +66,11 @@ void initialize_symbols() {
     if (!g_symbol_table) {
         g_symbol_table = alloc(internal_symbol_table);
     }
-    if (!s_mux) {
-        s_mux = alloc(mutex);
-    }
 }
 
 void finalize_symbols() {
     dealloc(g_symbol_table);
-    dealloc(s_mux);
     g_symbol_table = nullptr;
-    s_mux = nullptr;
 }
 
 symbol::symbol(char const * d) {