cprover: add external SMT2 solver backend (--smt2-solver)

regression/cprover/external_smt2_solver/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x;
+  __CPROVER_assume(x >= 2);
+  __CPROVER_assert(x >= 2, "holds");    // passes
+  __CPROVER_assert(x >= 3, "may fail"); // fails
+}

regression/cprover/external_smt2_solver/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--external-smt2-solver z3 --solve --inline --no-safety
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ holds: SUCCESS$
+^\[main\.assertion\.2\] line \d+ may fail: REFUTED$
+--
+^warning: ignoring
+--
+Exercises the external SMT2 solver backend (--external-smt2-solver) end to end:
+the state-encoding queries are discharged by an external z3 process instead of
+the built-in SAT backend, and the per-property results are as expected.  z3 is
+installed on every CI platform that runs this (CORE) suite.

src/cprover/counterexample_found.cpp

@@ -14,46 +14,18 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/cout_message.h>
 #include <util/simplify_expr.h>
 
-#include <solvers/sat/satcheck.h>
+#include <solvers/decision_procedure.h>
 
 #include "axioms.h"
-#include "bv_pointers_wide.h"
 #include "simplify_state_expr.h"
 #include "state.h"
+#include "state_encoding_solver_factory.h"
 
-void show_assignment(const bv_pointers_widet &solver)
-{
-#if 0
-  for(auto &entry : solver.get_cache())
-  {
-    const auto &expr = entry.first;
-    if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not)
-      continue;
-    auto value = solver.l_get(entry.second);
-#  if 0
-    std::cout << "|| " << format(expr) << " --> " << value << "\n";
-#  endif
-  }
-#endif
+#include <memory>
 
-#if 0
-  for(auto &entry : solver.get_map().get_mapping())
-  {
-    const auto &identifier = entry.first;
-    auto symbol = symbol_exprt(identifier, entry.second.type);
-    auto value = solver.get(symbol);
-    std::cout << "|| " << format(symbol) << " --> " << format(value) << "\n";
-  }
-#endif
-
-#if 0
-  for(auto &entry : solver.get_symbols())
-  {
-    const auto &identifier = entry.first;
-    auto value = solver.l_get(entry.second);
-    std::cout << "|| " << identifier << " --> " << value << "\n";
-  }
-#endif
+void show_assignment(const decision_proceduret &)
+{
+  // no-op: debug output not available for generic decision procedures
 }
 
 static exprt evaluator_rec(
@@ -106,7 +78,7 @@ static exprt evaluator(
 propertyt::tracet counterexample(
   const std::vector<framet> &frames,
   const workt &work,
-  const bv_pointers_widet &solver,
+  const decision_proceduret &solver,
   const axiomst &axioms,
   const namespacet &ns)
 {
@@ -175,7 +147,8 @@ std::optional<propertyt::tracet> counterexample_found(
   const workt &work,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
-  const namespacet &ns)
+  const namespacet &ns,
+  const std::string &smt2_solver_binary)
 {
   auto &f = frames[work.frame.index];
 
@@ -185,8 +158,11 @@ std::optional<propertyt::tracet> counterexample_found(
     {
       cout_message_handlert message_handler;
       message_handler.set_verbosity(verbose ? 10 : 1);
-      satcheckt satcheck(message_handler);
-      bv_pointers_widet solver(ns, satcheck, message_handler);
+
+      auto solver_bundle =
+        make_state_encoding_solver(ns, smt2_solver_binary, message_handler);
+      decision_proceduret &solver = solver_bundle.solver();
+
       axiomst axioms(solver, address_taken, verbose, ns);
 
       // These are initial states, i.e., initial_state(ς) ⇒ SInitial(ς).
@@ -198,12 +174,15 @@ std::optional<propertyt::tracet> counterexample_found(
       switch(solver())
       {
       case decision_proceduret::resultt::D_SATISFIABLE:
-        if(verbose)
-          show_assignment(solver);
         return counterexample(frames, work, solver, axioms, ns);
       case decision_proceduret::resultt::D_UNSATISFIABLE:
         break;
       case decision_proceduret::resultt::D_ERROR:
+        // D_ERROR covers both hard solver errors and an "unknown" answer.
+        // Treating it as "no counterexample" here would be unsound: the caller
+        // could then declare the property inductive and report SUCCESS,
+        // masking a genuine base-case violation.  Propagate the failure
+        // instead, regardless of backend.
         throw "error reported by solver";
       }
     }

src/cprover/counterexample_found.h

@@ -14,17 +14,19 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "solver_types.h"
 
+#include <string>
 #include <unordered_set>
 
 std::optional<propertyt::tracet> counterexample_found(
   const std::vector<framet> &,
   const workt &,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
-  const namespacet &);
+  const namespacet &,
+  const std::string &smt2_solver_binary = "");
 
-class bv_pointers_widet;
+class decision_proceduret;
 
-void show_assignment(const bv_pointers_widet &);
+void show_assignment(const decision_proceduret &);
 
 #endif // CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H

src/cprover/cprover_parse_options.cpp

@@ -277,6 +277,10 @@ int cprover_parse_optionst::main()
 
     solver_options.trace = cmdline.isset("trace");
     solver_options.verbose = cmdline.isset("verbose");
+    solver_options.smt2_solver_binary =
+      cmdline.isset("external-smt2-solver")
+        ? cmdline.get_value("external-smt2-solver")
+        : "";
 
     // solve
     auto result = state_encoding_solver(
@@ -327,5 +331,8 @@ void cprover_parse_optionst::help()
     " {y--outfile} {ufile-name} \t set output file for formula\n"
     " {y--smt2} \t output formula in SMT-LIB2 format\n"
     " {y--text} \t output formula in text format\n"
+    " {y--external-smt2-solver} {ucmd} \t discharge queries with the given"
+    " external SMT2 solver binary (e.g. {uz3}); defaults to the built-in SAT"
+    " backend\n"
     "\n");
 }

src/cprover/cprover_parse_options.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, dkr@amazon.com
   "(safety)(no-safety)(no-assertions)"                                         \
   "(contract):"                                                                \
   "(solve)(unwind):(trace)"                                                    \
+  "(external-smt2-solver):"                                                    \
   "(inline)(no-inline)"                                                        \
   "D:I:"                                                                       \
   "(32)(64)"                                                                   \

src/cprover/cprover_smt2_dec.h

@@ -0,0 +1,46 @@
+/*******************************************************************\
+
+Module: SMT2 decision procedure for cprover state encoding
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPROVER_CPROVER_SMT2_DEC_H
+#define CPROVER_CPROVER_CPROVER_SMT2_DEC_H
+
+#include <solvers/smt2/smt2_dec.h>
+
+#include <string>
+
+/// SMT2 decision procedure configured for cprover's state encoding.
+/// Uses datatypes for structs (instead of bitvector flattening) to
+/// support mathematical types (integer, real, string).
+///
+/// The emitted SMT2 uses solvert::GENERIC, i.e. standard SMT-LIBv2 without
+/// solver-specific options or encodings, so that any SMT2 binary configured
+/// via --external-smt2-solver (z3, cvc5, ...) can discharge the queries.  This
+/// trades solver-specific tuning for portability.
+class cprover_smt2_dect : public smt2_dect
+{
+public:
+  cprover_smt2_dect(
+    const namespacet &_ns,
+    const std::string &_solver_binary,
+    message_handlert &_message_handler)
+    : smt2_dect(
+        _ns,
+        "",
+        "cprover",
+        "ALL",
+        smt2_convt::solvert::GENERIC,
+        _solver_binary,
+        _message_handler)
+  {
+    use_array_of_bool = true;
+    use_as_const = true;
+    use_datatypes = true;
+  }
+};
+
+#endif // CPROVER_CPROVER_CPROVER_SMT2_DEC_H

src/cprover/inductiveness.cpp

@@ -20,12 +20,15 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "axioms.h"
 #include "bv_pointers_wide.h"
 #include "counterexample_found.h"
+#include "cprover_smt2_dec.h"
 #include "propagate.h"
 #include "solver.h"
+#include "state_encoding_solver_factory.h"
 
 #include <algorithm>
 #include <iomanip>
 #include <iostream>
+#include <memory>
 
 bool is_subsumed(
   const std::unordered_set<exprt, irep_hash> &a1,
@@ -34,7 +37,8 @@ bool is_subsumed(
   const exprt &b,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
-  const namespacet &ns)
+  const namespacet &ns,
+  const std::string &smt2_solver_binary)
 {
   if(b == true)
     return true; // anything subsumes 'true'
@@ -51,8 +55,11 @@ bool is_subsumed(
 #else
   message_handler.set_verbosity(1);
 #endif
-  satcheckt satcheck(message_handler);
-  bv_pointers_widet solver(ns, satcheck, message_handler);
+
+  auto solver_bundle =
+    make_state_encoding_solver(ns, smt2_solver_binary, message_handler);
+  decision_proceduret &solver = solver_bundle.solver();
+
   axiomst axioms(solver, address_taken, verbose, ns);
 
   // check if a => b is valid,
@@ -82,6 +89,14 @@ bool is_subsumed(
   case decision_proceduret::resultt::D_UNSATISFIABLE:
     return true;
   case decision_proceduret::resultt::D_ERROR:
+    // For the external SMT2 solver, treating unknown/error as "not subsumed"
+    // is conservative: at worst we keep an obligation we could have pruned,
+    // which is sound.  This is the deliberate *opposite* of
+    // counterexample_found(), where swallowing a D_ERROR would be unsound (it
+    // must not be reported as "no counterexample").  A hard error from the SAT
+    // backend is still surfaced.
+    if(!smt2_solver_binary.empty())
+      return false;
     throw "error reported by solver";
   }
 
@@ -173,7 +188,8 @@ inductiveness_resultt inductiveness_check(
                 invariant,
                 address_taken,
                 solver_options.verbose,
-                ns))
+                ns,
+                solver_options.smt2_solver_binary))
       {
         if(solver_options.verbose)
           std::cout << "subsumed " << format(invariant) << '\n';
@@ -231,7 +247,12 @@ inductiveness_resultt inductiveness_check(
 #endif
 
     auto counterexample_found = ::counterexample_found(
-      frames, work, address_taken, solver_options.verbose, ns);
+      frames,
+      work,
+      address_taken,
+      solver_options.verbose,
+      ns,
+      solver_options.smt2_solver_binary);
 
     if(counterexample_found)
     {

src/cprover/solver.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_CPROVER_SOLVER_H
 #define CPROVER_CPROVER_SOLVER_H
 
+#include <string>
 #include <vector>
 
 class exprt;
@@ -30,6 +31,7 @@ class solver_optionst
   bool trace;
   bool verbose;
   std::size_t loop_limit;
+  std::string smt2_solver_binary; // empty = use built-in SAT solver
 };
 
 solver_resultt

src/cprover/state_encoding_solver_factory.h

@@ -0,0 +1,79 @@
+/*******************************************************************\
+
+Module: State-encoding solver backend selection
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Construction of the decision procedure used for cprover's state-encoding
+/// queries: either the built-in SAT backend (bit-vector flattening) or an
+/// external SMT2 solver.
+
+#ifndef CPROVER_CPROVER_STATE_ENCODING_SOLVER_FACTORY_H
+#define CPROVER_CPROVER_STATE_ENCODING_SOLVER_FACTORY_H
+
+#include <util/invariant.h>
+#include <util/message.h>
+#include <util/namespace.h>
+
+#include <solvers/decision_procedure.h>
+#include <solvers/sat/satcheck.h>
+
+#include "bv_pointers_wide.h"
+#include "cprover_smt2_dec.h"
+
+#include <memory>
+#include <string>
+
+/// Owns the solver objects backing a state-encoding query and hands out the
+/// \ref decision_proceduret to use.  Exactly one backend is populated: the
+/// external SMT2 decision procedure when a solver binary is configured, or the
+/// SAT backend (satcheck + bit-vector flattening) otherwise.
+struct state_encoding_solvert
+{
+  // SAT backend (used when no SMT2 solver binary is configured)
+  std::unique_ptr<satcheckt> satcheck;
+  std::unique_ptr<bv_pointers_widet> bv;
+  // external SMT2 backend
+  std::unique_ptr<cprover_smt2_dect> smt2;
+
+  /// The decision procedure to drive the query with.
+  decision_proceduret &solver()
+  {
+    if(smt2 != nullptr)
+      return *smt2;
+    INVARIANT(
+      bv != nullptr, "state-encoding solver bundle must have a backend");
+    return *bv;
+  }
+};
+
+/// Construct the state-encoding solver backend.  When \p smt2_solver_binary is
+/// non-empty the external SMT2 solver is used; otherwise the built-in SAT
+/// backend is used.  Centralises the selection so the call sites stay
+/// consistent.
+inline state_encoding_solvert make_state_encoding_solver(
+  const namespacet &ns,
+  const std::string &smt2_solver_binary,
+  message_handlert &message_handler)
+{
+  state_encoding_solvert result;
+
+  if(smt2_solver_binary.empty())
+  {
+    result.satcheck = std::make_unique<satcheckt>(message_handler);
+    result.bv = std::make_unique<bv_pointers_widet>(
+      ns, *result.satcheck, message_handler);
+  }
+  else
+  {
+    result.smt2 = std::make_unique<cprover_smt2_dect>(
+      ns, smt2_solver_binary, message_handler);
+  }
+
+  return result;
+}
+
+#endif // CPROVER_CPROVER_STATE_ENCODING_SOLVER_FACTORY_H