Rework CBMC's solver-time-limit infrastructure

doc/man/cbmc.1

@@ -473,6 +473,10 @@ command to invoke SAT solver process
 \fB\-\-no\-sat\-preprocessor\fR
 disable the SAT solver's simplifier
 .TP
+\fB\-\-solver\-time\-limit\fR N
+abort the SAT/SMT solver after N seconds (best-effort; not all
+back-ends honour this)
+.TP
 \fB\-\-dimacs\fR
 generate CNF in DIMACS format
 .TP

doc/man/goto-synthesizer.1

@@ -93,6 +93,10 @@ refinement of arithmetic expressions only
 maximum refinement iterations for
 arithmetic expressions
 .TP
+\fB\-\-solver\-time\-limit\fR N
+abort the SAT/SMT solver after N seconds (best-effort; not all
+back-ends honour this)
+.TP
 \fB\-\-incremental\-smt2\-solver\fR \fIcmd\fR
 Use the incremental SMT backend where \fIcmd\fR is the command to invoke the SMT
 solver of choice.

doc/man/jbmc.1

@@ -458,6 +458,10 @@ output smt incremental formula to the given file
 \fB\-\-write\-solver\-stats\-to\fR \fIjson\-file\fR
 collect the solver query complexity
 .TP
+\fB\-\-solver\-time\-limit\fR N
+abort the SAT/SMT solver after N seconds (best-effort; not all
+back-ends honour this)
+.TP
 \fB\-\-no\-refine\-strings\fR
 turn off string refinement
 .TP

regression/cbmc/solver-time-limit/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int x = 1;
+  __CPROVER_assert(x == 1, "trivially true");
+  return 0;
+}

regression/cbmc/solver-time-limit/main_multi.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int a, b;
+  __CPROVER_assume(a >= 0 && a < 10);
+  __CPROVER_assume(b >= 0 && b < 10);
+  __CPROVER_assert(a + b >= 0, "sum is non-negative");
+  __CPROVER_assert(a < 10, "a is bounded");
+  __CPROVER_assert(b < 10, "b is bounded");
+  return 0;
+}

regression/cbmc/solver-time-limit/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--solver-time-limit 60
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line 4 trivially true: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+A solve that completes well within the budget should not be affected
+by `--solver-time-limit`. This pins down that the option is parsed
+and passed through to the solver layer without breaking the happy
+path.

regression/cbmc/solver-time-limit/test_all_properties.desc

@@ -0,0 +1,15 @@
+CORE
+main_multi.c
+--all-properties --solver-time-limit 60
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Exercises --solver-time-limit on the multi-property (incremental) path,
+which issues several solver calls on the same solver instance. This pins
+down that a watchdog interrupt from one (timed-out) solve does not leak
+into subsequent solves on the same instance (see the asynch_interrupt
+handling in satcheck_minisat2). All properties hold and finish well within
+the budget.

regression/cbmc/solver-time-limit/test_smt2.desc

@@ -0,0 +1,12 @@
+CORE smt-backend no-new-smt
+main.c
+--smt2 --z3 --solver-time-limit 60
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The --solver-time-limit option is accepted and propagated to the SMT2 (z3)
+back-end (as a solver command-line timeout) without spurious diagnostics on
+a solve that finishes well within the budget.

src/common

@@ -69,7 +69,8 @@ ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
 else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),)
   CP_CXXFLAGS +=
   LINKLIB = llvm-ar rcT $@ $^
-  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
+  # -pthread is needed for satcheck_minisat2.cpp's std::thread watchdog
+  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) -pthread
   LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -o $@ $^
   ifeq ($(origin CC),default)
     CC     = clang
@@ -80,7 +81,8 @@ else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),)
   YFLAGS ?= -v -Werror
 else
   LINKLIB = ar rcT $@ $^
-  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
+  # -pthread is needed for satcheck_minisat2.cpp's std::thread watchdog
+  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) -pthread
   LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -o $@ $^
   ifeq ($(origin CC),default)
     CC     = gcc

src/goto-checker/solver_factory.cpp

@@ -386,6 +386,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
     std::unique_ptr<boolbvt> bv_dimacs =
       std::make_unique<bv_dimacst>(ns, *prop, message_handler, std::cout);
 
+    set_decision_procedure_time_limit(*bv_dimacs);
     return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
   }
 
@@ -394,6 +395,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
   std::unique_ptr<boolbvt> bv_dimacs =
     std::make_unique<bv_dimacst>(ns, *prop, message_handler, *outfile);
 
