From 87a38e1abe61547e66aedfa595a73fb78184d609 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 20 Apr 2018 16:56:10 +0200 Subject: [SMTChecker] SMTPortfolio: use all SMT solvers available --- libsolidity/formal/SMTPortfolio.cpp | 150 ++++++++++++++++++++++++++++++++++++ 1 file changed, 150 insertions(+) create mode 100644 libsolidity/formal/SMTPortfolio.cpp (limited to 'libsolidity/formal/SMTPortfolio.cpp') diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp new file mode 100644 index 00000000..25795738 --- /dev/null +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -0,0 +1,150 @@ +/* + 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 . +*/ + +#include + +#ifdef HAVE_Z3 +#include +#endif +#ifdef HAVE_CVC4 +#include +#endif +#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) +#include +#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()); +#endif +#ifdef HAVE_CVC4 + m_solvers.emplace_back(make_shared()); +#endif +#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) + m_solvers.emplace_back(make_shared(_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, 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 and we abort. + * 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> SMTPortfolio::check(vector const& _expressionsToEvaluate) +{ + CheckResult lastResult = CheckResult::ERROR; + vector finalValues; + for (auto s : m_solvers) + { + CheckResult result; + vector values; + tie(result, values) = s->check(_expressionsToEvaluate); + if (solverAnswered(result)) + { + if (!solverAnswered(lastResult)) + { + lastResult = result; + finalValues = std::move(values); + } + else if (lastResult != result) + { + solAssert(false, "At least two SMT solvers gave opposing results."); + } + } + 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; +} -- cgit v1.2.3 From 55c1fb60b4ba60685262f332f2b197a7ef81d5b8 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 26 Jun 2018 12:41:26 +0200 Subject: [SMTChecker] Add CheckResult::CONFLICTING --- libsolidity/formal/SMTPortfolio.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal/SMTPortfolio.cpp') diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 25795738..64806097 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -92,7 +92,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr) * This comment explains how this result is decided. * * When a solver is queried, there are four possible answers: - * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, ERROR + * 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: @@ -107,7 +107,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr) * 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 and we abort. + * 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: @@ -135,7 +135,8 @@ pair> SMTPortfolio::check(vector const& } else if (lastResult != result) { - solAssert(false, "At least two SMT solvers gave opposing results."); + lastResult = CheckResult::CONFLICTING; + break; } } else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) -- cgit v1.2.3 From 179427fd659b5b5471d0a4b9a94f015bd6665c96 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Fri, 27 Jul 2018 22:39:36 +0100 Subject: Import dev::solidity namespace in SMTPortfolio --- libsolidity/formal/SMTPortfolio.cpp | 1 + 1 file changed, 1 insertion(+) (limited to 'libsolidity/formal/SMTPortfolio.cpp') diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 64806097..8b9fe9ce 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -29,6 +29,7 @@ using namespace std; using namespace dev; +using namespace dev::solidity; using namespace dev::solidity::smt; SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) -- cgit v1.2.3