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

Initial work on unified way to interact with solvers

Browse Source
This commit is contained in:
Martin Blicha 2023-06-20 16:10:45 +02:00
parent 16ae76cad7
commit 1e190abf6e
18 changed files with 43 additions and 1583 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
CMakeLists.txt
View File

@ -75,63 +75,6 @@ configure_file("${PROJECT_SOURCE_DIR}/cmake/templates/license.h.in" include/lice
include(EthOptions)
configure_project(TESTS)
set(LATEST_Z3_VERSION "4.12.1")
set(MINIMUM_Z3_VERSION "4.8.16")
find_package(Z3)
if (${Z3_FOUND})
if (${STRICT_Z3_VERSION})
if (NOT ("${Z3_VERSION_STRING}" VERSION_EQUAL ${LATEST_Z3_VERSION}))
message(
FATAL_ERROR
"SMTChecker tests require Z3 ${LATEST_Z3_VERSION} for all tests to pass.\n\
Build with -DSTRICT_Z3_VERSION=OFF if you want to use a different version. \
You can also use -DUSE_Z3=OFF to build without Z3. In both cases use --no-smt when running tests."
)
endif()
else()
if ("${Z3_VERSION_STRING}" VERSION_LESS ${MINIMUM_Z3_VERSION})
message(
FATAL_ERROR
"Solidity requires Z3 ${MINIMUM_Z3_VERSION} or newer. You can also use -DUSE_Z3=OFF to build without Z3."
)
endif()
endif()
endif()
if(${USE_Z3_DLOPEN})
add_definitions(-DHAVE_Z3)
add_definitions(-DHAVE_Z3_DLOPEN)
find_package(Python3 COMPONENTS Interpreter)
if(${Z3_FOUND})
get_target_property(Z3_HEADER_HINTS z3::libz3 INTERFACE_INCLUDE_DIRECTORIES)
endif()
find_path(Z3_HEADER_PATH z3.h HINTS ${Z3_HEADER_HINTS})
if(Z3_HEADER_PATH)
set(Z3_FOUND TRUE)
else()
message(SEND_ERROR "Dynamic loading of Z3 requires Z3 headers to be present at build time.")
endif()
if(NOT ${Python3_FOUND})
message(SEND_ERROR "Dynamic loading of Z3 requires Python 3 to be present at build time.")
endif()
if(${SOLC_LINK_STATIC})
message(SEND_ERROR "solc cannot be linked statically when dynamically loading Z3.")
endif()
elseif (${Z3_FOUND})
add_definitions(-DHAVE_Z3)
message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
endif()
find_package(CVC4 QUIET)
if (${CVC4_FOUND})
add_definitions(-DHAVE_CVC4)
message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
endif()
if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
\nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
endif()
add_subdirectory(libsolutil)
add_subdirectory(liblangutil)

19
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -183,13 +183,18 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
if (m_queryResponses.count(inputHash))
return m_queryResponses.at(inputHash);
smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld);
if (m_smtCallback)
{
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
if (result.success)
return result.responseOrErrorMessage;
}
smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld || m_enabledSolvers.z3);
smtAssert(m_smtCallback, "Callback must be set!");
std::string solverBinary = [&](){
if (m_enabledSolvers.eld)
return "eld";
if (m_enabledSolvers.z3)
return "z3";
return "";
}();
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input);
if (result.success)
return result.responseOrErrorMessage;
m_unhandledQueries.push_back(_input);
return "unknown\n";

34
libsmtutil/CMakeLists.txt
View File

@ -12,40 +12,8 @@ set(sources
Helpers.h
)
if (${Z3_FOUND})
set(z3_SRCS Z3Interface.cpp Z3Interface.h Z3CHCInterface.cpp Z3CHCInterface.h)
else()
set(z3_SRCS)
endif()
if (${CVC4_FOUND})
set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h)
else()
set(cvc4_SRCS)
endif()
if (${USE_Z3_DLOPEN})
file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h)
set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp)
add_custom_command(
OUTPUT ${Z3_WRAPPER}
COMMAND ${Python3_EXECUTABLE} genz3wrapper.py ${Z3_HEADERS} > ${Z3_WRAPPER}
DEPENDS ${Z3_HEADERS} genz3wrapper.py
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
)
set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h)
endif()
add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
add_library(smtutil ${sources})
target_link_libraries(smtutil PUBLIC solutil Boost::boost)
if (${USE_Z3_DLOPEN})
target_include_directories(smtutil PUBLIC ${Z3_HEADER_PATH})
target_link_libraries(smtutil PUBLIC ${CMAKE_DL_LIBS})
elseif (${Z3_FOUND})
target_link_libraries(smtutil PUBLIC z3::libz3)
endif()
if (${CVC4_FOUND})
target_link_libraries(smtutil PUBLIC CVC4::CVC4)
endif()

336
libsmtutil/CVC4Interface.cpp
View File

