From 48c3a5c2256ac30274c251f69d2e5eb1f4bacd9e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 3 Dec 2019 14:39:47 +0100 Subject: [PATCH] [SMTChecker] Create options to choose SMT solver in runtime --- libsolidity/formal/BMC.cpp | 24 +++++++++++++++--------- libsolidity/formal/BMC.h | 7 ++++++- libsolidity/formal/CHC.cpp | 10 ++++++++-- libsolidity/formal/CHC.h | 3 ++- libsolidity/formal/ModelChecker.cpp | 10 +++++++--- libsolidity/formal/ModelChecker.h | 7 ++++++- libsolidity/formal/SMTPortfolio.cpp | 12 +++++++++--- libsolidity/formal/SMTPortfolio.h | 5 ++++- libsolidity/formal/SolverInterface.h | 15 +++++++++++++++ 9 files changed, 72 insertions(+), 21 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index b852485f8..cea8e3d4f 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -27,19 +27,25 @@ using namespace dev; using namespace langutil; using namespace dev::solidity; -BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map const& _smtlib2Responses): +BMC::BMC( + smt::EncodingContext& _context, + ErrorReporter& _errorReporter, + map const& _smtlib2Responses, + smt::SMTSolverChoice _enabledSolvers +): SMTEncoder(_context), m_outerErrorReporter(_errorReporter), - m_interface(make_shared(_smtlib2Responses)) + m_interface(make_shared(_smtlib2Responses, _enabledSolvers)) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) - if (!_smtlib2Responses.empty()) - m_errorReporter.warning( - "SMT-LIB2 query responses were given in the auxiliary input, " - "but this Solidity binary uses an SMT solver (Z3/CVC4) directly." - "These responses will be ignored." - "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." - ); + if (_enabledSolvers.some()) + if (!_smtlib2Responses.empty()) + m_errorReporter.warning( + "SMT-LIB2 query responses were given in the auxiliary input, " + "but this Solidity binary uses an SMT solver (Z3/CVC4) directly." + "These responses will be ignored." + "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." + ); #endif } diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 432050e78..01ef36369 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -53,7 +53,12 @@ namespace solidity class BMC: public SMTEncoder { public: - BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); + BMC( + smt::EncodingContext& _context, + langutil::ErrorReporter& _errorReporter, + std::map const& _smtlib2Responses, + smt::SMTSolverChoice _enabledSolvers + ); void analyze(SourceUnit const& _sources, std::set _safeAssertions); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 0bc6a1adc..5e9495192 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -35,17 +35,23 @@ using namespace dev::solidity; CHC::CHC( smt::EncodingContext& _context, ErrorReporter& _errorReporter, - map const& _smtlib2Responses + map const& _smtlib2Responses, + smt::SMTSolverChoice _enabledSolvers ): SMTEncoder(_context), #ifdef HAVE_Z3 - m_interface(make_shared()), + m_interface( + _enabledSolvers.z3 ? + dynamic_pointer_cast(make_shared()) : + dynamic_pointer_cast(make_shared(_smtlib2Responses)) + ), #else m_interface(make_shared(_smtlib2Responses)), #endif m_outerErrorReporter(_errorReporter) { (void)_smtlib2Responses; + (void)_enabledSolvers; } void CHC::analyze(SourceUnit const& _source) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 9aa5871d5..a5ab9e06b 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -47,7 +47,8 @@ public: CHC( smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, - std::map const& _smtlib2Responses + std::map const& _smtlib2Responses, + smt::SMTSolverChoice _enabledSolvers ); void analyze(SourceUnit const& _sources); diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index c061c8416..508509805 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -22,9 +22,13 @@ using namespace dev; using namespace langutil; using namespace dev::solidity; -ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): - m_bmc(m_context, _errorReporter, _smtlib2Responses), - m_chc(m_context, _errorReporter, _smtlib2Responses), +ModelChecker::ModelChecker( + ErrorReporter& _errorReporter, + map const& _smtlib2Responses, + smt::SMTSolverChoice _enabledSolvers +): + m_bmc(m_context, _errorReporter, _smtlib2Responses, _enabledSolvers), + m_chc(m_context, _errorReporter, _smtlib2Responses, _enabledSolvers), m_context() { } diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 349ed76d4..be0d5c38e 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -25,6 +25,7 @@ #include #include #include +#include #include #include @@ -43,7 +44,11 @@ namespace solidity class ModelChecker { public: - ModelChecker(langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); + ModelChecker( + langutil::ErrorReporter& _errorReporter, + std::map const& _smtlib2Responses, + smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All() + ); void analyze(SourceUnit const& _sources); diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index d47c01f31..9b9795e9a 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -30,15 +30,21 @@ using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTPortfolio::SMTPortfolio(map const& _smtlib2Responses) +SMTPortfolio::SMTPortfolio( + map const& _smtlib2Responses, + SMTSolverChoice _enabledSolvers +) { m_solvers.emplace_back(make_unique(_smtlib2Responses)); #ifdef HAVE_Z3 - m_solvers.emplace_back(make_unique()); + if (_enabledSolvers.z3) + m_solvers.emplace_back(make_unique()); #endif #ifdef HAVE_CVC4 - m_solvers.emplace_back(make_unique()); + if (_enabledSolvers.cvc4) + m_solvers.emplace_back(make_unique()); #endif + (void)_enabledSolvers; } void SMTPortfolio::reset() diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h index d922affd2..41472c187 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsolidity/formal/SMTPortfolio.h @@ -42,7 +42,10 @@ namespace smt class SMTPortfolio: public SolverInterface, public boost::noncopyable { public: - SMTPortfolio(std::map const& _smtlib2Responses); + SMTPortfolio( + std::map const& _smtlib2Responses, + SMTSolverChoice _enabledSolvers + ); void reset() override; diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index a39e699af..81f6ea497 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -36,6 +36,21 @@ namespace solidity namespace smt { +struct SMTSolverChoice +{ + bool cvc4 = false; + bool z3 = false; + + static constexpr SMTSolverChoice All() { return {true, true}; } + static constexpr SMTSolverChoice CVC4() { return {true, false}; } + static constexpr SMTSolverChoice Z3() { return {false, true}; } + static constexpr SMTSolverChoice None() { return {false, false}; } + + bool none() { return !some(); } + bool some() { return cvc4 || z3; } + bool all() { return cvc4 && z3; } +}; + enum class CheckResult { SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR