From 4eee0b3cd40fcb936994b00e2c8e69004b3a3006 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 20:56:26 +0000 Subject: [PATCH] cprover: add external SMT2 solver backend (--external-smt2-solver) Add cprover_smt2_dect (a decision_proceduret that pipes constraints to an external SMT2 solver such as z3), an --external-smt2-solver command-line option, the solver_optionst::smt2_solver_binary field, and the plumbing in the inductiveness check and counterexample search to use the external solver when configured (falling back to the built-in SAT backend otherwise). The option is named to match the rest of the suite (cbmc's --external-smt2-solver) and to avoid confusion with cprover's own --smt2 output-formula flag; it is listed in --help. Backend selection is centralised in make_state_encoding_solver() (state_encoding_solver_factory.h) and shared by the counterexample search and the inductiveness/subsumption check, rather than duplicated. smt2_dect::read_result returns D_ERROR for an "unknown" answer as well as for hard errors. In the base-case counterexample search a D_ERROR is now propagated as an error rather than treated as "no counterexample" -- the latter would let an undecided query be reported as a proof, which is unsound. In the subsumption check, returning "not subsumed" on D_ERROR is conservative (we keep an obligation we could have pruned) and hence sound; this deliberately-opposite choice is documented at both sites. cprover_smt2_dect uses solvert::GENERIC (portable SMT2) so any configured solver binary can discharge the queries; this is now documented on the class, and the dead show_assignment(const bv_pointers_widet &) overload has been removed. regression/cprover/external_smt2_solver exercises the backend end to end with z3 (installed on every CI platform that runs this suite). Co-authored-by: Kiro --- .../cprover/external_smt2_solver/main.c | 7 ++ .../cprover/external_smt2_solver/test.desc | 14 ++++ src/cprover/counterexample_found.cpp | 59 +++++--------- src/cprover/counterexample_found.h | 8 +- src/cprover/cprover_parse_options.cpp | 7 ++ src/cprover/cprover_parse_options.h | 1 + src/cprover/cprover_smt2_dec.h | 46 +++++++++++ src/cprover/inductiveness.cpp | 31 ++++++-- src/cprover/solver.h | 2 + src/cprover/state_encoding_solver_factory.h | 79 +++++++++++++++++++ 10 files changed, 206 insertions(+), 48 deletions(-) create mode 100644 regression/cprover/external_smt2_solver/main.c create mode 100644 regression/cprover/external_smt2_solver/test.desc create mode 100644 src/cprover/cprover_smt2_dec.h create mode 100644 src/cprover/state_encoding_solver_factory.h diff --git a/regression/cprover/external_smt2_solver/main.c b/regression/cprover/external_smt2_solver/main.c new file mode 100644 index 00000000000..741ba62ae34 --- /dev/null +++ b/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 +} diff --git a/regression/cprover/external_smt2_solver/test.desc b/regression/cprover/external_smt2_solver/test.desc new file mode 100644 index 00000000000..2b1ec1036c5 --- /dev/null +++ b/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. diff --git a/src/cprover/counterexample_found.cpp b/src/cprover/counterexample_found.cpp index 40142d6a28b..7926bd953a6 100644 --- a/src/cprover/counterexample_found.cpp +++ b/src/cprover/counterexample_found.cpp @@ -14,46 +14,18 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -#include +#include #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 -#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 &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 counterexample_found( const workt &work, const std::unordered_set &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 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 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"; } } diff --git a/src/cprover/counterexample_found.h b/src/cprover/counterexample_found.h index 5a7fe9e2d37..df4f8165968 100644 --- a/src/cprover/counterexample_found.h +++ b/src/cprover/counterexample_found.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "solver_types.h" +#include #include std::optional counterexample_found( @@ -21,10 +22,11 @@ std::optional counterexample_found( const workt &, const std::unordered_set &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 diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp index c5993023c0b..84cb2a7b41b 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/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"); } diff --git a/src/cprover/cprover_parse_options.h b/src/cprover/cprover_parse_options.h index 3204b20ef6b..2aaa453dda5 100644 --- a/src/cprover/cprover_parse_options.h +++ b/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)" \ diff --git a/src/cprover/cprover_smt2_dec.h b/src/cprover/cprover_smt2_dec.h new file mode 100644 index 00000000000..70f4bd9caa2 --- /dev/null +++ b/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 + +#include + +/// 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 diff --git a/src/cprover/inductiveness.cpp b/src/cprover/inductiveness.cpp index aa2e07719e2..b249371ea80 100644 --- a/src/cprover/inductiveness.cpp +++ b/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 #include #include +#include bool is_subsumed( const std::unordered_set &a1, @@ -34,7 +37,8 @@ bool is_subsumed( const exprt &b, const std::unordered_set &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) { diff --git a/src/cprover/solver.h b/src/cprover/solver.h index 7d6f6460512..4b97f0220ec 100644 --- a/src/cprover/solver.h +++ b/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 #include 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 diff --git a/src/cprover/state_encoding_solver_factory.h b/src/cprover/state_encoding_solver_factory.h new file mode 100644 index 00000000000..55801b7a6b3 --- /dev/null +++ b/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 +#include +#include + +#include +#include + +#include "bv_pointers_wide.h" +#include "cprover_smt2_dec.h" + +#include +#include + +/// 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 satcheck; + std::unique_ptr bv; + // external SMT2 backend + std::unique_ptr 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(message_handler); + result.bv = std::make_unique( + ns, *result.satcheck, message_handler); + } + else + { + result.smt2 = std::make_unique( + ns, smt2_solver_binary, message_handler); + } + + return result; +} + +#endif // CPROVER_CPROVER_STATE_ENCODING_SOLVER_FACTORY_H