@ -1,336 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/CVC4Interface.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/Exceptions.h>
#include <cvc4/util/bitvector.h>
using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;
CVC4Interface::CVC4Interface(std::optional<unsigned> _queryTimeout):
SolverInterface(_queryTimeout),
m_solver(&m_context)
{
reset();
}
void CVC4Interface::reset()
{
m_variables.clear();
m_solver.reset();
m_solver.setOption("produce-models", true);
if (m_queryTimeout)
m_solver.setTimeLimit(*m_queryTimeout);
else
m_solver.setResourceLimit(resourceLimit);
}
void CVC4Interface::push()
{
m_solver.push();
}
void CVC4Interface::pop()
{
m_solver.pop();
}
void CVC4Interface::declareVariable(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort, "");
m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
}
void CVC4Interface::addAssertion(Expression const& _expr)
{
try
{
m_solver.assertFormula(toCVC4Expr(_expr));
}
catch (CVC4::TypeCheckingException const& _e)
{
smtAssert(false, _e.what());
}
catch (CVC4::LogicException const& _e)
{
smtAssert(false, _e.what());
}
catch (CVC4::UnsafeInterruptException const& _e)
{
smtAssert(false, _e.what());
}
catch (CVC4::Exception const& _e)
{
smtAssert(false, _e.what());
}
}
std::pair<CheckResult, std::vector<std::string>> CVC4Interface::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
std::vector<std::string> values;
try
{
switch (m_solver.checkSat().isSat())
{
case CVC4::Result::SAT:
result = CheckResult::SATISFIABLE;
break;
case CVC4::Result::UNSAT:
result = CheckResult::UNSATISFIABLE;
break;
case CVC4::Result::SAT_UNKNOWN:
result = CheckResult::UNKNOWN;
break;
default:
smtAssert(false, "");
}
if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
{
for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m_solver.getValue(toCVC4Expr(e))));
}
}
catch (CVC4::Exception const&)
{
result = CheckResult::ERROR;
values.clear();
}
return std::make_pair(result, values);
}
CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
{
// Variable
if (_expr.arguments.empty() && m_variables.count(_expr.name))
return m_variables.at(_expr.name);
std::vector<CVC4::Expr> arguments;
for (auto const& arg: _expr.arguments)
arguments.push_back(toCVC4Expr(arg));
try
{
std::string const& n = _expr.name;
// Function application
if (!arguments.empty() && m_variables.count(_expr.name))
return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments);
// Literal
else if (arguments.empty())
{
if (n == "true")
return m_context.mkConst(true);
else if (n == "false")
return m_context.mkConst(false);
else if (auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.sort))
return m_context.mkVar(n, cvc4Sort(*sortSort->inner));
else
try
{
return m_context.mkConst(CVC4::Rational(n));
}
catch (CVC4::TypeCheckingException const& _e)
{
smtAssert(false, _e.what());
}
catch (CVC4::Exception const& _e)
{
smtAssert(false, _e.what());
}
}
smtAssert(_expr.hasCorrectArity(), "");
if (n == "ite")
return arguments[0].iteExpr(arguments[1], arguments[2]);
else if (n == "not")
return arguments[0].notExpr();
else if (n == "and")
return arguments[0].andExpr(arguments[1]);
else if (n == "or")
return arguments[0].orExpr(arguments[1]);
else if (n == "=>")
return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
else if (n == "=")
return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
else if (n == "<")
return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]);
else if (n == "<=")
return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]);
else if (n == ">")
return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]);
else if (n == ">=")
return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]);
else if (n == "+")
return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]);
else if (n == "-")
return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
else if (n == "*")
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
else if (n == "div")
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
else if (n == "mod")
return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
else if (n == "bvnot")
return m_context.mkExpr(CVC4::kind::BITVECTOR_NOT, arguments[0]);
else if (n == "bvand")
return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]);
else if (n == "bvor")
return m_context.mkExpr(CVC4::kind::BITVECTOR_OR, arguments[0], arguments[1]);
else if (n == "bvxor")
return m_context.mkExpr(CVC4::kind::BITVECTOR_XOR, arguments[0], arguments[1]);
else if (n == "bvshl")
return m_context.mkExpr(CVC4::kind::BITVECTOR_SHL, arguments[0], arguments[1]);
else if (n == "bvlshr")
return m_context.mkExpr(CVC4::kind::BITVECTOR_LSHR, arguments[0], arguments[1]);
else if (n == "bvashr")
return m_context.mkExpr(CVC4::kind::BITVECTOR_ASHR, arguments[0], arguments[1]);
else if (n == "int2bv")
{
size_t size = std::stoul(_expr.arguments[1].name);
auto i2bvOp = m_context.mkConst(CVC4::IntToBitVector(static_cast<unsigned>(size)));
// CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
return m_context.mkExpr(
CVC4::kind::ITE,
m_context.mkExpr(CVC4::kind::GEQ, arguments[0], m_context.mkConst(CVC4::Rational(0))),
m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, arguments[0]),
m_context.mkExpr(
CVC4::kind::BITVECTOR_NEG,
m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, m_context.mkExpr(CVC4::kind::UMINUS, arguments[0]))
)
);
}
else if (n == "bv2int")
{
auto intSort = std::dynamic_pointer_cast<IntSort>(_expr.sort);
smtAssert(intSort, "");
auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]);
if (!intSort->isSigned)
return nat;
auto type = arguments[0].getType();
smtAssert(type.isBitVector(), "");
auto size = CVC4::BitVectorType(type).getSize();
// CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
auto extractOp = m_context.mkConst(CVC4::BitVectorExtract(size - 1, size - 1));
return m_context.mkExpr(CVC4::kind::ITE,
m_context.mkExpr(
CVC4::kind::EQUAL,
m_context.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, extractOp, arguments[0]),
m_context.mkConst(CVC4::BitVector(1, uint64_t{0}))
),
nat,
m_context.mkExpr(
CVC4::kind::UMINUS,
m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, m_context.mkExpr(CVC4::kind::BITVECTOR_NEG, arguments[0]))
)
);
}
else if (n == "select")
return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
else if (n == "store")
return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
else if (n == "const_array")
{
std::shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
smtAssert(sortSort, "");
return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
}
else if (n == "tuple_get")
{
std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
size_t index = std::stoul(_expr.arguments[1].name);
CVC4::Expr s = dt[0][index].getSelector();
return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
}
else if (n == "tuple_constructor")
{
std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
CVC4::Expr c = dt[0].getConstructor();
return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
}
smtAssert(false);
}
catch (CVC4::TypeCheckingException const& _e)
{
smtAssert(false, _e.what());
}
catch (CVC4::Exception const& _e)
{
smtAssert(false, _e.what());
}
smtAssert(false);
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
util::unreachable();
}
CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
{
switch (_sort.kind)
{
case Kind::Bool:
return m_context.booleanType();
case Kind::Int:
return m_context.integerType();
case Kind::BitVector:
return m_context.mkBitVectorType(dynamic_cast<BitVectorSort const&>(_sort).size);
case Kind::Function:
{
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
}
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
}
case Kind::Tuple:
{
auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
return m_context.mkTupleType(cvc4Sort(tupleSort.components));
}
default:
break;
}
smtAssert(false, "");
// Cannot be reached.
return m_context.integerType();
}
std::vector<CVC4::Type> CVC4Interface::cvc4Sort(std::vector<SortPointer> const& _sorts)
{
std::vector<CVC4::Type> cvc4Sorts;
for (auto const& _sort: _sorts)
cvc4Sorts.push_back(cvc4Sort(*_sort));
return cvc4Sorts;
}

