aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-04-20 22:56:10 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2018-07-27 23:15:34 +0800
commit87a38e1abe61547e66aedfa595a73fb78184d609 (patch)
treeba41f379fbf2713f2e885c0d641a5780a06d7fe4 /libsolidity
parent5faa60e8834b5302f8d58f719c6962ed3affb50f (diff)
downloaddexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.gz
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.bz2
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.lz
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.xz
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.zst
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.zip
[SMTChecker] SMTPortfolio: use all SMT solvers available
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/CMakeLists.txt29
-rw-r--r--libsolidity/formal/CVC4Interface.cpp9
-rw-r--r--libsolidity/formal/CVC4Interface.h6
-rw-r--r--libsolidity/formal/SMTChecker.cpp17
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp9
-rw-r--r--libsolidity/formal/SMTLib2Interface.h6
-rw-r--r--libsolidity/formal/SMTPortfolio.cpp150
-rw-r--r--libsolidity/formal/SMTPortfolio.h67
-rw-r--r--libsolidity/formal/SolverInterface.h12
-rw-r--r--libsolidity/formal/Z3Interface.cpp9
-rw-r--r--libsolidity/formal/Z3Interface.h6
11 files changed, 262 insertions, 58 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..67625556 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)
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..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 <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, 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<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)
+ {
+ 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;
+}
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..f8a2bebb 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -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;