diff options
author | Alex Beregszaszi <alex@rtfs.hu> | 2018-07-28 00:07:56 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-28 00:07:56 +0800 |
commit | 2794a22d84d05c83bd6e9f57d16a9e66a662812f (patch) | |
tree | c861a097b885416b67d2ef98f20ae9f91950756d /libsolidity | |
parent | 5faa60e8834b5302f8d58f719c6962ed3affb50f (diff) | |
parent | 55c1fb60b4ba60685262f332f2b197a7ef81d5b8 (diff) | |
download | dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.gz dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.bz2 dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.lz dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.xz dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.zst dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.zip |
Merge pull request #4351 from ethereum/smt_portfolio
[SMTChecker] SMTPortfolio: use all SMT solvers available
Diffstat (limited to 'libsolidity')
-rw-r--r-- | libsolidity/CMakeLists.txt | 29 | ||||
-rw-r--r-- | libsolidity/formal/CVC4Interface.cpp | 9 | ||||
-rw-r--r-- | libsolidity/formal/CVC4Interface.h | 6 | ||||
-rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 22 | ||||
-rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 9 | ||||
-rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 6 | ||||
-rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 151 | ||||
-rw-r--r-- | libsolidity/formal/SMTPortfolio.h | 67 | ||||
-rw-r--r-- | libsolidity/formal/SolverInterface.h | 14 | ||||
-rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 9 | ||||
-rw-r--r-- | libsolidity/formal/Z3Interface.h | 6 |
11 files changed, 269 insertions, 59 deletions
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 0bdec4b4..706b3b08 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -7,24 +7,27 @@ if (${Z3_FOUND}) include_directories(${Z3_INCLUDE_DIR}) add_definitions(-DHAVE_Z3) message("Z3 SMT solver found. This enables optional SMT checking with Z3.") - list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") else() 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() +endif() + +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("No SMT solver found (Z3 or CVC4). Optional SMT checking will not be available. Please install Z3 or CVC4 if it is desired.") + 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() + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") +endif() + +if (NOT (${Z3_FOUND} OR ${CVC4_FOUND})) + message("No SMT solver found. Optional SMT checking will not be available. Please install Z3 or CVC4 if it is desired.") endif() add_library(solidity ${sources} ${headers}) diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index 0530e940..84d36de0 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -50,23 +50,20 @@ void CVC4Interface::pop() m_solver.pop(); } -Expression CVC4Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void CVC4Interface::declareFunction(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) +void CVC4Interface::declareInteger(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) +void CVC4Interface::declareBool(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) diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h index cfaeb412..dcd87525 100644 --- a/libsolidity/formal/CVC4Interface.h +++ b/libsolidity/formal/CVC4Interface.h @@ -40,9 +40,9 @@ public: 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 declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 2623a2ba..109c8dbe 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -17,13 +17,7 @@ #include <libsolidity/formal/SMTChecker.h> -#ifdef HAVE_Z3 -#include <libsolidity/formal/Z3Interface.h> -#elif HAVE_CVC4 -#include <libsolidity/formal/CVC4Interface.h> -#else -#include <libsolidity/formal/SMTLib2Interface.h> -#endif +#include <libsolidity/formal/SMTPortfolio.h> #include <libsolidity/formal/SSAVariable.h> #include <libsolidity/formal/SymbolicIntVariable.h> @@ -39,16 +33,9 @@ using namespace dev; 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 + m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)), m_errorReporter(_errorReporter) { - (void)_readFileCallback; } void SMTChecker::analyze(SourceUnit const& _source) @@ -630,6 +617,9 @@ void SMTChecker::checkCondition( case smt::CheckResult::UNKNOWN: m_errorReporter.warning(_location, _description + " might happen here." + loopComment); break; + case smt::CheckResult::CONFLICTING: + m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); + break; case smt::CheckResult::ERROR: m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; @@ -657,6 +647,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); + else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING) + m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound."); else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE) { // everything fine. diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 00ac523f..d9ea6df6 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -62,7 +62,7 @@ void SMTLib2Interface::pop() m_accumulatedOutput.pop_back(); } -Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain) { write( "(declare-fun |" + @@ -73,19 +73,16 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom (_codomain == Sort::Int ? "Int" : "Bool") + ")" ); - return SolverInterface::newFunction(move(_name), _domain, _codomain); } -Expression SMTLib2Interface::newInteger(string _name) +void SMTLib2Interface::declareInteger(string _name) { write("(declare-const |" + _name + "| Int)"); - return SolverInterface::newInteger(move(_name)); } -Expression SMTLib2Interface::newBool(string _name) +void SMTLib2Interface::declareBool(string _name) { write("(declare-const |" + _name + "| Bool)"); - return SolverInterface::newBool(std::move(_name)); } void SMTLib2Interface::addAssertion(Expression const& _expr) diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 63188acd..61071fe5 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -48,9 +48,9 @@ public: 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 declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp new file mode 100644 index 00000000..64806097 --- /dev/null +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -0,0 +1,151 @@ +/* + 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/SMTPortfolio.h> + +#ifdef HAVE_Z3 +#include <libsolidity/formal/Z3Interface.h> +#endif +#ifdef HAVE_CVC4 +#include <libsolidity/formal/CVC4Interface.h> +#endif +#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) +#include <libsolidity/formal/SMTLib2Interface.h> +#endif + +using namespace std; +using namespace dev; +using namespace dev::solidity::smt; + +SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) +{ +#ifdef HAVE_Z3 + m_solvers.emplace_back(make_shared<smt::Z3Interface>()); +#endif +#ifdef HAVE_CVC4 + m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); +#endif +#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)), +#endif + (void)_readCallback; +} + +void SMTPortfolio::reset() +{ + for (auto s : m_solvers) + s->reset(); +} + +void SMTPortfolio::push() +{ + for (auto s : m_solvers) + s->push(); +} + +void SMTPortfolio::pop() +{ + for (auto s : m_solvers) + s->pop(); +} + +void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain) +{ + for (auto s : m_solvers) + s->declareFunction(_name, _domain, _codomain); +} + +void SMTPortfolio::declareInteger(string _name) +{ + for (auto s : m_solvers) + s->declareInteger(_name); +} + +void SMTPortfolio::declareBool(string _name) +{ + for (auto s : m_solvers) + s->declareBool(_name); +} + +void SMTPortfolio::addAssertion(Expression const& _expr) +{ + for (auto s : m_solvers) + s->addAssertion(_expr); +} + +/* + * Broadcasts the SMT query to all solvers and returns a single result. + * This comment explains how this result is decided. + * + * When a solver is queried, there are four possible answers: + * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR + * We say that a solver _answered_ the query if it returns either: + * SAT or UNSAT + * A solver did not answer the query if it returns either: + * UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc). + * + * Ideally all solvers answer the query and agree on what the answer is + * (all say SAT or all say UNSAT). + * + * The actual logic as as follows: + * 1) If at least one solver answers the query, all the non-answer results are ignored. + * Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR + * because one buggy solver/integration shouldn't break the portfolio. + * + * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy + * and the result is CONFLICTING. + * In the future if we have more than 2 solvers enabled we could go with the majority. + * + * 3) If NO solver answers the query: + * If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN. + * This is preferred over ERROR since the SMTChecker might decide to abstract the query + * when it is told that this is a hard query to solve. + * + * If all solvers return ERROR, the result is ERROR. +*/ +pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate) +{ + CheckResult lastResult = CheckResult::ERROR; + vector<string> finalValues; + for (auto s : m_solvers) + { + CheckResult result; + vector<string> values; + tie(result, values) = s->check(_expressionsToEvaluate); + if (solverAnswered(result)) + { + if (!solverAnswered(lastResult)) + { + lastResult = result; + finalValues = std::move(values); + } + else if (lastResult != result) + { + lastResult = CheckResult::CONFLICTING; + break; + } + } + else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) + lastResult = result; + } + return make_pair(lastResult, finalValues); +} + +bool SMTPortfolio::solverAnswered(CheckResult result) +{ + return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; +} diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h new file mode 100644 index 00000000..96c7ff57 --- /dev/null +++ b/libsolidity/formal/SMTPortfolio.h @@ -0,0 +1,67 @@ +/* + 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 <libsolidity/interface/ReadFile.h> + +#include <boost/noncopyable.hpp> + +#include <vector> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +/** + * The SMTPortfolio wraps all available solvers within a single interface, + * propagating the functionalities to all solvers. + * It also checks whether different solvers give conflicting answers + * to SMT queries. + */ +class SMTPortfolio: public SolverInterface, public boost::noncopyable +{ +public: + SMTPortfolio(ReadCallback::Callback const& _readCallback); + + void reset() override; + + void push() override; + void pop() override; + + void declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(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: + static bool solverAnswered(CheckResult result); + + std::vector<std::shared_ptr<smt::SolverInterface>> m_solvers; +}; + +} +} +} diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index a6d65ce2..8bbd0417 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -39,7 +39,7 @@ namespace smt enum class CheckResult { - SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR + SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR }; enum class Sort @@ -199,8 +199,10 @@ public: virtual void push() = 0; virtual void pop() = 0; - virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain) + virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0; + Expression newFunction(std::string _name, Sort _domain, Sort _codomain) { + declareFunction(_name, _domain, _codomain); solAssert(_domain == Sort::Int, "Function sort not supported."); // Subclasses should do something here switch (_codomain) @@ -214,14 +216,18 @@ public: break; } } - virtual Expression newInteger(std::string _name) + virtual void declareInteger(std::string _name) = 0; + Expression newInteger(std::string _name) { // Subclasses should do something here + declareInteger(_name); return Expression(std::move(_name), {}, Sort::Int); } - virtual Expression newBool(std::string _name) + virtual void declareBool(std::string _name) = 0; + Expression newBool(std::string _name) { // Subclasses should do something here + declareBool(_name); return Expression(std::move(_name), {}, Sort::Bool); } diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index b57bcb94..784fbd28 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -51,22 +51,19 @@ void Z3Interface::pop() m_solver.pop(); } -Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain) { m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); - return SolverInterface::newFunction(move(_name), _domain, _codomain); } -Expression Z3Interface::newInteger(string _name) +void Z3Interface::declareInteger(string _name) { m_constants.insert({_name, m_context.int_const(_name.c_str())}); - return SolverInterface::newInteger(move(_name)); } -Expression Z3Interface::newBool(string _name) +void Z3Interface::declareBool(string _name) { m_constants.insert({_name, m_context.bool_const(_name.c_str())}); - return SolverInterface::newBool(std::move(_name)); } void Z3Interface::addAssertion(Expression const& _expr) diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h index 354ded25..84880ff3 100644 --- a/libsolidity/formal/Z3Interface.h +++ b/libsolidity/formal/Z3Interface.h @@ -40,9 +40,9 @@ public: 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 declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; |