Branch data     Line data    Source code

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