Use file to communicate with z3.

5 files changed, 274 insertions, 15 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 29ca63fe..da14ddb7 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -16,7 +16,6 @@ option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms"
 # Let's find our dependencies
 include(EthDependencies)
 include(deps/jsoncpp.cmake)
-include(deps/z3.cmake)
 
 find_package(Threads)
 
diff --git a/deps b/deps
-Subproject cd9c6ff69134e8f53bde70d92cce12ad294752d
+Subproject e5c8316db8d3daa0abc3b5af8545ce330057608
diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp
index 028e4400..b86a0279 100644
--- a/libsolidity/formal/SMTCheckerImpl.cpp
+++ b/libsolidity/formal/SMTCheckerImpl.cpp
@@ -325,25 +325,40 @@ void SMTCheckerImpl::checkCondition(
 {
 	m_interface.push();
 	m_interface.addAssertion(_condition);
-	switch (m_interface.check())
+
+	vector<smt::Expression> expressionsToEvaluate;
+	if (m_currentFunction)
+	{
+		if (_additionalValue)
+			expressionsToEvaluate.emplace_back(*_additionalValue);
+		for (auto const& param: m_currentFunction->parameters())
+			if (knownVariable(*param))
+				expressionsToEvaluate.emplace_back(currentValue(*param));
+		for (auto const& var: m_currentFunction->localVariables())
+			if (knownVariable(*var))
+				expressionsToEvaluate.emplace_back(currentValue(*var));
+	}
+	smt::CheckResult result;
+	vector<string> values;
+	tie(result, values) = m_interface.check(expressionsToEvaluate);
+	switch (result)
 	{
 	case smt::CheckResult::SAT:
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
+		size_t i = 0;
 		if (m_currentFunction)
 		{
 			message << " for:\n";
 			if (_additionalValue)
-				message << "  " << _additionalValueName << " = " << m_interface.eval(*_additionalValue) << "\n";
+				message << "  " << _additionalValueName << " = " << values.at(i++) << "\n";
 			for (auto const& param: m_currentFunction->parameters())
 				if (knownVariable(*param))
-					message << "  " << param->name() << " = " << m_interface.eval(currentValue(*param)) << "\n";
+					message << "  " << param->name() << " = " << values.at(i++) << "\n";
 			for (auto const& var: m_currentFunction->localVariables())
 				if (knownVariable(*var))
-					message << "  " << var->name() << " = " << m_interface.eval(currentValue(*var)) << "\n";
-//			message << m << endl;
-//			message << m_solver << endl;
+					message << "  " << var->name() << " = " << values.at(i++) << "\n";
 		}
 		else
 			message << ".";
@@ -412,12 +427,12 @@ smt::Expression SMTCheckerImpl::newValue(const Declaration& _decl)
 
 smt::Expression SMTCheckerImpl::minValue(IntegerType const& _t)
 {
-	return m_interface.newInteger(_t.minValue());
+	return smt::Expression(_t.minValue());
 }
 
 smt::Expression SMTCheckerImpl::maxValue(IntegerType const& _t)
 {
-	return m_interface.newInteger(_t.maxValue());
+	return smt::Expression(_t.maxValue());
 }
 
 smt::Expression SMTCheckerImpl::expr(Expression const& _e)
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index c736ed2a..8d40c354 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -17,8 +17,230 @@
 
 #include <libsolidity/formal/SMTLib2Interface.h>
 
+#include <libsolidity/interface/Exceptions.h>
+
+#include <boost/algorithm/string/predicate.hpp>
+#include <boost/algorithm/string/join.hpp>
+
+#include <cstdio>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <stdexcept>
+#include <string>
+#include <array>
+
+#include <sys/types.h>
+#include <unistd.h>
+#include <stdio.h>
+#include <stdlib.h>
 
 using namespace std;
 using namespace dev;
 using namespace dev::solidity::smt;
 
+
+//namespace
+//{
+
+//void createSubprocess(FILE*& _readPipe, FILE*& _writePipe)
+//{
+//	int pipe_in[2];   /* This is the pipe with wich we write to the child process. */
+//	int pipe_out[2];  /* This is the pipe with wich we read from the child process. */
+
+//	solAssert(!pipe(pipe_in) && !pipe(pipe_out), "");
+
+//	/* Attempt to fork and check for errors */
+//	pid_t pid = fork();
+//	solAssert(pid != -1, "");
+
+//	if (pid)
+//	{
+//		/* The parent has the non-zero PID. */
+//		_readPipe = fdopen(pipe_out[0], "r");
+//		_writePipe = fdopen(pipe_in[1], "w");
+//		close(pipe_out[1]);
+//		close(pipe_in[0]);
+//	}
+//	else
+//	{
+//		/* The child has the zero pid returned by fork*/
+//		cout << "child" << endl;
+//		solAssert(dup2(pipe_out[1], 1) != -1, "");
+//		solAssert(dup2(pipe_in[0], 0) != -1, "");
+//		solAssert(close(pipe_out[0]) == 0, "");
+//		solAssert(close(pipe_out[1]) == 0, "");
+//		solAssert(close(pipe_in[0]) == 0, "");
+//		solAssert(close(pipe_in[1]) == 0, "");
+//		execl("/usr/bin/z3", "z3", "-smt2", "-in", NULL);
+//		exit(1); /* Only reached if execl() failed */
+//	}
+//}
+
+//}
+
+SMTLib2Interface::SMTLib2Interface()
+{
+	// TODO using pipes did not really work, so trying it the hard way for now.
+//	createSubprocess(m_solverWrite, m_solverRead);
+//	solAssert(m_solverWrite, "Unable to start Z3");
+//	solAssert(m_solverRead, "Unable to start Z3");
+//	write("(set-option :produce-models true)\n(set-logic QF_LIA)\n");
+	reset();
+}
+
+SMTLib2Interface::~SMTLib2Interface()
+{
+//	if (m_solverWrite)
+//	{
+//		write("(exit)\n");
+//		fflush(m_solverWrite);
+//		fclose(m_solverWrite);
+//		m_solverWrite = nullptr;
+//	}
+//	if (m_solverRead)
+//	{
+//		fclose(m_solverRead);
+//		m_solverRead = nullptr;
+//	}
+}
+
+void SMTLib2Interface::reset()
+{
+//	write("(reset)\n");
+//	write("(set-option :produce-models true)\n");
+	m_accumulatedOutput.clear();
+	m_accumulatedOutput.emplace_back();
+	write("(set-option :produce-models true)\n(set-logic QF_UFLIA)\n");
+}
+
+void SMTLib2Interface::push()
+{
+	m_accumulatedOutput.emplace_back();
+	//write("(push)\n");
+}
+
+void SMTLib2Interface::pop()
+{
+	//write("(pop)\n");
+	solAssert(!m_accumulatedOutput.empty(), "");
+	m_accumulatedOutput.pop_back();
+}
+
+Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+{
+	write(
+		"(declare-fun |" +
+		_name +
+		"| (" +
+		(_domain == Sort::Int ? "Int" : "Bool") +
+		") " +
+		(_codomain == Sort::Int ? "Int" : "Bool") +
+		")\n"
+	);
+	return Expression(_name, {});
+}
+
+Expression SMTLib2Interface::newInteger(string _name)
+{
+	write("(declare-const |" + _name + "| Int)\n");
+	return Expression(_name, {});
+}
+
+Expression SMTLib2Interface::newBool(string _name)
+{
+	write("(declare-const |" + _name + "| Bool)\n");
+	return Expression(_name, {});
+}
+
+void SMTLib2Interface::addAssertion(Expression _expr)
+{
+	write("(assert " + _expr.toSExpr() + ")\n");
+}
+
+pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	string checks;
+	if (_expressionsToEvaluate.empty())
+		checks = "(check-sat)\n";
+	else
+	{
+		// TODO make sure these are unique
+		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+		{
+			auto const& e = _expressionsToEvaluate.at(i);
+			// TODO they don't have to be ints...
+			checks += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
+			checks += "(assert (= |EVALEXPR_" + to_string(i) + "| " + e.toSExpr() + "))\n";
+		}
+		checks += "(check-sat)\n";
+		checks += "(get-value (";
+		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+			checks += "|EVALEXPR_" + to_string(i) + "| ";
+		checks += "))\n";
+	}
+	string response = communicate(boost::algorithm::join(m_accumulatedOutput, "\n") + checks);
+	CheckResult result;
+	// TODO proper parsing
+	if (boost::starts_with(response, "sat\n"))
+		result = CheckResult::SAT;
+	else if (boost::starts_with(response, "unsat\n"))
+		result = CheckResult::UNSAT;
+	else if (boost::starts_with(response, "unknown\n"))
+		result = CheckResult::UNKNOWN;
+	else
+		solAssert(false, "Invalid response to check-sat: " + response);
+
+	vector<string> values;
+	if (result != CheckResult::UNSAT)
+		values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
+	return make_pair(result, values);
+}
+
+//string SMTLib2Interface::eval(Expression _expr)
+//{
+//	write("(get-value (" + _expr.toSExpr() + ")\n");
+//	std::string reply = communicate();
+//	cout << "<-- Z3: " << reply << endl;
+//	// TODO parse
+//	return reply;
+//}
+
+void SMTLib2Interface::write(string _data)
+{
+//	cout << " --> Z3: " << _data << endl;
+//	solAssert(m_solverWrite, "");
+//	solAssert(fputs(_data.c_str(), m_solverWrite) >= 0 || true, "EOF while communicating with Z3.");
+//	solAssert(fflush(m_solverWrite) == 0 || true, "");
+	solAssert(!m_accumulatedOutput.empty(), "");
+	m_accumulatedOutput.back() += move(_data);
+}
+
+string SMTLib2Interface::communicate(std::string const& _input)
+{
+	ofstream("/tmp/z3exchange.smt2") << _input << "(exit)" << endl;
+	FILE* solverOutput = popen("z3 -smt2 /tmp/z3exchange.smt2", "r");
+	string result;
+	array<char, 128> buffer;
+	while (!feof(solverOutput))
+		if (fgets(buffer.data(), 127, solverOutput) != nullptr)
+			result += buffer.data();
+	fclose(solverOutput);
+	return result;
+}
+
+vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end)
+{
+	vector<string> values;
+	while (_start < _end)
+	{
+		auto valStart = find(_start, _end, ' ');
+		if (valStart < _end)
+			++valStart;
+		auto valEnd = find(valStart, _end, ')');
+		values.emplace_back(valStart, valEnd);
+		_start = find(valEnd, _end, '(');
+	}
+
+	return values;
+}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index f984cfb5..b7bab043 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -17,11 +17,14 @@
 
 #pragma once
 
+#include <libsolidity/interface/Exceptions.h>
+
+#include <libdevcore/Common.h>
+
 #include <map>
 #include <string>
 #include <vector>
-
-#include <libdevcore/Common.h>
+#include <cstdio>
 
 namespace dev
 {
@@ -49,7 +52,8 @@ class Expression
 
 public:
 	Expression(size_t _number): m_name(std::to_string(_number)) {}
-	Expression(u256 const& _number): m_name(std::to_string(_number)) {}
+	Expression(u256 const& _number): m_name(_number.str()) {}
+	Expression(bigint const& _number): m_name(_number.str()) {}
 
 	Expression(Expression const& _other) = default;
 	Expression(Expression&& _other) = default;
@@ -104,9 +108,16 @@ public:
 	{
 		return Expression("*", std::move(_a), std::move(_b));
 	}
+	Expression operator()(Expression _a) const
+	{
+		solAssert(m_arguments.empty(), "Attempted function application to non-function.");
+		return Expression(m_name, _a);
+	}
 
 	std::string toSExpr() const
 	{
+		if (m_arguments.empty())
+			return m_name;
 		std::string sexpr = "(" + m_name;
 		for (auto const& arg: m_arguments)
 			sexpr += " " + arg.toSExpr();
@@ -126,9 +137,11 @@ private:
 	std::vector<Expression> const m_arguments;
 };
 
-class SMTLib2Interface
+class SMTLib2Interface: public boost::noncopyable
 {
 public:
+	SMTLib2Interface();
+	~SMTLib2Interface();
 
 	void reset();
 
@@ -140,8 +153,18 @@ public:
 	Expression newBool(std::string _name);
 
 	void addAssertion(Expression _expr);
-	CheckResult check();
-	std::string eval(Expression _expr);
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate);
+//	std::string eval(Expression _expr);
+
+private:
+	void write(std::string _data);
+	std::string communicate(std::string const& _input);
+
+	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
+
+	std::vector<std::string> m_accumulatedOutput;
+//	FILE* m_solverWrite = nullptr;
+//	FILE* m_solverRead = nullptr;
 };