From 79cfb32ec7e44c38a08fcf1e66e0be6274e75f74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Sep 2014 08:00:21 -0700 Subject: [PATCH] refactor(util): explicit initialization/finalization --- src/tests/util/name.cpp | 4 +++ src/util/CMakeLists.txt | 9 +----- src/util/ascii.cpp | 37 +++++++++++------------ src/util/ascii.h | 3 ++ src/util/debug.cpp | 17 ++++++++--- src/util/debug.h | 2 ++ src/util/init_module.cpp | 15 ++++++++++ src/util/lean_path.cpp | 64 ++++++++++++++++++++++++---------------- src/util/lean_path.h | 3 ++ src/util/thread.cpp | 24 ++++++++------- src/util/thread.h | 5 ++++ src/util/trace.cpp | 13 ++++++-- src/util/trace.h | 2 ++ 13 files changed, 127 insertions(+), 71 deletions(-) diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp index e9c75f465..7391dd980 100644 --- a/src/tests/util/name.cpp +++ b/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; } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 4d2a10ede..23c037e77 100644 --- a/src/util/CMakeLists.txt +++ b/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}) diff --git a/src/util/ascii.cpp b/src/util/ascii.cpp index 93b6ff9d2..5d4615884 100644 --- a/src/util/ascii.cpp +++ b/src/util/ascii.cpp @@ -7,27 +7,24 @@ Author: Leonardo de Moura #include 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(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(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(c)]; diff --git a/src/util/ascii.h b/src/util/ascii.h index 33f9c0c31..33275fd6f 100644 --- a/src/util/ascii.h +++ b/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(); } diff --git a/src/util/debug.cpp b/src/util/debug.cpp index f9428ab38..29afce9c3 100644 --- a/src/util/debug.cpp +++ b/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> g_enabled_debug_tags; +static volatile bool g_has_violations = false; +static volatile bool g_enable_assertions = true; +static std::set * 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()); + g_enabled_debug_tags = new std::set(); g_enabled_debug_tags->insert(tag); } diff --git a/src/util/debug.h b/src/util/debug.h index 70a6dc1e7..873f48c65 100644 --- a/src/util/debug.h +++ b/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); diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp index 2482200c3..47c16913f 100644 --- a/src/util/init_module.cpp +++ b/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(); } } diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 7ee2a272e..be55a381c 100644 --- a/src/util/lean_path.cpp +++ b/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 g_lean_path_vector; +static std::string * g_lean_path = nullptr; +static std::vector * 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(); + 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 check_file_core(std::string file, char const * ext) { optional 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 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 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 con std::string find_file(std::string const & base, optional const & rel, name const & fname, std::initializer_list 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 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 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) { diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 077477002..16711e735 100644 --- a/src/util/lean_path.h +++ b/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(); } diff --git a/src/util/thread.cpp b/src/util/thread.cpp index 7dcdde659..d4ca58ded 100644 --- a/src/util/thread.cpp +++ b/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 } - diff --git a/src/util/thread.h b/src/util/thread.h index 8a7046d65..d1067292c 100644 --- a/src/util/thread.h +++ b/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(); +} diff --git a/src/util/trace.cpp b/src/util/trace.cpp index 9796e8d55..d37bb357d 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -21,11 +21,20 @@ std::ofstream tout(LEAN_TRACE_OUT); mutex trace_mutex; #endif -static std::unique_ptr> g_enabled_trace_tags; +static std::set * 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()); + g_enabled_trace_tags = new std::set(); g_enabled_trace_tags->insert(tag); } diff --git a/src/util/trace.h b/src/util/trace.h index dee441f96..11a942563 100644 --- a/src/util/trace.h +++ b/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(); }