mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

improve logging diagnostics and tracing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-01-09 15:43:16 -08:00
parent 52c6f7c3b1
commit bd879c1016
1 changed files with 53 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

94
src/api/z3_replayer.cpp
View file

@ -22,12 +22,14 @@ Notes:
#include"stream_buffer.h" #include"stream_buffer.h"
#include"symbol.h" #include"symbol.h"
#include"trace.h" #include"trace.h"
#include<sstream>
void register_z3_replayer_cmds(z3_replayer & in); void register_z3_replayer_cmds(z3_replayer & in);
void throw_invalid_reference() { void throw_invalid_reference() {
TRACE("z3_replayer", tout << "invalid argument reference\n";); TRACE("z3_replayer", tout << "invalid argument reference\n";);
throw z3_replayer_exception("invalid argument reference"); throw z3_replayer_exception("invalid argument reference1");
} }
struct z3_replayer::imp { struct z3_replayer::imp {
@ -46,6 +48,36 @@ struct z3_replayer::imp {
enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY }; enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY };
char const* kind2string(value_kind k) const {
switch (k) {
case INT64: return "int64";
case UINT64: return "uint64";
case DOUBLE: return "double";
case STRING: return "string";
case SYMBOL: return "symbol";
case OBJECT: return "object";
case UINT_ARRAY: return "uint_array";
case INT_ARRAY: return "int_array";
case SYMBOL_ARRAY: return "symbol_array";
case OBJECT_ARRAY: return "object_array";
default: UNREACHABLE(); return "unknown";
}
}
void check_arg(unsigned pos, value_kind k) const {
if (pos >= m_args.size()) {
TRACE("z3_replayer", tout << "too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";);
throw z3_replayer_exception("invalid argument reference2");
}
if (m_args[pos].m_kind != k) {
std::stringstream strm;
strm << "expecting " << kind2string(k) << " at position "
<< pos << " but got " << kind2string(m_args[pos].m_kind);
throw z3_replayer_exception(strm.str().c_str());
}
}
struct value { struct value {
value_kind m_kind; value_kind m_kind;
union { union {
@ -467,8 +499,7 @@ struct z3_replayer::imp {
next(); skip_blank(); read_ptr(); skip_blank(); read_uint64(); next(); skip_blank(); read_ptr(); skip_blank(); read_uint64();
unsigned pos = static_cast<unsigned>(m_uint64); unsigned pos = static_cast<unsigned>(m_uint64);
TRACE("z3_replayer", tout << "[" << m_line << "] " << "* " << m_ptr << " " << pos << "\n";); TRACE("z3_replayer", tout << "[" << m_line << "] " << "* " << m_ptr << " " << pos << "\n";);
if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT) check_arg(pos, OBJECT);
throw_invalid_reference();
m_heap.insert(m_ptr, m_args[pos].m_obj); m_heap.insert(m_ptr, m_args[pos].m_obj);
break; break;
} }
@ -477,8 +508,7 @@ struct z3_replayer::imp {
// @ obj_id array_pos idx // @ obj_id array_pos idx
next(); skip_blank(); read_ptr(); skip_blank(); read_uint64(); next(); skip_blank(); read_ptr(); skip_blank(); read_uint64();
unsigned pos = static_cast<unsigned>(m_uint64); unsigned pos = static_cast<unsigned>(m_uint64);
if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT_ARRAY) check_arg(pos, OBJECT_ARRAY);
throw_invalid_reference();
unsigned aidx = static_cast<unsigned>(m_args[pos].m_uint); unsigned aidx = static_cast<unsigned>(m_args[pos].m_uint);
ptr_vector<void> & v = m_obj_arrays[aidx]; ptr_vector<void> & v = m_obj_arrays[aidx];
skip_blank(); read_uint64(); skip_blank(); read_uint64();
@ -503,77 +533,65 @@ struct z3_replayer::imp {
} }
int get_int(unsigned pos) const { int get_int(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != INT64) check_arg(pos, INT64);
throw_invalid_reference();
return static_cast<int>(m_args[pos].m_int); return static_cast<int>(m_args[pos].m_int);
} }
__int64 get_int64(unsigned pos) const { __int64 get_int64(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != INT64) check_arg(pos, INT64);
throw_invalid_reference();
return m_args[pos].m_int; return m_args[pos].m_int;
} }
unsigned get_uint(unsigned pos) const { unsigned get_uint(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != UINT64) check_arg(pos, UINT64);
throw_invalid_reference();
return static_cast<unsigned>(m_args[pos].m_uint); return static_cast<unsigned>(m_args[pos].m_uint);
} }
__uint64 get_uint64(unsigned pos) const { __uint64 get_uint64(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != UINT64) check_arg(pos, UINT64);
throw_invalid_reference();
return m_args[pos].m_uint; return m_args[pos].m_uint;
} }
double get_double(unsigned pos) const { double get_double(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != DOUBLE) check_arg(pos, DOUBLE);
throw_invalid_reference();
return m_args[pos].m_double; return m_args[pos].m_double;
} }
Z3_string get_str(unsigned pos) const { Z3_string get_str(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != STRING) check_arg(pos, STRING);
throw_invalid_reference();
return m_args[pos].m_str; return m_args[pos].m_str;
} }
Z3_symbol get_symbol(unsigned pos) const { Z3_symbol get_symbol(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != SYMBOL) check_arg(pos, SYMBOL);
throw_invalid_reference();
return reinterpret_cast<Z3_symbol>(const_cast<char*>(m_args[pos].m_str)); return reinterpret_cast<Z3_symbol>(const_cast<char*>(m_args[pos].m_str));
} }
void * get_obj(unsigned pos) const { void * get_obj(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT) check_arg(pos, OBJECT);
throw_invalid_reference();
return m_args[pos].m_obj; return m_args[pos].m_obj;
} }
unsigned * get_uint_array(unsigned pos) const { unsigned * get_uint_array(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != UINT_ARRAY) check_arg(pos, UINT_ARRAY);
throw_invalid_reference();
unsigned idx = static_cast<unsigned>(m_args[pos].m_uint); unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
return m_unsigned_arrays[idx].c_ptr(); return m_unsigned_arrays[idx].c_ptr();
} }
int * get_int_array(unsigned pos) const { int * get_int_array(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != INT_ARRAY) check_arg(pos, INT_ARRAY);
throw_invalid_reference();
unsigned idx = static_cast<unsigned>(m_args[pos].m_uint); unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
return m_int_arrays[idx].c_ptr(); return m_int_arrays[idx].c_ptr();
} }
Z3_symbol * get_symbol_array(unsigned pos) const { Z3_symbol * get_symbol_array(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != SYMBOL_ARRAY) check_arg(pos, SYMBOL_ARRAY);
throw_invalid_reference();
unsigned idx = static_cast<unsigned>(m_args[pos].m_uint); unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
return m_sym_arrays[idx].c_ptr(); return m_sym_arrays[idx].c_ptr();
} }
void ** get_obj_array(unsigned pos) const { void ** get_obj_array(unsigned pos) const {
if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT_ARRAY) check_arg(pos, OBJECT_ARRAY);
throw_invalid_reference();
unsigned idx = static_cast<unsigned>(m_args[pos].m_uint); unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
ptr_vector<void> const & v = m_obj_arrays[idx]; ptr_vector<void> const & v = m_obj_arrays[idx];
TRACE("z3_replayer_bug", tout << "pos: " << pos << ", idx: " << idx << " size(): " << v.size() << "\n"; TRACE("z3_replayer_bug", tout << "pos: " << pos << ", idx: " << idx << " size(): " << v.size() << "\n";
@ -582,38 +600,32 @@ struct z3_replayer::imp {
} }
int * get_int_addr(unsigned pos) { int * get_int_addr(unsigned pos) {
if (pos >= m_args.size() || m_args[pos].m_kind != INT64) check_arg(pos, INT64);
throw_invalid_reference();
return reinterpret_cast<int*>(&(m_args[pos].m_int)); return reinterpret_cast<int*>(&(m_args[pos].m_int));
} }
__int64 * get_int64_addr(unsigned pos) { __int64 * get_int64_addr(unsigned pos) {
if (pos >= m_args.size() || m_args[pos].m_kind != INT64) check_arg(pos, INT64);
throw_invalid_reference();
return &(m_args[pos].m_int); return &(m_args[pos].m_int);
} }
unsigned * get_uint_addr(unsigned pos) { unsigned * get_uint_addr(unsigned pos) {
if (pos >= m_args.size() || m_args[pos].m_kind != UINT64) check_arg(pos, UINT64);
throw_invalid_reference();
return reinterpret_cast<unsigned*>(&(m_args[pos].m_uint)); return reinterpret_cast<unsigned*>(&(m_args[pos].m_uint));
} }
__uint64 * get_uint64_addr(unsigned pos) { __uint64 * get_uint64_addr(unsigned pos) {
if (pos >= m_args.size() || m_args[pos].m_kind != UINT64) check_arg(pos, UINT64);
throw_invalid_reference();
return &(m_args[pos].m_uint); return &(m_args[pos].m_uint);
} }
Z3_string * get_str_addr(unsigned pos) { Z3_string * get_str_addr(unsigned pos) {
if (pos >= m_args.size() || m_args[pos].m_kind != STRING) check_arg(pos, STRING);
throw_invalid_reference();
return &(m_args[pos].m_str); return &(m_args[pos].m_str);
} }
void ** get_obj_addr(unsigned pos) { void ** get_obj_addr(unsigned pos) {
if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT) check_arg(pos, OBJECT);
throw_invalid_reference();
return &(m_args[pos].m_obj); return &(m_args[pos].m_obj);
} }