1 files changed, 42 insertions, 126 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 8d40c354..63ab1679 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -21,6 +21,7 @@
 
 #include <boost/algorithm/string/predicate.hpp>
 #include <boost/algorithm/string/join.hpp>
+#include <boost/filesystem/operations.hpp>
 
 #include <cstdio>
 #include <fstream>
@@ -30,99 +31,31 @@
 #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()
+SMTLib2Interface::SMTLib2Interface(ReadFile::Callback const& _readFileCallback):
+	m_communicator(_readFileCallback)
 {
-	// 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");
+	write("(set-option :produce-models true)");
+	write("(set-logic QF_UFLIA)");
 }
 
 void SMTLib2Interface::push()
 {
 	m_accumulatedOutput.emplace_back();
-	//write("(push)\n");
 }
 
 void SMTLib2Interface::pop()
 {
-	//write("(pop)\n");
 	solAssert(!m_accumulatedOutput.empty(), "");
 	m_accumulatedOutput.pop_back();
 }
@@ -136,50 +69,34 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
 		(_domain == Sort::Int ? "Int" : "Bool") +
 		") " +
 		(_codomain == Sort::Int ? "Int" : "Bool") +
-		")\n"
+		")"
 	);
-	return Expression(_name, {});
+	return Expression(std::move(_name), {});
 }
 
 Expression SMTLib2Interface::newInteger(string _name)
 {
-	write("(declare-const |" + _name + "| Int)\n");
-	return Expression(_name, {});
+	write("(declare-const |" + _name + "| Int)");
+	return Expression(std::move(_name), {});
 }
 
 Expression SMTLib2Interface::newBool(string _name)
 {
-	write("(declare-const |" + _name + "| Bool)\n");
-	return Expression(_name, {});
+	write("(declare-const |" + _name + "| Bool)");
+	return Expression(std::move(_name), {});
 }
 
-void SMTLib2Interface::addAssertion(Expression _expr)
+void SMTLib2Interface::addAssertion(Expression const& _expr)
 {
-	write("(assert " + _expr.toSExpr() + ")\n");
+	write("(assert " + _expr.toSExpr() + ")");
 }
 
 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);
+	string response = m_communicator.communicate(
+		boost::algorithm::join(m_accumulatedOutput, "\n") +
+		checkSatAndGetValuesCommand(_expressionsToEvaluate)
+	);
 	CheckResult result;
 	// TODO proper parsing
 	if (boost::starts_with(response, "sat\n"))
@@ -189,44 +106,43 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 	else if (boost::starts_with(response, "unknown\n"))
 		result = CheckResult::UNKNOWN;
 	else
-		solAssert(false, "Invalid response to check-sat: " + response);
+		result = CheckResult::ERROR;
 
 	vector<string> values;
-	if (result != CheckResult::UNSAT)
+	if (result != CheckResult::UNSAT && result != CheckResult::ERROR)
 		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);
+	m_accumulatedOutput.back() += move(_data) + "\n";
 }
 
-string SMTLib2Interface::communicate(std::string const& _input)
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
 {
-	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;
+	string command;
+	if (_expressionsToEvaluate.empty())
+		command = "(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...
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
+			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + e.toSExpr() + "))\n";
+		}
+		command += "(check-sat)\n";
+		command += "(get-value (";
+		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+			command += "|EVALEXPR_" + to_string(i) + "| ";
+		command += "))\n";
+	}
+
+	return command;
 }
 
 vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end)