diff options
| -rw-r--r-- | Changelog.md | 4 | ||||
| -rw-r--r-- | cmake/FindCVC4.cmake | 4 | ||||
| -rw-r--r-- | cmake/FindGMP.cmake | 3 | ||||
| -rw-r--r-- | libsolidity/CMakeLists.txt | 26 | ||||
| -rw-r--r-- | libsolidity/formal/CVC4Interface.cpp | 200 | ||||
| -rw-r--r-- | libsolidity/formal/CVC4Interface.h | 62 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 4 | ||||
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 20 | ||||
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 17 | ||||
| -rw-r--r-- | libsolidity/formal/Z3Interface.h | 3 |
10 files changed, 318 insertions, 25 deletions
diff --git a/Changelog.md b/Changelog.md index 2279cd2b..cfd23ad0 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,12 +1,11 @@ ### 0.4.23 (unreleased) Features: - + * SMTChecker: Integration with CVC4 SMT solver Bugfixes: - ### 0.4.22 (2018-04-16) Features: @@ -34,7 +33,6 @@ Features: * Syntax Tests: Add source locations to syntax test expectations. * Type Checker: Improve documentation and warnings for accessing contract members inherited from ``address``. - Bugfixes: * Code Generator: Allow ``block.blockhash`` without being called. * Code Generator: Do not include internal functions in the runtime bytecode which are only referenced in the constructor. diff --git a/cmake/FindCVC4.cmake b/cmake/FindCVC4.cmake new file mode 100644 index 00000000..0fb13196 --- /dev/null +++ b/cmake/FindCVC4.cmake @@ -0,0 +1,4 @@ +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) diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake new file mode 100644 index 00000000..8abe354c --- /dev/null +++ b/cmake/FindGMP.cmake @@ -0,0 +1,3 @@ +find_library(GMP_LIBRARY NAMES gmp ) +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(GMP DEFAULT_MSG GMP_LIBRARY) diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 99612c40..97b01c83 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -6,10 +6,25 @@ find_package(Z3 QUIET) if (${Z3_FOUND}) include_directories(${Z3_INCLUDE_DIR}) add_definitions(-DHAVE_Z3) - message("Z3 SMT solver found. This enables optional SMT checking.") + message("Z3 SMT solver found. This enables optional SMT checking with Z3.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") else() - message("Z3 SMT solver NOT found. Optional SMT checking will not be available. Please install Z3 if it is desired.") list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp") + find_package(GMP QUIET) + find_package(CVC4 QUIET) + if (${CVC4_FOUND}) + if (${GMP_FOUND}) + include_directories(${CVC4_INCLUDE_DIR}) + add_definitions(-DHAVE_CVC4) + message("CVC4 SMT solver and GMP found. This enables optional SMT checking with CVC4.") + else() + message("CVC4 SMT solver found but its dependency GMP was NOT found. Optional SMT checking with CVC4 will not be available. Please install GMP if it is desired.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") + endif() + else() + message("No SMT solver found (Z3 or CVC4). Optional SMT checking will not be available. Please install Z3 or CVC4 if it is desired.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") + endif() endif() add_library(solidity ${sources} ${headers}) @@ -17,4 +32,9 @@ target_link_libraries(solidity PUBLIC evmasm devcore) if (${Z3_FOUND}) target_link_libraries(solidity PUBLIC ${Z3_LIBRARY}) -endif()
\ No newline at end of file +endif() + +if (${CVC4_FOUND} AND ${GMP_FOUND}) + target_link_libraries(solidity PUBLIC ${CVC4_LIBRARY}) + target_link_libraries(solidity PUBLIC ${GMP_LIBRARY}) +endif() diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp new file mode 100644 index 00000000..dba5823a --- /dev/null +++ b/libsolidity/formal/CVC4Interface.cpp @@ -0,0 +1,200 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/CVC4Interface.h> + +#include <libsolidity/interface/Exceptions.h> + +#include <libdevcore/CommonIO.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity::smt; + +CVC4Interface::CVC4Interface(): + m_solver(&m_context) +{ + reset(); +} + +void CVC4Interface::reset() +{ + m_constants.clear(); + m_functions.clear(); + m_solver.reset(); + m_solver.setOption("produce-models", true); +} + +void CVC4Interface::push() +{ + m_solver.push(); +} + +void CVC4Interface::pop() +{ + m_solver.pop(); +} + +Expression CVC4Interface::newFunction(string _name, Sort _domain, Sort _codomain) +{ + CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain)); + m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)}); + return SolverInterface::newFunction(move(_name), _domain, _codomain); +} + +Expression CVC4Interface::newInteger(string _name) +{ + m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())}); + return SolverInterface::newInteger(move(_name)); +} + +Expression CVC4Interface::newBool(string _name) +{ + m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())}); + return SolverInterface::newBool(std::move(_name)); +} + +void CVC4Interface::addAssertion(Expression const& _expr) +{ + try + { + m_solver.assertFormula(toCVC4Expr(_expr)); + } + catch (CVC4::TypeCheckingException const&) + { + solAssert(false, ""); + } + catch (CVC4::LogicException const&) + { + solAssert(false, ""); + } + catch (CVC4::UnsafeInterruptException const&) + { + solAssert(false, ""); + } +} + +pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& _expressionsToEvaluate) +{ + CheckResult result; + vector<string> values; + try + { + switch (m_solver.checkSat().isSat()) + { + case CVC4::Result::SAT: + result = CheckResult::SATISFIABLE; + break; + case CVC4::Result::UNSAT: + result = CheckResult::UNSATISFIABLE; + break; + case CVC4::Result::SAT_UNKNOWN: + result = CheckResult::UNKNOWN; + break; + default: + solAssert(false, ""); + } + + if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) + { + for (Expression const& e: _expressionsToEvaluate) + values.push_back(toString(m_solver.getValue(toCVC4Expr(e)))); + } + } + catch (CVC4::Exception & e) + { + result = CheckResult::ERROR; + values.clear(); + } + + return make_pair(result, values); +} + +CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) +{ + if (_expr.arguments.empty() && m_constants.count(_expr.name)) + return m_constants.at(_expr.name); + vector<CVC4::Expr> arguments; + for (auto const& arg: _expr.arguments) + arguments.push_back(toCVC4Expr(arg)); + + string const& n = _expr.name; + if (m_functions.count(n)) + return m_context.mkExpr(CVC4::kind::APPLY_UF, m_functions[n], arguments); + else if (m_constants.count(n)) + { + solAssert(arguments.empty(), ""); + return m_constants.at(n); + } + else if (arguments.empty()) + { + if (n == "true") + return m_context.mkConst(true); + else if (n == "false") + return m_context.mkConst(false); + else + // We assume it is an integer... + return m_context.mkConst(CVC4::Rational(n)); + } + + solAssert(_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::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 == "/") + return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]); + // Cannot reach here. + solAssert(false, ""); + return arguments[0]; +} + +CVC4::Type CVC4Interface::cvc4Sort(Sort _sort) +{ + switch (_sort) + { + case Sort::Bool: + return m_context.booleanType(); + case Sort::Int: + return m_context.integerType(); + default: + break; + } + solAssert(false, ""); + // Cannot be reached. + return m_context.integerType(); +} diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h new file mode 100644 index 00000000..cfaeb412 --- /dev/null +++ b/libsolidity/formal/CVC4Interface.h @@ -0,0 +1,62 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/formal/SolverInterface.h> + +#include <boost/noncopyable.hpp> + +#include <cvc4/cvc4.h> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +class CVC4Interface: public SolverInterface, public boost::noncopyable +{ +public: + CVC4Interface(); + + void reset() override; + + void push() override; + void pop() override; + + Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override; + Expression newInteger(std::string _name) override; + Expression newBool(std::string _name) override; + + void addAssertion(Expression const& _expr) override; + std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + +private: + CVC4::Expr toCVC4Expr(Expression const& _expr); + CVC4::Type cvc4Sort(smt::Sort _sort); + + CVC4::ExprManager m_context; + CVC4::SmtEngine m_solver; + std::map<std::string, CVC4::Expr> m_constants; + std::map<std::string, CVC4::Expr> m_functions; +}; + +} +} +} diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 8f4abdc2..da6b632c 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -19,6 +19,8 @@ #ifdef HAVE_Z3 #include <libsolidity/formal/Z3Interface.h> +#elif HAVE_CVC4 +#include <libsolidity/formal/CVC4Interface.h> #else #include <libsolidity/formal/SMTLib2Interface.h> #endif @@ -39,6 +41,8 @@ using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): #ifdef HAVE_Z3 m_interface(make_shared<smt::Z3Interface>()), +#elif HAVE_CVC4 + m_interface(make_shared<smt::CVC4Interface>()), #else m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)), #endif diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 0bdebb6c..e127bb55 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -65,6 +65,26 @@ public: Expression& operator=(Expression const&) = default; Expression& operator=(Expression&&) = default; + bool hasCorrectArity() const + { + static std::map<std::string, unsigned> const operatorsArity{ + {"ite", 3}, + {"not", 1}, + {"and", 2}, + {"or", 2}, + {"=", 2}, + {"<", 2}, + {"<=", 2}, + {">", 2}, + {">=", 2}, + {"+", 2}, + {"-", 2}, + {"*", 2}, + {"/", 2} + }; + return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size(); + } + static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) { solAssert(_trueValue.sort == _falseValue.sort, ""); diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 125da00d..41943c92 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -116,21 +116,6 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) for (auto const& arg: _expr.arguments) arguments.push_back(toZ3Expr(arg)); - static map<string, unsigned> arity{ - {"ite", 3}, - {"not", 1}, - {"and", 2}, - {"or", 2}, - {"=", 2}, - {"<", 2}, - {"<=", 2}, - {">", 2}, - {">=", 2}, - {"+", 2}, - {"-", 2}, - {"*", 2}, - {"/", 2} - }; string const& n = _expr.name; if (m_functions.count(n)) return m_functions.at(n)(arguments); @@ -150,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return m_context.int_val(n.c_str()); } - solAssert(arity.count(n) && arity.at(n) == arguments.size(), ""); + solAssert(_expr.hasCorrectArity(), ""); if (n == "ite") return z3::ite(arguments[0], arguments[1], arguments[2]); else if (n == "not") diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h index 44d4bb2f..354ded25 100644 --- a/libsolidity/formal/Z3Interface.h +++ b/libsolidity/formal/Z3Interface.h @@ -51,9 +51,6 @@ private: z3::expr toZ3Expr(Expression const& _expr); z3::sort z3Sort(smt::Sort _sort); - std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate); - std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end); - z3::context m_context; z3::solver m_solver; std::map<std::string, z3::expr> m_constants; |