diff --git a/scripts/update_api.py b/scripts/update_api.py index 27766b451..6392e439e 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1719,14 +1719,12 @@ def write_log_h_preamble(log_h): log_h.write('#define _Z3_UNUSED\n') log_h.write('#endif\n') # - log_h.write('#include\n') - log_h.write('#include\n') - log_h.write('extern std::ostream * g_z3_log;\n') - log_h.write('extern std::atomic g_z3_log_enabled;\n') - log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { m_prev = g_z3_log && g_z3_log_enabled.exchange(false); } ~z3_log_ctx() { if (g_z3_log) g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n') - log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n') + log_h.write('#include "util/mutex.h"\n') + log_h.write('extern atomic g_z3_log_enabled;\n') + log_h.write('void ctx_enable_logging();\n') + log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n') + log_h.write('void SetR(void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n') log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n') - log_h.write('void _Z3_append_log(char const * msg);\n') def write_log_c_preamble(log_c): diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index e6a6437d7..0f2473956 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -270,10 +270,8 @@ namespace api { void context::invoke_error_handler(Z3_error_code c) { if (m_error_handler) { - if (g_z3_log) { - // error handler can do crazy stuff such as longjmp - g_z3_log_enabled = true; - } + // error handler can do crazy stuff such as longjmp + ctx_enable_logging(); m_error_handler(reinterpret_cast(this), c); } } diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 55c8cb853..c1864ae8c 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -18,12 +18,13 @@ Revision History: #include #include "api/z3.h" #include "api/api_log_macros.h" +#include "api/z3_logger.h" #include "util/util.h" #include "util/z3_version.h" #include "util/mutex.h" -std::ostream * g_z3_log = nullptr; -std::atomic g_z3_log_enabled; +static std::ostream * g_z3_log = nullptr; +atomic g_z3_log_enabled; #ifdef Z3_LOG_SYNC static mutex g_log_mux; @@ -32,6 +33,78 @@ static mutex g_log_mux; #define SCOPED_LOCK() {} #endif +// functions called from api_log_macros.* +void SetR(void * obj) { + *g_z3_log << "= " << obj << '\n'; +} + +void SetO(void * obj, unsigned pos) { + *g_z3_log << "* " << obj << ' ' << pos << '\n'; +} + +void SetAO(void * obj, unsigned pos, unsigned idx) { + *g_z3_log << "@ " << obj << ' ' << pos << ' ' << idx << '\n'; +} + +namespace { +struct ll_escaped { char const * m_str; }; +std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { + char const * s = d.m_str; + while (*s) { + unsigned char c = *s; + if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') || + c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' || + c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' || + c == '<' || c == '>') { + out << c; + } + else { + unsigned char str[4] = {'0', '0', '0', 0}; + str[2] = '0' + (c % 10); + c /= 10; + str[1] = '0' + (c % 10); + c /= 10; + str[0] = '0' + c; + out << '\\' << str; + } + s++; + } + return out; +} +} + +void R() { *g_z3_log << 'R' << std::endl; } +void P(void * obj) { *g_z3_log << "P " << obj <bad() || g_z3_log->fail()) { dealloc(g_z3_log); @@ -54,16 +127,16 @@ extern "C" { res = false; } else { - *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n"; - g_z3_log->flush(); - g_z3_log_enabled = true; + *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << '"' << std::endl; + res = true; } + g_z3_log_enabled = res; return res; } void Z3_API Z3_append_log(Z3_string str) { - if (g_z3_log == nullptr) + if (!g_z3_log_enabled) return; SCOPED_LOCK(); if (g_z3_log != nullptr) @@ -71,9 +144,7 @@ extern "C" { } void Z3_API Z3_close_log(void) { - if (g_z3_log != nullptr) { - SCOPED_LOCK(); - Z3_close_log_unsafe(); - } + SCOPED_LOCK(); + Z3_close_log_unsafe(); } } diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 264644c45..646209575 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -16,57 +16,17 @@ Author: Notes: --*/ -#include #include "util/symbol.h" -struct ll_escaped { char const * m_str; ll_escaped(char const * str):m_str(str) {} }; -static std::ostream & operator<<(std::ostream & out, ll_escaped const & d); -static void __declspec(noinline) R() { *g_z3_log << "R\n"; g_z3_log->flush(); } -static void __declspec(noinline) P(void * obj) { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) I(int64_t i) { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) U(uint64_t u) { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) D(double d) { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); } -static void __declspec(noinline) Sy(Z3_symbol sym) { - symbol s = symbol::c_api_ext2symbol(sym); - if (s.is_null()) { - *g_z3_log << "N\n"; - } - else if (s.is_numerical()) { - *g_z3_log << "# " << s.get_num() << "\n"; - } - else { - *g_z3_log << "$ |" << ll_escaped(s.bare_str()) << "|\n"; - } - g_z3_log->flush(); -} -static void __declspec(noinline) Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) Ai(unsigned sz) { *g_z3_log << "i " << sz << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) C(unsigned id) { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); } -void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped(msg) << "\"\n"; g_z3_log->flush(); } - -static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { - char const * s = d.m_str; - while (*s) { - unsigned char c = *s; - if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') || - c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' || - c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' || - c == '<' || c == '>') { - out << c; - } - else { - unsigned char str[4] = {'0', '0', '0', 0}; - str[2] = '0' + (c % 10); - c /= 10; - str[1] = '0' + (c % 10); - c /= 10; - str[0] = '0' + c; - out << '\\' << str; - } - s++; - } - return out; -} +void R(); +void P(void * obj); +void I(int64_t i); +void U(uint64_t u); +void D(double d); +void S(Z3_string str); +void Sy(Z3_symbol sym); +void Ap(unsigned sz); +void Au(unsigned sz); +void Ai(unsigned sz); +void Asy(unsigned sz); +void C(unsigned id); diff --git a/src/util/mutex.h b/src/util/mutex.h index a5fd817c1..d49510131 100644 --- a/src/util/mutex.h +++ b/src/util/mutex.h @@ -16,6 +16,8 @@ Abstract: template using atomic = T; +#define ATOMIC_EXCHANGE(ret, var, val) ret = var; var = val + struct mutex { void lock() {} void unlock() {} @@ -38,6 +40,7 @@ template using atomic = std::atomic; typedef std::mutex mutex; typedef std::lock_guard lock_guard; +#define ATOMIC_EXCHANGE(ret, var, val) ret = var.exchange(val) #define DECLARE_MUTEX(name) mutex *name = nullptr #define DECLARE_INIT_MUTEX(name) mutex *name = new mutex #define ALLOC_MUTEX(name) name = alloc(mutex)