From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 8 Jul 2020 21:24:24 +0000 (+0200)
Subject: Re-implement handling of --tlimit (#4655)
X-Git-Tag: cvc5-1.0.0~3141
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0a389a1f7c16b6a1fb56b3ce8ee519cf5717f04;p=cvc5.git

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 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;
diff --git a/src/options/options.h b/src/options/options.h
index e0f68a182..0732d4ddb 100644
--- 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 26cf14dfe..c8104c584 100644
--- 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 0a3d65167..13791bfd6 100644
--- 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"