From f30d3710bfb3c65b55856d7efb99246f13046f56 Mon Sep 17 00:00:00 2001 From: Antoine Marendet Date: Thu, 6 Feb 2020 09:55:49 +0100 Subject: [PATCH 1/3] Add SIGINT handling in Solver on POSIX systems --- src/bin/ibexsolve.cpp | 8 +++++++- src/data/ibex_CovSolverData.cpp | 2 ++ src/solver/ibex_Solver.cpp | 22 ++++++++++++++++------ src/solver/ibex_Solver.h | 15 +++++++++++---- wscript | 6 +++++- 5 files changed, 41 insertions(+), 12 deletions(-) diff --git a/src/bin/ibexsolve.cpp b/src/bin/ibexsolve.cpp index 57297aa77..9d031f0ee 100644 --- a/src/bin/ibexsolve.cpp +++ b/src/bin/ibexsolve.cpp @@ -13,7 +13,7 @@ #include "ibex.h" #include "ibexsolve.h" - +#include "ibex_signals.h" #include using namespace std; @@ -223,6 +223,11 @@ int main(int argc, char** argv) { if (!quiet) cout << "running............" << endl << endl; +#ifdef IBEX_SIGNALS + ibex::signals::set_catch_SIGINT(true); + s.allow_sigint = true; +#endif + // 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; } } + diff --git a/src/data/ibex_CovSolverData.cpp b/src/data/ibex_CovSolverData.cpp index 1593b3b0e..e05dcc178 100644 --- a/src/data/ibex_CovSolverData.cpp +++ b/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."); } diff --git a/src/solver/ibex_Solver.cpp b/src/solver/ibex_Solver.cpp index 7560313e5..8eea51b3b 100644 --- a/src/solver/ibex_Solver.cpp +++ b/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 @@ -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; diff --git a/src/solver/ibex_Solver.h b/src/solver/ibex_Solver.h index 50f411c9a..eed51809c 100644 --- a/src/solver/ibex_Solver.h +++ b/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: /** diff --git a/wscript b/wscript index f431e759f..a8a31edb4 100644 --- a/wscript +++ b/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: From ad1c2a53f983e791d6cccaf3886f22ece9871a22 Mon Sep 17 00:00:00 2001 From: Antoine Marendet Date: Thu, 6 Feb 2020 15:18:56 +0100 Subject: [PATCH 2/3] Add ibex::signals::support_signals() to lessen the need of macros, and more clear implementation --- src/bin/ibexsolve.cpp | 8 ++--- src/tools/ibex_signals.cpp | 68 ++++++++++++++++++++++++++++++++++++++ src/tools/ibex_signals.h | 60 +++++++++++++++++++++++++++++++++ 3 files changed, 132 insertions(+), 4 deletions(-) create mode 100644 src/tools/ibex_signals.cpp create mode 100644 src/tools/ibex_signals.h diff --git a/src/bin/ibexsolve.cpp b/src/bin/ibexsolve.cpp index 9d031f0ee..afa4d1a8c 100644 --- a/src/bin/ibexsolve.cpp +++ b/src/bin/ibexsolve.cpp @@ -223,10 +223,10 @@ int main(int argc, char** argv) { if (!quiet) cout << "running............" << endl << endl; -#ifdef IBEX_SIGNALS - ibex::signals::set_catch_SIGINT(true); - s.allow_sigint = true; -#endif + if(ibex::signals::support_signals()) { + ibex::signals::set_catch_SIGINT(true); + s.allow_sigint = true; + } // Get the solutions if (input_file) diff --git a/src/tools/ibex_signals.cpp b/src/tools/ibex_signals.cpp new file mode 100644 index 000000000..df5e2eab8 --- /dev/null +++ b/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 + +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 \ No newline at end of file diff --git a/src/tools/ibex_signals.h b/src/tools/ibex_signals.h new file mode 100644 index 000000000..9bccff1df --- /dev/null +++ b/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 +#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 + #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__ \ No newline at end of file From e22c36965256179e7146406b687a97156ab4e225 Mon Sep 17 00:00:00 2001 From: Antoine Marendet Date: Thu, 6 Feb 2020 15:21:23 +0100 Subject: [PATCH 3/3] Add newlines --- src/tools/ibex_signals.cpp | 2 +- src/tools/ibex_signals.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tools/ibex_signals.cpp b/src/tools/ibex_signals.cpp index df5e2eab8..9121c5852 100644 --- a/src/tools/ibex_signals.cpp +++ b/src/tools/ibex_signals.cpp @@ -65,4 +65,4 @@ void check_SIGINT() { } // namespace signals -} // namespace ibex \ No newline at end of file +} // namespace ibex diff --git a/src/tools/ibex_signals.h b/src/tools/ibex_signals.h index 9bccff1df..72cd386ed 100644 --- a/src/tools/ibex_signals.h +++ b/src/tools/ibex_signals.h @@ -57,4 +57,4 @@ void check_SIGINT(); } // namespace signals } // namespace ibex -#endif // __IBEX_SIGNALS_H__ \ No newline at end of file +#endif // __IBEX_SIGNALS_H__