mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
logging cleanup
move everything out-of-line as common path doesn't log fix some race conditions on file ptr vs enable_logging vars
This commit is contained in:
Nuno Lopes
parent
1f4a7c5101
commit
9b5ec6d004
5 changed files with 106 additions and 76 deletions
|
|
@ -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<iostream>\n')
|
||||
log_h.write('#include<atomic>\n')
|
||||
log_h.write('extern std::ostream * g_z3_log;\n')
|
||||
log_h.write('extern std::atomic<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 && 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<bool> 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):
|
||||
|
|
|
|||
|
|
@ -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<Z3_context>(this), c);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -18,12 +18,13 @@ Revision History:
|
|||
#include<fstream>
|
||||
#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<bool> g_z3_log_enabled;
|
||||
static std::ostream * g_z3_log = nullptr;
|
||||
atomic<bool> 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 <<std::endl; }
|
||||
void I(int64_t i) { *g_z3_log << "I " << i << std::endl; }
|
||||
void U(uint64_t u) { *g_z3_log << "U " << u << std::endl; }
|
||||
void D(double d) { *g_z3_log << "D " << d << std::endl; }
|
||||
void S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped{str} << '"' << std::endl; }
|
||||
void Sy(Z3_symbol sym) {
|
||||
symbol s = symbol::c_api_ext2symbol(sym);
|
||||
if (s.is_null()) {
|
||||
*g_z3_log << 'N';
|
||||
}
|
||||
else if (s.is_numerical()) {
|
||||
*g_z3_log << "# " << s.get_num();
|
||||
}
|
||||
else {
|
||||
*g_z3_log << "$ |" << ll_escaped{s.bare_str()} << '|';
|
||||
}
|
||||
*g_z3_log << std::endl;
|
||||
}
|
||||
void Ap(unsigned sz) { *g_z3_log << "p " << sz << std::endl; }
|
||||
void Au(unsigned sz) { *g_z3_log << "u " << sz << std::endl; }
|
||||
void Ai(unsigned sz) { *g_z3_log << "i " << sz << std::endl; }
|
||||
void Asy(unsigned sz) { *g_z3_log << "s " << sz << std::endl; }
|
||||
void C(unsigned id) { *g_z3_log << "C " << id << std::endl; }
|
||||
static void _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped{msg} << '"' << std::endl; }
|
||||
|
||||
void ctx_enable_logging() {
|
||||
SCOPED_LOCK();
|
||||
if (g_z3_log != nullptr)
|
||||
g_z3_log_enabled = true;
|
||||
}
|
||||
|
||||
static void Z3_close_log_unsafe(void) {
|
||||
if (g_z3_log != nullptr) {
|
||||
g_z3_log_enabled = false;
|
||||
|
|
@ -42,11 +115,11 @@ static void Z3_close_log_unsafe(void) {
|
|||
|
||||
extern "C" {
|
||||
bool Z3_API Z3_open_log(Z3_string filename) {
|
||||
bool res = true;
|
||||
bool res;
|
||||
|
||||
SCOPED_LOCK();
|
||||
if (g_z3_log != nullptr)
|
||||
Z3_close_log_unsafe();
|
||||
Z3_close_log_unsafe();
|
||||
|
||||
g_z3_log = alloc(std::ofstream, filename);
|
||||
if (g_z3_log->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();
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -16,57 +16,17 @@ Author:
|
|||
Notes:
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#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);
|
||||
|
|
|
|||
|
|
@ -16,6 +16,8 @@ Abstract:
|
|||
|
||||
template<typename T> using atomic = T;
|
||||
|
||||
#define ATOMIC_EXCHANGE(ret, var, val) ret = var; var = val
|
||||
|
||||
struct mutex {
|
||||
void lock() {}
|
||||
void unlock() {}
|
||||
|
|
@ -38,6 +40,7 @@ template<typename T> using atomic = std::atomic<T>;
|
|||
typedef std::mutex mutex;
|
||||
typedef std::lock_guard<std::mutex> 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)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue