Merge pull request #3840 from ethereum/smt_cvc4

[SMTChecker] Integration with CVC4

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.

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)

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)

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()
+endif()
+
+if (${CVC4_FOUND} AND ${GMP_FOUND})
+  target_link_libraries(solidity PUBLIC ${CVC4_LIBRARY})
+  target_link_libraries(solidity PUBLIC ${GMP_LIBRARY})
+endif()

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

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

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

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, "");

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")

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;