Add SIGINT handling in Solver on POSIX systems

src/bin/ibexsolve.cpp

@@ -13,7 +13,7 @@
 
 #include "ibex.h"
 #include "ibexsolve.h"
-
+#include "ibex_signals.h"
 #include <sstream>
 
 using namespace std;
@@ -223,6 +223,11 @@ int main(int argc, char** argv) {
 		if (!quiet)
 			cout << "running............" << endl << endl;
 
+		if(ibex::signals::support_signals()) {
+			ibex::signals::set_catch_SIGINT(true);
+			s.allow_sigint = true;
+		}
+
 		// Get the solutions
 		if (input_file)
 			s.solve(input_file.Get().c_str());
@@ -257,3 +262,4 @@ int main(int argc, char** argv) {
 		cout << e << endl;
 	}
 }
+

src/data/ibex_CovSolverData.cpp

@@ -188,6 +188,8 @@ ifstream* CovSolverData::read(const char* filename, CovSolverData& cov, std::sta
 		case 2: cov.data->_solver_solver_status = (unsigned int) Solver::NOT_ALL_VALIDATED; break;
 		case 3: cov.data->_solver_solver_status = (unsigned int) Solver::TIME_OUT;          break;
 		case 4: cov.data->_solver_solver_status = (unsigned int) Solver::CELL_OVERFLOW;     break;
+		case 5: cov.data->_solver_solver_status = (unsigned int) Solver::USER_ABORT;     	break;
+
 		default: ibex_error("[CovSolverData]: invalid solver status.");
 		}
 

src/solver/ibex_Solver.cpp

@@ -1,5 +1,5 @@
 //============================================================================
-//                                  I B E X                                   
+//                                  I B E X
 // File        : ibex_Solver.cpp
 // Author      : Gilles Chabert
 // Copyright   : IMT Atlantique (France)
@@ -13,6 +13,7 @@
 #include "ibex_NoBisectableVariableException.h"
 #include "ibex_LinearException.h"
 #include "ibex_CovSolverData.h"
+#include "ibex_signals.h"
 
 #include <cassert>
 
@@ -285,11 +286,16 @@ Solver::Status Solver::solve() {
 
 			if (status==CovSolverData::UNKNOWN)
 				final_status=NOT_ALL_VALIDATED;
+			if (allow_sigint)
+				ibex::signals::check_SIGINT();
 		}
 	} catch(CellLimitException&) {
 		final_status=CELL_OVERFLOW;
 	} catch(TimeOutException&) {
 		final_status=TIME_OUT;
+	} catch(ibex::signals::SignalSIGINT&) {
+		std::cout << "ibex::Solver: SIGINT received, aborting search..." << std::endl;
+		final_status=USER_ABORT;
 	}
 
 	manif->set_solver_status(final_status);
