diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 95cf94e6e..e986d6b49 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -805,7 +805,7 @@ extern "C" { cancel_eh eh(m.limit()); api::context::set_interruptable si(*(mk_c(c)), eh); { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); try { m_rw(a, result); diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 3d437e983..0b3eb989d 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -287,7 +287,7 @@ extern "C" { cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); scoped_timer timer(timeout, &eh); - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); try { r = to_fixedpoint_ref(d)->ctx().query(to_expr(q)); } diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index ef215941e..c3774dd85 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -154,7 +154,7 @@ extern "C" { bool use_ctrl_c = to_optimize_ptr(o)->get_params().get_bool("ctrl_c", true); api::context::set_interruptable si(*(mk_c(c)), eh); { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 13a6c1930..29c012b86 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -650,7 +650,7 @@ extern "C" { api::context::set_interruptable si(*(mk_c(c)), eh); lbool result = l_undef; { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { @@ -748,7 +748,7 @@ extern "C" { cancel_eh eh(mk_c(c)->m().limit()); to_solver(s)->set_eh(&eh); { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { @@ -871,7 +871,7 @@ extern "C" { to_solver(s)->set_eh(&eh); api::context::set_interruptable si(*(mk_c(c)), eh); { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { @@ -919,7 +919,7 @@ extern "C" { to_solver(s)->set_eh(&eh); api::context::set_interruptable si(*(mk_c(c)), eh); { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index af5696132..67476060d 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -427,7 +427,7 @@ extern "C" { api::context::set_interruptable si(*(mk_c(c)), eh); { - scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_ctrl_c ctrlc(eh, use_ctrl_c); scoped_timer timer(timeout, &eh); try { exec(*to_tactic_ref(t), new_goal, ref->m_subgoals); diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index 525c12f25..645e777fd 100644 --- a/src/test/sat_local_search.cpp +++ b/src/test/sat_local_search.cpp @@ -122,7 +122,7 @@ void tst_sat_local_search(char ** argv, int argc, int& i) { // set up cancellation/timeout environment. cancel_eh eh(local_search.rlimit()); - scoped_ctrl_c ctrlc(eh, false, true); + scoped_ctrl_c ctrlc(eh); scoped_timer timer(cutoff_time*1000, &eh); local_search.check(0, nullptr, nullptr); diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index d609b957a..473492717 100644 --- a/src/util/cancel_eh.h +++ b/src/util/cancel_eh.h @@ -18,6 +18,8 @@ Revision History: --*/ #pragma once +#include +#include #include "util/event_handler.h" /** @@ -25,22 +27,29 @@ Revision History: */ template class cancel_eh : public event_handler { - bool m_canceled = false; + std::mutex m_mutex; + std::atomic m_canceled = false; bool m_auto_cancel = false; T & m_obj; public: cancel_eh(T & o): m_obj(o) {} ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); if (m_auto_cancel) m_obj.auto_cancel(); } + + // Note that this method doesn't race with the destructor since + // potential callers like scoped_ctrl_c/scoped_timer are destroyed + // before the cancel_eh destructor is invoked. + // Thus, the only races are with itself and with the getters. void operator()(event_handler_caller_t caller_id) override { + std::lock_guard lock(m_mutex); if (!m_canceled) { m_caller_id = caller_id; + m_obj.inc_cancel(); m_canceled = true; - m_obj.inc_cancel(); } } + bool canceled() const { return m_canceled; } void reset() { m_canceled = false; } T& t() { return m_obj; } void set_auto_cancel() { m_auto_cancel = true; } }; - diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 2d60787fd..360543fc4 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -16,45 +16,49 @@ Author: Revision History: --*/ -#include +#include +#include +#include #include "util/scoped_ctrl_c.h" #include "util/gparams.h" -static scoped_ctrl_c * g_obj = nullptr; +static std::vector g_list; +static std::mutex g_list_mutex; +static void (*g_old_handler)(int); static void on_ctrl_c(int) { - if (g_obj->m_first) { - g_obj->m_cancel_eh(CTRL_C_EH_CALLER); - if (g_obj->m_once) { - g_obj->m_first = false; - signal(SIGINT, on_ctrl_c); // re-install the handler + std::lock_guard lock(g_list_mutex); + for (auto handler : g_list) { + if (handler->m_enabled) { + handler->m_cancel_eh(CTRL_C_EH_CALLER); } } - else { - signal(SIGINT, g_obj->m_old_handler); - raise(SIGINT); - } + signal(SIGINT, g_old_handler); } -scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled): - m_cancel_eh(eh), - m_first(true), - m_once(once), - m_enabled(enabled), - m_old_scoped_ctrl_c(g_obj) { - if (gparams::get_value("ctrl_c") == "false") +scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool enabled): + m_cancel_eh(eh), + m_enabled(enabled) { + if (enabled && gparams::get_value("ctrl_c") == "false") m_enabled = false; + if (m_enabled) { - g_obj = this; - m_old_handler = signal(SIGINT, on_ctrl_c); + std::lock_guard lock(g_list_mutex); + if (g_list.empty()) { + g_old_handler = signal(SIGINT, on_ctrl_c); + } + g_list.push_back(this); } } scoped_ctrl_c::~scoped_ctrl_c() { if (m_enabled) { - g_obj = m_old_scoped_ctrl_c; - if (m_old_handler != SIG_ERR) { - signal(SIGINT, m_old_handler); + std::lock_guard lock(g_list_mutex); + auto it = std::find(g_list.begin(), g_list.end(), this); + SASSERT(it != g_list.end()); + g_list.erase(it); + if (g_list.empty()) { + signal(SIGINT, g_old_handler); } } } diff --git a/src/util/scoped_ctrl_c.h b/src/util/scoped_ctrl_c.h index 09bc55c05..65181ce46 100644 --- a/src/util/scoped_ctrl_c.h +++ b/src/util/scoped_ctrl_c.h @@ -23,17 +23,9 @@ Revision History: struct scoped_ctrl_c { event_handler & m_cancel_eh; - bool m_first; - bool m_once; bool m_enabled; - void (STD_CALL *m_old_handler)(int); - scoped_ctrl_c * m_old_scoped_ctrl_c; public: - // If once == true, then the cancel_eh is invoked only at the first Ctrl-C. - // The next time, the old signal handler will take over. // if enabled == false, then scoped_ctrl_c is a noop - scoped_ctrl_c(event_handler & eh, bool once=true, bool enabled=true); + scoped_ctrl_c(event_handler & eh, bool enabled = true); ~scoped_ctrl_c(); - void reset() { m_first = true; } }; -