Refactor Z3 read callback.

6 files changed, 46 insertions, 133 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a8ad60ed..c2f5c56d 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -17,7 +17,11 @@
 
 #include <libsolidity/formal/SMTChecker.h>
 
+#ifdef HAVE_Z3
+#include <libsolidity/formal/Z3Interface.h>
+#else
 #include <libsolidity/formal/SMTLib2Interface.h>
+#endif
 
 #include <libsolidity/interface/ErrorReporter.h>
 
@@ -25,10 +29,15 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback):
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
+#ifdef HAVE_Z3
+	m_interface(make_shared<smt::Z3Interface>()),
+#else
 	m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
+#endif
 	m_errorReporter(_errorReporter)
 {
+	(void)_readFileCallback;
 }
 
 void SMTChecker::analyze(SourceUnit const& _source)
@@ -36,7 +45,7 @@ void SMTChecker::analyze(SourceUnit const& _source)
 	bool pragmaFound = false;
 	for (auto const& node: _source.nodes())
 		if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
-			if (pragma->literals()[0] == "checkAssertionsZ3")
+			if (pragma->literals()[0] == "checkAssertions")
 				pragmaFound = true;
 	if (pragmaFound)
 	{
@@ -345,7 +354,19 @@ void SMTChecker::checkCondition(
 	}
 	smt::CheckResult result;
 	vector<string> values;
-	tie(result, values) = m_interface->check(expressionsToEvaluate);
+	try
+	{
+		tie(result, values) = m_interface->check(expressionsToEvaluate);
+	}
+	catch (smt::SolverError const& _e)
+	{
+		string description("Error querying SMT solver");
+		if (_e.comment())
+			description += ": " + *_e.comment();
+		m_errorReporter.warning(_location, description);
+		return;
+	}
+
 	switch (result)
 	{
 	case smt::CheckResult::SAT:
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 4b118abc..e7a9ef8c 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -95,10 +95,11 @@ void SMTLib2Interface::addAssertion(Expression const& _expr)
 
 pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
 {
-	string response = m_communicator.communicate(
+	string response = querySolver(
 		boost::algorithm::join(m_accumulatedOutput, "\n") +
 		checkSatAndGetValuesCommand(_expressionsToEvaluate)
 	);
+
 	CheckResult result;
 	// TODO proper parsing
 	if (boost::starts_with(response, "sat\n"))
@@ -173,3 +174,14 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
 
 	return values;
 }
+
+string SMTLib2Interface::querySolver(string const& _input)
+{
+	if (!m_queryCallback)
+		BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
+
+	ReadCallback::Result queryResult = m_queryCallback(_input);
+	if (!queryResult.success)
+		BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
+	return queryResult.responseOrErrorMessage;
+}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 957f2ea4..b8dac366 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -17,7 +17,6 @@
 
 #pragma once
 
-#include <libsolidity/formal/SMTSolverCommunicator.h>
 #include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/Exceptions.h>
@@ -64,7 +63,10 @@ private:
 	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
 	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
 
-	SMTSolverCommunicator m_communicator;
+	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
+	std::string querySolver(std::string const& _input);
+
+	ReadCallback::Callback m_queryCallback;
 	std::vector<std::string> m_accumulatedOutput;
 };
 
diff --git a/libsolidity/formal/SMTSolverCommunicator.cpp b/libsolidity/formal/SMTSolverCommunicator.cpp
deleted file mode 100644
index a97e5fcc..00000000
--- a/libsolidity/formal/SMTSolverCommunicator.cpp
+++ /dev/null
@@ -1,75 +0,0 @@
-/*
-	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/SMTSolverCommunicator.h>
-
-#include <libdevcore/Common.h>
-
-#include <boost/filesystem/operations.hpp>
-
-#include <fstream>
-
-#include <stdio.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity::smt;
-
-#ifdef EMSCRIPTEN
-
-string SMTSolverCommunicator::communicate(string const& _input)
-{
-	auto result = m_readFileCallback("SMTLIB2Solver>> " + _input);
-	if (result.success)
-		return result.contentsOrErrorMessage;
-	else
-		return "";
-}
-
-#else
-
-#ifndef _WIN32
-inline FILE* _popen(char const* command, char const* type)
-{
-	return popen(command, type);
-}
-inline int _pclose(FILE* file)
-{
-	return pclose(file);
-}
-#endif
-
-string SMTSolverCommunicator::communicate(string const& _input)
-{
-	namespace fs = boost::filesystem;
-	auto tempPath = fs::unique_path(fs::temp_directory_path() / "%%%%-%%%%-%%%%.smt2");
-	ScopeGuard s1([&]() { fs::remove(tempPath); });
-	ofstream(tempPath.string()) << _input << "(exit)" << endl;
-
-	// TODO Escaping might not be 100% perfect.
-	FILE* solverOutput = _popen(("z3 -smt2 \"" + tempPath.string() + "\"").c_str(), "r");
-	ScopeGuard s2([&]() { _pclose(solverOutput); });
-
-	string result;
-	array<char, 128> buffer;
-	while (!feof(solverOutput))
-		if (fgets(buffer.data(), 127, solverOutput) != nullptr)
-			result += buffer.data();
-	return result;
-}
-
-#endif
diff --git a/libsolidity/formal/SMTSolverCommunicator.h b/libsolidity/formal/SMTSolverCommunicator.h
deleted file mode 100644
index 25aeba61..00000000
--- a/libsolidity/formal/SMTSolverCommunicator.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*
-	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/interface/ReadFile.h>
-
-#include <string>
-
-namespace dev
-{
-namespace solidity
-{
-namespace smt
-{
-
-/// Platform-specific way to access the SMT solver.
-class SMTSolverCommunicator
-{
-public:
-	/// Creates the communicator, the read file callback is used only
-	/// on the emscripten platform.
-	SMTSolverCommunicator(ReadFile::Callback const& _readFileCallback):
-		m_readFileCallback(_readFileCallback)
-	{}
-
-	std::string communicate(std::string const& _input);
-
-private:
-	ReadFile::Callback m_readFileCallback;
-};
-
-
-}
-}
-}
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index e9fa5cc7..2c00d030 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -17,12 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/SMTSolverCommunicator.h>
-
 #include <libsolidity/interface/Exceptions.h>
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libdevcore/Common.h>
+#include <libdevcore/Exceptions.h>
 
 #include <boost/noncopyable.hpp>
 
@@ -132,6 +131,8 @@ private:
 		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
 };
 
+DEV_SIMPLE_EXCEPTION(SolverError);
+
 class SolverInterface
 {
 public:
@@ -158,6 +159,8 @@ public:
 
 	virtual void addAssertion(Expression const& _expr) = 0;
 
+	/// Checks for satisfiability, evaluates the expressions if a model
+	/// is available. Throws SMTSolverError on error.
 	virtual std::pair<CheckResult, std::vector<std::string>>
 	check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
 };