@@ -509,20 +515,24 @@ const char* white() {
 void Solver::report() {
 
 	switch ((Status) manif->solver_status()) {
-	case SUCCESS: 
+	case SUCCESS:
 		cout << green() << " solving successful!" << endl;
 		break;
-	case INFEASIBLE: 
+	case INFEASIBLE:
 		cout << red() << " infeasible problem" << endl;
 		break;
-	case NOT_ALL_VALIDATED: 
+	case NOT_ALL_VALIDATED:
 		cout << red() << " done! but some boxes have 'unknown' status." << endl;
 		break;
-	case TIME_OUT: 
+	case TIME_OUT:
 		cout << red() << " time limit " << time_limit << "s. reached " << endl;
 		break;
-	case CELL_OVERFLOW: 
+	case CELL_OVERFLOW:
 		cout << red() << " cell overflow" << endl;
+		break;
+	case USER_ABORT:
+		cout << red() << " user abort" << endl;
+		break;
 	}
 
 	cout << white() << endl;

src/solver/ibex_Solver.h

@@ -1,5 +1,5 @@
 //============================================================================
-//                                  I B E X                                   
+//                                  I B E X
 // File        : ibex_Solver.h
 // Author      : Gilles Chabert
 // Copyright   : IMT Atlantique (France)
@@ -47,7 +47,7 @@ class Solver {
 	 *
 	 * See comments for solve(...) below.
 	 */
-	typedef enum { SUCCESS, INFEASIBLE, NOT_ALL_VALIDATED, TIME_OUT, CELL_OVERFLOW } Status;
+	typedef enum { SUCCESS, INFEASIBLE, NOT_ALL_VALIDATED, TIME_OUT, CELL_OVERFLOW, USER_ABORT } Status;
 
 	/**
 	 * \brief Boundary test strength
@@ -90,7 +90,7 @@ class Solver {
 	 * \brief Solve the system (non-interactive mode).
 	 *
 	 * \param init_box - the initial box (the search space)
-	 * 
+	 *
 	 * \return Possible values:
 	 *
 	 *   SUCCESS:           (complete search) all solutions found and all
@@ -107,6 +107,7 @@ class Solver {
 	 *   CELL_OVERFLOW:     (incomplete search) cell overflow : the number of
 	 *                      cell has exceeded the limit.
 	 *
+	 *   USER_ABORT:		(incomplete search) search has been aborted by the user.
 	 * The vector of "solutions" (output boxes) found by the solver
 	 * are retrieved with #get_solutions().
 	 */
@@ -206,7 +207,7 @@ class Solver {
 	 * generally, a sequence (with or without fixpoint) of different contractors (HC4,
 	 * Acid, Newton, a linear relaxation, ... )
 	 *
-	 */ 
+	 */
 	Ctc& ctc;
 
 	/**
@@ -262,6 +263,12 @@ class Solver {
 	 */
 	int trace;
 
+	/**
+	 * \brief Wether SIGINT catching is allowed, using SignalHandler.
+	 * Should always be false in a multithreaded context.
+	 */
+	bool allow_sigint = false;
+
 
 protected:
 	/**

src/tools/ibex_signals.cpp

@@ -0,0 +1,68 @@
+//============================================================================
+//                                  I B E X
+// File        : ibex_signals.cpp
+// Author      : Antoine Marendet
+// Copyright   : IMT Atlantique (France)
+// License     : See the LICENSE file
+// Created     : Feb 5, 2020
+// Last Update : Feb 5, 2020
+//============================================================================
+
+#include "ibex_signals.h"
+#include <iostream>
+
+namespace ibex {
+
+#ifdef IBEX_POSIX_SIGNALS
+namespace {
+    // 0 if no SIGINT received, 1 otherwise
+    sig_atomic_t sigint = 0;
+    // sigaction handler
+    struct sigaction sigint_handler;
+    /* Store the old sigaction handler, to reset the manager to its previous behaviour
+     * when deactivating signals
+     */
+    struct sigaction* old_sigaction = NULL;
+
+    // sigaction action to perform when receiving SIGINT
+    void sigint_action(int signal_value) {
+        pid_t pid = getpid();
+        std::cout << " SIGINT received on PID " << pid << std::endl;
+        sigint = 1;
+    }
+
+} // anonymous namespace
+#endif // _POSIX_VERSION
+
+namespace signals {
+
+void set_catch_SIGINT(bool turn_on) {
+#ifdef IBEX_POSIX_SIGNALS
+    if(turn_on) {
+        sigint_handler.sa_handler = sigint_action;
+	    sigemptyset(&sigint_handler.sa_mask);
+	    sigint_handler.sa_flags = 0;
+        sigaction(SIGINT, &sigint_handler, old_sigaction);
+    } else {
+        sigaction(SIGINT, old_sigaction, NULL);
+    }
+#else
+    if(turn_on) {
+        ibex_warning("Signals not supported on this system.");
+    }
+#endif
+}
+
+void check_SIGINT() {
+#ifdef IBEX_POSIX_SIGNALS
+    if(sigint) {
+        // Clear sigint
+        sigint = 0;
+        throw SignalSIGINT();
+    }
+#endif
+}
+
+} // namespace signals
+
+} // namespace ibex

src/tools/ibex_signals.h

@@ -0,0 +1,60 @@
+//============================================================================
+//                                  I B E X
+// File        : ibex_signals.h
+// Author      : Antoine Marendet
+// Copyright   : IMT Atlantique (France)
+// License     : See the LICENSE file
+// Created     : Feb 5, 2020
+// Last Update : Feb 5, 2020
+//============================================================================
+
+#ifndef __IBEX_SIGNALS_H__
+#define __IBEX_SIGNALS_H__
+
+#include "ibex_Exception.h"
+
+#ifdef HAVE_UNISTD_H
+    #include <unistd.h>
+#endif
+// if _POSIX_VERSION is defined in unistd.h, we can use the POSIX-1 specification
+#if defined(HAVE_SIGNAL_H) && defined(_POSIX_VERSION)
+    #include <signal.h>
+    #define IBEX_POSIX_SIGNALS
+#endif
+
+namespace ibex {
+
+/**
+ * \brief Helper functions for OS signals handling
+ */
+namespace signals {
+
+class SignalSIGINT: Exception { };
+
+/**
+ * \brief Return true if the current version of Ibex supports signals.
+ */
+constexpr bool support_signals() {
+#ifdef IBEX_POSIX_SIGNALS
+    return true;
+#else
+    return false;
+#endif
+}
+
+/**
+ * \brief Activate or deactivate SIGINT catching on POSIX compliant systems.
+ *
+ * Do not use in a multithreaded context.
+ */
+void set_catch_SIGINT(bool turn_on);
+
+/**
+ * \brief Throw SignalSIGINT if a SIGINT has been received since the last call to this function.
+ */
+void check_SIGINT();
+
+} // namespace signals
+} // namespace ibex
+
+#endif  // __IBEX_SIGNALS_H__

wscript

@@ -85,10 +85,14 @@ def configure (conf):
 		conf.env.DEBUG = False
 	for f in flags.split():
 		conf.check_cxx(cxxflags=f, use="IBEX", mandatory=False, uselib_store="IBEX")
-	
+
 	# To fix Windows compilation problem (strdup with std=c++11, see issue #287)
 	conf.check_cxx(cxxflags = "-U__STRICT_ANSI__", uselib_store="IBEX")
 
+	# Check for unistd.h and signal.h compliance
+	conf.check_cxx(header_name="unistd.h", mandatory=False, uselib_store="IBEX")
+	conf.check_cxx(header_name="signal.h", mandatory=False, uselib_store="IBEX")
+
 	# Build as shared lib is asked
 	conf.start_msg ("Ibex will be built as a")
 	if conf.options.ENABLE_SHARED: