summaryrefslogtreecommitdiff
path: root/src/main/time_limit.cpp
blob: be506a51882d6f80655857bca1cb2398eb0ce312 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
/*********************                                                        */
/*! \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;
  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));
  }
#endif
}

}  // namespace main
}  // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback