From 6f4737786a56a7d27de30dc2246c23397dd35030 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 (--smt2-solver) Add cprover_smt2_dect (a decision_proceduret that pipes constraints to an external SMT2 solver such as z3), a --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). Co-authored-by: Kiro --- src/cprover/counterexample_found.cpp | 42 ++++++++++++++++++++++---- src/cprover/counterexample_found.h | 6 +++- src/cprover/cprover_parse_options.cpp | 2 ++ src/cprover/cprover_parse_options.h | 1 + src/cprover/cprover_smt2_dec.h | 39 ++++++++++++++++++++++++ src/cprover/inductiveness.cpp | 43 +++++++++++++++++++++++---- src/cprover/solver.h | 2 ++ 7 files changed, 123 insertions(+), 12 deletions(-) create mode 100644 src/cprover/cprover_smt2_dec.h diff --git a/src/cprover/counterexample_found.cpp b/src/cprover/counterexample_found.cpp index 40142d6a28b..cbd0dacc862 100644 --- a/src/cprover/counterexample_found.cpp +++ b/src/cprover/counterexample_found.cpp @@ -14,13 +14,17 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include #include #include "axioms.h" #include "bv_pointers_wide.h" +#include "cprover_smt2_dec.h" #include "simplify_state_expr.h" #include "state.h" +#include + void show_assignment(const bv_pointers_widet &solver) { #if 0 @@ -56,6 +60,11 @@ void show_assignment(const bv_pointers_widet &solver) #endif } +void show_assignment(const decision_proceduret &) +{ + // no-op: debug output not available for generic decision procedures +} + static exprt evaluator_rec( const std::unordered_map &memory, const decision_proceduret &solver, @@ -106,7 +115,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 +184,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 +195,28 @@ 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); + + std::unique_ptr solver_ptr; + std::unique_ptr satcheck_ptr; + std::unique_ptr bv_ptr; + + if(!smt2_solver_binary.empty()) + { + solver_ptr = std::make_unique( + ns, smt2_solver_binary, message_handler); + } + else + { + satcheck_ptr = std::make_unique(message_handler); + bv_ptr = std::make_unique( + ns, *satcheck_ptr, message_handler); + } + + decision_proceduret &solver = + smt2_solver_binary.empty() + ? static_cast(*bv_ptr) + : static_cast(*solver_ptr); + axiomst axioms(solver, address_taken, verbose, ns); // These are initial states, i.e., initial_state(ς) ⇒ SInitial(ς). @@ -198,12 +228,12 @@ 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: + if(!smt2_solver_binary.empty()) + break; // conservatively treat as no counterexample found throw "error reported by solver"; } } diff --git a/src/cprover/counterexample_found.h b/src/cprover/counterexample_found.h index 5a7fe9e2d37..447978b19f8 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,13 @@ 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..289731d625a 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/src/cprover/cprover_parse_options.cpp @@ -277,6 +277,8 @@ int cprover_parse_optionst::main() solver_options.trace = cmdline.isset("trace"); solver_options.verbose = cmdline.isset("verbose"); + solver_options.smt2_solver_binary = + cmdline.isset("smt2-solver") ? cmdline.get_value("smt2-solver") : ""; // solve auto result = state_encoding_solver( diff --git a/src/cprover/cprover_parse_options.h b/src/cprover/cprover_parse_options.h index 3204b20ef6b..437736ce501 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)" \ + "(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..b30f2a5f552 --- /dev/null +++ b/src/cprover/cprover_smt2_dec.h @@ -0,0 +1,39 @@ +/*******************************************************************\ + +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 + +/// SMT2 decision procedure configured for cprover's state encoding. +/// Uses datatypes for structs (instead of bitvector flattening) to +/// support mathematical types (integer, real, string). +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..bf60a427999 100644 --- a/src/cprover/inductiveness.cpp +++ b/src/cprover/inductiveness.cpp @@ -20,12 +20,14 @@ 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 #include #include +#include bool is_subsumed( const std::unordered_set &a1, @@ -34,7 +36,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 +54,30 @@ bool is_subsumed( #else message_handler.set_verbosity(1); #endif - satcheckt satcheck(message_handler); - bv_pointers_widet solver(ns, satcheck, message_handler); + + std::unique_ptr solver_ptr; + if(!smt2_solver_binary.empty()) + { + solver_ptr = std::make_unique( + ns, smt2_solver_binary, message_handler); + } + + // SAT solver objects (only used when not using SMT2) + std::unique_ptr satcheck_ptr; + std::unique_ptr bv_ptr; + if(smt2_solver_binary.empty()) + { + satcheck_ptr = std::make_unique(message_handler); + bv_ptr = + std::make_unique(ns, *satcheck_ptr, message_handler); + solver_ptr = nullptr; + } + + decision_proceduret &solver = + smt2_solver_binary.empty() + ? static_cast(*bv_ptr) + : static_cast(*solver_ptr); + axiomst axioms(solver, address_taken, verbose, ns); // check if a => b is valid, @@ -82,6 +107,8 @@ bool is_subsumed( case decision_proceduret::resultt::D_UNSATISFIABLE: return true; case decision_proceduret::resultt::D_ERROR: + if(!smt2_solver_binary.empty()) + return false; // conservatively treat unknown/error as not subsumed throw "error reported by solver"; } @@ -173,7 +200,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 +259,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