cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker]: Update CVC4 to cvc5

Browse Source
This commit is contained in:
Martin Blicha 2023-05-29 18:05:11 +02:00
parent facc38097d
commit 43f7a0f1cb
20 changed files with 210 additions and 240 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
CMakeLists.txt
View File

@ -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)

2
cmake/EthCompilerSettings.cmake
View File

@ -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)

33
cmake/FindCVC4.cmake
View File

@ -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()

33
cmake/FindCVC5.cmake Normal file
View File

@ -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()

4
docs/installing-solidity.rst
View File

@ -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/

6
docs/smtchecker.rst
View File

@ -821,10 +821,10 @@ which is primarily an SMT solver and makes `Spacer
<https://github.com/uuverifiers/eldarica>`_ which does both.
The user can choose which solvers should be used, if available, via the CLI
option ``--model-checker-solvers {all,cvc4,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 <http://smtlib.cs.uiowa.edu/>`_ format.
These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that
@ -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

2
docs/using-the-compiler.rst
View File

@ -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,

12
libsmtutil/CMakeLists.txt
View File

@ -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()

240
libsmtutil/CVC4Interface.cpp
View File

@ -18,102 +18,82 @@
#include <libsmtutil/CVC4Interface.h>
#include <libsolutil/CommonData.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/Exceptions.h>
#include <cvc4/util/bitvector.h>
using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;
CVC4Interface::CVC4Interface(optional<unsigned> _queryTimeout):
SolverInterface(_queryTimeout),
m_solver(&m_context)
CVC5Interface::CVC5Interface(optional<unsigned> _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<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& _expressionsToEvaluate)
pair<CheckResult, vector<string>> CVC5Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
vector<string> 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<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> 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<CVC4::Expr> arguments;
vector<cvc5::Term> 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<cvc5::Term>{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<SortSort>(_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<unsigned>(size)));
// CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
return m_context.mkExpr(
CVC4::kind::ITE,
m_context.mkExpr(CVC4::kind::GEQ, arguments[0], m_context.mkConst(CVC4::Rational(0))),
m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, arguments[0]),
m_context.mkExpr(
CVC4::kind::BITVECTOR_NEG,
m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, m_context.mkExpr(CVC4::kind::UMINUS, arguments[0]))
)
auto i2bvOp = m_solver.mkOp(cvc5::Kind::INT_TO_BITVECTOR, {static_cast<unsigned>(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<IntSort>(_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> sortSort = std::dynamic_pointer_cast<SortSort>(_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> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
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> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
CVC4::Expr c = dt[0].getConstructor();
return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
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<cvc5::Term>{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<BitVectorSort const&>(_sort).size);
return m_solver.mkBitVectorSort(dynamic_cast<BitVectorSort const&>(_sort).size);
case Kind::Function:
{
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
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<ArraySort const&>(_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<TupleSort const&>(_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<CVC4::Type> CVC4Interface::cvc4Sort(vector<SortPointer> const& _sorts)
vector<cvc5::Sort> CVC5Interface::CVC5Sort(vector<SortPointer> const& _sorts)
{
vector<CVC4::Type> cvc4Sorts;
vector<cvc5::Sort> CVC5Sorts;
for (auto const& _sort: _sorts)
cvc4Sorts.push_back(cvc4Sort(*_sort));
return cvc4Sorts;
CVC5Sorts.push_back(CVC5Sort(*_sort));
return CVC5Sorts;
}

36
libsmtutil/CVC4Interface.h
View File

@ -20,30 +20,19 @@
#include <libsmtutil/SolverInterface.h>
#if defined(__GLIBC__)
// The CVC4 headers includes the deprecated system headers <ext/hash_map>
// and <ext/hash_set>. These headers cause a warning that will break the
// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set.
#define _GLIBCXX_PERMIT_BACKWARD_HASH
#endif
#include <cvc4/cvc4.h>
#if defined(__GLIBC__)
#undef _GLIBCXX_PERMIT_BACKWARD_HASH
#endif
#include <cvc5/cvc5.h>
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<unsigned> _queryTimeout = {});
CVC5Interface(std::optional<unsigned> _queryTimeout = {});
void reset() override;
@ -56,17 +45,16 @@ public:
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
CVC4::Type cvc4Sort(Sort const& _sort);
std::vector<CVC4::Type> cvc4Sort(std::vector<SortPointer> const& _sorts);
cvc5::Term toCVC5Expr(Expression const& _expr);
cvc5::Sort CVC5Sort(Sort const& _sort);
std::vector<cvc5::Sort> CVC5Sort(std::vector<SortPointer> const& _sorts);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;
std::map<std::string, CVC4::Expr> m_variables;
cvc5::Solver m_solver;
std::map<std::string, cvc5::Term> 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;
};

8
libsmtutil/SMTPortfolio.cpp
View File

@ -21,7 +21,7 @@
#ifdef HAVE_Z3
#include <libsmtutil/Z3Interface.h>
#endif
#ifdef HAVE_CVC4
#ifdef HAVE_CVC5
#include <libsmtutil/CVC4Interface.h>
#endif
#include <libsmtutil/SMTLib2Interface.h>
@ -46,9 +46,9 @@ SMTPortfolio::SMTPortfolio(
if (_enabledSolvers.z3 && Z3Interface::available())
m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
#endif
#ifdef HAVE_CVC4
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(make_unique<CVC4Interface>(m_queryTimeout));
#ifdef HAVE_CVC5
if (_enabledSolvers.cvc5)
m_solvers.emplace_back(make_unique<CVC5Interface>(m_queryTimeout));
#endif
}

18
libsmtutil/SolverInterface.h
View File

@ -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<std::string> const solvers{"cvc4", "eld", "smtlib2", "z3"};
static std::set<std::string> 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

16
libsolidity/formal/BMC.cpp
View File

@ -49,15 +49,15 @@ BMC::BMC(
SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_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<ASTNode const*, set<VerificationTargetType>, 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<ASTNode const*, set<Verificatio
);
// If this check is true, Z3 and CVC4 are not available
// If this check is true, Z3 and cvc5 are not available
// and the query answers were not provided, since SMTPortfolio
// guarantees that SmtLib2Interface is the first solver, if enabled.
if (
@ -132,7 +132,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_errorReporter.warning(
8084_error,
SourceLocation(),
"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
"BMC analysis was not possible. No SMT solver (Z3 or cvc5) was available."
" None of the installed solvers was enabled."
#ifdef HAVE_Z3_DLOPEN
" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."

10
libsolidity/formal/ModelChecker.cpp
View File

@ -170,8 +170,8 @@ SMTSolverChoice ModelChecker::availableSolvers()
#ifdef HAVE_Z3
available.z3 = solidity::smtutil::Z3Interface::available();
#endif
#ifdef HAVE_CVC4
available.cvc4 = true;
#ifdef HAVE_CVC5
available.cvc5 = true;
#endif
return available;
}
@ -180,13 +180,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."
);
}

2
solc/CommandLineParser.cpp
View File

@ -855,7 +855,7 @@ General Information)").c_str(),
)
(
g_strModelCheckerSolvers.c_str(),
po::value<string>()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"),
po::value<string>()->value_name("cvc5,eld,z3,smtlib2")->default_value("z3"),
"Select model checker solvers."
)
(

2
test/cmdlineTests/model_checker_solvers_smtlib2/err
View File

@ -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.

4
test/cmdlineTests/standard_model_checker_solvers_none/output.json
View File

@ -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"
}

4
test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
View File

@ -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"
}

2
test/libsolidity/SMTCheckerTest.h
View File

@ -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.

4
test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol
View File

@ -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.