From 43f7a0f1cb2be5d4940f2d88b2a005436269c36d Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 29 May 2023 18:05:11 +0200 Subject: [PATCH] [SMTChecker]: Update CVC4 to cvc5 --- CMakeLists.txt | 12 +- cmake/EthCompilerSettings.cmake | 2 +- cmake/FindCVC4.cmake | 33 --- cmake/FindCVC5.cmake | 33 +++ docs/installing-solidity.rst | 4 +- docs/smtchecker.rst | 6 +- docs/using-the-compiler.rst | 2 +- libsmtutil/CMakeLists.txt | 12 +- libsmtutil/CVC4Interface.cpp | 240 ++++++++---------- libsmtutil/CVC4Interface.h | 36 +-- libsmtutil/SMTPortfolio.cpp | 8 +- libsmtutil/SolverInterface.h | 18 +- libsolidity/formal/BMC.cpp | 16 +- libsolidity/formal/ModelChecker.cpp | 10 +- solc/CommandLineParser.cpp | 2 +- .../model_checker_solvers_smtlib2/err | 2 +- .../output.json | 4 +- .../output.json | 4 +- test/libsolidity/SMTCheckerTest.h | 2 +- .../imports/duplicated_errors_1.sol | 4 +- 20 files changed, 210 insertions(+), 240 deletions(-) delete mode 100644 cmake/FindCVC4.cmake create mode 100644 cmake/FindCVC5.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 85d2f64ce..ea5ee327f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -122,15 +122,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_package(CVC5 QUIET) +if (${CVC5_FOUND}) + add_definitions(-DHAVE_CVC5) + 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_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).") + \nPlease install Z3 or cvc5 or remove the option disabling them (USE_Z3, USE_CVC5).") endif() add_subdirectory(libsolutil) diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index 4dd593458..baa770c45 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -266,7 +266,7 @@ 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) +option(USE_CVC5 "Allow compiling with CVC5 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 887b907b8..000000000 --- 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/cmake/FindCVC5.cmake b/cmake/FindCVC5.cmake new file mode 100644 index 000000000..4373e680f --- /dev/null +++ b/cmake/FindCVC5.cmake @@ -0,0 +1,33 @@ +if (USE_CVC5) + find_path(CVC5_INCLUDE_DIR cvc5/cvc5.h) + find_library(CVC5_LIBRARY NAMES cvc5) + include(FindPackageHandleStandardArgs) + find_package_handle_standard_args(CVC5 DEFAULT_MSG CVC5_LIBRARY CVC5_INCLUDE_DIR) + if(CVC5_FOUND) + # CVC5 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(CVC5_LIBRARIES ${CVC5_LIBRARY}) + + if (CLN_FOUND) + set(CVC5_LIBRARIES ${CVC5_LIBRARIES} CLN::CLN) + endif () + + if (GMP_FOUND) + set(CVC5_LIBRARIES ${CVC5_LIBRARIES} GMP::GMP) + endif () + + if (NOT TARGET CVC5::CVC5) + add_library(CVC5::CVC5 UNKNOWN IMPORTED) + set_property(TARGET CVC5::CVC5 PROPERTY IMPORTED_LOCATION ${CVC5_LIBRARY}) + set_property(TARGET CVC5::CVC5 PROPERTY INTERFACE_LINK_LIBRARIES ${CVC5_LIBRARIES}) + set_property(TARGET CVC5::CVC5 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${CVC5_INCLUDE_DIR}) + endif() + endif() +else() + set(CVC5_FOUND FALSE) +endif() diff --git a/docs/installing-solidity.rst b/docs/installing-solidity.rst index bd954ece0..2b725cc8e 100644 --- a/docs/installing-solidity.rst +++ b/docs/installing-solidity.rst @@ -328,10 +328,10 @@ 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. | +| `cvc5`_ (Optional) | For use with SMT checker. | +-----------------------------------+-------------------------------------------------------+ -.. _cvc4: https://cvc4.cs.stanford.edu/web/ +.. _cvc5: https://cvc5.github.io/downloads.html .. _Git: https://git-scm.com/download .. _Boost: https://www.boost.org .. _CMake: https://cmake.org/download/ diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index b68d58ed3..fd31ba147 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -821,10 +821,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 only available if the ``solc`` binary is compiled with it. 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 @@ -848,7 +848,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 6fb32871c..7427e720d 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -457,7 +457,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 af7f47b60..e3abdfa04 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -18,10 +18,10 @@ else() set(z3_SRCS) endif() -if (${CVC4_FOUND}) - set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h) +if (${CVC5_FOUND}) + set(cvc5_SRCS CVC4Interface.cpp CVC4Interface.h) else() - set(cvc4_SRCS) + set(cvc5_SRCS) endif() if (${USE_Z3_DLOPEN}) @@ -36,7 +36,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} ${cvc5_SRCS}) target_link_libraries(smtutil PUBLIC solutil Boost::boost) if (${USE_Z3_DLOPEN}) @@ -46,6 +46,6 @@ elseif (${Z3_FOUND}) target_link_libraries(smtutil PUBLIC z3::libz3) endif() -if (${CVC4_FOUND}) - target_link_libraries(smtutil PUBLIC CVC4::CVC4) +if (${CVC5_FOUND}) + target_link_libraries(smtutil PUBLIC CVC5::CVC5) endif() diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 3c047782a..9f2af746a 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -18,102 +18,82 @@ #include +#include #include #include -#include - using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::smtutil; -CVC4Interface::CVC4Interface(optional _queryTimeout): - SolverInterface(_queryTimeout), - m_solver(&m_context) +CVC5Interface::CVC5Interface(optional _queryTimeout): + SolverInterface(_queryTimeout) { reset(); } -void CVC4Interface::reset() +void CVC5Interface::reset() { m_variables.clear(); - m_solver.reset(); - m_solver.setOption("produce-models", true); + m_solver.resetAssertions(); + m_solver.setOption("produce-models", "true"); if (m_queryTimeout) - m_solver.setTimeLimit(*m_queryTimeout); + m_solver.setOption("tlimit-per", std::to_string(*m_queryTimeout)); else - m_solver.setResourceLimit(resourceLimit); + m_solver.setOption("rlimit", std::to_string(resourceLimit)); } -void CVC4Interface::push() +void CVC5Interface::push() { m_solver.push(); } -void CVC4Interface::pop() +void CVC5Interface::pop() { m_solver.pop(); } -void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort) +void CVC5Interface::declareVariable(string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); - m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort)); + m_variables[_name] = m_solver.mkConst(CVC5Sort(*_sort), _name); } -void CVC4Interface::addAssertion(Expression const& _expr) +void CVC5Interface::addAssertion(Expression const& _expr) { try { - m_solver.assertFormula(toCVC4Expr(_expr)); + m_solver.assertFormula(toCVC5Expr(_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) + catch (cvc5::CVC5ApiException const& _e) { smtAssert(false, _e.what()); } } -pair> CVC4Interface::check(vector const& _expressionsToEvaluate) +pair> CVC5Interface::check(vector const& _expressionsToEvaluate) { CheckResult result; vector values; try { - switch (m_solver.checkSat().isSat()) - { - case CVC4::Result::SAT: + cvc5::Result res = m_solver.checkSat(); + if (res.isSat()) result = CheckResult::SATISFIABLE; - break; - case CVC4::Result::UNSAT: + else if (res.isUnsat()) result = CheckResult::UNSATISFIABLE; - break; - case CVC4::Result::SAT_UNKNOWN: + else if (res.isUnknown()) result = CheckResult::UNKNOWN; - break; - default: + else smtAssert(false, ""); - } - if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) { for (Expression const& e: _expressionsToEvaluate) - values.push_back(toString(m_solver.getValue(toCVC4Expr(e)))); + values.push_back(toString(m_solver.getValue(toCVC5Expr(e)))); } } - catch (CVC4::Exception const&) + catch (cvc5::CVC5ApiException const&) { result = CheckResult::ERROR; values.clear(); @@ -122,41 +102,41 @@ pair> CVC4Interface::check(vector const& return make_pair(result, values); } -CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) +cvc5::Term CVC5Interface::toCVC5Expr(Expression const& _expr) { // Variable if (_expr.arguments.empty() && m_variables.count(_expr.name)) return m_variables.at(_expr.name); - vector arguments; + vector arguments; for (auto const& arg: _expr.arguments) - arguments.push_back(toCVC4Expr(arg)); + arguments.push_back(toCVC5Expr(arg)); try { 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); + return m_solver.mkTerm(cvc5::Kind::APPLY_UF, vector{m_variables.at(n)} + arguments); // Literal else if (arguments.empty()) { if (n == "true") - return m_context.mkConst(true); + return m_solver.mkTrue(); else if (n == "false") - return m_context.mkConst(false); + return m_solver.mkFalse(); else if (auto sortSort = dynamic_pointer_cast(_expr.sort)) - return m_context.mkVar(n, cvc4Sort(*sortSort->inner)); + return m_solver.mkVar(CVC5Sort(*sortSort->inner), n); else try { - return m_context.mkConst(CVC4::Rational(n)); + return m_solver.mkInteger(n); } - catch (CVC4::TypeCheckingException const& _e) + catch (cvc5::CVC5ApiRecoverableException const& _e) { smtAssert(false, _e.what()); } - catch (CVC4::Exception const& _e) + catch (cvc5::CVC5ApiException const& _e) { smtAssert(false, _e.what()); } @@ -164,127 +144,127 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) smtAssert(_expr.hasCorrectArity(), ""); if (n == "ite") - return arguments[0].iteExpr(arguments[1], arguments[2]); + return arguments[0].iteTerm(arguments[1], arguments[2]); else if (n == "not") - return arguments[0].notExpr(); + return arguments[0].notTerm(); else if (n == "and") - return arguments[0].andExpr(arguments[1]); + return arguments[0].andTerm(arguments[1]); else if (n == "or") - return arguments[0].orExpr(arguments[1]); + return arguments[0].orTerm(arguments[1]); else if (n == "=>") - return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::IMPLIES, {arguments[0], arguments[1]}); else if (n == "=") - return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::EQUAL, {arguments[0], arguments[1]}); else if (n == "<") - return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::LT, {arguments[0], arguments[1]}); else if (n == "<=") - return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::LEQ, {arguments[0], arguments[1]}); else if (n == ">") - return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::GT, {arguments[0], arguments[1]}); else if (n == ">=") - return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::GEQ, {arguments[0], arguments[1]}); else if (n == "+") - return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::ADD, {arguments[0], arguments[1]}); else if (n == "-") - return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::SUB, {arguments[0], arguments[1]}); else if (n == "*") - return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::MULT, {arguments[0], arguments[1]}); else if (n == "div") - return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::INTS_DIVISION, {arguments[0], arguments[1]}); else if (n == "mod") - return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::INTS_MODULUS, {arguments[0], arguments[1]}); else if (n == "bvnot") - return m_context.mkExpr(CVC4::kind::BITVECTOR_NOT, arguments[0]); + return m_solver.mkTerm(cvc5::Kind::BITVECTOR_NOT, {arguments[0]}); else if (n == "bvand") - return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::BITVECTOR_AND, {arguments[0], arguments[1]}); else if (n == "bvor") - return m_context.mkExpr(CVC4::kind::BITVECTOR_OR, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::BITVECTOR_OR, {arguments[0], arguments[1]}); else if (n == "bvxor") - return m_context.mkExpr(CVC4::kind::BITVECTOR_XOR, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::BITVECTOR_XOR, {arguments[0], arguments[1]}); else if (n == "bvshl") - return m_context.mkExpr(CVC4::kind::BITVECTOR_SHL, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::BITVECTOR_SHL, {arguments[0], arguments[1]}); else if (n == "bvlshr") - return m_context.mkExpr(CVC4::kind::BITVECTOR_LSHR, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::BITVECTOR_LSHR, {arguments[0], arguments[1]}); else if (n == "bvashr") - return m_context.mkExpr(CVC4::kind::BITVECTOR_ASHR, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::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])) - ) + auto i2bvOp = m_solver.mkOp(cvc5::Kind::INT_TO_BITVECTOR, {static_cast(size)}); + // CVC5 treats all BVs as unsigned, so we need to manually apply 2's complement if needed. + return m_solver.mkTerm( + cvc5::Kind::ITE, + { + m_solver.mkTerm(cvc5::Kind::GEQ, {arguments[0], m_solver.mkInteger(0)}), + m_solver.mkTerm(i2bvOp, {arguments[0]}), + m_solver.mkTerm( + cvc5::Kind::BITVECTOR_NEG, + {m_solver.mkTerm(i2bvOp, {m_solver.mkTerm(cvc5::Kind::NEG, {arguments[0]})})} + ) + } ); } else if (n == "bv2int") { auto intSort = dynamic_pointer_cast(_expr.sort); smtAssert(intSort, ""); - auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]); + auto nat = m_solver.mkTerm(cvc5::Kind::BITVECTOR_TO_NAT, {arguments[0]}); if (!intSort->isSigned) return nat; - auto type = arguments[0].getType(); + auto type = arguments[0].getSort(); 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])) - ) + auto size = type.getBitVectorSize(); + // CVC5 treats all BVs as unsigned, so we need to manually apply 2's complement if needed. + auto extractOp = m_solver.mkOp(cvc5::Kind::BITVECTOR_EXTRACT, {size - 1, size - 1}); + return m_solver.mkTerm( + cvc5::Kind::ITE, + { + m_solver.mkTerm( + cvc5::Kind::EQUAL, + {m_solver.mkTerm(extractOp, {arguments[0]}), m_solver.mkBitVector(1, uint64_t{0})} + ), + nat, + m_solver.mkTerm( + cvc5::Kind::NEG, + {m_solver.mkTerm(cvc5::Kind::BITVECTOR_TO_NAT, {m_solver.mkTerm(cvc5::Kind::BITVECTOR_NEG, {arguments[0]})})} + ) + } ); } else if (n == "select") - return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]); + return m_solver.mkTerm(cvc5::Kind::SELECT, {arguments[0], arguments[1]}); else if (n == "store") - return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]); + return m_solver.mkTerm(cvc5::Kind::STORE, {arguments[0], arguments[1], arguments[2]}); else if (n == "const_array") { shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); smtAssert(sortSort, ""); - return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1])); + return m_solver.mkConstArray(CVC5Sort(*sortSort->inner), arguments[1]); } else if (n == "tuple_get") { 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(); + auto tt = m_solver.mkTupleSort(CVC5Sort(tupleSort->components)); + cvc5::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]); + cvc5::DatatypeSelector s = dt[0][index]; + return m_solver.mkTerm(cvc5::Kind::APPLY_SELECTOR, {s.getTerm(), arguments[0]}); } else if (n == "tuple_constructor") { 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); + auto tt = m_solver.mkTupleSort(CVC5Sort(tupleSort->components)); + cvc5::Datatype const& dt = tt.getDatatype(); + cvc5::DatatypeConstructor c = dt[0]; + return m_solver.mkTerm(cvc5::Kind::APPLY_CONSTRUCTOR, vector{c.getTerm()} + arguments); } smtAssert(false); } - catch (CVC4::TypeCheckingException const& _e) - { - smtAssert(false, _e.what()); - } - catch (CVC4::Exception const& _e) + catch (cvc5::CVC5ApiException const& _e) { smtAssert(false, _e.what()); } @@ -295,43 +275,45 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) util::unreachable(); } -CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) +cvc5::Sort CVC5Interface::CVC5Sort(Sort const& _sort) { switch (_sort.kind) { case Kind::Bool: - return m_context.booleanType(); + return m_solver.getBooleanSort(); case Kind::Int: - return m_context.integerType(); + return m_solver.getIntegerSort(); case Kind::BitVector: - return m_context.mkBitVectorType(dynamic_cast(_sort).size); + return m_solver.mkBitVectorSort(dynamic_cast(_sort).size); case Kind::Function: { FunctionSort const& fSort = dynamic_cast(_sort); - return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain)); + if (fSort.domain.empty()) // function sort in cvc5 must have nonempty domain + return CVC5Sort(*fSort.codomain); + return m_solver.mkFunctionSort(CVC5Sort(fSort.domain), CVC5Sort(*fSort.codomain)); } case Kind::Array: { auto const& arraySort = dynamic_cast(_sort); - return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range)); + return m_solver.mkArraySort(CVC5Sort(*arraySort.domain), CVC5Sort(*arraySort.range)); } case Kind::Tuple: { auto const& tupleSort = dynamic_cast(_sort); - return m_context.mkTupleType(cvc4Sort(tupleSort.components)); + return m_solver.mkTupleSort(CVC5Sort(tupleSort.components)); } default: break; } smtAssert(false, ""); // Cannot be reached. - return m_context.integerType(); + return m_solver.getIntegerSort(); } -vector CVC4Interface::cvc4Sort(vector const& _sorts) +vector CVC5Interface::CVC5Sort(vector const& _sorts) { - vector cvc4Sorts; + vector CVC5Sorts; for (auto const& _sort: _sorts) - cvc4Sorts.push_back(cvc4Sort(*_sort)); - return cvc4Sorts; + CVC5Sorts.push_back(CVC5Sort(*_sort)); + return CVC5Sorts; } diff --git a/libsmtutil/CVC4Interface.h b/libsmtutil/CVC4Interface.h index cc3c0577c..a08e0f563 100644 --- a/libsmtutil/CVC4Interface.h +++ b/libsmtutil/CVC4Interface.h @@ -20,30 +20,19 @@ #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 +#include namespace solidity::smtutil { -class CVC4Interface: public SolverInterface +class CVC5Interface: public SolverInterface { public: /// Noncopyable. - CVC4Interface(CVC4Interface const&) = delete; - CVC4Interface& operator=(CVC4Interface const&) = delete; + CVC5Interface(CVC5Interface const&) = delete; + CVC5Interface& operator=(CVC5Interface const&) = delete; - CVC4Interface(std::optional _queryTimeout = {}); + CVC5Interface(std::optional _queryTimeout = {}); void reset() override; @@ -56,17 +45,16 @@ public: 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); + cvc5::Term toCVC5Expr(Expression const& _expr); + cvc5::Sort CVC5Sort(Sort const& _sort); + std::vector CVC5Sort(std::vector const& _sorts); - CVC4::ExprManager m_context; - CVC4::SmtEngine m_solver; - std::map m_variables; + cvc5::Solver m_solver; + std::map m_variables; - // CVC4 "basic resources" limit. + // CVC5 "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, + // The tests start failing for CVC5 with less than 6000, // so using double that. static int const resourceLimit = 12000; }; diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 77a404a47..a44bb8005 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -21,7 +21,7 @@ #ifdef HAVE_Z3 #include #endif -#ifdef HAVE_CVC4 +#ifdef HAVE_CVC5 #include #endif #include @@ -46,9 +46,9 @@ SMTPortfolio::SMTPortfolio( if (_enabledSolvers.z3 && Z3Interface::available()) m_solvers.emplace_back(make_unique(m_queryTimeout)); #endif -#ifdef HAVE_CVC4 - if (_enabledSolvers.cvc4) - m_solvers.emplace_back(make_unique(m_queryTimeout)); +#ifdef HAVE_CVC5 + if (_enabledSolvers.cvc5) + m_solvers.emplace_back(make_unique(m_queryTimeout)); #endif } diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 4a21f1841..f17395148 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 be29000fe..a27f1da44 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -49,15 +49,15 @@ BMC::BMC( SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), m_interface(make_unique(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)) { -#if defined (HAVE_Z3) || defined (HAVE_CVC4) - if (m_settings.solvers.cvc4 || m_settings.solvers.z3) +#if defined (HAVE_Z3) || defined (HAVE_CVC5) + if (m_settings.solvers.cvc5 || 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/cvc5) directly." "These responses will be ignored." - "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." + "Consider disabling Z3/cvc5 at compilation time in order to use SMT-LIB2 responses." ); #endif } @@ -65,13 +65,13 @@ BMC::BMC( void BMC::analyze(SourceUnit const& _source, 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; } @@ -121,7 +121,7 @@ void BMC::analyze(SourceUnit const& _source, map()->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_solvers_smtlib2/err b/test/cmdlineTests/model_checker_solvers_smtlib2/err index 3aa989348..452e2b31d 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/cmdlineTests/standard_model_checker_solvers_none/output.json b/test/cmdlineTests/standard_model_checker_solvers_none/output.json index e5d356ce5..9437e445f 100644 --- a/test/cmdlineTests/standard_model_checker_solvers_none/output.json +++ b/test/cmdlineTests/standard_model_checker_solvers_none/output.json @@ -14,10 +14,10 @@ { "component": "general", "errorCode": "7710", - "formattedMessage": "Warning: BMC analysis was not possible since no SMT solver was found and enabled. The accepted solvers for BMC are cvc4 and z3. + "formattedMessage": "Warning: BMC analysis was not possible since no SMT solver was found and enabled. The accepted solvers for BMC are cvc5 and z3. ", - "message": "BMC analysis was not possible since no SMT solver was found and enabled. The accepted solvers for BMC are cvc4 and z3.", + "message": "BMC analysis was not possible since no SMT solver was found and enabled. The accepted solvers for BMC are cvc5 and z3.", "severity": "warning", "type": "Warning" } diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json index bf59a0d9d..1ea71a0cf 100644 --- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json +++ b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json @@ -189,10 +189,10 @@ { "component": "general", "errorCode": "8084", - "formattedMessage": "Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. + "formattedMessage": "Warning: BMC analysis was not possible. No SMT solver (Z3 or cvc5) was available. None of the installed solvers was enabled. ", - "message": "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.", + "message": "BMC analysis was not possible. No SMT solver (Z3 or cvc5) was available. None of the installed solvers was enabled.", "severity": "warning", "type": "Warning" } diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index 965705f30..4e014e5b5 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -53,7 +53,7 @@ protected: 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 a98ba962a..c225fe0b4 100644 --- a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol +++ b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol @@ -19,8 +19,8 @@ contract C is B { // Warning 6328: (b.sol:62-75): 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: (b.sol:62-75): 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. // 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.