+  set_decision_procedure_time_limit(*bv_dimacs);
   return std::make_unique<solvert>(
     std::move(bv_dimacs), std::move(prop), std::move(outfile));
 }
@@ -410,6 +412,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
   std::unique_ptr<boolbvt> bv_pointers =
     std::make_unique<bv_pointerst>(ns, *prop, message_handler);
 
+  set_decision_procedure_time_limit(*bv_pointers);
   return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
 }
 
@@ -504,6 +507,14 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
         out_filename, message_handler, "--dump-smt-formula"));
   }
 
+  if(options.get_signed_int_option("solver-time-limit") > 0)
+  {
+    messaget{message_handler}.warning()
+      << "solver-time-limit is not propagated to the incremental SMT2 "
+         "back-end and will be ignored"
+      << messaget::eom;
+  }
+
   return std::make_unique<solvert>(
     std::make_unique<smt2_incremental_decision_proceduret>(
       ns, std::move(solver_process), message_handler));
@@ -538,6 +549,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_dec->use_FPA_theory = true;
 
+    set_decision_procedure_time_limit(*smt2_dec);
     return std::make_unique<solvert>(std::move(smt2_dec));
   }
   else if(filename == "-")
@@ -803,4 +815,10 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options)
     options.set_option(
       "max-node-refinement", cmdline.get_value("max-node-refinement"));
   }
+
+  if(cmdline.isset("solver-time-limit"))
+  {
+    options.set_option(
+      "solver-time-limit", cmdline.get_value("solver-time-limit"));
+  }
 }

src/goto-checker/solver_factory.h

@@ -84,9 +84,14 @@ class solver_factoryt final
 
   smt2_dect::solvert get_smt2_solver_type() const;
 
-  /// Sets the timeout of \p decision_procedure if the `solver-time-limit`
+  /// Sets the time limit of \p decision_procedure if the `solver-time-limit`
   /// option has a positive value (in seconds).
-  /// \note Most solvers silently ignore the time limit at the moment.
+  /// \note Honoured by the MiniSat 2, IPASIR and CaDiCaL SAT back-ends (which
+  ///   have native interrupt support) and by the SMT2 back-end when invoking a
+  ///   solver that accepts a command-line timeout (Z3, cvc5). Other SAT
+  ///   back-ends (PicoSAT, Glucose, Lingeling, external-SAT, ...), the
+  ///   incremental SMT2 back-end and plain DIMACS/SMT2 output modes log a
+  ///   warning and ignore the limit.
   void set_decision_procedure_time_limit(
     solver_resource_limitst &decision_procedure);
 
@@ -119,7 +124,8 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "(refine-arithmetic)"                                                        \
   "(outfile):"                                                                 \
   "(dump-smt-formula):"                                                        \
-  "(write-solver-stats-to):"
+  "(write-solver-stats-to):"                                                   \
+  "(solver-time-limit):"
 
 #define HELP_SOLVER                                                            \
   " {y--sat-solver} {usolver} \t use specified SAT solver\n"                   \
@@ -151,6 +157,9 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   " {y--dump-smt-formula} {ufilename} \t "                                     \
   "output smt incremental formula to the given file\n"                         \
   " {y--write-solver-stats-to} {ujson-file} \t "                               \
-  "collect the solver query complexity\n"
+  "collect the solver query complexity\n"                                      \
+  " {y--solver-time-limit} {uN} \t "                                           \
+  "abort the SAT/SMT solver after N seconds (best-effort; not all "            \
+  "back-ends honour this)\n"
 
 #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H

src/libcprover-cpp/CMakeLists.txt

@@ -54,6 +54,15 @@ target_link_libraries(cprover-api-cpp
                       PRIVATE
                       ${LIBRARY_DEPENDENCIES})
 
+# satcheck_minisat2.cpp inside libcprover.<version>.a uses std::thread (see
+# the matching note in src/solvers/CMakeLists.txt).  Because the solvers
+# dependency above is PRIVATE, the `-pthread` link option attached to the
+# solvers target does not propagate to consumers of cprover-api-cpp such as
+# goto-bmc.  Re-publish it as an INTERFACE option so consumers get it.
+if(NOT WIN32)
+    target_link_options(cprover-api-cpp INTERFACE -pthread)
+endif()
+
 # To be able to invoke `ar` on the dependencies we need the paths of the libraries `.a` files.
 # Ths is done by using the cmake generator `$<TARGET_FILE:dependency>`, that in turn will be
 # substituted with the absolute path of the `dependency` output file (a `.a` file in this case).

src/solvers/CMakeLists.txt

