Merge pull request #4351 from ethereum/smt_portfolio

[SMTChecker] SMTPortfolio: use all SMT solvers available

libsolidity/CMakeLists.txt

@@ -7,9 +7,10 @@ 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")
+endif()
+
 find_package(GMP QUIET)
 find_package(CVC4 QUIET)
 if (${CVC4_FOUND})
@@ -22,9 +23,11 @@ else()
     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()
+
+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})

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)

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;
+	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
-	Expression newInteger(std::string _name) override;
+	void declareInteger(std::string _name) override;
-	Expression newBool(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;

libsolidity/formal/SMTChecker.cpp

@@ -17,13 +17,7 @@
 
 #include <libsolidity/formal/SMTChecker.h>
 
-#ifdef HAVE_Z3
+#include <libsolidity/formal/SMTPortfolio.h>
-#include <libsolidity/formal/Z3Interface.h>
-#elif HAVE_CVC4
-#include <libsolidity/formal/CVC4Interface.h>
-#else
-#include <libsolidity/formal/SMTLib2Interface.h>
-#endif
 
 #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::SMTPortfolio>(_readFileCallback)),
-	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_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.

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)

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;
+	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
-	Expression newInteger(std::string _name) override;
+	void declareInteger(std::string _name) override;
-	Expression newBool(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;

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;
+}

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;
+};
+
+}
+}
+}

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);
 	}
 

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)

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;
+	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
-	Expression newInteger(std::string _name) override;
+	void declareInteger(std::string _name) override;
-	Expression newBool(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;