From aa0ebc6efc1d5f30f6f33ae1232031872f82fced Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 27 Jul 2026 12:46:32 -0700 Subject: [PATCH] Prevent `Z3_solver_reset` abort after `memory_max_size` OOM by making reset memory-limit-safe (#10254) `memory_max_size` OOMs were recoverable at `check_sat` time (`Z3_L_UNDEF` + error handler), but `Z3_solver_reset` could still terminate the process with an uncaught `out_of_memory_error`. This change keeps reset on the C API error-reporting path instead of letting teardown allocations trip the same hard limit. - **Reset path hardening** - `Z3_solver_reset` now performs solver teardown under a temporary suspension of the global memory cap, then restores the previous cap afterward. - This avoids aborts when allocator accounting is still above `memory_max_size` at reset time. - **Memory manager support** - Added `memory::get_max_size()` to snapshot/restore the active cap precisely. - **Regression coverage** - Extended `src/test/memory.cpp` with a focused scenario that trips `Z3_MEMOUT_FAIL` and then calls `Z3_solver_reset` under a non-throwing error handler, covering the previously aborting recovery path. ```cpp struct scoped_memory_limit_reset { size_t m_prev_max; scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) { memory::set_max_size(0); } ~scoped_memory_limit_reset() { memory::set_max_size(m_prev_max); } } scoped_max_memory; ``` - Fixes #10250 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/api/api_solver.cpp | 10 +++++++++ src/test/memory.cpp | 41 +++++++++++++++++++++++++++++++++++++ src/util/memory_manager.cpp | 5 +++++ src/util/memory_manager.h | 2 +- 4 files changed, 57 insertions(+), 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 2d39e3287a..be1b701223 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -22,6 +22,7 @@ Revision History: #include "util/file_path.h" #include "util/scoped_timer.h" #include "util/file_path.h" +#include "util/memory_manager.h" #include "ast/ast_pp.h" #include "api/z3.h" #include "api/api_log_macros.h" @@ -514,6 +515,15 @@ extern "C" { Z3_TRY; LOG_Z3_solver_reset(c, s); RESET_ERROR_CODE(); + struct scoped_memory_limit_reset { + size_t m_prev_max; + scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) { + memory::set_max_size(0); + } + ~scoped_memory_limit_reset() { + memory::set_max_size(m_prev_max); + } + } scoped_max_memory; to_solver(s)->m_solver = nullptr; to_solver(s)->m_cmd_context = nullptr; if (to_solver(s)->m_pp) to_solver(s)->m_pp->reset(); diff --git a/src/test/memory.cpp b/src/test/memory.cpp index 58e8855b64..e751f29553 100644 --- a/src/test/memory.cpp +++ b/src/test/memory.cpp @@ -11,6 +11,8 @@ Copyright (c) 2015 Microsoft Corporation #include "util/trace.h" static bool oom = false; +static unsigned oom_handler_calls = 0; +static Z3_error_code oom_handler_last_code = Z3_OK; static void err_handler(Z3_context c, Z3_error_code e) { @@ -18,6 +20,11 @@ static void err_handler(Z3_context c, Z3_error_code e) { throw std::bad_alloc(); } +static void err_handler_noexcept(Z3_context, Z3_error_code e) { + ++oom_handler_calls; + oom_handler_last_code = e; +} + static void hit_me(char const* wm) { Z3_config cfg; Z3_context ctx; @@ -49,6 +56,37 @@ static void hit_me(char const* wm) { Z3_del_config(cfg); } +static void solver_reset_after_oom(char const* wm) { + Z3_config cfg; + Z3_context ctx; + + oom_handler_calls = 0; + oom_handler_last_code = Z3_OK; + + cfg = Z3_mk_config(); + if (!cfg) { + return; + } + Z3_global_param_set("MEMORY_MAX_SIZE", wm); + ctx = Z3_mk_context(cfg); + if (ctx) { + Z3_set_error_handler(ctx, &err_handler_noexcept); + Z3_solver s = Z3_mk_solver(ctx); + Z3_symbol p = Z3_mk_string_symbol(ctx, "p"); + Z3_ast b = Z3_mk_const(ctx, p, Z3_mk_bool_sort(ctx)); + Z3_solver_assert(ctx, s, b); + Z3_solver_check(ctx, s); + for (unsigned i = 1; oom_handler_last_code != Z3_MEMOUT_FAIL; ++i) { + Z3_mk_bv_sort(ctx, i); + } + VERIFY(oom_handler_last_code == Z3_MEMOUT_FAIL); + VERIFY(oom_handler_calls > 0); + Z3_solver_reset(ctx, s); + Z3_del_context(ctx); + } + Z3_del_config(cfg); +} + void tst_memory() { hit_me("10"); Z3_reset_memory(); @@ -56,5 +94,8 @@ void tst_memory() { Z3_reset_memory(); hit_me("30"); Z3_reset_memory(); + solver_reset_after_oom("30"); + Z3_reset_memory(); + Z3_global_param_set("MEMORY_MAX_SIZE", "0"); } diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index eddadb989c..6fbf175e0e 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -143,6 +143,11 @@ void memory::set_max_size(size_t max_size) { g_memory_max_size = max_size; } +size_t memory::get_max_size() { + lock_guard lock(*g_memory_mux); + return g_memory_max_size <= 0 ? 0 : static_cast(g_memory_max_size); +} + void memory::set_max_alloc_count(size_t max_count) { g_memory_max_alloc_count = max_count; } diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 1d9a604afb..c90198b398 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -55,6 +55,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 size_t get_max_size(); static void set_max_alloc_count(size_t max_count); static void finalize(bool shutdown = true); static void display_max_usage(std::ostream& os); @@ -157,4 +158,3 @@ inline std::ostream & operator<<(std::ostream & out, mem_stat const & m) { } -