Implement --tlimit for windows (#4716)

The new mechanism for --tlimit only works for POSIX compatible systems (that implement setitimer). This PR implements an alternative (though roughly equivalent) approach for windows, based on SetWaitableTimer().

To make this work (without code duplication) we need to call the timeout_handler function from time_limit.cpp as the windows solution employs an asynchronous callback instead of signals. I used the opportunity to rename util.cpp to signal_handlers.cpp (as it really does not do anything else) and reformat the file.

As I do not have a windows system at hand, I have not been able to actually test this apart from making sure that it compiles with the mingw setup.

6 files changed, 238 insertions, 68 deletions

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 723d6346f..4fbb14183 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -6,9 +6,10 @@ set(libmain_src_files
   interactive_shell.cpp
   interactive_shell.h
   main.h
+  signal_handlers.cpp
+  signal_handlers.h
   time_limit.cpp
   time_limit.h
-  util.cpp
 )
 
 #-----------------------------------------------------------------------------#
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 955fa7b74..b8d845f9e 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/signal_handlers.h"
 #include "main/time_limit.h"
 #include "options/options.h"
 #include "options/set_language.h"
@@ -92,7 +93,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   pOptions = &opts;
 
   // Initialize the signal handlers
-  cvc4_init();
+  signal_handlers::install();
 
   progPath = argv[0];
 
@@ -507,7 +508,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   pTotalTime = NULL;
   pExecutor = NULL;
 
-  cvc4_shutdown();
+  signal_handlers::cleanup();
 
   return returnValue;
 }
diff --git a/src/main/util.cpp b/src/main/signal_handlers.cpp
index 888cb7645..6f24dfc9b 100644
--- a/src/main/util.cpp
+++ b/src/main/signal_handlers.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file util.cpp
+/*! \file signal_handlers.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Morgan Deters, Andres Noetzli, Tim King
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Utilities for the main driver.
+ ** \brief Implementation of signal handlers.
  **
- ** Utilities for the main driver.
+ ** Implementation of signal handlers.
  **
  ** It is important to only call async-signal-safe functions from signal
  ** handlers. See: http://man7.org/linux/man-pages/man7/signal-safety.7.html for
@@ -19,6 +19,7 @@
  **/
 
 #include <string.h>
+
 #include <cerrno>
 #include <cstdio>
 #include <cstdlib>
