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-05-15 17:45:43 +02:00
parent 0841255a85
commit ee9773bcff
5 changed files with 82 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -16,12 +16,16 @@
*/
// SPDX-License-Identifier: GPL-3.0
#include <boost/filesystem/operations.hpp>
#include <libsmtutil/CHCSmtLib2Interface.h>
#include <libsolutil/Keccak256.h>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include <boost/filesystem.hpp>
#include <boost/filesystem/fstream.hpp>
#include <boost/process.hpp>
#include <range/v3/view.hpp>
@ -40,12 +44,14 @@ using namespace solidity::smtutil;
CHCSmtLib2Interface::CHCSmtLib2Interface(
map<h256, string> const& _queryResponses,
ReadCallback::Callback _smtCallback,
SMTSolverChoice _enabledSolvers,
optional<unsigned> _queryTimeout
):
CHCSolverInterface(_queryTimeout),
m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
m_queryResponses(move(_queryResponses)),
m_smtCallback(_smtCallback)
m_smtCallback(_smtCallback),
m_enabledSolvers(_enabledSolvers)
{
reset();
}
@ -203,12 +209,46 @@ string CHCSmtLib2Interface::querySolver(string const& _input)
util::h256 inputHash = util::keccak256(_input);
if (m_queryResponses.count(inputHash))
return m_queryResponses.at(inputHash);
if (m_smtCallback)
if (m_enabledSolvers.smtlib2 && m_smtCallback)
{
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
if (result.success)
return result.responseOrErrorMessage;
}
if (m_enabledSolvers.eld)
{
auto tempDir = boost::filesystem::temp_directory_path();
auto queryFileName = tempDir / "query.smt2";
auto queryFile = boost::filesystem::ofstream(queryFileName);
queryFile << _input;
auto eldBin = boost::process::search_path("eld");
if (!eldBin.empty())
{
boost::process::ipstream is;
boost::process::child eld(
eldBin,
"-ssol",
"-scex",
queryFileName,
boost::process::std_out > is
);
vector<string> data;
string line;
while (eld.running() && std::getline(is, line))
if (!line.empty())
data.push_back(line);
eld.wait();
return boost::join(data, "\n");
}
}
m_unhandledQueries.push_back(_input);
return "unknown\n";
}

2
libsmtutil/CHCSmtLib2Interface.h
View File

@ -35,6 +35,7 @@ public:
explicit CHCSmtLib2Interface(
std::map<util::h256, std::string> const& _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
std::optional<unsigned> _queryTimeout = {}
);
@ -78,6 +79,7 @@ private:
std::vector<std::string> m_unhandledQueries;
frontend::ReadCallback::Callback m_smtCallback;
SMTSolverChoice m_enabledSolvers;
std::map<Sort const*, std::string> m_sortNames;
};

23
libsmtutil/SolverInterface.h
View File

@ -42,14 +42,16 @@ namespace solidity::smtutil
struct SMTSolverChoice
{
bool cvc4 = false;
bool eld = false;
bool smtlib2 = false;
bool z3 = false;
static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; }
static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; }
static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, true, false}; }
static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; }
static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; }
static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; }
static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; }
static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; }
static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; }
static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; }
static constexpr SMTSolverChoice None() noexcept { return {false, false, false, false}; }
static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
{
@ -57,6 +59,7 @@ struct SMTSolverChoice
if (_solvers == "all")
{
smtAssert(solvers.setSolver("cvc4"), "");
smtAssert(solvers.setSolver("eld"), "");
smtAssert(solvers.setSolver("smtlib2"), "");
smtAssert(solvers.setSolver("z3"), "");
}
@ -71,6 +74,7 @@ struct SMTSolverChoice
SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
{
cvc4 &= _other.cvc4;
eld &= _other.eld;
smtlib2 &= _other.smtlib2;
z3 &= _other.z3;
return *this;
@ -87,17 +91,20 @@ struct SMTSolverChoice
bool operator==(SMTSolverChoice const& _other) const noexcept
{
return cvc4 == _other.cvc4 &&
eld == _other.eld &&
smtlib2 == _other.smtlib2 &&
z3 == _other.z3;
}
bool setSolver(std::string const& _solver)
{
static std::set<std::string> const solvers{"cvc4", "smtlib2", "z3"};
static std::set<std::string> const solvers{"cvc4", "eld", "smtlib2", "z3"};
if (!solvers.count(_solver))
return false;
if (_solver == "cvc4")
cvc4 = true;
if (_solver == "eld")
eld = true;
else if (_solver == "smtlib2")
smtlib2 = true;
else if (_solver == "z3")
@ -106,8 +113,8 @@ struct SMTSolverChoice
}
bool none() const noexcept { return !some(); }
bool some() const noexcept { return cvc4 || smtlib2 || z3; }
bool all() const noexcept { return cvc4 && smtlib2 && z3; }
bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; }
bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; }
};
enum class CheckResult

23
libsolidity/formal/CHC.cpp
View File

@ -18,6 +18,8 @@
#include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/ModelChecker.h>
#ifdef HAVE_Z3
#include <libsmtutil/Z3CHCInterface.h>
#endif
@ -89,7 +91,7 @@ void CHC::analyze(SourceUnit const& _source)
}
#endif
if (!usesZ3 && !m_settings.solvers.smtlib2)
if (!usesZ3 && !m_settings.solvers.smtlib2 && !m_settings.solvers.eld)
{
m_errorReporter.warning(
7649_error,
@ -99,6 +101,20 @@ void CHC::analyze(SourceUnit const& _source)
return;
}
if (
m_settings.solvers == SMTSolverChoice::ELD() &&
!ModelChecker::availableSolvers().eld
)
{
m_errorReporter.warning(
7267_error,
SourceLocation(),
"CHC analysis was not possible since Eldarica was the only"
" Horn solver enabled, but it was not found in the system."
);
return;
}
resetSourceAnalysis();
auto sources = sourceDependencies(_source);
@ -115,7 +131,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)
@ -1179,7 +1196,7 @@ void CHC::resetSourceAnalysis()
solAssert(m_settings.solvers.smtlib2);
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, "");

3
libsolidity/formal/ModelChecker.cpp
View File

@ -21,6 +21,8 @@
#include <libsmtutil/Z3Interface.h>
#endif
#include <boost/process.hpp>
#include <range/v3/algorithm/any_of.hpp>
#include <range/v3/view.hpp>
@ -138,6 +140,7 @@ vector<string> ModelChecker::unhandledQueries()
solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
{
smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
available.eld = !boost::process::search_path("eld").empty();
#ifdef HAVE_Z3
available.z3 = solidity::smtutil::Z3Interface::available();
#endif