Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Mathias Preiner
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Implementation of time limits that are imposed by the --tlimit option.
      14                 :            :  *
      15                 :            :  * There are various strategies to implement time limits, with different
      16                 :            :  * advantages and disadvantages:
      17                 :            :  *
      18                 :            :  * std::thread: we can spawn a new thread which waits for the time limit.
      19                 :            :  * Unless we use std::jthread (from C++20), std::thread is not interruptible
      20                 :            :  * and thus we need a synchronization mechanism so that the main thread can
      21                 :            :  * communicate to the timer thread that it wants to finish. Apparently, this
      22                 :            :  * is the only platform independent way.
      23                 :            :  *
      24                 :            :  * POSIX setitimer: a very simple way that instructs the kernel to send a
      25                 :            :  * signal after some time. If available, this is what we want!
      26                 :            :  *
      27                 :            :  * Win32 CreateWaitableTimer: unfortunately, this mechanism only calls the
      28                 :            :  * completion routine (the callback) when the main thread "enters an
      29                 :            :  * alertable wait state", i.e. it sleeps. We don't want our main thread to
      30                 :            :  * sleep, thus this approach is not appropriate.
      31                 :            :  *
      32                 :            :  * Win32 SetTimer: while we can specify a callback function, we still need
      33                 :            :  * to process the windows event queue for the callback to be called. (see
      34                 :            :  * https://stackoverflow.com/a/15406527/2375725). We don't want our main
      35                 :            :  * thread to continuously monitor the event queue.
      36                 :            :  *
      37                 :            :  *
      38                 :            :  * We thus use the setitimer variant whenever possible, and the std::thread
      39                 :            :  * variant otherwise.
      40                 :            :  */
      41                 :            : 
      42                 :            : #include "time_limit.h"
      43                 :            : 
      44                 :            : #include "base/cvc5config.h"
      45                 :            : 
      46                 :            : #if HAVE_SETITIMER
      47                 :            : #include <signal.h>
      48                 :            : #include <sys/time.h>
      49                 :            : #else
      50                 :            : #include <atomic>
      51                 :            : #include <chrono>
      52                 :            : #include <thread>
      53                 :            : #endif
      54                 :            : 
      55                 :            : #include <cerrno>
      56                 :            : #include <cstring>
      57                 :            : 
      58                 :            : #include "base/exception.h"
      59                 :            : #include "signal_handlers.h"
      60                 :            : 
      61                 :            : namespace cvc5::main {
      62                 :            : 
      63                 :            : #if HAVE_SETITIMER
      64                 :      23967 : TimeLimit::~TimeLimit() {}
      65                 :            : 
      66                 :          0 : void posix_timeout_handler(int sig, siginfo_t* info, void*)
      67                 :            : {
      68                 :          0 :   signal_handlers::timeout_handler();
      69                 :          0 : }
      70                 :            : #else
      71                 :            : std::atomic<bool> abort_timer_flag;
      72                 :            : 
      73                 :            : TimeLimit::~TimeLimit()
      74                 :            : {
      75                 :            :   abort_timer_flag.store(true);
      76                 :            : }
      77                 :            : #endif
      78                 :            : 
      79                 :      23967 : TimeLimit install_time_limit(uint64_t ms)
      80                 :            : {
      81                 :            :   // Skip if no time limit shall be set.
      82         [ +  - ]:      23967 :   if (ms == 0) {
      83                 :      23967 :     return TimeLimit();
      84                 :            :   }
      85                 :            : 
      86                 :            : #if HAVE_SETITIMER
      87                 :            :   // Install a signal handler for SIGALRM
      88                 :            :   struct sigaction sact;
      89                 :          0 :   sact.sa_sigaction = posix_timeout_handler;
      90                 :          0 :   sact.sa_flags = SA_SIGINFO;
      91                 :          0 :   sigemptyset(&sact.sa_mask);
      92         [ -  - ]:          0 :   if (sigaction(SIGALRM, &sact, NULL))
      93                 :            :   {
      94                 :          0 :     throw internal::Exception(std::string("sigaction(SIGALRM) failure: ")
      95                 :          0 :                               + strerror(errno));
      96                 :            :   }
      97                 :            : 
      98                 :            :   // Check https://linux.die.net/man/2/setitimer
      99                 :            :   // Then time is up, the kernel will send a SIGALRM
     100                 :            :   struct itimerval timerspec;
     101                 :          0 :   timerspec.it_value.tv_sec = ms / 1000;
     102                 :          0 :   timerspec.it_value.tv_usec = (ms % 1000) * 1000;
     103                 :          0 :   timerspec.it_interval.tv_sec = 0;
     104                 :          0 :   timerspec.it_interval.tv_usec = 0;
     105                 :            :   // Argument 1: which timer to set, we want the real time
     106                 :            :   // Argument 2: timer configuration, relative to current time
     107                 :            :   // Argument 3: old timer configuration, we don't want to know
     108         [ -  - ]:          0 :   if (setitimer(ITIMER_REAL, &timerspec, nullptr))
     109                 :            :   {
     110                 :          0 :     throw internal::Exception(std::string("timer_settime() failure: ")
     111                 :          0 :                               + strerror(errno));
     112                 :            :   }
     113                 :            : #else
     114                 :            :   abort_timer_flag.store(false);
     115                 :            :   std::thread t([ms]()
     116                 :            :   {
     117                 :            :     // when to stop
     118                 :            :     auto limit = std::chrono::system_clock::now() + std::chrono::milliseconds(ms);
     119                 :            :     while (limit > std::chrono::system_clock::now())
     120                 :            :     {
     121                 :            :       // check if the main thread is done
     122                 :            :       if (abort_timer_flag.load()) return;
     123                 :            :       std::this_thread::sleep_for(std::chrono::milliseconds(100));
     124                 :            :     }
     125                 :            :     // trigger the timeout handler
     126                 :            :     signal_handlers::timeout_handler();
     127                 :            :   });
     128                 :            :   // detach the thread
     129                 :            :   t.detach();
     130                 :            : #endif
     131                 :          0 :   return TimeLimit();
     132                 :            : }
     133                 :            : 
     134                 :            : }  // namespace cvc5::main