fix #7603: race condition in Ctrl-C handling (#7755)

* fix #7603: race condition in Ctrl-C handling

* fix race in cancel_eh

* fix build

src/api/api_ast.cpp

@@ -805,7 +805,7 @@ extern "C" {
         cancel_eh<reslimit> 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);

src/api/api_datalog.cpp

@@ -287,7 +287,7 @@ extern "C" {
             cancel_eh<reslimit> 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));
             }

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 {

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<reslimit> 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 {

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);

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<reslimit> 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);    
 

src/util/cancel_eh.h

@@ -18,6 +18,8 @@ Revision History:
 --*/
 #pragma once
 
+#include <atomic>
+#include <mutex>
 #include "util/event_handler.h"
 
 /**
@@ -25,22 +27,29 @@ Revision History:
 */
 template<typename T>
 class cancel_eh : public event_handler {
-    bool m_canceled = false;
+    std::mutex m_mutex;
+    std::atomic<bool> 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; }
 };
-

src/util/scoped_ctrl_c.cpp

@@ -16,45 +16,49 @@ Author:
 Revision History:
 
 --*/
-#include<signal.h>
+#include <mutex>
+#include <vector>
+#include <signal.h>
 #include "util/scoped_ctrl_c.h"
 #include "util/gparams.h"
 
-static scoped_ctrl_c * g_obj = nullptr;
+static std::vector<scoped_ctrl_c*> 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) {
+    std::lock_guard lock(g_list_mutex);
-        g_obj->m_cancel_eh(CTRL_C_EH_CALLER);
+    for (auto handler : g_list) {
-        if (g_obj->m_once) {
+        if (handler->m_enabled) {
-            g_obj->m_first = false;
+            handler->m_cancel_eh(CTRL_C_EH_CALLER);
-            signal(SIGINT, on_ctrl_c); // re-install the handler
         }
     }
-    else {
+    signal(SIGINT, g_old_handler);
-        signal(SIGINT, g_obj->m_old_handler); 
-        raise(SIGINT);
-    }
 }
 
-scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled):
+scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool enabled):
-    m_cancel_eh(eh), 
+    m_cancel_eh(eh),
-    m_first(true),
+    m_enabled(enabled) {
-    m_once(once),
+    if (enabled && gparams::get_value("ctrl_c") == "false")
-    m_enabled(enabled),
-    m_old_scoped_ctrl_c(g_obj) {
-    if (gparams::get_value("ctrl_c") == "false")
         m_enabled = false;
+
     if (m_enabled) {
-        g_obj = this;
+        std::lock_guard lock(g_list_mutex);
-        m_old_handler = signal(SIGINT, on_ctrl_c); 
+        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;
+        std::lock_guard lock(g_list_mutex);
-        if (m_old_handler != SIG_ERR) {
+        auto it = std::find(g_list.begin(), g_list.end(), this);
-            signal(SIGINT, m_old_handler);
+        SASSERT(it != g_list.end());
+        g_list.erase(it);
+        if (g_list.empty()) {
+            signal(SIGINT, g_old_handler);
         }
     }
 }

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; }
 };
-