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                 :            :  * Regression test for ResourceManager::getRemainingTime() uint64_t underflow.
      11                 :            :  *
      12                 :            :  * `getRemainingTime()` returns
      13                 :            :  *   `perCallMillisecondLimit - d_perCallTimer.elapsed()`
      14                 :            :  * with both operands `uint64_t`. Once the per-call wall-clock timer overruns
      15                 :            :  * the limit, the subtraction wraps to a value close to 2^64. Callers consume
      16                 :            :  * this as either a huge double (cryptominisat, cocoa_util) or as a "remaining"
      17                 :            :  * value, silently passing the deadline.
      18                 :            :  *
      19                 :            :  * The test pokes `WallClockTimer`'s internal time points directly via the
      20                 :            :  * white-box build (`-fno-access-control`) instead of sleeping, so the timer
      21                 :            :  * deterministically reports a 1 s overrun against the 5 ms limit. Sleep-based
      22                 :            :  * tests against `WallClockTimer::clock` (a `std::chrono::system_clock`) are
      23                 :            :  * vulnerable to NTP rewinds on CI VMs.
      24                 :            :  */
      25                 :            : 
      26                 :            : #include <chrono>
      27                 :            : 
      28                 :            : #include "options/base_options.h"
      29                 :            : #include "options/options.h"
      30                 :            : #include "test.h"
      31                 :            : #include "util/resource_manager.h"
      32                 :            : #include "util/statistics_registry.h"
      33                 :            : 
      34                 :            : namespace cvc5::internal {
      35                 :            : namespace test {
      36                 :            : 
      37                 :            : class TestResourceManagerWhite : public TestInternal
      38                 :            : {
      39                 :            : };
      40                 :            : 
      41                 :          4 : TEST_F(TestResourceManagerWhite, RemainingTimeSaturatesOnOverrun)
      42                 :            : {
      43                 :          1 :   Options options;
      44                 :          1 :   options.write_base().perCallMillisecondLimit = 5;
      45                 :          1 :   StatisticsRegistry stats;
      46                 :          1 :   ResourceManager rm(stats, options);
      47                 :            : 
      48                 :          1 :   rm.beginCall();
      49                 :            : 
      50                 :            :   // White-box: rewind the per-call timer's start so `elapsed()` returns
      51                 :            :   // ~1000 ms regardless of wall-clock progress.
      52                 :            :   using timer_time_point = decltype(rm.d_perCallTimer.d_start);
      53                 :          1 :   auto now = timer_time_point::clock::now();
      54                 :          1 :   rm.d_perCallTimer.d_start = now - std::chrono::milliseconds(1000);
      55                 :            : 
      56                 :            :   // Pre-fix: huge value (~2^64). Post-fix: 0.
      57         [ -  + ]:          1 :   EXPECT_EQ(rm.getRemainingTime(), 0);
      58                 :          1 : }
      59                 :            : 
      60                 :            : }  // namespace test
      61                 :            : }  // namespace cvc5::internal