cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Create options to choose SMT solver in runtime

Browse Source
This commit is contained in:
Leonardo Alt 2019-12-03 14:39:47 +01:00
parent e24cca314e
commit 48c3a5c225
9 changed files with 72 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
libsolidity/formal/BMC.cpp
View File

@ -27,19 +27,25 @@ using namespace dev;
using namespace langutil;
using namespace dev::solidity;
BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
BMC::BMC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
smt::SMTSolverChoice _enabledSolvers
):
SMTEncoder(_context),
m_outerErrorReporter(_errorReporter),
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses))
m_interface(make_shared<smt::SMTPortfolio>(_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
}

7
libsolidity/formal/BMC.h
View File

@ -53,7 +53,12 @@ namespace solidity
class BMC: public SMTEncoder
{
public:
BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
BMC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
smt::SMTSolverChoice _enabledSolvers
);
void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);

10
libsolidity/formal/CHC.cpp
View File

@ -35,17 +35,23 @@ using namespace dev::solidity;
CHC::CHC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses
map<h256, string> const& _smtlib2Responses,
smt::SMTSolverChoice _enabledSolvers
):
SMTEncoder(_context),
#ifdef HAVE_Z3
m_interface(make_shared<smt::Z3CHCInterface>()),
m_interface(
_enabledSolvers.z3 ?
dynamic_pointer_cast<smt::CHCSolverInterface>(make_shared<smt::Z3CHCInterface>()) :
dynamic_pointer_cast<smt::CHCSolverInterface>(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses))
),
#else
m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
#endif
m_outerErrorReporter(_errorReporter)
{
(void)_smtlib2Responses;
(void)_enabledSolvers;
}
void CHC::analyze(SourceUnit const& _source)

3
libsolidity/formal/CHC.h
View File

@ -47,7 +47,8 @@ public:
CHC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses
std::map<h256, std::string> const& _smtlib2Responses,
smt::SMTSolverChoice _enabledSolvers
);
void analyze(SourceUnit const& _sources);

10
libsolidity/formal/ModelChecker.cpp
View File

@ -22,9 +22,13 @@ using namespace dev;
using namespace langutil;
using namespace dev::solidity;
ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
m_bmc(m_context, _errorReporter, _smtlib2Responses),
m_chc(m_context, _errorReporter, _smtlib2Responses),
ModelChecker::ModelChecker(
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
smt::SMTSolverChoice _enabledSolvers
):
m_bmc(m_context, _errorReporter, _smtlib2Responses, _enabledSolvers),
m_chc(m_context, _errorReporter, _smtlib2Responses, _enabledSolvers),
m_context()
{
}

7
libsolidity/formal/ModelChecker.h
View File

@ -25,6 +25,7 @@
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
@ -43,7 +44,11 @@ namespace solidity
class ModelChecker
{
public:
ModelChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
ModelChecker(
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All()
);
void analyze(SourceUnit const& _sources);

12
libsolidity/formal/SMTPortfolio.cpp
View File

@ -30,15 +30,21 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
SMTPortfolio::SMTPortfolio(
map<h256, string> const& _smtlib2Responses,
SMTSolverChoice _enabledSolvers
)
{
m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses));
#ifdef HAVE_Z3
m_solvers.emplace_back(make_unique<smt::Z3Interface>());
if (_enabledSolvers.z3)
m_solvers.emplace_back(make_unique<smt::Z3Interface>());
#endif
#ifdef HAVE_CVC4
m_solvers.emplace_back(make_unique<smt::CVC4Interface>());
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(make_unique<smt::CVC4Interface>());
#endif
(void)_enabledSolvers;
}
void SMTPortfolio::reset()

5
libsolidity/formal/SMTPortfolio.h
View File

@ -42,7 +42,10 @@ namespace smt
class SMTPortfolio: public SolverInterface, public boost::noncopyable
{
public:
SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
SMTPortfolio(
std::map<h256, std::string> const& _smtlib2Responses,
SMTSolverChoice _enabledSolvers
);
void reset() override;

15
libsolidity/formal/SolverInterface.h
View File

@ -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