From 1e190abf6e6096aa3988f46272051a692e342026 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Tue, 20 Jun 2023 16:10:45 +0200 Subject: [PATCH] Initial work on unified way to interact with solvers --- CMakeLists.txt | 57 --- libsmtutil/CHCSmtLib2Interface.cpp | 19 +- libsmtutil/CMakeLists.txt | 34 +- libsmtutil/CVC4Interface.cpp | 336 --------------- libsmtutil/CVC4Interface.h | 74 ---- libsmtutil/SMTPortfolio.cpp | 14 - libsmtutil/Z3CHCInterface.cpp | 242 ----------- libsmtutil/Z3CHCInterface.h | 72 ---- libsmtutil/Z3Interface.cpp | 479 --------------------- libsmtutil/Z3Interface.h | 75 ---- libsmtutil/Z3Loader.cpp | 69 --- libsmtutil/Z3Loader.h | 38 -- libsolidity/formal/BMC.cpp | 8 - libsolidity/formal/CHC.cpp | 60 +-- libsolidity/formal/ModelChecker.cpp | 11 +- libsolidity/interface/SMTSolverCommand.cpp | 25 +- libsolidity/interface/SMTSolverCommand.h | 11 +- solc/CommandLineInterface.h | 2 +- 18 files changed, 43 insertions(+), 1583 deletions(-) delete mode 100644 libsmtutil/CVC4Interface.cpp delete mode 100644 libsmtutil/CVC4Interface.h delete mode 100644 libsmtutil/Z3CHCInterface.cpp delete mode 100644 libsmtutil/Z3CHCInterface.h delete mode 100644 libsmtutil/Z3Interface.cpp delete mode 100644 libsmtutil/Z3Interface.h delete mode 100644 libsmtutil/Z3Loader.cpp delete mode 100644 libsmtutil/Z3Loader.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 73e7930b7..29a23a20e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index ef7c56ac0..89cee2a3f 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -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"; diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index af7f47b60..0c1afda8d 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -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() diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp deleted file mode 100644 index f53c92ab5..000000000 --- a/libsmtutil/CVC4Interface.cpp +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include - -#include -#include - -#include - -using namespace solidity; -using namespace solidity::util; -using namespace solidity::smtutil; - -CVC4Interface::CVC4Interface(std::optional _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> CVC4Interface::check(std::vector const& _expressionsToEvaluate) -{ - CheckResult result; - std::vector 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 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(_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(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(_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 = std::dynamic_pointer_cast(_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 = std::dynamic_pointer_cast(_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 = std::dynamic_pointer_cast(_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(_sort).size); - case Kind::Function: - { - FunctionSort const& fSort = dynamic_cast(_sort); - return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain)); - } - case Kind::Array: - { - auto const& arraySort = dynamic_cast(_sort); - return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range)); - } - case Kind::Tuple: - { - auto const& tupleSort = dynamic_cast(_sort); - return m_context.mkTupleType(cvc4Sort(tupleSort.components)); - } - default: - break; - } - smtAssert(false, ""); - // Cannot be reached. - return m_context.integerType(); -} - -std::vector CVC4Interface::cvc4Sort(std::vector const& _sorts) -{ - std::vector cvc4Sorts; - for (auto const& _sort: _sorts) - cvc4Sorts.push_back(cvc4Sort(*_sort)); - return cvc4Sorts; -} diff --git a/libsmtutil/CVC4Interface.h b/libsmtutil/CVC4Interface.h deleted file mode 100644 index cc3c0577c..000000000 --- a/libsmtutil/CVC4Interface.h +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#pragma once - -#include - -#if defined(__GLIBC__) -// The CVC4 headers includes the deprecated system headers -// and . These headers cause a warning that will break the -// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set. -#define _GLIBCXX_PERMIT_BACKWARD_HASH -#endif - -#include - -#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 _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> check(std::vector const& _expressionsToEvaluate) override; - -private: - CVC4::Expr toCVC4Expr(Expression const& _expr); - CVC4::Type cvc4Sort(Sort const& _sort); - std::vector cvc4Sort(std::vector const& _sorts); - - CVC4::ExprManager m_context; - CVC4::SmtEngine m_solver; - std::map 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; -}; - -} diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 76c69d018..89c2d410c 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -18,12 +18,6 @@ #include -#ifdef HAVE_Z3 -#include -#endif -#ifdef HAVE_CVC4 -#include -#endif #include 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(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout)); -#ifdef HAVE_Z3 - if (_enabledSolvers.z3 && Z3Interface::available()) - m_solvers.emplace_back(std::make_unique(m_queryTimeout)); -#endif -#ifdef HAVE_CVC4 - if (_enabledSolvers.cvc4) - m_solvers.emplace_back(std::make_unique(m_queryTimeout)); -#endif } void SMTPortfolio::reset() diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp deleted file mode 100644 index a25890e8d..000000000 --- a/libsmtutil/Z3CHCInterface.cpp +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include - -#include - -#include -#include - -using namespace solidity; -using namespace solidity::smtutil; - -Z3CHCInterface::Z3CHCInterface(std::optional _queryTimeout): - CHCSolverInterface(_queryTimeout), - m_z3Interface(std::make_unique(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 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 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 proofStack; - proofStack.push(_proof.arg(0)); - - auto const& root = proofStack.top(); - graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root))); - - std::set 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 Z3CHCInterface::arguments(z3::expr const& _predicate) -{ - smtAssert(_predicate.is_app(), ""); - std::vector args; - for (unsigned i = 0; i < _predicate.num_args(); ++i) - args.emplace_back(_predicate.arg(i).to_string()); - return args; -} diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h deleted file mode 100644 index 5a768f65c..000000000 --- a/libsmtutil/Z3CHCInterface.h +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -/** - * Z3 specific Horn solver interface. - */ - -#pragma once - -#include -#include - -#include -#include - -namespace solidity::smtutil -{ - -class Z3CHCInterface: public CHCSolverInterface -{ -public: - Z3CHCInterface(std::optional _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 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 arguments(z3::expr const& _predicate); - - // Used to handle variables. - std::unique_ptr m_z3Interface; - - z3::context* m_context; - // Horn solver. - z3::fixedpoint m_solver; - - std::tuple m_version = std::tuple(0, 0, 0, 0); -}; - -} diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp deleted file mode 100644 index a16e75668..000000000 --- a/libsmtutil/Z3Interface.cpp +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include - -#include -#include -#include - -#ifdef HAVE_Z3_DLOPEN -#include -#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 _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(_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> Z3Interface::check(std::vector const& _expressionsToEvaluate) -{ - CheckResult result; - std::vector 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 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(_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(size), arguments[0]); - } - else if (n == "bv2int") - { - auto intSort = std::dynamic_pointer_cast(_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 = std::dynamic_pointer_cast(_expr.arguments[0].sort); - smtAssert(sortSort, ""); - auto arraySort = std::dynamic_pointer_cast(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(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 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(fromZ3Sort(_expr.get_sort())); - return Expression::const_array(Expression(sortSort), arguments[0]); - } - else if (kind == Z3_OP_DT_CONSTRUCTOR) - { - auto sortSort = std::make_shared(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(_sort).size); - case Kind::Array: - { - auto const& arraySort = dynamic_cast(_sort); - return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range)); - } - case Kind::Tuple: - { - auto const& tupleSort = dynamic_cast(_sort); - std::vector 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 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(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 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(_sort.bv_size()); - if (_sort.is_array()) - return std::make_shared(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 memberNames; - std::vector 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(name, memberNames, memberSorts); - } - smtAssert(false, ""); -} - -std::vector Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts) -{ - return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); }); -} diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h deleted file mode 100644 index ee268ac41..000000000 --- a/libsmtutil/Z3Interface.h +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#pragma once - -#include -#include - -namespace solidity::smtutil -{ - -class Z3Interface: public SolverInterface -{ -public: - /// Noncopyable. - Z3Interface(Z3Interface const&) = delete; - Z3Interface& operator=(Z3Interface const&) = delete; - - Z3Interface(std::optional _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> check(std::vector const& _expressionsToEvaluate) override; - - z3::expr toZ3Expr(Expression const& _expr); - smtutil::Expression fromZ3Expr(z3::expr const& _expr); - - std::map constants() const { return m_constants; } - std::map 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 const& _sorts); - smtutil::SortPointer fromZ3Sort(z3::sort const& _sort); - std::vector fromZ3Sort(z3::sort_vector const& _sorts); - - z3::context m_context; - z3::solver m_solver; - - std::map m_constants; - std::map m_functions; -}; - -} diff --git a/libsmtutil/Z3Loader.cpp b/libsmtutil/Z3Loader.cpp deleted file mode 100644 index 0211f600d..000000000 --- a/libsmtutil/Z3Loader.cpp +++ /dev/null @@ -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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include -#include -#include -#include -#include - -#ifndef _GNU_SOURCE -#define _GNU_SOURCE -#endif -#include - -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); -} diff --git a/libsmtutil/Z3Loader.h b/libsmtutil/Z3Loader.h deleted file mode 100644 index 5e755cb24..000000000 --- a/libsmtutil/Z3Loader.h +++ /dev/null @@ -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 . -*/ -// 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; -}; - -} \ No newline at end of file diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dede97cc0..cb6b027f9 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -27,9 +27,6 @@ #include -#ifdef HAVE_Z3_DLOPEN -#include -#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, smt::EncodingContext::IdCompare> _solvedTargets) @@ -136,9 +131,6 @@ void BMC::analyze(SourceUnit const& _source, std::map #include -#ifdef HAVE_Z3_DLOPEN -#include -#endif - #include #include @@ -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(m_settings.timeout); - auto z3Interface = dynamic_cast(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(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); + if (!m_interface) + m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); - auto smtlib2Interface = dynamic_cast(m_interface.get()); - solAssert(smtlib2Interface, ""); - smtlib2Interface->reset(); - m_context.setSolver(smtlib2Interface->smtlib2Interface()); - } + auto smtlib2Interface = dynamic_cast(m_interface.get()); + solAssert(smtlib2Interface, ""); + smtlib2Interface->reset(); + m_context.setSolver(smtlib2Interface->smtlib2Interface()); m_context.reset(); m_context.resetUniqueId(); @@ -1821,32 +1800,7 @@ std::tuple 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(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: diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 5632ff5c4..1644e6a92 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -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 ); } diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp index 92e0485b8..2c8209f75 100644 --- a/libsolidity/interface/SMTSolverCommand.cpp +++ b/libsolidity/interface/SMTSolverCommand.cpp @@ -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 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")}; } diff --git a/libsolidity/interface/SMTSolverCommand.h b/libsolidity/interface/SMTSolverCommand.h index 56a6ba171..fad3dfe4b 100644 --- a/libsolidity/interface/SMTSolverCommand.h +++ b/libsolidity/interface/SMTSolverCommand.h @@ -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; }; } diff --git a/solc/CommandLineInterface.h b/solc/CommandLineInterface.h index 5de69270b..22ac6023a 100644 --- a/solc/CommandLineInterface.h +++ b/solc/CommandLineInterface.h @@ -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 m_standardJsonInput; std::unique_ptr m_compiler;