From 3cf099bf01dd7911c1bb347b608bd8b45e64420c Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 6 May 2024 18:58:58 +0200 Subject: [PATCH] SMTChecker: Upgrade CVC4 to cvc5 Instead of compiling `solc` itself with CVC4 support, it is now enough to have `cvc5` executable on PATH when running the compiler. Instead of using API of CVC4, we now use SMT-LIB2 interface. That means we write the queries to temporary SMT-LIB2 files and call the solver process directly to run on the file. --- CMakeLists.txt | 12 +- cmake/EthCompilerSettings.cmake | 1 - cmake/FindCVC4.cmake | 33 -- docs/installing-solidity.rst | 9 - docs/smtchecker.rst | 6 +- docs/using-the-compiler.rst | 2 +- libsmtutil/CMakeLists.txt | 12 +- libsmtutil/CVC4Interface.cpp | 336 ------------------ libsmtutil/CVC4Interface.h | 74 ---- libsmtutil/SMTLib2Interface.cpp | 6 +- libsmtutil/SMTPortfolio.cpp | 9 +- libsmtutil/SolverInterface.h | 18 +- libsolidity/formal/BMC.cpp | 16 +- libsolidity/formal/ModelChecker.cpp | 14 +- libsolidity/interface/CompilerStack.cpp | 4 + libsolidity/interface/SMTSolverCommand.cpp | 30 +- libsolidity/interface/SMTSolverCommand.h | 1 + solc/CommandLineParser.cpp | 2 +- test/cmdlineTests/model_checker_cvc4/args | 1 + test/cmdlineTests/model_checker_cvc4/err | 10 + .../cmdlineTests/model_checker_cvc4/input.sol | 7 + .../model_checker_print_query_all/err | 2 +- .../model_checker_print_query_bmc/err | 2 +- .../model_checker_solvers_smtlib2/err | 2 +- test/libsolidity/SMTCheckerTest.h | 2 +- .../imports/duplicated_errors_1.sol | 2 +- 26 files changed, 88 insertions(+), 525 deletions(-) delete mode 100644 cmake/FindCVC4.cmake delete mode 100644 libsmtutil/CVC4Interface.cpp delete mode 100644 libsmtutil/CVC4Interface.h create mode 100644 test/cmdlineTests/model_checker_cvc4/args create mode 100644 test/cmdlineTests/model_checker_cvc4/err create mode 100644 test/cmdlineTests/model_checker_cvc4/input.sol diff --git a/CMakeLists.txt b/CMakeLists.txt index 91c1056ec3a4..86636d5c3c61 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -133,15 +133,15 @@ elseif (${Z3_FOUND}) 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.") +find_program(CVC5_PATH cvc5) +if (CVC5_PATH) + add_compile_definitions(CVC5_PATH=${CVC5_PATH}) + message("cvc5 SMT solver found. This enables optional SMT checking with cvc5.") endif() -if (NOT (${Z3_FOUND} OR ${CVC4_FOUND})) +if (NOT (${Z3_FOUND} OR CVC5_PATH)) 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).") + \nPlease install Z3 or cvc5 or remove the option disabling them (USE_Z3).") endif() add_subdirectory(libsolutil) diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index 5c2802d1fe20..eda0e404ddd6 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -266,7 +266,6 @@ option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON) if(UNIX AND NOT APPLE) option(USE_Z3_DLOPEN "Dynamically load the Z3 SMT solver instead of linking against it." OFF) endif() -option(USE_CVC4 "Allow compiling with CVC4 SMT solver integration" ON) if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) option(USE_LD_GOLD "Use GNU gold linker" ON) diff --git a/cmake/FindCVC4.cmake b/cmake/FindCVC4.cmake deleted file mode 100644 index 887b907b8320..000000000000 --- a/cmake/FindCVC4.cmake +++ /dev/null @@ -1,33 +0,0 @@ -if (USE_CVC4) - find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h) - find_library(CVC4_LIBRARY NAMES cvc4) - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR) - if(CVC4_FOUND) - # CVC4 may depend on either CLN or GMP. - # We can assume that the one it requires is present on the system, - # so we quietly try to find both and link against them, if they are - # present. - find_package(CLN QUIET) - find_package(GMP QUIET) - - set(CVC4_LIBRARIES ${CVC4_LIBRARY}) - - if (CLN_FOUND) - set(CVC4_LIBRARIES ${CVC4_LIBRARIES} CLN::CLN) - endif () - - if (GMP_FOUND) - set(CVC4_LIBRARIES ${CVC4_LIBRARIES} GMP::GMP) - endif () - - if (NOT TARGET CVC4::CVC4) - add_library(CVC4::CVC4 UNKNOWN IMPORTED) - set_property(TARGET CVC4::CVC4 PROPERTY IMPORTED_LOCATION ${CVC4_LIBRARY}) - set_property(TARGET CVC4::CVC4 PROPERTY INTERFACE_LINK_LIBRARIES ${CVC4_LIBRARIES}) - set_property(TARGET CVC4::CVC4 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${CVC4_INCLUDE_DIR}) - endif() - endif() -else() - set(CVC4_FOUND FALSE) -endif() diff --git a/docs/installing-solidity.rst b/docs/installing-solidity.rst index f079fb0245a8..e37fc19853f1 100644 --- a/docs/installing-solidity.rst +++ b/docs/installing-solidity.rst @@ -333,10 +333,7 @@ The following are dependencies for all builds of Solidity: +-----------------------------------+-------------------------------------------------------+ | `z3`_ (version 4.8.16+, Optional) | For use with SMT checker. | +-----------------------------------+-------------------------------------------------------+ -| `cvc4`_ (Optional) | For use with SMT checker. | -+-----------------------------------+-------------------------------------------------------+ -.. _cvc4: https://cvc4.cs.stanford.edu/web/ .. _Git: https://git-scm.com/download .. _Boost: https://www.boost.org .. _CMake: https://cmake.org/download/ @@ -543,12 +540,6 @@ Inside the build folder you can disable them, since they are enabled by default: # disables only Z3 SMT Solver. cmake .. -DUSE_Z3=OFF - # disables only CVC4 SMT Solver. - cmake .. -DUSE_CVC4=OFF - - # disables both Z3 and CVC4 - cmake .. -DUSE_CVC4=OFF -DUSE_Z3=OFF - The Version String in Detail ============================ diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index dfdcf465198b..fc7978256a9d 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -822,10 +822,10 @@ which is primarily an SMT solver and makes `Spacer `_ which does both. The user can choose which solvers should be used, if available, via the CLI -option ``--model-checker-solvers {all,cvc4,eld,smtlib2,z3}`` or the JSON option +option ``--model-checker-solvers {all,cvc5,eld,smtlib2,z3}`` or the JSON option ``settings.modelChecker.solvers=[smtlib2,z3]``, where: -- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``. +- ``cvc5`` is used via its binary which must be installed in the system. Only BMC uses ``cvc5``. - ``eld`` is used via its binary which must be installed in the system. Only CHC uses ``eld``, and only if ``z3`` is not enabled. - ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 `_ format. These can be used together with the compiler's `callback mechanism `_ so that @@ -849,7 +849,7 @@ concerned about this option. More advanced users might apply this option to try alternative solvers on more complex problems. Please note that certain combinations of chosen engine and solver will lead to -the SMTChecker doing nothing, for example choosing CHC and ``cvc4``. +the SMTChecker doing nothing, for example choosing CHC and ``cvc5``. ******************************* Abstraction and False Positives diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 875c15b09d6d..34813c4062d1 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -485,7 +485,7 @@ Input Description "showUnsupported": true, // Choose which solvers should be used, if available. // See the Formal Verification section for the solvers description. - "solvers": ["cvc4", "smtlib2", "z3"], + "solvers": ["cvc5", "smtlib2", "z3"], // Choose which targets should be checked: constantCondition, // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds. // If the option is not given all targets are checked by default, diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index cb222e22c4a1..005fbeb8049e 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -20,12 +20,6 @@ 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) @@ -38,7 +32,7 @@ if (${USE_Z3_DLOPEN}) set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h) endif() -add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS}) +add_library(smtutil ${sources} ${z3_SRCS}) target_link_libraries(smtutil PUBLIC solutil Boost::boost) if (${USE_Z3_DLOPEN}) @@ -47,7 +41,3 @@ if (${USE_Z3_DLOPEN}) 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 f53c92ab5705..000000000000 --- 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 cc3c0577ce45..000000000000 --- 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/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 12469a4ae05f..cfe1bc0bef2c 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -123,11 +123,11 @@ std::pair> SMTLib2Interface::check(std::ve CheckResult result; // TODO proper parsing - if (boost::starts_with(response, "sat\n")) + if (boost::starts_with(response, "sat")) result = CheckResult::SATISFIABLE; - else if (boost::starts_with(response, "unsat\n")) + else if (boost::starts_with(response, "unsat")) result = CheckResult::UNSATISFIABLE; - else if (boost::starts_with(response, "unknown\n")) + else if (boost::starts_with(response, "unknown")) result = CheckResult::UNKNOWN; else result = CheckResult::ERROR; diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 76c69d0180a3..1435cc9d801c 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -21,9 +21,6 @@ #ifdef HAVE_Z3 #include #endif -#ifdef HAVE_CVC4 -#include -#endif #include using namespace solidity; @@ -41,16 +38,12 @@ SMTPortfolio::SMTPortfolio( SolverInterface(_queryTimeout) { solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); - if (_enabledSolvers.smtlib2) + if (_enabledSolvers.smtlib2 || _enabledSolvers.cvc5) 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/SolverInterface.h b/libsmtutil/SolverInterface.h index 13803de6e91a..92f9c8f75b7d 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -41,13 +41,13 @@ namespace solidity::smtutil struct SMTSolverChoice { - bool cvc4 = false; + bool cvc5 = false; bool eld = false; bool smtlib2 = false; bool z3 = false; static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; } - static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; } + static constexpr SMTSolverChoice CVC5() noexcept { return {true, false, false, false}; } static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; } static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; } static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; } @@ -65,7 +65,7 @@ struct SMTSolverChoice SMTSolverChoice& operator&=(SMTSolverChoice const& _other) { - cvc4 &= _other.cvc4; + cvc5 &= _other.cvc5; eld &= _other.eld; smtlib2 &= _other.smtlib2; z3 &= _other.z3; @@ -82,7 +82,7 @@ struct SMTSolverChoice bool operator==(SMTSolverChoice const& _other) const noexcept { - return cvc4 == _other.cvc4 && + return cvc5 == _other.cvc5 && eld == _other.eld && smtlib2 == _other.smtlib2 && z3 == _other.z3; @@ -90,11 +90,11 @@ struct SMTSolverChoice bool setSolver(std::string const& _solver) { - static std::set const solvers{"cvc4", "eld", "smtlib2", "z3"}; + static std::set const solvers{"cvc5", "eld", "smtlib2", "z3"}; if (!solvers.count(_solver)) return false; - if (_solver == "cvc4") - cvc4 = true; + if (_solver == "cvc5") + cvc5 = true; if (_solver == "eld") eld = true; else if (_solver == "smtlib2") @@ -105,8 +105,8 @@ struct SMTSolverChoice } bool none() const noexcept { return !some(); } - bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; } - bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; } + bool some() const noexcept { return cvc5 || eld || smtlib2 || z3; } + bool all() const noexcept { return cvc5 && eld && smtlib2 && z3; } }; enum class CheckResult diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 97dd7050fef8..4f588d491839 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -51,15 +51,15 @@ 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 defined (HAVE_Z3) + if (m_settings.solvers.z3) if (!_smtlib2Responses.empty()) m_errorReporter.warning( 5622_error, "SMT-LIB2 query responses were given in the auxiliary input, " - "but this Solidity binary uses an SMT solver (Z3/CVC4) directly." + "but this Solidity binary uses an SMT solver Z3 directly." "These responses will be ignored." - "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." + "Consider disabling Z3 at compilation time in order to use SMT-LIB2 responses." ); #endif } @@ -67,13 +67,13 @@ BMC::BMC( void BMC::analyze(SourceUnit const& _source, std::map, smt::EncodingContext::IdCompare> _solvedTargets) { // At this point every enabled solver is available. - if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) + if (!m_settings.solvers.cvc5 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) { m_errorReporter.warning( 7710_error, SourceLocation(), "BMC analysis was not possible since no SMT solver was found and enabled." - " The accepted solvers for BMC are cvc4 and z3." + " The accepted solvers for BMC are cvc5 and z3." ); return; } @@ -123,7 +123,7 @@ void BMC::analyze(SourceUnit const& _source, std::map #endif -#if defined(__linux) || defined(__APPLE__) #include -#endif #include #include @@ -163,14 +161,10 @@ std::vector ModelChecker::unhandledQueries() SMTSolverChoice ModelChecker::availableSolvers() { smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2(); -#if defined(__linux) || defined(__APPLE__) available.eld = !boost::process::search_path("eld").empty(); -#endif + available.cvc5 = !boost::process::search_path("cvc5").empty(); #ifdef HAVE_Z3 available.z3 = solidity::smtutil::Z3Interface::available(); -#endif -#ifdef HAVE_CVC4 - available.cvc4 = true; #endif return available; } @@ -179,13 +173,13 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er { SMTSolverChoice availableSolvers{ModelChecker::availableSolvers()}; - if (_enabled.cvc4 && !availableSolvers.cvc4) + if (_enabled.cvc5 && !availableSolvers.cvc5) { - _enabled.cvc4 = false; + _enabled.cvc5 = false; _errorReporter.warning( 4902_error, SourceLocation(), - "Solver CVC4 was selected for SMTChecker but it is not available." + "Solver CVC5 was selected for SMTChecker but it is not available." ); } diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 2a9005680678..d5fe44ca167a 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -656,8 +656,12 @@ bool CompilerStack::analyzeLegacy(bool _noErrorsSoFar) { m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter); if (auto* universalCallback = m_readFile.target()) + { if (m_modelCheckerSettings.solvers.eld) universalCallback->smtCommand().setEldarica(m_modelCheckerSettings.timeout, m_modelCheckerSettings.invariants != ModelCheckerInvariants::None()); + if (m_modelCheckerSettings.solvers.cvc5) + universalCallback->smtCommand().setCvc5(m_modelCheckerSettings.timeout); + } } ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile); diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp index 7d814cd9c3c4..b9eb392c635b 100644 --- a/libsolidity/interface/SMTSolverCommand.cpp +++ b/libsolidity/interface/SMTSolverCommand.cpp @@ -51,6 +51,22 @@ void SMTSolverCommand::setEldarica(std::optional timeoutInMillisec m_arguments.emplace_back("-ssol"); } +void SMTSolverCommand::setCvc5(std::optional timeoutInMilliseconds) +{ + m_arguments.clear(); + m_solverCmd = "cvc5"; + if (timeoutInMilliseconds) + { + m_arguments.push_back("--tlimit-per"); + m_arguments.push_back(std::to_string(timeoutInMilliseconds.value())); + } + else + { + m_arguments.push_back("--rlimit"); + m_arguments.push_back(std::to_string(12000)); + } +} + ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query) { try @@ -68,29 +84,29 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri auto queryFile = boost::filesystem::ofstream(queryFileName); queryFile << _query << std::flush; - auto eldBin = boost::process::search_path(m_solverCmd); + auto solverBin = boost::process::search_path(m_solverCmd); - if (eldBin.empty()) + if (solverBin.empty()) return ReadCallback::Result{false, m_solverCmd + " binary not found."}; auto args = m_arguments; args.push_back(queryFileName.string()); boost::process::ipstream pipe; - boost::process::child eld( - eldBin, + boost::process::child solverProcess( + solverBin, args, boost::process::std_out > pipe, - boost::process::std_err >boost::process::null + boost::process::std_err > boost::process::null ); std::vector data; std::string line; - while (eld.running() && std::getline(pipe, line)) + while (solverProcess.running() && std::getline(pipe, line)) if (!line.empty()) data.push_back(line); - eld.wait(); + solverProcess.wait(); return ReadCallback::Result{true, boost::join(data, "\n")}; } diff --git a/libsolidity/interface/SMTSolverCommand.h b/libsolidity/interface/SMTSolverCommand.h index 665c19c1b767..3b1022740524 100644 --- a/libsolidity/interface/SMTSolverCommand.h +++ b/libsolidity/interface/SMTSolverCommand.h @@ -37,6 +37,7 @@ class SMTSolverCommand } void setEldarica(std::optional timeoutInMilliseconds, bool computeInvariants); + void setCvc5(std::optional timeoutInMilliseconds); private: /// The name of the solver's binary. diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 824c899110a2..5d734bdf8961 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -877,7 +877,7 @@ General Information)").c_str(), ) ( g_strModelCheckerSolvers.c_str(), - po::value()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"), + po::value()->value_name("cvc5,eld,z3,smtlib2")->default_value("z3"), "Select model checker solvers." ) ( diff --git a/test/cmdlineTests/model_checker_cvc4/args b/test/cmdlineTests/model_checker_cvc4/args new file mode 100644 index 000000000000..84280d4061ce --- /dev/null +++ b/test/cmdlineTests/model_checker_cvc4/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-solvers cvc5 diff --git a/test/cmdlineTests/model_checker_cvc4/err b/test/cmdlineTests/model_checker_cvc4/err new file mode 100644 index 000000000000..cca467b8936d --- /dev/null +++ b/test/cmdlineTests/model_checker_cvc4/err @@ -0,0 +1,10 @@ +Warning: BMC: Assertion violation happens here. + --> test/cmdlineTests/model_checker_cvc4/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 0 + +Note: Callstack: +Note: diff --git a/test/cmdlineTests/model_checker_cvc4/input.sol b/test/cmdlineTests/model_checker_cvc4/input.sol new file mode 100644 index 000000000000..ef11e87eb8fc --- /dev/null +++ b/test/cmdlineTests/model_checker_cvc4/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} diff --git a/test/cmdlineTests/model_checker_print_query_all/err b/test/cmdlineTests/model_checker_print_query_all/err index 1a04042cd778..2e72d3e86bcc 100644 --- a/test/cmdlineTests/model_checker_print_query_all/err +++ b/test/cmdlineTests/model_checker_print_query_all/err @@ -162,4 +162,4 @@ Info: BMC: Requested query: Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. -Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC5) was available. None of the installed solvers was enabled. diff --git a/test/cmdlineTests/model_checker_print_query_bmc/err b/test/cmdlineTests/model_checker_print_query_bmc/err index 1a59f87b0d95..34e8b1598ef4 100644 --- a/test/cmdlineTests/model_checker_print_query_bmc/err +++ b/test/cmdlineTests/model_checker_print_query_bmc/err @@ -29,4 +29,4 @@ Info: BMC: Requested query: Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. -Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC5) was available. None of the installed solvers was enabled. diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/err b/test/cmdlineTests/model_checker_solvers_smtlib2/err index 3aa9893489bc..7e9dd15ea709 100644 --- a/test/cmdlineTests/model_checker_solvers_smtlib2/err +++ b/test/cmdlineTests/model_checker_solvers_smtlib2/err @@ -4,4 +4,4 @@ Warning: CHC analysis was not possible. No Horn solver was available. None of th Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. -Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC5) was available. None of the installed solvers was enabled. diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index d42572dc5b29..884e09a371d4 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -54,7 +54,7 @@ class SMTCheckerTest: public SyntaxTest Set in m_modelCheckerSettings. SMTShowUnproved: `yes`, `no`, where the default is `yes`. Set in m_modelCheckerSettings. - SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`. + SMTSolvers: `all`, `cvc5`, `z3`, `none`, where the default is `all`. Set in m_modelCheckerSettings. BMCLoopIterations: number of loop iterations for BMC engine, the default is 1. Set in m_modelCheckerSettings. diff --git a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol index a98ba962a7bf..aeca300c566a 100644 --- a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol +++ b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol @@ -23,4 +23,4 @@ contract C is B { // Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here. // Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. // Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here. -// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC5) was available. None of the installed solvers was enabled.