Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[SMTChecker] Solver option #11421

Merged
merged 1 commit into from
Jul 27, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .circleci/config.yml
Original file line number Diff line number Diff line change
Expand Up @@ -811,7 +811,7 @@ jobs:

t_ems_solcjs:
docker:
- image: buildpack-deps:latest
- image: << pipeline.parameters.ubuntu-2004-docker-image >>
leonardoalt marked this conversation as resolved.
Show resolved Hide resolved
environment:
TERM: xterm
steps:
Expand All @@ -822,7 +822,7 @@ jobs:
name: Install test dependencies
command: |
apt-get update
apt-get install -qqy --no-install-recommends nodejs npm cvc4
apt-get install -qqy --no-install-recommends nodejs npm
cameel marked this conversation as resolved.
Show resolved Hide resolved
- run:
name: Test solcjs
no_output_timeout: 30m
Expand Down
33 changes: 33 additions & 0 deletions docs/smtchecker.rst
Original file line number Diff line number Diff line change
Expand Up @@ -558,6 +558,39 @@ calls assume the called code is unknown and can do anything.
The CHC engine is much more powerful than BMC in terms of what it can prove,
and might require more computing resources.

SMT and Horn solvers
====================

The two engines detailed above use automated theorem provers as their logical
backends. BMC uses an SMT solver, whereas CHC uses a Horn solver. Often the
same tool can act as both, as seen in `z3 <https://github.com/Z3Prover/z3>`_,
which is primarily an SMT solver and makes `Spacer
<https://spacer.bitbucket.io/>`_ available as a Horn solver, and `Eldarica
<https://github.com/uuverifiers/eldarica>`_ which does both.

The user can choose which solvers should be used, if available, via the CLI
option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option
``settings.modelChecker.solvers=[smtlib2,z3]``, where:

- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
- ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 <http://smtlib.cs.uiowa.edu/>`_ format.
These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that
any solver binary from the system can be employed to synchronously return the results of the queries to the compiler.
This is currently the only way to use Eldarica, for example, since it does not have a C++ API.
This can be used by both BMC and CHC depending on which solvers are called.
- ``z3`` is available

- if ``solc`` is compiled with it;
- if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6);
- statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler.

Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety
of environments, including in the browser, most users will almost never need to be
concerned about this option. More advanced users might apply this option to try
alternative solvers on more complex problems.

Please note that certain combinations of chosen engine and solver will lead to
the SMTChecker doing nothing, for example choosing CHC and ``cvc4``.

*******************************
Abstraction and False Positives
Expand Down
12 changes: 7 additions & 5 deletions libsmtutil/SMTPortfolio.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,8 @@ SMTPortfolio::SMTPortfolio(
):
SolverInterface(_queryTimeout)
{
m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
if (_enabledSolvers.smtlib2)
m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
#ifdef HAVE_Z3
if (_enabledSolvers.z3 && Z3Interface::available())
m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
Expand Down Expand Up @@ -143,10 +144,11 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
vector<string> SMTPortfolio::unhandledQueries()
{
// This code assumes that the constructor guarantees that
// SmtLib2Interface is in position 0.
smtAssert(!m_solvers.empty(), "");
smtAssert(dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()), "");
return m_solvers.front()->unhandledQueries();
// SmtLib2Interface is in position 0, if enabled.
if (!m_solvers.empty())
if (auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()))
return smtlib2->unhandledQueries();
return {};
}

bool SMTPortfolio::solverAnswered(CheckResult result)
Expand Down
70 changes: 64 additions & 6 deletions libsmtutil/SolverInterface.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,13 @@

#include <libsolutil/Common.h>

#include <range/v3/view.hpp>

#include <cstdio>
#include <map>
#include <memory>
#include <optional>
#include <set>
#include <string>
#include <vector>

Expand All @@ -36,16 +39,71 @@ namespace solidity::smtutil
struct SMTSolverChoice
{
bool cvc4 = false;
bool smtlib2 = 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}; }
static constexpr SMTSolverChoice All() { return {true, true, true}; }
static constexpr SMTSolverChoice CVC4() { return {true, false, false}; }
static constexpr SMTSolverChoice SMTLIB2() { return {false, true, false}; }
static constexpr SMTSolverChoice Z3() { return {false, false, true}; }
static constexpr SMTSolverChoice None() { return {false, false, false}; }

static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
{
SMTSolverChoice solvers;
if (_solvers == "all")
{
smtAssert(solvers.setSolver("cvc4"), "");
smtAssert(solvers.setSolver("smtlib2"), "");
smtAssert(solvers.setSolver("z3"), "");
}
else
for (auto&& s: _solvers | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
if (!solvers.setSolver(s))
return {};

return solvers;
}

SMTSolverChoice& operator&(SMTSolverChoice const& _other)
{
cvc4 &= _other.cvc4;
smtlib2 &= _other.smtlib2;
z3 &= _other.z3;
return *this;
}

SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
{
return *this & _other;
}

bool operator!=(SMTSolverChoice const& _other) const noexcept { return !(*this == _other); }

bool operator==(SMTSolverChoice const& _other) const noexcept
{
return cvc4 == _other.cvc4 &&
smtlib2 == _other.smtlib2 &&
z3 == _other.z3;
}

bool setSolver(std::string const& _solver)
{
static std::set<std::string> const solvers{"cvc4", "smtlib2", "z3"};
if (!solvers.count(_solver))
return false;
if (_solver == "cvc4")
cvc4 = true;
else if (_solver == "smtlib2")
smtlib2 = true;
else if (_solver == "z3")
z3 = true;
return true;
}

bool none() { return !some(); }
bool some() { return cvc4 || z3; }
bool all() { return cvc4 && z3; }
bool some() { return cvc4 || smtlib2 || z3; }
bool all() { return cvc4 && smtlib2 && z3; }
};