74
libsmtutil/CVC4Interface.h
View File

@ -1,74 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsmtutil/SolverInterface.h>
#if defined(__GLIBC__)
// The CVC4 headers includes the deprecated system headers <ext/hash_map>
// and <ext/hash_set>. These headers cause a warning that will break the
// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set.
#define _GLIBCXX_PERMIT_BACKWARD_HASH
#endif
#include <cvc4/cvc4.h>
#if defined(__GLIBC__)
#undef _GLIBCXX_PERMIT_BACKWARD_HASH
#endif
namespace solidity::smtutil
{
class CVC4Interface: public SolverInterface
{
public:
/// Noncopyable.
CVC4Interface(CVC4Interface const&) = delete;
CVC4Interface& operator=(CVC4Interface const&) = delete;
CVC4Interface(std::optional<unsigned> _queryTimeout = {});
void reset() override;
void push() override;
void pop() override;
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
CVC4::Type cvc4Sort(Sort const& _sort);
std::vector<CVC4::Type> cvc4Sort(std::vector<SortPointer> const& _sorts);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;
std::map<std::string, CVC4::Expr> m_variables;
// CVC4 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
// The tests start failing for CVC4 with less than 6000,
// so using double that.
static int const resourceLimit = 12000;
};
}

14
libsmtutil/SMTPortfolio.cpp
View File

@ -18,12 +18,6 @@
#include <libsmtutil/SMTPortfolio.h>
#ifdef HAVE_Z3
#include <libsmtutil/Z3Interface.h>
#endif
#ifdef HAVE_CVC4
#include <libsmtutil/CVC4Interface.h>
#endif
#include <libsmtutil/SMTLib2Interface.h>
using namespace solidity;
@ -43,14 +37,6 @@ SMTPortfolio::SMTPortfolio(
solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
if (_enabledSolvers.smtlib2)
m_solvers.emplace_back(std::make_unique<SMTLib2Interface>(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout));
#ifdef HAVE_Z3
if (_enabledSolvers.z3 && Z3Interface::available())
m_solvers.emplace_back(std::make_unique<Z3Interface>(m_queryTimeout));
#endif
#ifdef HAVE_CVC4
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(std::make_unique<CVC4Interface>(m_queryTimeout));
#endif
}
void SMTPortfolio::reset()

242
libsmtutil/Z3CHCInterface.cpp
View File

@ -1,242 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/Z3CHCInterface.h>
#include <libsolutil/CommonIO.h>
#include <set>
#include <stack>
using namespace solidity;
using namespace solidity::smtutil;
Z3CHCInterface::Z3CHCInterface(std::optional<unsigned> _queryTimeout):
CHCSolverInterface(_queryTimeout),
m_z3Interface(std::make_unique<Z3Interface>(m_queryTimeout)),
m_context(m_z3Interface->context()),
m_solver(*m_context)
{
Z3_get_version(
&std::get<0>(m_version),
&std::get<1>(m_version),
&std::get<2>(m_version),
&std::get<3>(m_version)
);
// These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true);
if (m_queryTimeout)
m_context->set("timeout", int(*m_queryTimeout));
else
z3::set_param("rlimit", Z3Interface::resourceLimit);
setSpacerOptions();
}
void Z3CHCInterface::declareVariable(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort, "");
m_z3Interface->declareVariable(_name, _sort);
}
void Z3CHCInterface::registerRelation(Expression const& _expr)
{
m_solver.register_relation(m_z3Interface->functions().at(_expr.name));
}
void Z3CHCInterface::addRule(Expression const& _expr, std::string const& _name)
{
z3::expr rule = m_z3Interface->toZ3Expr(_expr);
if (m_z3Interface->constants().empty())
m_solver.add_rule(rule, m_context->str_symbol(_name.c_str()));
else
{
z3::expr_vector variables(*m_context);
for (auto const& var: m_z3Interface->constants())
variables.push_back(var.second);
z3::expr boundRule = z3::forall(variables, rule);
m_solver.add_rule(boundRule, m_context->str_symbol(_name.c_str()));
}
}
std::tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
{
CheckResult result;
try
{
z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
switch (m_solver.query(z3Expr))
{
case z3::check_result::sat:
{
result = CheckResult::SATISFIABLE;
// z3 version 4.8.8 modified Spacer to also return
// proofs containing nonlinear clauses.
if (m_version >= std::tuple(4, 8, 8, 0))
{
auto proof = m_solver.get_answer();
return {result, Expression(true), cexGraph(proof)};
}
break;
}
case z3::check_result::unsat:
{
result = CheckResult::UNSATISFIABLE;
auto invariants = m_z3Interface->fromZ3Expr(m_solver.get_answer());
return {result, std::move(invariants), {}};
}
case z3::check_result::unknown:
{
result = CheckResult::UNKNOWN;
break;
}
}
// TODO retrieve model / invariants
}
catch (z3::exception const& _err)
{
std::set<std::string> msgs{
/// Resource limit (rlimit) exhausted.
"max. resource limit exceeded",
/// User given timeout exhausted.
"canceled"
};
if (msgs.count(_err.msg()))
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
}
return {result, Expression(true), {}};
}
void Z3CHCInterface::setSpacerOptions(bool _preProcessing)
{
// Spacer options.
// These needs to be set in the solver.
// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
z3::params p(*m_context);
// These are useful for solving problems with arrays and loops.
// Use quantified lemma generalizer.
p.set("fp.spacer.q3.use_qgen", true);
p.set("fp.spacer.mbqi", false);
// Ground pobs by using values from a model.
p.set("fp.spacer.ground_pobs", false);
// Spacer optimization should be
// - enabled for better solving (default)
// - disable for counterexample generation
p.set("fp.xform.slice", _preProcessing);
p.set("fp.xform.inline_linear", _preProcessing);
p.set("fp.xform.inline_eager", _preProcessing);
m_solver.set(p);
}
/**
Convert a ground refutation into a linear or nonlinear counterexample.
The counterexample is given as an implication graph of the form
`premises => conclusion` where `premises` are the predicates
from the body of nonlinear clauses, representing the proof graph.
This function is based on and similar to
https://github.com/Z3Prover/z3/blob/z3-4.8.8/src/muz/spacer/spacer_context.cpp#L2919
(spacer::context::get_ground_sat_answer)
which generates linear counterexamples.
It is modified here to accept nonlinear CHCs as well, generating a DAG
instead of a path.
*/
CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
{
/// The root fact of the refutation proof is `false`.
/// The node itself is not a hyper resolution, so we need to
/// extract the `query` hyper resolution node from the
/// `false` node (the first child).
/// The proof has the shape above for z3 >=4.8.8.
/// If an older version is used, this check will fail and no
/// counterexample will be generated.
if (!_proof.is_app() || fact(_proof).decl().decl_kind() != Z3_OP_FALSE)
return {};
CexGraph graph;
std::stack<z3::expr> proofStack;
proofStack.push(_proof.arg(0));
auto const& root = proofStack.top();
graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root)));
std::set<unsigned> visited;
visited.insert(root.id());
while (!proofStack.empty())
{
z3::expr proofNode = proofStack.top();
smtAssert(graph.nodes.count(proofNode.id()), "");
proofStack.pop();
if (proofNode.is_app() && proofNode.decl().decl_kind() == Z3_OP_PR_HYPER_RESOLVE)
{
smtAssert(proofNode.num_args() > 0, "");
for (unsigned i = 1; i < proofNode.num_args() - 1; ++i)
{
z3::expr child = proofNode.arg(i);
if (!visited.count(child.id()))
{
visited.insert(child.id());
proofStack.push(child);
}
if (!graph.nodes.count(child.id()))
{
graph.nodes.emplace(child.id(), m_z3Interface->fromZ3Expr(fact(child)));
graph.edges[child.id()] = {};
}
graph.edges[proofNode.id()].push_back(child.id());
}
}
}
return graph;
}
z3::expr Z3CHCInterface::fact(z3::expr const& _node)
{
smtAssert(_node.is_app(), "");
if (_node.num_args() == 0)
return _node;
return _node.arg(_node.num_args() - 1);
}
std::string Z3CHCInterface::name(z3::expr const& _predicate)
{
smtAssert(_predicate.is_app(), "");
return _predicate.decl().name().str();
}
std::vector<std::string> Z3CHCInterface::arguments(z3::expr const& _predicate)
{
smtAssert(_predicate.is_app(), "");
std::vector<std::string> args;
for (unsigned i = 0; i < _predicate.num_args(); ++i)
args.emplace_back(_predicate.arg(i).to_string());
return args;
}

72
libsmtutil/Z3CHCInterface.h
View File

@ -1,72 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
/**
* Z3 specific Horn solver interface.
*/
#pragma once
#include <libsmtutil/CHCSolverInterface.h>
#include <libsmtutil/Z3Interface.h>
#include <tuple>
#include <vector>
namespace solidity::smtutil
{
class Z3CHCInterface: public CHCSolverInterface
{
public:
Z3CHCInterface(std::optional<unsigned> _queryTimeout = {});
/// Forwards variable declaration to Z3Interface.
void declareVariable(std::string const& _name, SortPointer const& _sort) override;
void registerRelation(Expression const& _expr) override;
void addRule(Expression const& _expr, std::string const& _name) override;
std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
Z3Interface* z3Interface() const { return m_z3Interface.get(); }
void setSpacerOptions(bool _preProcessing = true);
private:
/// Constructs a nonlinear counterexample graph from the refutation.
CHCSolverInterface::CexGraph cexGraph(z3::expr const& _proof);
/// @returns the fact from a proof node.
z3::expr fact(z3::expr const& _node);
/// @returns @a _predicate's name.
std::string name(z3::expr const& _predicate);
/// @returns the arguments of @a _predicate.
std::vector<std::string> arguments(z3::expr const& _predicate);
// Used to handle variables.
std::unique_ptr<Z3Interface> m_z3Interface;
z3::context* m_context;
// Horn solver.
z3::fixedpoint m_solver;
std::tuple<unsigned, unsigned, unsigned, unsigned> m_version = std::tuple(0, 0, 0, 0);
};
}

