mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4675643271
commit
564da787fb
|
@ -355,10 +355,7 @@ extern "C" {
|
|||
init_solver(c, s);
|
||||
Z3_stats_ref * st = alloc(Z3_stats_ref);
|
||||
to_solver_ref(s)->collect_statistics(st->m_stats);
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
st->m_stats.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
|
||||
st->m_stats.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
|
||||
get_memory_statistics(st->m_stats);
|
||||
mk_c(c)->save_object(st);
|
||||
Z3_stats r = of_stats(st);
|
||||
RETURN_Z3(r);
|
||||
|
|
|
@ -1624,11 +1624,10 @@ void cmd_context::set_solver_factory(solver_factory * f) {
|
|||
|
||||
void cmd_context::display_statistics(bool show_total_time, double total_time) {
|
||||
statistics st;
|
||||
unsigned long long mem = memory::get_max_used_memory();
|
||||
if (show_total_time)
|
||||
st.update("total time", total_time);
|
||||
st.update("time", get_seconds());
|
||||
st.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
|
||||
get_memory_statistics(st);
|
||||
if (m_check_sat_result) {
|
||||
m_check_sat_result->collect_statistics(st);
|
||||
}
|
||||
|
|
|
@ -157,11 +157,8 @@ public:
|
|||
|
||||
void display_statistics(cmd_context & ctx, tactic * t) {
|
||||
statistics stats;
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
get_memory_statistics(stats);
|
||||
stats.update("time", ctx.get_seconds());
|
||||
stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
|
||||
stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
|
||||
t->collect_statistics(stats);
|
||||
stats.display_smt2(ctx.regular_stream());
|
||||
}
|
||||
|
|
|
@ -945,10 +945,7 @@ namespace datalog {
|
|||
if (m_engine) {
|
||||
m_engine->collect_statistics(st);
|
||||
}
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
st.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
|
||||
st.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
|
||||
get_memory_statistics(st);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -338,12 +338,8 @@ private:
|
|||
if (m_dl_ctx->get_params().print_statistics()) {
|
||||
statistics st;
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
dlctx.collect_statistics(st);
|
||||
st.update("time", ctx.get_seconds());
|
||||
st.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
|
||||
st.update("max-memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
|
||||
st.display_smt2(ctx.regular_stream());
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1188,10 +1188,7 @@ namespace opt {
|
|||
for (; it != end; ++it) {
|
||||
it->m_value->collect_statistics(stats);
|
||||
}
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
|
||||
stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
|
||||
get_memory_statistics(stats);
|
||||
}
|
||||
|
||||
void context::collect_param_descrs(param_descrs & r) {
|
||||
|
|
|
@ -203,22 +203,32 @@ public:
|
|||
return BR_FAILED;
|
||||
}
|
||||
|
||||
// (+ (f x) y)
|
||||
// (f (+ x y))
|
||||
//
|
||||
bool is_arith_op(expr* e) {
|
||||
return is_app(e) && to_app(e)->get_family_id() == u().get_family_id();
|
||||
}
|
||||
br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
|
||||
bool has_interface = false;
|
||||
bool is_arith = false;
|
||||
if (f->get_family_id() == u().get_family_id()) {
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_NUM: case OP_IRRATIONAL_ALGEBRAIC_NUM:
|
||||
case OP_ADD: case OP_MUL: case OP_SUB:
|
||||
case OP_UMINUS: case OP_ABS: case OP_POWER:
|
||||
return BR_FAILED;
|
||||
default:
|
||||
is_arith = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_args.reset();
|
||||
for (unsigned i = 0; i < num; ++i) {
|
||||
expr* arg = args[i];
|
||||
if (u().is_real(arg)) {
|
||||
if (is_arith && !is_arith_op(arg)) {
|
||||
has_interface = true;
|
||||
m_args.push_back(mk_interface_var(arg));
|
||||
}
|
||||
else if (!is_arith && u().is_real(arg)) {
|
||||
has_interface = true;
|
||||
m_args.push_back(mk_interface_var(arg));
|
||||
}
|
||||
|
|
|
@ -27,6 +27,7 @@ void env_params::updt_params() {
|
|||
set_verbosity_level(p.get_uint("verbose", get_verbosity_level()));
|
||||
enable_warning_messages(p.get_bool("warning", true));
|
||||
memory::set_max_size(megabytes_to_bytes(p.get_uint("memory_max_size", 0)));
|
||||
memory::set_max_alloc_count(p.get_uint("memory_max_alloc_count", 0));
|
||||
memory::set_high_watermark(p.get_uint("memory_high_watermark", 0));
|
||||
}
|
||||
|
||||
|
@ -34,5 +35,6 @@ void env_params::collect_param_descrs(param_descrs & d) {
|
|||
d.insert("verbose", CPK_UINT, "be verbose, where the value is the verbosity level", "0");
|
||||
d.insert("warning", CPK_BOOL, "enable/disable warning messages", "true");
|
||||
d.insert("memory_max_size", CPK_UINT, "set hard upper limit for memory consumption (in megabytes), if 0 then there is no limit", "0");
|
||||
d.insert("memory_max_alloc_count", CPK_UINT, "set hard upper limit for memory allocations, if 0 then there is no limit", "0");
|
||||
d.insert("memory_high_watermark", CPK_UINT, "set high watermark for memory consumption (in megabytes), if 0 then there is no limit", "0");
|
||||
}
|
||||
|
|
|
@ -32,6 +32,7 @@ Revision History:
|
|||
#define ERR_INTERNAL_FATAL 110
|
||||
#define ERR_TYPE_CHECK 111
|
||||
#define ERR_UNKNOWN_RESULT 112
|
||||
#define ERR_ALLOC_EXCEEDED 113
|
||||
|
||||
#endif /* _ERROR_CODES_H_ */
|
||||
|
||||
|
|
|
@ -33,12 +33,17 @@ void mem_finalize();
|
|||
out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
|
||||
}
|
||||
|
||||
exceeded_memory_allocations::exceeded_memory_allocations():z3_error(ERR_ALLOC_EXCEEDED) {
|
||||
}
|
||||
|
||||
static volatile bool g_memory_out_of_memory = false;
|
||||
static bool g_memory_initialized = false;
|
||||
static long long g_memory_alloc_size = 0;
|
||||
static long long g_memory_max_size = 0;
|
||||
static long long g_memory_max_used_size = 0;
|
||||
static long long g_memory_watermark = 0;
|
||||
static long long g_memory_alloc_count = 0;
|
||||
static long long g_memory_max_alloc_count = 0;
|
||||
static bool g_exit_when_out_of_memory = false;
|
||||
static char const * g_out_of_memory_msg = "ERROR: out of memory";
|
||||
static volatile bool g_memory_fully_initialized = false;
|
||||
|
@ -52,9 +57,7 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) {
|
|||
static void throw_out_of_memory() {
|
||||
#pragma omp critical (z3_memory_manager)
|
||||
{
|
||||
if (!g_memory_out_of_memory) {
|
||||
g_memory_out_of_memory = true;
|
||||
}
|
||||
g_memory_out_of_memory = true;
|
||||
}
|
||||
if (g_exit_when_out_of_memory) {
|
||||
std::cerr << g_out_of_memory_msg << "\n";
|
||||
|
@ -65,12 +68,18 @@ static void throw_out_of_memory() {
|
|||
}
|
||||
}
|
||||
|
||||
static void throw_alloc_counts_exceeded() {
|
||||
throw exceeded_memory_allocations();
|
||||
}
|
||||
|
||||
|
||||
#ifdef PROFILE_MEMORY
|
||||
static unsigned g_synch_counter = 0;
|
||||
class mem_usage_report {
|
||||
public:
|
||||
~mem_usage_report() {
|
||||
std::cerr << "(memory :max " << g_memory_max_used_size
|
||||
<< " :allocs " << g_memory_alloc_count
|
||||
<< " :final " << g_memory_alloc_size
|
||||
<< " :synch " << g_synch_counter << ")" << std::endl;
|
||||
}
|
||||
|
@ -129,11 +138,17 @@ bool memory::above_high_watermark() {
|
|||
return r;
|
||||
}
|
||||
|
||||
// The following methods are only safe to invoke at
|
||||
// initialization time, that is, before threads are created.
|
||||
|
||||
void memory::set_max_size(size_t max_size) {
|
||||
// This method is only safe to invoke at initialization time, that is, before the threads are created.
|
||||
g_memory_max_size = max_size;
|
||||
}
|
||||
|
||||
void memory::set_max_alloc_count(size_t max_count) {
|
||||
g_memory_max_alloc_count = max_count;
|
||||
}
|
||||
|
||||
static bool g_finalizing = false;
|
||||
|
||||
void memory::finalize() {
|
||||
|
@ -165,6 +180,11 @@ unsigned long long memory::get_max_used_memory() {
|
|||
return r;
|
||||
}
|
||||
|
||||
unsigned long long memory::get_allocation_count() {
|
||||
return g_memory_alloc_count;
|
||||
}
|
||||
|
||||
|
||||
void memory::display_max_usage(std::ostream & os) {
|
||||
unsigned long long mem = get_max_used_memory();
|
||||
os << "max. heap size: "
|
||||
|
@ -207,9 +227,11 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
|
|||
#ifdef _WINDOWS
|
||||
// Actually this is VS specific instead of Windows specific.
|
||||
__declspec(thread) long long g_memory_thread_alloc_size = 0;
|
||||
__declspec(thread) long long g_memory_thread_alloc_count = 0;
|
||||
#else
|
||||
// GCC style
|
||||
__thread long long g_memory_thread_alloc_size = 0;
|
||||
__thread long long g_memory_thread_alloc_count = 0;
|
||||
#endif
|
||||
|
||||
static void synchronize_counters(bool allocating) {
|
||||
|
@ -218,18 +240,25 @@ static void synchronize_counters(bool allocating) {
|
|||
#endif
|
||||
|
||||
bool out_of_mem = false;
|
||||
bool counts_exceeded = false;
|
||||
#pragma omp critical (z3_memory_manager)
|
||||
{
|
||||
g_memory_alloc_size += g_memory_thread_alloc_size;
|
||||
g_memory_alloc_count += g_memory_thread_alloc_count;
|
||||
if (g_memory_alloc_size > g_memory_max_used_size)
|
||||
g_memory_max_used_size = g_memory_alloc_size;
|
||||
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
||||
out_of_mem = true;
|
||||
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
||||
counts_exceeded = true;
|
||||
}
|
||||
g_memory_thread_alloc_size = 0;
|
||||
if (out_of_mem && allocating) {
|
||||
throw_out_of_memory();
|
||||
}
|
||||
if (counts_exceeded && allocating) {
|
||||
throw_alloc_counts_exceeded();
|
||||
}
|
||||
}
|
||||
|
||||
void memory::deallocate(void * p) {
|
||||
|
@ -252,6 +281,7 @@ void * memory::allocate(size_t s) {
|
|||
throw_out_of_memory();
|
||||
*(static_cast<size_t*>(r)) = s;
|
||||
g_memory_thread_alloc_size += s;
|
||||
g_memory_thread_alloc_count += 1;
|
||||
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
||||
synchronize_counters(true);
|
||||
}
|
||||
|
@ -265,6 +295,7 @@ void* memory::reallocate(void *p, size_t s) {
|
|||
s = s + sizeof(size_t); // we allocate an extra field!
|
||||
|
||||
g_memory_thread_alloc_size += s - sz;
|
||||
g_memory_thread_alloc_count += 1;
|
||||
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
||||
synchronize_counters(true);
|
||||
}
|
||||
|
@ -299,17 +330,22 @@ void * memory::allocate(size_t s) {
|
|||
if (s == 0)
|
||||
return 0;
|
||||
s = s + sizeof(size_t); // we allocate an extra field!
|
||||
bool out_of_mem = false;
|
||||
bool out_of_mem = false, counts_exceeded = false;
|
||||
#pragma omp critical (z3_memory_manager)
|
||||
{
|
||||
g_memory_alloc_size += s;
|
||||
g_memory_alloc_count += 1;
|
||||
if (g_memory_alloc_size > g_memory_max_used_size)
|
||||
g_memory_max_used_size = g_memory_alloc_size;
|
||||
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
||||
out_of_mem = true;
|
||||
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
||||
counts_exceeded = true;
|
||||
}
|
||||
if (out_of_mem)
|
||||
throw_out_of_memory();
|
||||
if (counts_exceeded)
|
||||
throw_alloc_counts_exceeded();
|
||||
void * r = malloc(s);
|
||||
if (r == 0)
|
||||
throw_out_of_memory();
|
||||
|
@ -322,18 +358,22 @@ void* memory::reallocate(void *p, size_t s) {
|
|||
size_t sz = *sz_p;
|
||||
void * real_p = reinterpret_cast<void*>(sz_p);
|
||||
s = s + sizeof(size_t); // we allocate an extra field!
|
||||
bool out_of_mem = false;
|
||||
bool out_of_mem = false, counts_exceeded = false;
|
||||
#pragma omp critical (z3_memory_manager)
|
||||
{
|
||||
g_memory_alloc_size += s - sz;
|
||||
g_memory_alloc_count += 1;
|
||||
if (g_memory_alloc_size > g_memory_max_used_size)
|
||||
g_memory_max_used_size = g_memory_alloc_size;
|
||||
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
||||
out_of_mem = true;
|
||||
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
||||
counts_exceeded = true;
|
||||
}
|
||||
if (out_of_mem)
|
||||
throw_out_of_memory();
|
||||
|
||||
if (counts_exceeded)
|
||||
throw_alloc_counts_exceeded();
|
||||
void *r = realloc(real_p, s);
|
||||
if (r == 0)
|
||||
throw_out_of_memory();
|
||||
|
|
|
@ -46,6 +46,11 @@ public:
|
|||
out_of_memory_error();
|
||||
};
|
||||
|
||||
class exceeded_memory_allocations : public z3_error {
|
||||
public:
|
||||
exceeded_memory_allocations();
|
||||
};
|
||||
|
||||
class memory {
|
||||
public:
|
||||
static bool is_out_of_memory();
|
||||
|
@ -53,6 +58,7 @@ public:
|
|||
static void set_high_watermark(size_t watermak);
|
||||
static bool above_high_watermark();
|
||||
static void set_max_size(size_t max_size);
|
||||
static void set_max_alloc_count(size_t max_count);
|
||||
static void finalize();
|
||||
static void display_max_usage(std::ostream& os);
|
||||
static void display_i_max_usage(std::ostream& os);
|
||||
|
@ -65,6 +71,7 @@ public:
|
|||
#endif
|
||||
static unsigned long long get_allocation_size();
|
||||
static unsigned long long get_max_used_memory();
|
||||
static unsigned long long get_allocation_count();
|
||||
// temporary hack to avoid out-of-memory crash in z3.exe
|
||||
static void exit_when_out_of_memory(bool flag, char const * msg);
|
||||
};
|
||||
|
|
|
@ -226,3 +226,13 @@ double statistics::get_double_value(unsigned idx) const {
|
|||
SASSERT(!is_uint(idx));
|
||||
return m_d_stats[idx - m_stats.size()].second;
|
||||
}
|
||||
|
||||
void get_memory_statistics(statistics& st) {
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
max_mem = (100*max_mem)/(1024*1024);
|
||||
mem = (100*mem)/(1024*1024);
|
||||
st.update("max memory", static_cast<double>(max_mem)/100.0);
|
||||
st.update("memory", static_cast<double>(mem)/100.0);
|
||||
st.update("num allocs", static_cast<double>(memory::get_allocation_count()));
|
||||
}
|
||||
|
|
|
@ -42,4 +42,6 @@ public:
|
|||
double get_double_value(unsigned idx) const;
|
||||
};
|
||||
|
||||
void get_memory_statistics(statistics& st);
|
||||
|
||||
#endif
|
||||
|
|
|
@ -49,6 +49,7 @@ char const * z3_error::msg() const {
|
|||
case ERR_CMD_LINE: return "invalid command line";
|
||||
case ERR_INTERNAL_FATAL: return "internal error";
|
||||
case ERR_TYPE_CHECK: return "type error";
|
||||
case ERR_ALLOC_EXCEEDED: return "number of configured allocations exceeded";
|
||||
default: return "unknown error";
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue