Introduce native Z3 support.

2 files changed, 244 insertions, 0 deletions

diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
new file mode 100644
index 00000000..0d59a3c7
--- /dev/null
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -0,0 +1,179 @@
+/*
+	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/Z3Interface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+
+#include <libdevcore/CommonIO.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity::smt;
+
+Z3Interface::Z3Interface():
+	m_solver(m_context)
+{
+}
+
+void Z3Interface::reset()
+{
+	m_constants.clear();
+	m_functions.clear();
+	m_solver.reset();
+}
+
+void Z3Interface::push()
+{
+	m_solver.push();
+}
+
+void Z3Interface::pop()
+{
+	m_solver.pop();
+}
+
+Expression Z3Interface::newFunction(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)
+{
+	m_constants.insert({_name, m_context.int_const(_name.c_str())});
+	return SolverInterface::newInteger(move(_name));
+}
+
+Expression Z3Interface::newBool(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)
+{
+	m_solver.add(toZ3Expr(_expr));
+}
+
+pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	CheckResult result;
+	switch (m_solver.check())
+	{
+	case z3::check_result::sat:
+		result = CheckResult::SAT;
+		break;
+	case z3::check_result::unsat:
+		result = CheckResult::UNSAT;
+		break;
+	case z3::check_result::unknown:
+		result = CheckResult::UNKNOWN;
+		break;
+	default:
+		solAssert(false, "");
+	}
+
+	vector<string> values;
+	if (result != CheckResult::UNSAT)
+	{
+		z3::model m = m_solver.get_model();
+		for (Expression const& e: _expressionsToEvaluate)
+			values.push_back(toString(m.eval(toZ3Expr(e))));
+	}
+	return make_pair(result, values);
+}
+
+z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
+{
+	if (_expr.arguments.empty() && m_constants.count(_expr.name))
+		return m_constants.at(_expr.name);
+	z3::expr_vector arguments(m_context);
+	for (auto const& arg: _expr.arguments)
+		arguments.push_back(toZ3Expr(arg));
+
+	static map<string, unsigned> arity{
+		{"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);
+	else if (m_constants.count(n))
+	{
+		solAssert(arguments.empty(), "");
+		return m_constants.at(n);
+	}
+	else if (arguments.empty())
+	{
+		// We assume it is an integer...
+		return m_context.int_val(n.c_str());
+	}
+
+	assert(arity.count(n) && arity.at(n) == arguments.size());
+	if (n == "not")
+		return !arguments[0];
+	else if (n == "and")
+		return arguments[0] && arguments[1];
+	else if (n == "or")
+		return arguments[0] || arguments[1];
+	else if (n == "=")
+		return arguments[0] == arguments[1];
+	else if (n == "<")
+		return arguments[0] < arguments[1];
+	else if (n == "<=")
+		return arguments[0] <= arguments[1];
+	else if (n == ">")
+		return arguments[0] > arguments[1];
+	else if (n == ">=")
+		return arguments[0] >= arguments[1];
+	else if (n == "+")
+		return arguments[0] + arguments[1];
+	else if (n == "-")
+		return arguments[0] - arguments[1];
+	else if (n == "*")
+		return arguments[0] * arguments[1];
+	// Cannot reach here.
+	solAssert(false, "");
+	return arguments[0];
+}
+
+z3::sort Z3Interface::z3Sort(Sort _sort)
+{
+	switch (_sort)
+	{
+	case Sort::Bool:
+		return m_context.bool_sort();
+	case Sort::Int:
+		return m_context.int_sort();
+	default:
+		break;
+	}
+	solAssert(false, "");
+	// Cannot be reached.
+	return m_context.int_sort();
+}
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
new file mode 100644
index 00000000..44d4bb2f
--- /dev/null
+++ b/libsolidity/formal/Z3Interface.h
@@ -0,0 +1,65 @@
+/*
+	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 <z3++.h>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class Z3Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+	Z3Interface();
+
+	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:
+	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;
+	std::map<std::string, z3::func_decl> m_functions;
+};
+
+}
+}
+}