From 2d5ac61cdbb4bdb9a35d76d0f8fc2deac83973d2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 1 Jul 2025 10:21:31 -0700 Subject: [PATCH] declare m_global_stats as std::unique_ptr Signed-off-by: Lev Nachmanson --- src/cmd_context/cmd_context.cpp | 30 ++++++++++++++++++++---------- src/cmd_context/cmd_context.h | 6 +++++- src/smt/smt_context.cpp | 20 +++++++++++++++----- 3 files changed, 40 insertions(+), 16 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index bf97daccb..f2b54826a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -609,6 +609,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_own_manager(m == nullptr), m_regular("stdout", std::cout), m_diagnostic("stderr", std::cerr), + m_global_stats(std::make_unique()), m_stats_collected(false) { SASSERT(m != 0 || !has_manager()); install_basic_cmds(*this); @@ -2291,22 +2292,29 @@ void cmd_context::set_solver_factory(solver_factory * f) { } void cmd_context::display_statistics(bool show_total_time, double total_time) { + lock_guard lock(m_stats_mutex); + // If statistics haven't been collected yet, collect them now if (!m_stats_collected) { - flush_statistics(); + flush_statistics_unlocked(); // Call unlocked version since we already have the lock } // Add time and memory statistics if (show_total_time) - m_global_stats.update("total time", total_time); - m_global_stats.update("time", get_seconds()); - get_memory_statistics(m_global_stats); - get_rlimit_statistics(m().limit(), m_global_stats); + m_global_stats->update("total time", total_time); + m_global_stats->update("time", get_seconds()); + get_memory_statistics(*m_global_stats); + get_rlimit_statistics(m().limit(), *m_global_stats); - m_global_stats.display_smt2(regular_stream()); + m_global_stats->display_smt2(regular_stream()); } void cmd_context::flush_statistics() { + lock_guard lock(m_stats_mutex); + flush_statistics_unlocked(); +} + +void cmd_context::flush_statistics_unlocked() { // Only collect statistics once to avoid duplication if (m_stats_collected) { return; @@ -2323,7 +2331,7 @@ void cmd_context::flush_statistics() { m_check_sat_result->flush_statistics(); // Also collect the statistics immediately into our singleton - m_check_sat_result->collect_statistics(m_global_stats); + m_check_sat_result->collect_statistics(*m_global_stats); collected_from_check_sat = true; } @@ -2332,7 +2340,7 @@ void cmd_context::flush_statistics() { m_solver->flush_statistics(); // Also collect the statistics immediately into our singleton - m_solver->collect_statistics(m_global_stats); + m_solver->collect_statistics(*m_global_stats); } // Try to get access to any other solver contexts @@ -2340,16 +2348,18 @@ void cmd_context::flush_statistics() { // m_opt->flush_statistics(); // Not implemented for optimization // But we can still collect stats - m_opt->collect_statistics(m_global_stats); + m_opt->collect_statistics(*m_global_stats); } m_stats_collected = true; } void cmd_context::collect_smt_statistics(smt::context& smt_ctx) { + lock_guard lock(m_stats_mutex); + // Collect statistics from SMT context directly into our singleton // Collect from the SMT context which should have aggregated theory stats - smt_ctx.collect_statistics(m_global_stats); + smt_ctx.collect_statistics(*m_global_stats); m_stats_collected = true; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index db6fc3481..ac5a7d28c 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -23,6 +23,7 @@ Notes: #include #include #include "util/stopwatch.h" +#include "util/mutex.h" #include "util/stats.h" #include "util/cmd_context_types.h" #include "util/event_handler.h" @@ -309,8 +310,10 @@ protected: // Singleton statistics object to accumulate stats throughout the run // This ensures theory statistics collected during timeout are preserved - statistics m_global_stats; + // Using a pointer to avoid any accidental copying + std::unique_ptr m_global_stats; bool m_stats_collected; + mutex m_stats_mutex; // Protect statistics access class dt_eh : public new_datatype_eh { cmd_context & m_owner; @@ -518,6 +521,7 @@ public: void display_assertions(); void display_statistics(bool show_total_time = false, double total_time = 0.0); void flush_statistics(); // Force aggregation of theory statistics + void flush_statistics_unlocked(); // Internal helper, requires m_stats_mutex to be held void collect_smt_statistics(smt::context& smt_ctx); // Collect stats from SMT context into singleton void display_dimacs(); void display_parameters(std::ostream& out); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 34d826329..d5159387a 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -21,6 +21,7 @@ Revision History: #include "util/warning.h" #include "util/timeit.h" #include "util/union_find.h" +#include "util/mutex.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/ast_smt2_pp.h" @@ -50,7 +51,9 @@ Revision History: namespace smt { // Global pointer to current SMT context for timeout statistics collection + // Protected by mutex for thread safety static context* g_smt_context = nullptr; + static mutex g_smt_context_mutex; context::context(ast_manager & m, smt_params & p, params_ref const & _p): m(m), @@ -102,8 +105,11 @@ namespace smt { m_model_generator->set_context(this); - // Register this SMT context for timeout statistics collection - g_smt_context = this; + // Register this SMT context for timeout statistics collection (thread-safe) + { + lock_guard lock(g_smt_context_mutex); + g_smt_context = this; + } } /** @@ -195,9 +201,12 @@ namespace smt { } context::~context() { - // Unregister this SMT context - if (g_smt_context == this) { - g_smt_context = nullptr; + // Unregister this SMT context (thread-safe) + { + lock_guard lock(g_smt_context_mutex); + if (g_smt_context == this) { + g_smt_context = nullptr; + } } flush(); m_asserted_formulas.finalize(); @@ -4820,6 +4829,7 @@ namespace smt { } // Function to get the current global SMT context (for timeout handling) context* get_current_smt_context() { + lock_guard lock(g_smt_context_mutex); return g_smt_context; }