@@ -54,15 +55,27 @@ namespace main {
  */
 bool segvSpin = false;
 
-void print_statistics() {
-  if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL) {
-    if (pTotalTime != NULL && pTotalTime->running()) {
+namespace signal_handlers {
+
+void print_statistics()
+{
+  if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL)
+  {
+    if (pTotalTime != NULL && pTotalTime->running())
+    {
       pTotalTime->stop();
     }
     pExecutor->safeFlushStatistics(STDERR_FILENO);
   }
 }
 
+void timeout_handler()
+{
+  safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n");
+  print_statistics();
+  abort();
+}
+
 #ifndef __WIN32__
 
 #ifdef HAVE_SIGALTSTACK
@@ -71,11 +84,7 @@ void* cvc4StackBase;
 #endif /* HAVE_SIGALTSTACK */
 
 /** 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();
-  abort();
-}
+void timeout_handler(int sig, siginfo_t* info, void*) { timeout_handler(); }
 
 /** Handler for SIGTERM. */
 void sigterm_handler(int sig, siginfo_t* info, void*)
@@ -86,7 +95,8 @@ void sigterm_handler(int sig, siginfo_t* info, void*)
 }
 
 /** Handler for SIGINT, i.e., when the user hits control C. */
-void sigint_handler(int sig, siginfo_t* info, void*) {
+void sigint_handler(int sig, siginfo_t* info, void*)
+{
   safe_print(STDERR_FILENO, "CVC4 interrupted by user.\n");
   print_statistics();
   abort();
@@ -94,7 +104,8 @@ void sigint_handler(int sig, siginfo_t* info, void*) {
 
 #ifdef HAVE_SIGALTSTACK
 /** Handler for SIGSEGV (segfault). */
-void segv_handler(int sig, siginfo_t* info, void* c) {
+void segv_handler(int sig, siginfo_t* info, void* c)
+{
   uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize;
   uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr);
 #ifdef CVC4_DEBUG
@@ -102,23 +113,29 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   safe_print(STDERR_FILENO, "Offending address is ");
   safe_print(STDERR_FILENO, info->si_addr);
   safe_print(STDERR_FILENO, "\n");
-  //cerr << "base is " << (void*)cvc4StackBase << endl;
-  //cerr << "size is " << cvc4StackSize << endl;
-  //cerr << "extent is " << (void*)extent << endl;
-  if(addr >= extent && addr <= extent + 10*1024) {
+  // cerr << "base is " << (void*)cvc4StackBase << endl;
+  // cerr << "size is " << cvc4StackSize << endl;
+  // cerr << "extent is " << (void*)extent << endl;
+  if (addr >= extent && addr <= extent + 10 * 1024)
+  {
     safe_print(STDERR_FILENO,
                "Looks like this is likely due to stack overflow.\n");
     safe_print(STDERR_FILENO,
                "You might consider increasing the limit with `ulimit -s' or "
                "equivalent.\n");
-  } else if(addr < 10*1024) {
+  }
+  else if (addr < 10 * 1024)
+  {
     safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
   }
 
-  if(!segvSpin) {
+  if (!segvSpin)
+  {
     print_statistics();
     abort();
-  } else {
+  }
+  else
+  {
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
@@ -131,22 +148,26 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
     safe_print(STDERR_FILENO, " ");
     safe_print(STDERR_FILENO, *progName);
     safe_print(STDERR_FILENO, "\n");
-    for(;;) {
+    for (;;)
+    {
       sleep(60);
     }
   }
-#else /* CVC4_DEBUG */
+#else  /* CVC4_DEBUG */
   safe_print(STDERR_FILENO, "CVC4 suffered a segfault.\n");
   safe_print(STDERR_FILENO, "Offending address is ");
   safe_print(STDERR_FILENO, info->si_addr);
   safe_print(STDERR_FILENO, "\n");
-  if(addr >= extent && addr <= extent + 10*1024) {
+  if (addr >= extent && addr <= extent + 10 * 1024)
+  {
     safe_print(STDERR_FILENO,
                "Looks like this is likely due to stack overflow.\n");
     safe_print(STDERR_FILENO,
                "You might consider increasing the limit with `ulimit -s' or "
                "equivalent.\n");
-  } else if(addr < 10*1024) {
+  }
+  else if (addr < 10 * 1024)
+  {
     safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
   }
   print_statistics();
@@ -156,14 +177,18 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 #endif /* HAVE_SIGALTSTACK */
 
 /** Handler for SIGILL (illegal instruction). */
-void ill_handler(int sig, siginfo_t* info, void*) {
+void ill_handler(int sig, siginfo_t* info, void*)
+{
 #ifdef CVC4_DEBUG
   safe_print(STDERR_FILENO,
              "CVC4 executed an illegal instruction in DEBUG mode.\n");
-  if(!segvSpin) {
+  if (!segvSpin)
+  {
     print_statistics();
     abort();
-  } else {
+  }
+  else
+  {
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
@@ -176,11 +201,12 @@ void ill_handler(int sig, siginfo_t* info, void*) {
     safe_print(STDERR_FILENO, " ");
     safe_print(STDERR_FILENO, *progName);
     safe_print(STDERR_FILENO, "\n");
-    for(;;) {
+    for (;;)
+    {
       sleep(60);
     }
   }
-#else /* CVC4_DEBUG */
+#else  /* CVC4_DEBUG */
   safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction.\n");
   print_statistics();
   abort();
@@ -191,7 +217,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
 
 static terminate_handler default_terminator;
 
-void cvc4unexpected() {
+void cvc4unexpected()
+{
 #if defined(CVC4_DEBUG) && !defined(__WIN32__)
   safe_print(STDERR_FILENO,
              "\n"
@@ -201,19 +228,25 @@ void cvc4unexpected() {
 
   const char* lastContents = LastExceptionBuffer::currentContents();
 
-  if(lastContents == NULL) {
+  if (lastContents == NULL)
+  {
     safe_print(
         STDERR_FILENO,
         "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
-  } else {
+  }
+  else
+  {
     safe_print(STDERR_FILENO, "The exception is:\n");
     safe_print(STDERR_FILENO, lastContents);
     safe_print(STDERR_FILENO, "\n\n");
   }
-  if(!segvSpin) {
+  if (!segvSpin)
+  {
     print_statistics();
     set_terminate(default_terminator);
-  } else {
+  }
+  else
+  {
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
@@ -226,18 +259,20 @@ void cvc4unexpected() {
     safe_print(STDERR_FILENO, " ");
     safe_print(STDERR_FILENO, *progName);
     safe_print(STDERR_FILENO, "\n");
-    for(;;) {
+    for (;;)
+    {
       sleep(60);
     }
   }
-#else /* CVC4_DEBUG */
+#else  /* CVC4_DEBUG */
   safe_print(STDERR_FILENO, "CVC4 threw an \"unexpected\" exception.\n");
   print_statistics();
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
 }
 
-void cvc4terminate() {
+void cvc4terminate()
+{
   set_terminate(default_terminator);
 #ifdef CVC4_DEBUG
   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
@@ -251,7 +286,7 @@ void cvc4terminate() {
              "(Don't do that.)\n");
   print_statistics();
   default_terminator();
-#else /* CVC4_DEBUG */
+#else  /* CVC4_DEBUG */
   safe_print(STDERR_FILENO,
              "CVC4 was terminated by the C++ runtime.\n"
              "Perhaps an exception was thrown during stack unwinding.\n");
@@ -260,8 +295,7 @@ void cvc4terminate() {
 #endif /* CVC4_DEBUG */
 }
 
-/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
-void cvc4_init()
+void install()
 {
 #ifdef CVC4_DEBUG
   LastExceptionBuffer::setCurrent(new LastExceptionBuffer());
@@ -269,15 +303,19 @@ void cvc4_init()
 
 #ifndef __WIN32__
   struct rlimit limit;
-  if(getrlimit(RLIMIT_STACK, &limit)) {
+  if (getrlimit(RLIMIT_STACK, &limit))
+  {
     throw Exception(string("getrlimit() failure: ") + strerror(errno));
   }
-  if(limit.rlim_cur != limit.rlim_max) {
+  if (limit.rlim_cur != limit.rlim_max)
+  {
     limit.rlim_cur = limit.rlim_max;
-    if(setrlimit(RLIMIT_STACK, &limit)) {
+    if (setrlimit(RLIMIT_STACK, &limit))
+    {
       throw Exception(string("setrlimit() failure: ") + strerror(errno));
     }
-    if(getrlimit(RLIMIT_STACK, &limit)) {
+    if (getrlimit(RLIMIT_STACK, &limit))
+    {
       throw Exception(string("getrlimit() failure: ") + strerror(errno));
     }
   }
@@ -286,7 +324,8 @@ void cvc4_init()
   act1.sa_sigaction = sigint_handler;
   act1.sa_flags = SA_SIGINFO;
   sigemptyset(&act1.sa_mask);
-  if(sigaction(SIGINT, &act1, NULL)) {
+  if (sigaction(SIGINT, &act1, NULL))
+  {
     throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
   }
 
@@ -294,35 +333,31 @@ void cvc4_init()
   act2.sa_sigaction = timeout_handler;
   act2.sa_flags = SA_SIGINFO;
   sigemptyset(&act2.sa_mask);
-  if(sigaction(SIGXCPU, &act2, NULL)) {
+  if (sigaction(SIGXCPU, &act2, NULL))
+  {
     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;
   sigemptyset(&act3.sa_mask);
-  if(sigaction(SIGILL, &act3, NULL)) {
+  if (sigaction(SIGILL, &act3, NULL))
+  {
     throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
   }
 
 #ifdef HAVE_SIGALTSTACK
   stack_t ss;
-  ss.ss_sp = (char*) malloc(SIGSTKSZ);
-  if(ss.ss_sp == NULL) {
+  ss.ss_sp = (char*)malloc(SIGSTKSZ);
+  if (ss.ss_sp == NULL)
+  {
     throw Exception("Can't malloc() space for a signal stack");
   }
   ss.ss_size = SIGSTKSZ;
   ss.ss_flags = 0;
-  if(sigaltstack(&ss, NULL) == -1) {
+  if (sigaltstack(&ss, NULL) == -1)
+  {
     throw Exception(string("sigaltstack() failure: ") + strerror(errno));
   }
 
@@ -333,7 +368,8 @@ void cvc4_init()
   act4.sa_sigaction = segv_handler;
   act4.sa_flags = SA_SIGINFO | SA_ONSTACK;
   sigemptyset(&act4.sa_mask);
-  if(sigaction(SIGSEGV, &act4, NULL)) {
+  if (sigaction(SIGSEGV, &act4, NULL))
+  {
     throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
   }
 #endif /* HAVE_SIGALTSTACK */
@@ -349,11 +385,11 @@ void cvc4_init()
 
 #endif /* __WIN32__ */
 
-  set_unexpected(cvc4unexpected);
+  std::set_unexpected(cvc4unexpected);
   default_terminator = set_terminate(cvc4terminate);
 }
 
-void cvc4_shutdown() noexcept
+void cleanup() noexcept
 {
 #ifndef __WIN32__
 #ifdef HAVE_SIGALTSTACK
@@ -364,5 +400,6 @@ void cvc4_shutdown() noexcept
 #endif /* __WIN32__ */
 }
 
-}/* CVC4::main namespace */
-}/* CVC4 namespace */
+}  // namespace signal_handlers
+}  // namespace main
+}  // namespace CVC4
diff --git a/src/main/signal_handlers.h b/src/main/signal_handlers.h
new file mode 100644
index 000000000..cc1917418
--- /dev/null
+++ b/src/main/signal_handlers.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file signal_handlers.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of signal handlers.
+ **
+ ** Implementation of signal handlers.
+ **/
+
+#ifndef CVC4__MAIN__SIGNAL_HANDLERS_H
+#define CVC4__MAIN__SIGNAL_HANDLERS_H
+
+namespace CVC4 {
+namespace main {
+namespace signal_handlers {
+
+/**
+ * Performs last steps before termination due to a timeout.
+ * Prints an appropriate message and solver statistics.
+ */
+void timeout_handler();
+
+/**
+ * Installs (almost) all signal handlers.
+ * A handler for SIGALRM is set in time_limit.cpp.
+ * Also sets callbacks via std::set_unexpected and std:set_terminate.
+ */
+void install();
+
+/**
+ * Performs cleanup related to the signal handlers.
+ */
+void cleanup();
+
+}  // namespace signal_handlers
+}  // namespace main
+}  // namespace CVC4
+
+#endif /* CVC4__MAIN__SIGNAL_HANDLERS_H */
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index 973d48f6f..fb07b5523 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -1,19 +1,86 @@
+/*********************                                                        */
+/*! \file time_limit.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of time limits.
+ **
+ ** Implementation of time limits that are imposed by the --tlimit option.
+ **/
+
 #include "time_limit.h"
 
+#if defined(__MINGW32__) || defined(__MINGW64__)
+#include <windows.h>
+#else
+#include <signal.h>
 #include <sys/time.h>
+#endif
 
 #include <cerrno>
 #include <cstring>
 
+#include "signal_handlers.h"
+
 namespace CVC4 {
 namespace main {
 
+#if defined(__MINGW32__) || defined(__MINGW64__)
+void CALLBACK win_timeout_handler(LPVOID lpArg,
+                                  DWORD dwTimerLowValue,
+                                  DWORD dwTimerHighValue)
+{
+  signal_handlers::timeout_handler();
+}
+#else
+void posix_timeout_handler(int sig, siginfo_t* info, void*)
+{
+  signal_handlers::timeout_handler();
+}
+#endif
+
 void install_time_limit(const Options& opts)
 {
   unsigned long ms = opts.getCumulativeTimeLimit();
+  // Skip if no time limit shall be set.
   if (ms == 0) return;
 
+#if defined(__MINGW32__) || defined(__MINGW64__)
+  HANDLE hTimer = CreateWaitableTimer(nullptr, true, TEXT("CVC4::Timeout"));
+  if (hTimer == nullptr)
+  {
+    throw Exception(std::string("CreateWaitableTimer() failure: ")
+                    + std::to_string(GetLastError()));
+  }
+  LARGE_INTEGER liDueTime;
+  liDueTime.LowPart = (DWORD)(ms & 0xFFFFFFFF);
+  liDueTime.HighPart = 0;
+  if (!SetWaitableTimer(
+          hTimer, &liDueTime, 0, win_timeout_handler, nullptr, false))
+  {
+    throw Exception(std::string("SetWaitableTimer() failure: ")
+                    + std::to_string(GetLastError()));
+  }
+#else
+  // Install a signal handler for SIGALRM
+  struct sigaction sact;
+  sact.sa_sigaction = posix_timeout_handler;
+  sact.sa_flags = SA_SIGINFO;
+  sigemptyset(&sact.sa_mask);
+  if (sigaction(SIGALRM, &sact, NULL))
+  {
+    throw Exception(std::string("sigaction(SIGALRM) failure: ")
+                    + strerror(errno));
+  }
+
   // Check https://linux.die.net/man/2/setitimer
+  // Then time is up, the kernel will send a SIGALRM
   struct itimerval timerspec;
   timerspec.it_value.tv_sec = ms / 1000;
   timerspec.it_value.tv_usec = (ms % 1000) * 1000;
@@ -26,6 +93,7 @@ void install_time_limit(const Options& opts)
   {
     throw Exception(std::string("timer_settime() failure: ") + strerror(errno));
   }
+#endif
 }
 
 }  // namespace main
diff --git a/src/main/time_limit.h b/src/main/time_limit.h
index ba179fea0..4da3e6845 100644
--- a/src/main/time_limit.h
+++ b/src/main/time_limit.h
@@ -1,3 +1,19 @@
+/*********************                                                        */
+/*! \file time_limit.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of time limits.
+ **
+ ** Implementation of time limits that are imposed by the --tlimit option.
+ **/
+
 #ifndef CVC4__MAIN__TIME_LIMIT_H
 #define CVC4__MAIN__TIME_LIMIT_H
 
@@ -10,9 +26,10 @@ 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.
+ * timeout_handler() in signal_handler.cpp.
+ * For windows, we use a timer (via SetWaitableTimer()) that uses
+ * timeout_handler() as callback function.
  */
-
 void install_time_limit(const Options& opts);
 
 }  // namespace main