SignalHandlerGuard Class Reference

Sets a new signal handler and restores the old one when it goes out of scope. More...

#include </home/soonhokong/work/dreal4/dreal/util/signal_handler_guard.h>

Public Types
using	handler_t = void(*)(int)

Public Member Functions
	SignalHandlerGuard (int sig, handler_t handler, volatile std::atomic_bool *flag)
	Registers the new handler and saves the current one.
	SignalHandlerGuard (const SignalHandlerGuard &)=delete
	SignalHandlerGuard (SignalHandlerGuard &&)=delete
SignalHandlerGuard &	operator= (const SignalHandlerGuard &)=delete
SignalHandlerGuard &	operator= (SignalHandlerGuard &&)=delete
	~SignalHandlerGuard ()
	Restores the old signal handler. If the flag is set, clear it.

Detailed Description

Sets a new signal handler and restores the old one when it goes out of scope.

When the flag is set, its destructor clears it out.

Motivation

Python's signal handler merely set a flag which is only checked in the next python instruction. As a result, "C/C++ code may run uninterrupted for an arbitrary amount of time" (from : https://docs.python.org/3/library/signal.html#execution-of-python-signal-handlers)

Our approach

We provide a custom signal handler for SIGINT, which sets a global flag (g_interrupted) which is monitored inside of dReal code. When the flag is set, the checking code is supposed to throw an exception, which will terminate the C++ call gracefully. The C++ exception will be handled by pybind11, which will translate it to a Python exception.

---

The documentation for this class was generated from the following files:

• /home/soonhokong/work/dreal4/dreal/util/signal_handler_guard.h
• /home/soonhokong/work/dreal4/dreal/util/signal_handler_guard.cc