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)

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 96e0078ed0eae2a3e7e5e58a1688ed0373e4decf..723d6346f76a39e4ac0287c7ebb9d638b97ed602 100644 (file)
--- 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 374f68257120449f85434641dfc4baa7caabe0c4..955fa7b749791de24a92597eae411e76727a4259 100644 (file)
--- 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 (file)
index 0000000..973d48f
--- /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 (file)
index 0000000..ba179fe
--- /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 69f79e56cf6f751b643451b8ed4abdc8a648e913..888cb7645e1ded57650af70edb52e0a501d7a39b 100644 (file)
--- 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;

diff --git a/src/options/options.h b/src/options/options.h
index e0f68a1821cac9dfcb1b3f9629f4d5c2ce3af1d8..0732d4ddb79640e74fa1598223dc28a062b80bdb 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -203,6 +203,7 @@ public:
   bool getStatsHideZeros() const;
   bool getStrictParsing() const;
   int getTearDownIncremental() const;
+  unsigned long getCumulativeTimeLimit() const;
   bool getVersion() const;
   const std::string& getForceLogicString() const;
   int getVerbosity() const;

diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 26cf14dfe488627667e9804e03529ff5a4af6fbb..c8104c58492364de2ea65a39c0e3f5d74bd9ca92 100644 (file)
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -157,6 +157,10 @@ int Options::getTearDownIncremental() const{
   return (*this)[options::tearDownIncremental];
 }
 
+unsigned long Options::getCumulativeTimeLimit() const {
+  return (*this)[options::cumulativeMillisecondLimit];
+}
+
 bool Options::getVersion() const{
   return (*this)[options::version];
 }

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 0a3d6516756a04838d2a527ea85ea59f09eb1ea5..13791bfd6beeff9ad070c6144b9ba476e4733958 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -451,7 +451,7 @@ header = "options/smt_options.h"
   type       = "unsigned long"
   handler    = "limitHandler"
   read_only  = true
-  help       = "enable time limiting (give milliseconds)"
+  help       = "enable time limiting of wall clock time (give milliseconds)"
 
 [[option]]
   name       = "perCallMillisecondLimit"