refactor(util): explicit initialization/finalization

src/tests/util/name.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "util/name_generator.h"
 #include "util/name_set.h"
+#include "util/init_module.h"
 using namespace lean;
 
 static void tst1() {
@@ -172,6 +173,8 @@ static void tst13() {
 }
 
 int main() {
+    save_stack_info();
+    initialize_util_module();
     tst1();
     tst2();
     tst3();
@@ -185,5 +188,6 @@ int main() {
     tst11();
     tst12();
     tst13();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }

src/util/CMakeLists.txt

@@ -1,16 +1,9 @@
-if (("${BOOST}" MATCHES "ON") AND ("${MULTI_THREAD}" MATCHES "ON"))
-  set(THREAD_CPP "thread.cpp")
-else()
-  set(THREAD_CPP "")
-endif()
-
 add_library(util trace.cpp debug.cpp name.cpp name_set.cpp
   name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp
   bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp
   realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp
   lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp
   serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp
-  init_module.cpp
-  ${THREAD_CPP})
+  init_module.cpp thread.cpp)
 
 target_link_libraries(util ${LEAN_LIBS})

src/util/ascii.cpp

@@ -7,27 +7,24 @@ Author: Leonardo de Moura
 #include <initializer_list>
 namespace lean {
 static char g_safe_ascii[256];
-/**
-   \brief Initializer for the \c g_safe_ascii table of "safe" ASCII characters.
-*/
-class init_safe_ascii {
-    void set(int i, bool v) { g_safe_ascii[static_cast<unsigned char>(i)] = v; }
-public:
-    init_safe_ascii() {
-        for (int i = 0; i <= 255; i++)
-            set(i, false);
-        // digits and characters are safe
-        for (int i = '0'; i <= '9'; i++) set(i, true);
-        for (int i = 'a'; i <= 'z'; i++) set(i, true);
-        for (int i = 'A'; i <= 'Z'; i++) set(i, true);
-        // the following characters are also safe
-        for (unsigned char b : {'_', ' ', '\t', '\r', '\n', '(', ')', '{', '}', ':', '.', ',', '\"', '\'', '`', '!', '#',
-                    '=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']'})
-            set(b, true);
-    }
-};
 
-static init_safe_ascii g_init_safe_ascii;
+static void set(int i, bool v) { g_safe_ascii[static_cast<unsigned char>(i)] = v; }
+
+void initialize_ascii() {
+    for (int i = 0; i <= 255; i++)
+        set(i, false);
+    // digits and characters are safe
+    for (int i = '0'; i <= '9'; i++) set(i, true);
+    for (int i = 'a'; i <= 'z'; i++) set(i, true);
+    for (int i = 'A'; i <= 'Z'; i++) set(i, true);
+    // the following characters are also safe
+    for (unsigned char b : {'_', ' ', '\t', '\r', '\n', '(', ')', '{', '}', ':', '.', ',', '\"', '\'', '`', '!', '#',
+                '=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']'})
+        set(b, true);
+}
+
+void finalize_ascii() {
+}
 
 bool is_safe_ascii(char c) {
     return g_safe_ascii[static_cast<unsigned char>(c)];

src/util/ascii.h

@@ -16,4 +16,7 @@ bool is_safe_ascii(char c);
     ASCII character.
 */
 bool is_safe_ascii(char const * str);
+
+void initialize_ascii();
+void finalize_ascii();
 }

src/util/debug.cpp

@@ -17,9 +17,18 @@ Author: Leonardo de Moura
 #include "util/debug.h"
 
 namespace lean {
-static volatile bool                          g_has_violations    = false;
-static volatile bool                          g_enable_assertions = true;
-static std::unique_ptr<std::set<std::string>> g_enabled_debug_tags;
+static volatile bool           g_has_violations     = false;
+static volatile bool           g_enable_assertions  = true;
+static std::set<std::string> * g_enabled_debug_tags = nullptr;
+
+void initialize_debug() {
+    // lazy initialization
+}
+
+void finalize_debug() {
+    if (g_enabled_debug_tags)
+        delete g_enabled_debug_tags;
+}
 
 bool has_violations() {
     return g_has_violations;
@@ -43,7 +52,7 @@ void notify_assertion_violation(const char * fileName, int line, const char * co
 
 void enable_debug(char const * tag) {
     if (!g_enabled_debug_tags)
-        g_enabled_debug_tags.reset(new std::set<std::string>());
+        g_enabled_debug_tags = new std::set<std::string>();
     g_enabled_debug_tags->insert(tag);
 }
 

src/util/debug.h

@@ -93,6 +93,8 @@ Author: Leonardo de Moura
 #define lean_assert_le(A, B) lean_assert(A <= B, A, B)
 
 namespace lean {
+void initialize_debug();
+void finalize_debug();
 void notify_assertion_violation(char const * file_name, int line, char const * condition);
 void enable_debug(char const * tag);
 void disable_debug(char const * tag);

src/util/init_module.cpp

@@ -4,16 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/ascii.h"
+#include "util/debug.h"
+#include "util/trace.h"
 #include "util/serializer.h"
 #include "util/name.h"
+#include "util/lean_path.h"
+#include "util/thread.h"
 
 namespace lean {
 void initialize_util_module() {
+    initialize_debug();
+    initialize_trace();
+    initialize_thread();
+    initialize_ascii();
+    initialize_lean_path();
     initialize_serializer();
     initialize_name();
 }
 void finalize_util_module() {
     finalize_name();
     finalize_serializer();
+    finalize_lean_path();
+    finalize_ascii();
+    finalize_thread();
+    finalize_trace();
+    finalize_debug();
 }
 }

src/util/lean_path.cpp

@@ -29,7 +29,7 @@ file_not_found_exception::file_not_found_exception(std::string const & fname):
     exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"),
     m_fname(fname) {}
 
-static std::string g_default_file_name(LEAN_DEFAULT_MODULE_FILE_NAME);
+static std::string * g_default_file_name = nullptr;
 
 bool is_directory(char const * pathname) {
     struct stat info;
@@ -115,39 +115,51 @@ std::string get_path(std::string f) {
     }
 }
 
-static std::string              g_lean_path;
-static std::vector<std::string> g_lean_path_vector;
+static std::string *              g_lean_path = nullptr;
+static std::vector<std::string> * g_lean_path_vector = nullptr;
+
 void init_lean_path() {
     char * r = getenv("LEAN_PATH");
     if (r == nullptr) {
-        g_lean_path  = ".";
+        *g_lean_path  = ".";
         std::string exe_path = get_path(get_exe_location());
-        g_lean_path += g_path_sep;
-        g_lean_path += exe_path + g_sep + ".." + g_sep + "library";
+        *g_lean_path += g_path_sep;
+        *g_lean_path += exe_path + g_sep + ".." + g_sep + "library";
     } else {
-        g_lean_path = r;
+        *g_lean_path = r;
     }
-    g_lean_path_vector.clear();
-    g_lean_path = normalize_path(g_lean_path);
+    g_lean_path_vector->clear();
+    *g_lean_path = normalize_path(*g_lean_path);
     unsigned i  = 0;
     unsigned j  = 0;
-    unsigned sz = g_lean_path.size();
+    unsigned sz = g_lean_path->size();
     for (; j < sz; j++) {
-        if (is_path_sep(g_lean_path[j])) {
+        if (is_path_sep((*g_lean_path)[j])) {
             if (j > i)
-                g_lean_path_vector.push_back(g_lean_path.substr(i, j - i));
+                g_lean_path_vector->push_back(g_lean_path->substr(i, j - i));
             i = j + 1;
         }
     }
     if (j > i)
-        g_lean_path_vector.push_back(g_lean_path.substr(i, j - i));
+        g_lean_path_vector->push_back(g_lean_path->substr(i, j - i));
 }
 
-struct init_lean_path_fn {
-    init_lean_path_fn() { init_lean_path(); }
-};
-static init_lean_path_fn g_init_lean_path_fn;
-static std::string       g_sep_str(1, g_sep);
+static char g_sep_str[2];
+
+void initialize_lean_path() {
+    g_default_file_name = new std::string(LEAN_DEFAULT_MODULE_FILE_NAME);
+    g_lean_path         = new std::string();
+    g_lean_path_vector  = new std::vector<std::string>();
+    g_sep_str[0]        = g_sep;
+    g_sep_str[1]        = 0;
+    init_lean_path();
+}
+
+void finalize_lean_path() {
+    delete g_lean_path_vector;
+    delete g_lean_path;
+    delete g_default_file_name;
+}
 
 bool has_file_ext(std::string const & fname, char const * ext) {
     unsigned ext_len = strlen(ext);
@@ -183,7 +195,7 @@ optional<std::string> check_file_core(std::string file, char const * ext) {
 optional<std::string> check_file(std::string const & path, std::string const & fname, char const * ext = nullptr) {
     std::string file = path + g_sep + fname;
     if (is_directory(file.c_str())) {
-        std::string default_file = file + g_sep + g_default_file_name;
+        std::string default_file = file + g_sep + *g_default_file_name;
         if (auto r1 = check_file_core(default_file, ext)) {
             if (auto r2 = check_file_core(file, ext))
                 throw exception(sstream() << "ambiguous import, it can be '" << *r1 << "' or '" << *r2 << "'");
@@ -194,13 +206,13 @@ optional<std::string> check_file(std::string const & path, std::string const & f
 }
 
 std::string name_to_file(name const & fname) {
-    return fname.to_string(g_sep_str.c_str());
+    return fname.to_string(g_sep_str);
 }
 
 std::string find_file(std::string fname, std::initializer_list<char const *> const & extensions) {
     bool is_known = is_known_file_ext(fname);
     fname = normalize_path(fname);
-    for (auto path : g_lean_path_vector) {
+    for (auto path : *g_lean_path_vector) {
         if (is_known) {
             if (auto r = check_file(path, fname))
                 return *r;
@@ -217,7 +229,7 @@ std::string find_file(std::string fname, std::initializer_list<char const *> con
 std::string find_file(std::string const & base, optional<unsigned> const & rel, name const & fname,
                       std::initializer_list<char const *> const & extensions) {
     if (!rel) {
-        return find_file(fname.to_string(g_sep_str.c_str()), extensions);
+        return find_file(fname.to_string(g_sep_str), extensions);
     } else {
         auto path = base;
         for (unsigned i = 0; i < *rel; i++) {
@@ -225,7 +237,7 @@ std::string find_file(std::string const & base, optional<unsigned> const & rel,
             path += "..";
         }
         for (auto ext : extensions) {
-            if (auto r = check_file(path, fname.to_string(g_sep_str.c_str()), ext))
+            if (auto r = check_file(path, fname.to_string(g_sep_str), ext))
                 return *r;
         }
         throw file_not_found_exception(fname.to_string());
@@ -241,15 +253,15 @@ std::string find_file(std::string fname) {
 }
 
 std::string find_file(name const & fname) {
-    return find_file(fname.to_string(g_sep_str.c_str()));
+    return find_file(fname.to_string(g_sep_str));
 }
 
 std::string find_file(name const & fname, std::initializer_list<char const *> const & exts) {
-    return find_file(fname.to_string(g_sep_str.c_str()), exts);
+    return find_file(fname.to_string(g_sep_str), exts);
 }
 
 char const * get_lean_path() {
-    return g_lean_path.c_str();
+    return g_lean_path->c_str();
 }
 
 void display_path(std::ostream & out, std::string const & fname) {

src/util/lean_path.h

@@ -54,4 +54,7 @@ void display_path(std::ostream & out, std::string const & fname);
 
 std::string dirname(char const * fname);
 std::string path_append(char const * path1, char const * path2);
+
+void initialize_lean_path();
+void finalize_lean_path();
 }

src/util/thread.cpp

@@ -8,20 +8,22 @@ Author: Leonardo de Moura
 
 namespace lean {
 #if defined(LEAN_USE_BOOST)
-static boost::thread::attributes g_thread_attributes;
-class init_thread_attributes {
-public:
-    init_thread_attributes() {
-        g_thread_attributes.set_stack_size(8192*1024); // 8Mb
-    }
-};
-static init_thread_attributes g_init_thread_attributes;
+static boost::thread::attributes * g_thread_attributes = nullptr;
+void initialize_thread() {
+    g_thread_attributes = new boost::thread::attributes();
+    g_thread_attributes->set_stack_size(8192*1024); // 8Mb
+}
+void finalize_thread() {
+    delete g_thread_attributes;
+}
 void set_thread_stack_size(size_t sz) {
-    g_thread_attributes.set_stack_size(sz);
+    g_thread_attributes->set_stack_size(sz);
 }
 boost::thread::attributes const & get_thread_attributes() {
-    return g_thread_attributes;
+    return *g_thread_attributes;
 }
+#else
+void initialize_thread() {}
+void finalize_thread() {}
 #endif
 }
-

src/util/thread.h

@@ -203,3 +203,8 @@ static T & GETTER_NAME() {                              \
 #define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) static T & GETTER_NAME() { static T LEAN_THREAD_LOCAL r(DEF_VALUE); return r; }
 #define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) static T & GETTER_NAME() { static T LEAN_THREAD_LOCAL r; return r; }
 #endif
+
+namespace lean {
+void initialize_thread();
+void finalize_thread();
+}

src/util/trace.cpp

@@ -21,11 +21,20 @@ std::ofstream tout(LEAN_TRACE_OUT);
 mutex         trace_mutex;
 #endif
 
-static std::unique_ptr<std::set<std::string>> g_enabled_trace_tags;
+static std::set<std::string> * g_enabled_trace_tags = nullptr;
+
+void initialize_trace() {
+    // lazy initialization
+}
+
+void finalize_trace() {
+    if (g_enabled_trace_tags)
+        delete g_enabled_trace_tags;
+}
 
 void enable_trace(char const * tag) {
     if (!g_enabled_trace_tags)
-        g_enabled_trace_tags.reset(new std::set<std::string>());
+        g_enabled_trace_tags = new std::set<std::string>();
     g_enabled_trace_tags->insert(tag);
 }
 

src/util/trace.h

@@ -28,4 +28,6 @@ namespace lean {
 void enable_trace(char const * tag);
 void disable_trace(char const * tag);
 bool is_trace_enabled(char const * tag);
+void initialize_trace();
+void finalize_trace();
 }