diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-07-08 23:24:24 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-08 16:24:24 -0500 |
commit | a0a389a1f7c16b6a1fb56b3ce8ee519cf5717f04 (patch) | |
tree | 6908a4c3aed1be0100057c5b8f97a40673c99779 /src/main | |
parent | 37801c1da918ad1c4de97e8a64ca7d1177b61de4 (diff) |
Re-implement handling of --tlimit (#4655)
As a first step within this project, this PR provides a new implementation that backs --tlimit. It uses setitimer (as timer_settime is not available on MacOS) to make the OS send a signal after the given wall clock time has passed.
In more detail, this PR:
removes the current handling of --tlimit (TlimitListener and its integration in the NodeManager)
adds a new TimeLimitListener that lives in src/main
uses TimeLimitListener directly in runCvc4()
adds a signal handler for SIGALRM (that also uses the existing timeout_handler)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 3 | ||||
-rw-r--r-- | src/main/time_limit.cpp | 32 | ||||
-rw-r--r-- | src/main/time_limit.h | 21 | ||||
-rw-r--r-- | src/main/util.cpp | 10 |
5 files changed, 67 insertions, 1 deletions
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 96e0078ed..723d6346f 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -6,6 +6,8 @@ set(libmain_src_files interactive_shell.cpp interactive_shell.h main.h + time_limit.cpp + time_limit.h util.cpp ) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 374f68257..955fa7b74 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -32,6 +32,7 @@ #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" +#include "main/time_limit.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -98,6 +99,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Parse the options vector<string> filenames = Options::parseOptions(&opts, argc, argv); + install_time_limit(opts); + string progNameStr = opts.getBinaryName(); progName = &progNameStr; diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp new file mode 100644 index 000000000..973d48f6f --- /dev/null +++ b/src/main/time_limit.cpp @@ -0,0 +1,32 @@ +#include "time_limit.h" + +#include <sys/time.h> + +#include <cerrno> +#include <cstring> + +namespace CVC4 { +namespace main { + +void install_time_limit(const Options& opts) +{ + unsigned long ms = opts.getCumulativeTimeLimit(); + if (ms == 0) return; + + // Check https://linux.die.net/man/2/setitimer + struct itimerval timerspec; + timerspec.it_value.tv_sec = ms / 1000; + timerspec.it_value.tv_usec = (ms % 1000) * 1000; + timerspec.it_interval.tv_sec = 0; + timerspec.it_interval.tv_usec = 0; + // Argument 1: which timer to set, we want the real time + // Argument 2: timer configuration, relative to current time + // Argument 3: old timer configuration, we don't want to know + if (setitimer(ITIMER_REAL, &timerspec, nullptr)) + { + throw Exception(std::string("timer_settime() failure: ") + strerror(errno)); + } +} + +} // namespace main +} // namespace CVC4 diff --git a/src/main/time_limit.h b/src/main/time_limit.h new file mode 100644 index 000000000..ba179fea0 --- /dev/null +++ b/src/main/time_limit.h @@ -0,0 +1,21 @@ +#ifndef CVC4__MAIN__TIME_LIMIT_H +#define CVC4__MAIN__TIME_LIMIT_H + +#include "options/options.h" + +namespace CVC4 { +namespace main { + +/** + * Installs an overall wall-clock time limit for the solver binary. + * It retrieves the time limit and creates a POSIX timer (via setitimer()). + * This timer signals its expiration with an SIGALRM that is handled by + * timeout_handler() in util.cpp. + */ + +void install_time_limit(const Options& opts); + +} // namespace main +} // namespace CVC4 + +#endif /* CVC4__MAIN__TIME_LIMIT_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp index 69f79e56c..888cb7645 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -70,7 +70,7 @@ size_t cvc4StackSize; void* cvc4StackBase; #endif /* HAVE_SIGALTSTACK */ -/** Handler for SIGXCPU, i.e., timeout. */ +/** Handler for SIGXCPU and SIGALRM, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n"); print_statistics(); @@ -298,6 +298,14 @@ void cvc4_init() throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno)); } + struct sigaction act2b; + act2b.sa_sigaction = timeout_handler; + act2b.sa_flags = SA_SIGINFO; + sigemptyset(&act2b.sa_mask); + if(sigaction(SIGALRM, &act2b, NULL)) { + throw Exception(string("sigaction(SIGALRM) failure: ") + strerror(errno)); + } + struct sigaction act3; act3.sa_sigaction = ill_handler; act3.sa_flags = SA_SIGINFO; |