cerc-io/solidity
11
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

Allow running Eldarica from the command line

Browse Source
This commit is contained in:
Leo Alt
2022-11-22 21:16:45 +01:00
parent be8ecb17d8
commit 24df40de9a
67 changed files with 386 additions and 3187 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+5 -5
View File
@@ -18,6 +18,7 @@
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsmtutil/SMTPortfolio.h>
@@ -40,7 +41,7 @@ BMC::BMC(
UniqueErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
ModelCheckerSettings _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
@@ -61,15 +62,14 @@ BMC::BMC(
void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
{
if (m_interface->solvers() == 0)
// At this point every enabled solver is available.
if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
{
m_errorReporter.warning(
7710_error,
SourceLocation(),
"BMC analysis was not possible since no SMT solver was found and enabled."
#ifdef HAVE_Z3_DLOPEN
" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
#endif
" The accepted solvers for BMC are cvc4 and z3."
);
return;
}
libsolidity/formal/BMC.h
+1 -1
View File
@@ -62,7 +62,7 @@ public:
langutil::UniqueErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
ModelCheckerSettings _settings,
langutil::CharStreamProvider const& _charStreamProvider
);
libsolidity/formal/CHC.cpp
+37 -30
View File
@@ -18,6 +18,8 @@
#include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/ModelChecker.h>
#ifdef HAVE_Z3
#include <libsmtutil/Z3CHCInterface.h>
#endif
@@ -62,7 +64,7 @@ CHC::CHC(
UniqueErrorReporter& _errorReporter,
map<util::h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
ModelCheckerSettings _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
@@ -73,32 +75,30 @@ CHC::CHC(
void CHC::analyze(SourceUnit const& _source)
{
if (!shouldAnalyze(_source))
return;
bool usesZ3 = m_settings.solvers.z3;
#ifdef HAVE_Z3_DLOPEN
if (m_settings.solvers.z3 && !Z3Interface::available())
{
usesZ3 = false;
m_errorReporter.warning(
8158_error,
SourceLocation(),
"z3 was selected as a Horn solver for CHC analysis but libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
);
}
#endif
if (!usesZ3 && !m_settings.solvers.smtlib2)
// At this point every enabled solver is available.
if (!m_settings.solvers.eld && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
{
m_errorReporter.warning(
7649_error,
SourceLocation(),
"CHC analysis was not possible since no Horn solver was found and enabled."
" The accepted solvers for CHC are Eldarica and z3."
);
return;
}
if (m_settings.solvers.eld && m_settings.solvers.z3)
m_errorReporter.warning(
5798_error,
SourceLocation(),
"Multiple Horn solvers were selected for CHC."
" CHC only supports one solver at a time, therefore only z3 will be used."
" If you wish to use Eldarica, please enable Eldarica only."
);
if (!shouldAnalyze(_source))
return;
resetSourceAnalysis();
auto sources = sourceDependencies(_source);
@@ -115,7 +115,8 @@ void CHC::analyze(SourceUnit const& _source)
bool ranSolver = true;
// If ranSolver is true here it's because an SMT solver callback was
// actually given and the queries were solved.
// actually given and the queries were solved,
// or Eldarica was chosen and was present in the system.
if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
ranSolver = smtLibInterface->unhandledQueries().empty();
if (!ranSolver)
@@ -994,24 +995,27 @@ void CHC::resetSourceAnalysis()
ArraySlicePredicate::reset();
m_blockCounter = 0;
bool usesZ3 = false;
#ifdef HAVE_Z3
usesZ3 = m_settings.solvers.z3 && Z3Interface::available();
if (usesZ3)
// At this point every enabled solver is available.
// If more than one Horn solver is selected we go with z3.
// We still need the ifdef because of Z3CHCInterface.
if (m_settings.solvers.z3)
{
/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
#ifdef HAVE_Z3
// z3::fixedpoint does not have a reset mechanism, so we need to create another.
m_interface = std::make_unique<Z3CHCInterface>(m_settings.timeout);
auto z3Interface = dynamic_cast<Z3CHCInterface const*>(m_interface.get());
solAssert(z3Interface, "");
m_context.setSolver(z3Interface->z3Interface());
}
#else
solAssert(false);
#endif
if (!usesZ3)
}
if (!m_settings.solvers.z3)
{
solAssert(m_settings.solvers.smtlib2);
solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld);
if (!m_interface)
m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, "");
@@ -1551,9 +1555,10 @@ tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query
{
case CheckResult::SATISFIABLE:
{
#ifdef HAVE_Z3
// We still need the ifdef because of Z3CHCInterface.
if (m_settings.solvers.z3)
{
#ifdef HAVE_Z3
// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
// We now disable those optimizations and check whether we can still solve the problem.
auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
@@ -1569,8 +1574,10 @@ tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query
cex = std::move(cexNoOpt);
spacer->setSpacerOptions(true);
}
#else
solAssert(false);
#endif
}
break;
}
case CheckResult::UNSATISFIABLE:
libsolidity/formal/CHC.h
+1 -1
View File
@@ -59,7 +59,7 @@ public:
langutil::UniqueErrorReporter& _errorReporter,
std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
ModelCheckerSettings _settings,
langutil::CharStreamProvider const& _charStreamProvider
);
libsolidity/formal/ModelChecker.cpp
+58 -5
View File
@@ -20,6 +20,13 @@
#ifdef HAVE_Z3
#include <libsmtutil/Z3Interface.h>
#endif
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#endif
#if defined(__linux) || defined(__APPLE__)
#include <boost/process.hpp>
#endif
#include <range/v3/algorithm/any_of.hpp>
#include <range/v3/view.hpp>
@@ -29,6 +36,7 @@ using namespace solidity;
using namespace solidity::util;
using namespace solidity::langutil;
using namespace solidity::frontend;
using namespace solidity::smtutil;
ModelChecker::ModelChecker(
ErrorReporter& _errorReporter,
@@ -46,13 +54,11 @@ ModelChecker::ModelChecker(
}
// TODO This should be removed for 0.9.0.
void ModelChecker::enableAllEnginesIfPragmaPresent(vector<shared_ptr<SourceUnit>> const& _sources)
bool ModelChecker::isPragmaPresent(vector<shared_ptr<SourceUnit>> const& _sources)
{
bool hasPragma = ranges::any_of(_sources, [](auto _source) {
return ranges::any_of(_sources, [](auto _source) {
return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker);
});
if (hasPragma)
m_settings.engine = ModelCheckerEngine::All();
}
void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUnit>> const& _sources)
@@ -135,9 +141,12 @@ vector<string> ModelChecker::unhandledQueries()
return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
}
solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
SMTSolverChoice ModelChecker::availableSolvers()
{
smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
#if defined(__linux) || defined(__APPLE__)
available.eld = !boost::process::search_path("eld").empty();
#endif
#ifdef HAVE_Z3
available.z3 = solidity::smtutil::Z3Interface::available();
#endif
@@ -146,3 +155,47 @@ solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
#endif
return available;
}
SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, ErrorReporter& _errorReporter)
{
SMTSolverChoice availableSolvers{ModelChecker::availableSolvers()};
if (_enabled.cvc4 && !availableSolvers.cvc4)
{
_enabled.cvc4 = false;
_errorReporter.warning(
4902_error,
SourceLocation(),
"Solver CVC4 was selected for SMTChecker but it is not available."
);
}
if (_enabled.eld && !availableSolvers.eld)
{
_enabled.eld = false;
_errorReporter.warning(
4458_error,
SourceLocation(),
#if defined(__linux) || defined(__APPLE__)
"Solver Eldarica was selected for SMTChecker but it was not found in the system."
#else
"Solver Eldarica was selected for SMTChecker but it is only supported on Linux and MacOS."
#endif
);
}
if (_enabled.z3 && !availableSolvers.z3)
{
_enabled.z3 = false;
_errorReporter.warning(
8158_error,
SourceLocation(),
"Solver z3 was selected for SMTChecker but it is not available."
#ifdef HAVE_Z3_DLOPEN
" libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
#endif
);
}
return _enabled;
}
libsolidity/formal/ModelChecker.h
+5 -1
View File
@@ -58,7 +58,7 @@ public:
);
// TODO This should be removed for 0.9.0.
void enableAllEnginesIfPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> const& _sources);
static bool isPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> const& _sources);
/// Generates error messages if the requested sources and contracts
/// do not exist.
@@ -74,6 +74,10 @@ public:
/// @returns SMT solvers that are available via the C++ API.
static smtutil::SMTSolverChoice availableSolvers();
/// @returns the intersection of the enabled and available solvers,
/// reporting warnings when a solver is enabled but not available.
static smtutil::SMTSolverChoice checkRequestedSolvers(smtutil::SMTSolverChoice _enabled, langutil::ErrorReporter& _errorReporter);
private:
/// Error reporter from CompilerStack.
/// We need to append m_uniqueErrorReporter
libsolidity/formal/ModelCheckerSettings.h
+1 -1
View File
@@ -153,7 +153,7 @@ struct ModelCheckerSettings
ModelCheckerEngine engine = ModelCheckerEngine::None();
ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
bool showUnproved = false;
smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
ModelCheckerTargets targets = ModelCheckerTargets::Default();
std::optional<unsigned> timeout;
libsolidity/formal/SMTEncoder.cpp
+2 -2
View File
@@ -47,13 +47,13 @@ using namespace solidity::frontend;
SMTEncoder::SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings,
ModelCheckerSettings _settings,
UniqueErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider
):
m_errorReporter(_errorReporter),
m_context(_context),
m_settings(_settings),
m_settings(std::move(_settings)),
m_charStreamProvider(_charStreamProvider)
{
}
libsolidity/formal/SMTEncoder.h
+2 -2
View File
@@ -54,7 +54,7 @@ class SMTEncoder: public ASTConstVisitor
public:
SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings,
ModelCheckerSettings _settings,
langutil::UniqueErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider
);
@@ -483,7 +483,7 @@ protected:
/// Stores the context of the encoding.
smt::EncodingContext& m_context;
ModelCheckerSettings const& m_settings;
ModelCheckerSettings m_settings;
/// Character stream for each source,
/// used for retrieving source text of expressions for e.g. counter-examples.