From 79d4502771c184bea495eaad1a12286dc667bbf8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Sep 2019 20:22:35 -0700 Subject: [PATCH] atomics for #2565 Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 5 +++-- src/api/api_log.cpp | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 94cabf72b..64d6ea8c6 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1687,9 +1687,10 @@ def write_log_h_preamble(log_h): 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 bool g_z3_log_enabled;\n') - log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\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_enabled.exchange(false); } ~z3_log_ctx() { 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('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n') log_h.write('void _Z3_append_log(char const * msg);\n') diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 5f2d8f8af..e82ec3fd1 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -23,7 +23,7 @@ Revision History: #include "util/z3_version.h" std::ostream * g_z3_log = nullptr; -bool g_z3_log_enabled = false; +std::atomic g_z3_log_enabled; #ifdef Z3_LOG_SYNC static std::mutex g_log_mux;