479
libsmtutil/Z3Interface.cpp
View File

@ -1,479 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/Z3Interface.h>
#include <libsolutil/CommonData.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/Exceptions.h>
#ifdef HAVE_Z3_DLOPEN
#include <libsmtutil/Z3Loader.h>
#endif
using namespace solidity::smtutil;
using namespace solidity::util;
bool Z3Interface::available()
{
#ifdef HAVE_Z3_DLOPEN
return Z3Loader::get().available();
#else
return true;
#endif
}
Z3Interface::Z3Interface(std::optional<unsigned> _queryTimeout):
SolverInterface(_queryTimeout),
m_solver(m_context)
{
// These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true);
if (m_queryTimeout)
m_context.set("timeout", int(*m_queryTimeout));
else
z3::set_param("rlimit", resourceLimit);
}
void Z3Interface::reset()
{
m_constants.clear();
m_functions.clear();
m_solver.reset();
}
void Z3Interface::push()
{
m_solver.push();
}
void Z3Interface::pop()
{
m_solver.pop();
}
void Z3Interface::declareVariable(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, *_sort);
else if (m_constants.count(_name))
m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(*_sort));
else
m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(*_sort)));
}
void Z3Interface::declareFunction(std::string const& _name, Sort const& _sort)
{
smtAssert(_sort.kind == Kind::Function, "");
FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
if (m_functions.count(_name))
m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain));
else
m_functions.emplace(_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain)));
}
void Z3Interface::addAssertion(Expression const& _expr)
{
m_solver.add(toZ3Expr(_expr));
}
std::pair<CheckResult, std::vector<std::string>> Z3Interface::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
std::vector<std::string> values;
try
{
switch (m_solver.check())
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
break;
}
if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
values.push_back(util::toString(m.eval(toZ3Expr(e))));
}
}
catch (z3::exception const& _err)
{
std::set<std::string> msgs{
/// Resource limit (rlimit) exhausted.
"max. resource limit exceeded",
/// User given timeout exhausted.
"canceled"
};
if (msgs.count(_err.msg()))
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
values.clear();
}
return std::make_pair(result, values);
}
z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
{
if (_expr.arguments.empty() && m_constants.count(_expr.name))
return m_constants.at(_expr.name);
z3::expr_vector arguments(m_context);
for (auto const& arg: _expr.arguments)
arguments.push_back(toZ3Expr(arg));
try
{
std::string const& n = _expr.name;
if (m_functions.count(n))
return m_functions.at(n)(arguments);
else if (m_constants.count(n))
{
smtAssert(arguments.empty(), "");
return m_constants.at(n);
}
else if (arguments.empty())
{
if (n == "true")
return m_context.bool_val(true);
else if (n == "false")
return m_context.bool_val(false);
else if (_expr.sort->kind == Kind::Sort)
{
auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.sort);
smtAssert(sortSort, "");
return m_context.constant(n.c_str(), z3Sort(*sortSort->inner));
}
else
try
{
return m_context.int_val(n.c_str());
}
catch (z3::exception const& _e)
{
smtAssert(false, _e.msg());
}
}
smtAssert(_expr.hasCorrectArity(), "");
if (n == "ite")
return z3::ite(arguments[0], arguments[1], arguments[2]);
else if (n == "not")
return !arguments[0];
else if (n == "and")
return arguments[0] && arguments[1];
else if (n == "or")
return arguments[0] || arguments[1];
else if (n == "=>")
return z3::implies(arguments[0], arguments[1]);
else if (n == "=")
return arguments[0] == arguments[1];
else if (n == "<")
return arguments[0] < arguments[1];
else if (n == "<=")
return arguments[0] <= arguments[1];
else if (n == ">")
return arguments[0] > arguments[1];
else if (n == ">=")
return arguments[0] >= arguments[1];
else if (n == "+")
return arguments[0] + arguments[1];
else if (n == "-")
return arguments[0] - arguments[1];
else if (n == "*")
return arguments[0] * arguments[1];
else if (n == "div")
return arguments[0] / arguments[1];
else if (n == "mod")
return z3::mod(arguments[0], arguments[1]);
else if (n == "bvnot")
return ~arguments[0];
else if (n == "bvand")
return arguments[0] & arguments[1];
else if (n == "bvor")
return arguments[0] | arguments[1];
else if (n == "bvxor")
return arguments[0] ^ arguments[1];
else if (n == "bvshl")
return z3::shl(arguments[0], arguments[1]);
else if (n == "bvlshr")
return z3::lshr(arguments[0], arguments[1]);
else if (n == "bvashr")
return z3::ashr(arguments[0], arguments[1]);
else if (n == "int2bv")
{
size_t size = std::stoul(_expr.arguments[1].name);
return z3::int2bv(static_cast<unsigned>(size), arguments[0]);
}
else if (n == "bv2int")
{
auto intSort = std::dynamic_pointer_cast<IntSort>(_expr.sort);
smtAssert(intSort, "");
return z3::bv2int(arguments[0], intSort->isSigned);
}
else if (n == "select")
return z3::select(arguments[0], arguments[1]);
else if (n == "store")
return z3::store(arguments[0], arguments[1], arguments[2]);
else if (n == "const_array")
{
std::shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
smtAssert(sortSort, "");
auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
smtAssert(arraySort && arraySort->domain, "");
return z3::const_array(z3Sort(*arraySort->domain), arguments[1]);
}
else if (n == "tuple_get")
{
size_t index = stoul(_expr.arguments[1].name);
return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), static_cast<unsigned>(index)))(arguments[0]);
}
else if (n == "tuple_constructor")
{
auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
smtAssert(constructor.arity() == arguments.size(), "");
z3::expr_vector args(m_context);
for (auto const& arg: arguments)
args.push_back(arg);
return constructor(args);
}
smtAssert(false);
}
catch (z3::exception const& _e)
{
smtAssert(false, _e.msg());
}
smtAssert(false);
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
util::unreachable();
}
Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
{
auto sort = fromZ3Sort(_expr.get_sort());
if (_expr.is_const() || _expr.is_var())
return Expression(_expr.to_string(), {}, sort);
if (_expr.is_quantifier())
{
std::string quantifierName;
if (_expr.is_exists())
quantifierName = "exists";
else if (_expr.is_forall())
quantifierName = "forall";
else if (_expr.is_lambda())
quantifierName = "lambda";
else
smtAssert(false, "");
return Expression(quantifierName, {fromZ3Expr(_expr.body())}, sort);
}
smtAssert(_expr.is_app(), "");
std::vector<Expression> arguments;
for (unsigned i = 0; i < _expr.num_args(); ++i)
arguments.push_back(fromZ3Expr(_expr.arg(i)));
auto kind = _expr.decl().decl_kind();
if (_expr.is_ite())
return Expression::ite(arguments[0], arguments[1], arguments[2]);
else if (_expr.is_not())
return !arguments[0];
else if (_expr.is_and())
return Expression::mkAnd(arguments);
else if (_expr.is_or())
return Expression::mkOr(arguments);
else if (_expr.is_implies())
return Expression::implies(arguments[0], arguments[1]);
else if (_expr.is_eq())
{
smtAssert(arguments.size() == 2, "");
return arguments[0] == arguments[1];
}
else if (kind == Z3_OP_ULT || kind == Z3_OP_SLT)
return arguments[0] < arguments[1];
else if (kind == Z3_OP_LE || kind == Z3_OP_ULEQ || kind == Z3_OP_SLEQ)
return arguments[0] <= arguments[1];
else if (kind == Z3_OP_GT || kind == Z3_OP_SGT)
return arguments[0] > arguments[1];
else if (kind == Z3_OP_GE || kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ)
return arguments[0] >= arguments[1];
else if (kind == Z3_OP_ADD)
return Expression::mkPlus(arguments);
else if (kind == Z3_OP_SUB)
{
smtAssert(arguments.size() == 2, "");
return arguments[0] - arguments[1];
}
else if (kind == Z3_OP_MUL)
return Expression::mkMul(arguments);
else if (kind == Z3_OP_DIV)
{
smtAssert(arguments.size() == 2, "");
return arguments[0] / arguments[1];
}
else if (kind == Z3_OP_MOD)
return arguments[0] % arguments[1];
else if (kind == Z3_OP_XOR)
return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BOR)
return arguments[0] | arguments[1];
else if (kind == Z3_OP_BAND)
return arguments[0] & arguments[1];
else if (kind == Z3_OP_BXOR)
return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BNOT)
return !arguments[0];
else if (kind == Z3_OP_BSHL)
return arguments[0] << arguments[1];
else if (kind == Z3_OP_BLSHR)
return arguments[0] >> arguments[1];
else if (kind == Z3_OP_BASHR)
return Expression::ashr(arguments[0], arguments[1]);
else if (kind == Z3_OP_INT2BV)
return Expression::int2bv(arguments[0], _expr.get_sort().bv_size());
else if (kind == Z3_OP_BV2INT)
return Expression::bv2int(arguments[0]);
else if (kind == Z3_OP_EXTRACT)
return Expression("extract", arguments, sort);
else if (kind == Z3_OP_SELECT)
return Expression::select(arguments[0], arguments[1]);
else if (kind == Z3_OP_STORE)
return Expression::store(arguments[0], arguments[1], arguments[2]);
else if (kind == Z3_OP_CONST_ARRAY)
{
auto sortSort = std::make_shared<SortSort>(fromZ3Sort(_expr.get_sort()));
return Expression::const_array(Expression(sortSort), arguments[0]);
}
else if (kind == Z3_OP_DT_CONSTRUCTOR)
{
auto sortSort = std::make_shared<SortSort>(fromZ3Sort(_expr.get_sort()));
return Expression::tuple_constructor(Expression(sortSort), arguments);
}
else if (kind == Z3_OP_DT_ACCESSOR)
return Expression("dt_accessor_" + _expr.decl().name().str(), arguments, sort);
else if (kind == Z3_OP_DT_IS)
return Expression("dt_is", {arguments.at(0)}, sort);
else if (
kind == Z3_OP_UNINTERPRETED ||
kind == Z3_OP_RECURSIVE
)
return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
smtAssert(false);
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
util::unreachable();
}
z3::sort Z3Interface::z3Sort(Sort const& _sort)
{
switch (_sort.kind)
{
case Kind::Bool:
return m_context.bool_sort();
case Kind::Int:
return m_context.int_sort();
case Kind::BitVector:
return m_context.bv_sort(dynamic_cast<BitVectorSort const&>(_sort).size);
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range));
}
case Kind::Tuple:
{
auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
std::vector<char const*> cMembers;
for (auto const& member: tupleSort.members)
cMembers.emplace_back(member.c_str());
/// Using this instead of the function below because with that one
/// we can't use `&sorts[0]` here.
std::vector<z3::sort> sorts;
for (auto const& sort: tupleSort.components)
sorts.push_back(z3Sort(*sort));
z3::func_decl_vector projs(m_context);
z3::func_decl tupleConstructor = m_context.tuple_sort(
tupleSort.name.c_str(),
static_cast<unsigned>(tupleSort.members.size()),
cMembers.data(),
sorts.data(),
projs
);
return tupleConstructor.range();
}
default:
break;
}
smtAssert(false, "");
// Cannot be reached.
return m_context.int_sort();
}
z3::sort_vector Z3Interface::z3Sort(std::vector<SortPointer> const& _sorts)
{
z3::sort_vector z3Sorts(m_context);
for (auto const& _sort: _sorts)
z3Sorts.push_back(z3Sort(*_sort));
return z3Sorts;
}
SortPointer Z3Interface::fromZ3Sort(z3::sort const& _sort)
{
if (_sort.is_bool())
return SortProvider::boolSort;
if (_sort.is_int())
return SortProvider::sintSort;
if (_sort.is_bv())
return std::make_shared<BitVectorSort>(_sort.bv_size());
if (_sort.is_array())
return std::make_shared<ArraySort>(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range()));
if (_sort.is_datatype())
{
auto name = _sort.name().str();
auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, _sort));
std::vector<std::string> memberNames;
std::vector<SortPointer> memberSorts;
for (unsigned i = 0; i < constructor.arity(); ++i)
{
auto accessor = z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, _sort, i));
memberNames.push_back(accessor.name().str());
memberSorts.push_back(fromZ3Sort(accessor.range()));
}
return std::make_shared<TupleSort>(name, memberNames, memberSorts);
}
smtAssert(false, "");
}
std::vector<SortPointer> Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts)
{
return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); });
}

75
libsmtutil/Z3Interface.h
View File

@ -1,75 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsmtutil/SolverInterface.h>
#include <z3++.h>
namespace solidity::smtutil
{
class Z3Interface: public SolverInterface
{
public:
/// Noncopyable.
Z3Interface(Z3Interface const&) = delete;
Z3Interface& operator=(Z3Interface const&) = delete;
Z3Interface(std::optional<unsigned> _queryTimeout = {});
static bool available();
void reset() override;
void push() override;
void pop() override;
void declareVariable(std::string const& _name, SortPointer const& _sort) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
z3::expr toZ3Expr(Expression const& _expr);
smtutil::Expression fromZ3Expr(z3::expr const& _expr);
std::map<std::string, z3::expr> constants() const { return m_constants; }
std::map<std::string, z3::func_decl> functions() const { return m_functions; }
z3::context* context() { return &m_context; }
// Z3 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
static int const resourceLimit = 1000000;
private:
void declareFunction(std::string const& _name, Sort const& _sort);
z3::sort z3Sort(Sort const& _sort);
z3::sort_vector z3Sort(std::vector<SortPointer> const& _sorts);
smtutil::SortPointer fromZ3Sort(z3::sort const& _sort);
std::vector<smtutil::SortPointer> fromZ3Sort(z3::sort_vector const& _sorts);
z3::context m_context;
z3::solver m_solver;
std::map<std::string, z3::expr> m_constants;
std::map<std::string, z3::func_decl> m_functions;
};
}

69
libsmtutil/Z3Loader.cpp
View File

@ -1,69 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/Z3Loader.h>
#include <libsmtutil/Exceptions.h>
#include <z3.h>
#include <z3_version.h>
#include <vector>
#ifndef _GNU_SOURCE
#define _GNU_SOURCE
#endif
#include <dlfcn.h>
using namespace solidity;
using namespace solidity::smtutil;
Z3Loader const& Z3Loader::get()
{
static Z3Loader z3;
return z3;
}
void* Z3Loader::loadSymbol(char const* _name) const
{
smtAssert(m_handle, "Attempted to use dynamically loaded Z3, even though it is not available.");
void* sym = dlsym(m_handle, _name);
smtAssert(sym, std::string("Symbol \"") + _name + "\" not found in libz3.so");
return sym;
}
bool Z3Loader::available() const
{
if (m_handle == nullptr)
return false;
unsigned major = 0;
unsigned minor = 0;
unsigned build = 0;
unsigned rev = 0;
Z3_get_version(&major, &minor, &build, &rev);
return major == Z3_MAJOR_VERSION && minor == Z3_MINOR_VERSION;
}
Z3Loader::Z3Loader()
{
std::string libname{"libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION)};
m_handle = dlmopen(LM_ID_NEWLM, libname.c_str(), RTLD_NOW);
}
Z3Loader::~Z3Loader()
{
if (m_handle)
dlclose(m_handle);
}

38
libsmtutil/Z3Loader.h
View File

@ -1,38 +0,0 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
namespace solidity::smtutil
{
class Z3Loader
{
public:
Z3Loader(Z3Loader const&) = delete;
Z3Loader& operator=(Z3Loader const&) = delete;
static Z3Loader const& get();
void* loadSymbol(char const* _name) const;
bool available() const;
private:
Z3Loader();
~Z3Loader();
void* m_handle = nullptr;
};
}

8
libsolidity/formal/BMC.cpp
View File

@ -27,9 +27,6 @@
#include <utility>
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#endif
using namespace solidity;
using namespace solidity::util;
@ -51,7 +48,6 @@ BMC::BMC(
))
{
solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
if (!_smtlib2Responses.empty())
m_errorReporter.warning(
@ -61,7 +57,6 @@ BMC::BMC(
"These responses will be ignored."
"Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
);
#endif
}
void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
@ -136,9 +131,6 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
SourceLocation(),
"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." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION) + " to enable Z3."
#endif
);
}