enum class CheckResult
Expand Down
53 changes: 37 additions & 16 deletions libsolidity/formal/BMC.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -40,16 +40,15 @@ BMC::BMC(
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
m_outerErrorReporter(_errorReporter)
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (_enabledSolvers.some())
if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
if (!_smtlib2Responses.empty())
m_errorReporter.warning(
5622_error,
Expand All @@ -63,6 +62,20 @@ BMC::BMC(

void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
{
if (m_interface->solvers() == 0)
{
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
7710_error,
SourceLocation(),
"BMC analysis was not possible since no SMT solver was found and enabled."
);
}
return;
}

if (SMTEncoder::analyze(_source))
{
m_solvedTargets = move(_solvedTargets);
Expand All @@ -75,19 +88,23 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
_source.accept(*this);
}

solAssert(m_interface->solvers() > 0, "");
// If this check is true, Z3 and CVC4 are not available
// and the query answers were not provided, since SMTPortfolio
// guarantees that SmtLib2Interface is the first solver.
if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
// guarantees that SmtLib2Interface is the first solver, if enabled.
if (
!m_interface->unhandledQueries().empty() &&
m_interface->solvers() == 1 &&
m_settings.solvers.smtlib2
)
{
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
8084_error,
SourceLocation(),
"BMC analysis was not possible since no SMT solver (Z3 or CVC4) was found."
"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
" None of the installed solvers was enabled."
#ifdef HAVE_Z3_DLOPEN
" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
#endif
Expand Down Expand Up @@ -916,16 +933,20 @@ void BMC::checkCondition(
solAssert(!_callStack.empty(), "");
std::ostringstream message;
message << "BMC: " << _description << " happens here.";

std::ostringstream modelMessage;
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);

for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
// Sometimes models have complex smtlib2 expressions that SMTLib2Interface fails to parse.
if (values.size() == expressionNames.size())
{
modelMessage << "Counterexample:\n";
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);

for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
}

m_errorReporter.warning(
_errorHappens,
Expand Down
1 change: 0 additions & 1 deletion libsolidity/formal/BMC.h
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,6 @@ class BMC: public SMTEncoder
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings,
langutil::CharStreamProvider const& _charStreamProvider
);
Expand Down
54 changes: 36 additions & 18 deletions libsolidity/formal/CHC.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -56,26 +56,38 @@ CHC::CHC(
ErrorReporter& _errorReporter,
[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _charStreamProvider),
m_outerErrorReporter(_errorReporter),
m_enabledSolvers(_enabledSolvers)
m_outerErrorReporter(_errorReporter)
{
bool usesZ3 = _enabledSolvers.z3;
bool usesZ3 = m_settings.solvers.z3;
#ifdef HAVE_Z3
usesZ3 = usesZ3 && Z3Interface::available();
#else
usesZ3 = false;
#endif
if (!usesZ3)
if (!usesZ3 && m_settings.solvers.smtlib2)
m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
}

void CHC::analyze(SourceUnit const& _source)
{
if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
{
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
7649_error,
SourceLocation(),
"CHC analysis was not possible since no Horn solver was enabled."
);
}
return;
}

if (SMTEncoder::analyze(_source))
{
resetSourceAnalysis();
Expand All @@ -92,6 +104,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.
if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
ranSolver = smtLibInterface->unhandledQueries().empty();
if (!ranSolver && !m_noSolverWarning)
Expand All @@ -103,7 +117,8 @@ void CHC::analyze(SourceUnit const& _source)
#ifdef HAVE_Z3_DLOPEN
"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
#else
"CHC analysis was not possible since no integrated z3 SMT solver was found."
"CHC analysis was not possible. No Horn solver was available."
" None of the installed solvers was enabled."
#endif
);
}
Expand Down Expand Up @@ -933,7 +948,7 @@ void CHC::resetSourceAnalysis()

bool usesZ3 = false;
#ifdef HAVE_Z3
usesZ3 = m_enabledSolvers.z3 && Z3Interface::available();
usesZ3 = m_settings.solvers.z3 && Z3Interface::available();
if (usesZ3)
{
/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
Expand Down Expand Up @@ -1427,20 +1442,23 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
case CheckResult::SATISFIABLE:
{
#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());
solAssert(spacer, "");
spacer->setSpacerOptions(false);
if (m_settings.solvers.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());
solAssert(spacer, "");
spacer->setSpacerOptions(false);

CheckResult resultNoOpt;
CHCSolverInterface::CexGraph cexNoOpt;
tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
CheckResult resultNoOpt;
CHCSolverInterface::CexGraph cexNoOpt;
tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);

if (resultNoOpt == CheckResult::SATISFIABLE)
cex = move(cexNoOpt);
if (resultNoOpt == CheckResult::SATISFIABLE)
cex = move(cexNoOpt);

spacer->setSpacerOptions(true);
spacer->setSpacerOptions(true);
}
#endif
break;
}
Expand Down
Loading