@@ -59,6 +59,18 @@ list(REMOVE_ITEM sources
 
 add_library(solvers ${sources})
 
+# satcheck_minisat2.cpp uses std::thread (a watchdog for the per-solve time
+# limit), so the solvers library needs to link against the host's threads
+# library on platforms where that is not implicit (FreeBSD, NetBSD, some
+# minimal Linux glibc setups, Docker images using gcc without -pthread by
+# default).  We avoid the imported Threads::Threads target because
+# libcprover-cpp's archive-aggregation loop in src/libcprover-cpp/CMakeLists.txt
+# tries to resolve every dependency to a .a file and Threads::Threads has no
+# such backing file.
+if(NOT WIN32)
+    target_link_options(solvers PUBLIC -pthread)
+endif()
+
 include("${CBMC_SOURCE_DIR}/cmake/DownloadProject.cmake")
 
 foreach(SOLVER ${sat_impl})

src/solvers/prop/prop.h

@@ -16,12 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/threeval.h>
 
 #include "literal.h"
+#include "solver_resource_limits.h"
 
 #include <cstdint>
 
 /*! \brief TO_BE_DOCUMENTED
 */
-class propt
+class propt : public solver_resource_limitst
 {
 public:
   explicit propt(message_handlert &message_handler) : log(message_handler)
@@ -117,14 +118,24 @@ class propt
   virtual void set_frozen(literalt) { }
 
   // Resource limits:
-  virtual void set_time_limit_seconds(uint32_t)
+
+  /// \copydoc solver_resource_limitst::set_time_limit_milliseconds
+  /// This default implementation logs a warning and ignores the limit;
+  /// back-ends with native interrupt support override it to store the limit
+  /// in \ref time_limit_milliseconds and honour it in \ref do_prop_solve.
+  void set_time_limit_milliseconds(uint32_t) override
   {
     log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
   std::size_t get_number_of_solver_calls() const;
 
 protected:
+  /// Wall-clock time limit for each solver call, in milliseconds; 0 disables
+  /// it. Stored here so the back-ends share a single member (the seconds
+  /// helper and API live in solver_resource_limitst).
+  uint32_t time_limit_milliseconds = 0;
+
   // solve under the given assumption
   virtual resultt do_prop_solve(const bvt &assumptions) = 0;
 

src/solvers/prop/prop_conv_solver.h

@@ -92,9 +92,9 @@ class prop_conv_solvert : public conflict_providert,
     return symbols;
   }
 
-  void set_time_limit_seconds(uint32_t lim) override
+  void set_time_limit_milliseconds(uint32_t lim) override
   {
-    prop.set_time_limit_seconds(lim);
+    prop.set_time_limit_milliseconds(lim);
   }
 
   std::size_t get_number_of_solver_calls() const override;

src/solvers/prop/solver_resource_limits.h

@@ -12,11 +12,34 @@ Author: Peter Schrammel
 #ifndef CPROVER_SOLVERS_PROP_SOLVER_RESOURCE_LIMITS_H
 #define CPROVER_SOLVERS_PROP_SOLVER_RESOURCE_LIMITS_H
 
+#include <cstdint>
+#include <limits>
+
 class solver_resource_limitst
 {
 public:
-  /// Set the limit for the solver to time out in seconds
-  virtual void set_time_limit_seconds(uint32_t) = 0;
+  /// Set a wall-clock time limit for each solver call, in
+  /// milliseconds. A value of 0 disables the time limit. Granularity
+  /// is best-effort: back-ends may round up or, where the underlying
+  /// solver does not support timeouts, log a warning and ignore the
+  /// limit.
+  virtual void set_time_limit_milliseconds(uint32_t) = 0;
+
+  /// Helper accepting a time limit in whole seconds; forwards to
+  /// `set_time_limit_milliseconds` after multiplying by 1000.
+  /// Provided for backward compatibility with callers that still
+  /// express the limit in seconds (e.g. dependent projects predating
+  /// the millisecond-precision rework).
+  void set_time_limit_seconds(uint32_t lim)
+  {
+    // Saturate to UINT32_MAX milliseconds (~49.7 days) to avoid silently
+    // wrapping for inputs greater than ~4.29 million seconds.
+    const uint64_t ms = static_cast<uint64_t>(lim) * 1000u;
+    set_time_limit_milliseconds(
+      ms > std::numeric_limits<uint32_t>::max()
+        ? std::numeric_limits<uint32_t>::max()
+        : static_cast<uint32_t>(ms));
+  }
 
   virtual ~solver_resource_limitst() = default;
 };