60
libsolidity/formal/CHC.cpp
View File

@ -37,10 +37,6 @@
#include <libsolutil/Algorithms.h>
#include <libsolutil/StringUtils.h>
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#endif
#include <boost/algorithm/string.hpp>
#include <range/v3/algorithm/for_each.hpp>
@ -1172,32 +1168,15 @@ void CHC::resetSourceAnalysis()
m_blockCounter = 0;
// 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)
{
#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 (!m_settings.solvers.z3)
{
solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld);
solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld || m_settings.solvers.z3);
if (!m_interface)
m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
if (!m_interface)
m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, "");
smtlib2Interface->reset();
m_context.setSolver(smtlib2Interface->smtlib2Interface());
}
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, "");
smtlib2Interface->reset();
m_context.setSolver(smtlib2Interface->smtlib2Interface());
m_context.reset();
m_context.resetUniqueId();
@ -1821,32 +1800,7 @@ std::tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::
switch (result)
{
case CheckResult::SATISFIABLE:
{
// 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());
solAssert(spacer, "");
spacer->setSpacerOptions(false);
CheckResult resultNoOpt;
smtutil::Expression invariantNoOpt(true);
CHCSolverInterface::CexGraph cexNoOpt;
std::tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query);
if (resultNoOpt == CheckResult::SATISFIABLE)
cex = std::move(cexNoOpt);
spacer->setSpacerOptions(true);
#else
solAssert(false);
#endif
}
break;
}
case CheckResult::UNSATISFIABLE:
break;
case CheckResult::UNKNOWN:

11
libsolidity/formal/ModelChecker.cpp
View File

@ -165,12 +165,8 @@ 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
#ifdef HAVE_CVC4
available.cvc4 = true;
available.z3 = !boost::process::search_path("z3").empty();
available.cvc4 = !boost::process::search_path("cvc4").empty();
#endif
return available;
}
@ -210,9 +206,6 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er
8158_error,
SourceLocation(),
"Solver z3 was selected for SMTChecker but it is not available."
#ifdef HAVE_Z3_DLOPEN
" libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION) + " was not found."
#endif
);
}

25
libsolidity/interface/SMTSolverCommand.cpp
View File

@ -37,41 +37,44 @@ using solidity::util::errinfo_comment;
namespace solidity::frontend
{
SMTSolverCommand::SMTSolverCommand(std::string _solverCmd) : m_solverCmd(_solverCmd) {}
ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query)
{
try
{
if (_kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
solAssert(false, "SMTQuery callback used as callback kind " + _kind);
auto pos = _kind.find(' ');
auto kind = _kind.substr(0, pos);
auto solverCommand = _kind.substr(pos + 1);
if (kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
solAssert(false, "SMTQuery callback used as callback kind " + kind);
auto tempDir = solidity::util::TemporaryDirectory("smt");
util::h256 queryHash = util::keccak256(_query);
auto queryFileName = tempDir.path() / ("query_" + queryHash.hex() + ".smt2");
auto queryFile = boost::filesystem::ofstream(queryFileName);
queryFile << _query;
auto eldBin = boost::process::search_path(m_solverCmd);
std::string solverBinary = solverCommand.substr(0, solverCommand.find(' '));
auto pathToBinary = boost::process::search_path(solverBinary);
if (eldBin.empty())
return ReadCallback::Result{false, m_solverCmd + " binary not found."};
if (pathToBinary.empty())
return ReadCallback::Result{false, solverBinary + " binary not found."};
boost::process::ipstream pipe;
boost::process::child eld(
eldBin,
boost::process::child solver(
pathToBinary,
queryFileName,
boost::process::std_out > pipe
);
std::vector<std::string> data;
std::string line;
while (eld.running() && std::getline(pipe, line))
while (solver.running() && std::getline(pipe, line))
if (!line.empty())
data.push_back(line);
eld.wait();
solver.wait();
return ReadCallback::Result{true, boost::join(data, "\n")};
}

11
libsolidity/interface/SMTSolverCommand.h
View File

@ -28,19 +28,20 @@ namespace solidity::frontend
class SMTSolverCommand
{
public:
SMTSolverCommand(std::string _solverCmd);
SMTSolverCommand() = default;
/// Calls an SMT solver with the given query.
frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query);
frontend::ReadCallback::Callback solver()
{
return [this](std::string const& _kind, std::string const& _query) { return solve(_kind, _query); };
return [this](std::string const& _kind, std::string const& _query) {
// TODO: Should be equal
solAssert(_kind.rfind(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), 0) == 0);
return solve(_kind, _query);
};
}
private:
/// The name of the solver's binary.
std::string const m_solverCmd;
};
}

2
solc/CommandLineInterface.h
View File

@ -141,7 +141,7 @@ private:
std::ostream& m_serr;
bool m_hasOutput = false;
FileReader m_fileReader;
SMTSolverCommand m_solverCommand{"eld"};
SMTSolverCommand m_solverCommand;
UniversalCallback m_universalCallback{m_fileReader, m_solverCommand};
std::optional<std::string> m_standardJsonInput;
std::unique_ptr<frontend::CompilerStack> m_compiler;