Insert abstraction layer.

libsolidity/formal/SMTChecker.cpp

@@ -17,6 +17,7 @@
 
 #include <libsolidity/formal/SMTChecker.h>
 
+#include <libsolidity/formal/SMTLib2Interface.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
 
@@ -25,7 +26,7 @@ using namespace dev;
 using namespace dev::solidity;
 
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback):
-	m_interface(_readFileCallback),
+	m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
 	m_errorReporter(_errorReporter)
 {
 }
@@ -39,7 +40,7 @@ void SMTChecker::analyze(SourceUnit const& _source)
 				pragmaFound = true;
 	if (pragmaFound)
 	{
-		m_interface.reset();
+		m_interface->reset();
 		m_currentSequenceCounter.clear();
 		_source.accept(*this);
 	}
@@ -69,7 +70,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		);
 	// TODO actually we probably also have to reset all local variables and similar things.
 	m_currentFunction = &_function;
-	m_interface.push();
+	m_interface->push();
 	return true;
 }
 
@@ -79,7 +80,7 @@ void SMTChecker::endVisit(FunctionDefinition const&)
 	// We only handle local variables, so we clear everything.
 	// If we add storage variables, those should be cleared differently.
 	m_currentSequenceCounter.clear();
-	m_interface.pop();
+	m_interface->pop();
 	m_currentFunction = nullptr;
 }
 
@@ -93,7 +94,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 	else if (knownVariable(*_varDecl.declarations()[0]) && _varDecl.initialValue())
 		// TODO more checks?
 		// TODO add restrictions about type (might be assignment from smaller type)
-		m_interface.addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
+		m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
 	else
 		m_errorReporter.warning(
 			_varDecl.location(),
@@ -123,7 +124,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		if (knownVariable(*decl))
 			// TODO more checks?
 			// TODO add restrictions about type (might be assignment from smaller type)
-			m_interface.addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
+			m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
 		else
 			m_errorReporter.warning(
 				_assignment.location(),
@@ -145,7 +146,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 			"Assertion checker does not yet implement tules and inline arrays."
 		);
 	else
-		m_interface.addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
+		m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
 }
 
 void SMTChecker::endVisit(BinaryOperation const& _op)
@@ -173,13 +174,13 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		solAssert(args.size() == 1, "");
 		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
 		checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
-		m_interface.addAssertion(expr(*args[0]));
+		m_interface->addAssertion(expr(*args[0]));
 	}
 	else if (funType.kind() == FunctionType::Kind::Require)
 	{
 		solAssert(args.size() == 1, "");
 		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
-		m_interface.addAssertion(expr(*args[0]));
+		m_interface->addAssertion(expr(*args[0]));
 		checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code");
 		// TODO is there something meaningful we can check here?
 		// We can check whether the condition is always fulfilled or never fulfilled.
@@ -192,7 +193,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	solAssert(decl, "");
 	if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
 	{
-		m_interface.addAssertion(expr(_identifier) == currentValue(*decl));
+		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
 		return;
 	}
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
@@ -217,7 +218,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 		if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
 			solAssert(!rational->isFractional(), "");
 
-		m_interface.addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
+		m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
 	}
 	else
 		m_errorReporter.warning(
@@ -264,7 +265,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 			&value
 		);
 
-		m_interface.addAssertion(expr(_op) == value);
+		m_interface->addAssertion(expr(_op) == value);
 		break;
 	}
 	default:
@@ -292,7 +293,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
 			/*op == Token::GreaterThanOrEqual*/ (left >= right)
 		);
 		// TODO: check that other values for op are not possible.
-		m_interface.addAssertion(expr(_op) == value);
+		m_interface->addAssertion(expr(_op) == value);
 	}
 	else
 		m_errorReporter.warning(
@@ -308,9 +309,9 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 	if (_op.annotation().commonType->category() == Type::Category::Bool)
 	{
 		if (_op.getOperator() == Token::And)
-			m_interface.addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
+			m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		else
-			m_interface.addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
+			m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
 	}
 	else
 		m_errorReporter.warning(
@@ -327,8 +328,8 @@ void SMTChecker::checkCondition(
 	smt::Expression* _additionalValue
 )
 {
-	m_interface.push();
+	m_interface->push();
-	m_interface.addAssertion(_condition);
+	m_interface->addAssertion(_condition);
 
 	vector<smt::Expression> expressionsToEvaluate;
 	if (m_currentFunction)
@@ -344,7 +345,7 @@ void SMTChecker::checkCondition(
 	}
 	smt::CheckResult result;
 	vector<string> values;
-	tie(result, values) = m_interface.check(expressionsToEvaluate);
+	tie(result, values) = m_interface->check(expressionsToEvaluate);
 	switch (result)
 	{
 	case smt::CheckResult::SAT:
@@ -380,7 +381,7 @@ void SMTChecker::checkCondition(
 	default:
 		solAssert(false, "");
 	}
-	m_interface.pop();
+	m_interface->pop();
 }
 
 void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
@@ -390,13 +391,13 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
 		solAssert(m_z3Variables.count(&_varDecl) == 0, "");
 		m_currentSequenceCounter[&_varDecl] = 0;
-		m_z3Variables.emplace(&_varDecl, m_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		m_z3Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
 		if (_setToZero)
-			m_interface.addAssertion(currentValue(_varDecl) == 0);
+			m_interface->addAssertion(currentValue(_varDecl) == 0);
 		else
 		{
-			m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType));
+			m_interface->addAssertion(currentValue(_varDecl) >= minValue(*intType));
-			m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType));
+			m_interface->addAssertion(currentValue(_varDecl) <= maxValue(*intType));
 		}
 	}
 	else
@@ -455,14 +456,14 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 		{
 			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
 				solAssert(!rational->isFractional(), "");
-			m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
+			m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		}
 		case Type::Category::Integer:
-			m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
+			m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		case Type::Category::Bool:
-			m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e)));
+			m_z3Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
 			break;
 		default:
 			solAssert(false, "Type not implemented.");

libsolidity/formal/SMTChecker.h

@@ -18,7 +18,7 @@
 #pragma once
 
 #include <libsolidity/ast/ASTVisitor.h>
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
@@ -85,7 +85,7 @@ private:
 	/// The function takes one argument which is the "sequence number".
 	smt::Expression var(Declaration const& _decl);
 
-	smt::SMTLib2Interface m_interface;
+	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_z3Expressions;
 	std::map<Declaration const*, smt::Expression> m_z3Variables;

libsolidity/formal/SMTLib2Interface.cpp

@@ -71,24 +71,24 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
 		(_codomain == Sort::Int ? "Int" : "Bool") +
 		")"
 	);
-	return Expression(std::move(_name), {});
+	return SolverInterface::newFunction(move(_name), _domain, _codomain);
 }
 
 Expression SMTLib2Interface::newInteger(string _name)
 {
 	write("(declare-const |" + _name + "| Int)");
-	return Expression(std::move(_name), {});
+	return SolverInterface::newInteger(move(_name));
 }
 
 Expression SMTLib2Interface::newBool(string _name)
 {
 	write("(declare-const |" + _name + "| Bool)");
-	return Expression(std::move(_name), {});
+	return SolverInterface::newBool(std::move(_name));
 }
 
 void SMTLib2Interface::addAssertion(Expression const& _expr)
 {
-	write("(assert " + _expr.toSExpr() + ")");
+	write("(assert " + toSExpr(_expr) + ")");
 }
 
 pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
@@ -114,6 +114,17 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 	return make_pair(result, values);
 }
 
+string SMTLib2Interface::toSExpr(Expression const& _expr)
+{
+	if (_expr.arguments.empty())
+		return _expr.name;
+	std::string sexpr = "(" + _expr.name;
+	for (auto const& arg: _expr.arguments)
+		sexpr += " " + toSExpr(arg);
+	sexpr += ")";
+	return sexpr;
+}
+
 void SMTLib2Interface::write(string _data)
 {
 	solAssert(!m_accumulatedOutput.empty(), "");
@@ -133,7 +144,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 			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 += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
 		command += "(check-sat)\n";
 		command += "(get-value (";

libsolidity/formal/SMTLib2Interface.h

@@ -18,6 +18,7 @@
 #pragma once
 
 #include <libsolidity/formal/SMTSolverCommunicator.h>
+#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/Exceptions.h>
 #include <libsolidity/interface/ReadFile.h>
@@ -38,129 +39,26 @@ namespace solidity
 namespace smt
 {
 
-enum class CheckResult
+class SMTLib2Interface: public SolverInterface, public boost::noncopyable
-{
-	SAT, UNSAT, UNKNOWN, ERROR
-};
-
-enum class Sort
-{
-	Int, Bool
-};
-
-/// C++ representation of an SMTLIB2 expression.
-class Expression
-{
-	friend class SMTLib2Interface;
-	/// Manual constructor, should only be used by SMTLib2Interface and the class itself.
-	Expression(std::string _name, std::vector<Expression> _arguments):
-		m_name(std::move(_name)), m_arguments(std::move(_arguments)) {}
-
-public:
-	Expression(size_t _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;
-	Expression& operator=(Expression const& _other) = default;
-	Expression& operator=(Expression&& _other) = default;
-
-	friend Expression operator!(Expression _a)
-	{
-		return Expression("not", std::move(_a));
-	}
-	friend Expression operator&&(Expression _a, Expression _b)
-	{
-		return Expression("and", std::move(_a), std::move(_b));
-	}
-	friend Expression operator||(Expression _a, Expression _b)
-	{
-		return Expression("or", std::move(_a), std::move(_b));
-	}
-	friend Expression operator==(Expression _a, Expression _b)
-	{
-		return Expression("=", std::move(_a), std::move(_b));
-	}
-	friend Expression operator!=(Expression _a, Expression _b)
-	{
-		return !(std::move(_a) == std::move(_b));
-	}
-	friend Expression operator<(Expression _a, Expression _b)
-	{
-		return Expression("<", std::move(_a), std::move(_b));
-	}
-	friend Expression operator<=(Expression _a, Expression _b)
-	{
-		return Expression("<=", std::move(_a), std::move(_b));
-	}
-	friend Expression operator>(Expression _a, Expression _b)
-	{
-		return Expression(">", std::move(_a), std::move(_b));
-	}
-	friend Expression operator>=(Expression _a, Expression _b)
-	{
-		return Expression(">=", std::move(_a), std::move(_b));
-	}
-	friend Expression operator+(Expression _a, Expression _b)
-	{
-		return Expression("+", std::move(_a), std::move(_b));
-	}
-	friend Expression operator-(Expression _a, Expression _b)
-	{
-		return Expression("-", std::move(_a), std::move(_b));
-	}
-	friend Expression operator*(Expression _a, Expression _b)
-	{
-		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();
-		sexpr += ")";
-		return sexpr;
-	}
-
-private:
-	explicit Expression(std::string _name):
-		Expression(std::move(_name), std::vector<Expression>{}) {}
-	Expression(std::string _name, Expression _arg):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
-	Expression(std::string _name, Expression _arg1, Expression _arg2):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
-
-	std::string const m_name;
-	std::vector<Expression> const m_arguments;
-};
-
-class SMTLib2Interface: public boost::noncopyable
 {
 public:
 	SMTLib2Interface(ReadFile::Callback const& _readFileCallback);
 
-	void reset();
+	void reset() override;
 
-	void push();
+	void push() override;
-	void pop();
+	void pop() override;
 
-	Expression newFunction(std::string _name, Sort _domain, Sort _codomain);
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
-	Expression newInteger(std::string _name);
+	Expression newInteger(std::string _name) override;
-	Expression newBool(std::string _name);
+	Expression newBool(std::string _name) override;
 
-	void addAssertion(Expression const& _expr);
+	void addAssertion(Expression const& _expr) override;
-	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate);
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 private:
+	std::string toSExpr(Expression const& _expr);
+
 	void write(std::string _data);
 
 	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
@@ -170,7 +68,6 @@ private:
 	std::vector<std::string> m_accumulatedOutput;
 };
 
-
 }
 }
 }

libsolidity/formal/SolverInterface.h

@@ -0,0 +1,168 @@
+/*
+	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/SMTSolverCommunicator.h>
+
+#include <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <libdevcore/Common.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <map>
+#include <string>
+#include <vector>
+#include <cstdio>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+enum class CheckResult
+{
+	SAT, UNSAT, UNKNOWN, ERROR
+};
+
+enum class Sort
+{
+	Int, Bool
+};
+
+/// C++ representation of an SMTLIB2 expression.
+class Expression
+{
+	friend class SolverInterface;
+public:
+	Expression(size_t _number): name(std::to_string(_number)) {}
+	Expression(u256 const& _number): name(_number.str()) {}
+	Expression(bigint const& _number): name(_number.str()) {}
+
+	Expression(Expression const& _other) = default;
+	Expression(Expression&& _other) = default;
+	Expression& operator=(Expression const& _other) = default;
+	Expression& operator=(Expression&& _other) = default;
+
+	friend Expression operator!(Expression _a)
+	{
+		return Expression("not", std::move(_a));
+	}
+	friend Expression operator&&(Expression _a, Expression _b)
+	{
+		return Expression("and", std::move(_a), std::move(_b));
+	}
+	friend Expression operator||(Expression _a, Expression _b)
+	{
+		return Expression("or", std::move(_a), std::move(_b));
+	}
+	friend Expression operator==(Expression _a, Expression _b)
+	{
+		return Expression("=", std::move(_a), std::move(_b));
+	}
+	friend Expression operator!=(Expression _a, Expression _b)
+	{
+		return !(std::move(_a) == std::move(_b));
+	}
+	friend Expression operator<(Expression _a, Expression _b)
+	{
+		return Expression("<", std::move(_a), std::move(_b));
+	}
+	friend Expression operator<=(Expression _a, Expression _b)
+	{
+		return Expression("<=", std::move(_a), std::move(_b));
+	}
+	friend Expression operator>(Expression _a, Expression _b)
+	{
+		return Expression(">", std::move(_a), std::move(_b));
+	}
+	friend Expression operator>=(Expression _a, Expression _b)
+	{
+		return Expression(">=", std::move(_a), std::move(_b));
+	}
+	friend Expression operator+(Expression _a, Expression _b)
+	{
+		return Expression("+", std::move(_a), std::move(_b));
+	}
+	friend Expression operator-(Expression _a, Expression _b)
+	{
+		return Expression("-", std::move(_a), std::move(_b));
+	}
+	friend Expression operator*(Expression _a, Expression _b)
+	{
+		return Expression("*", std::move(_a), std::move(_b));
+	}
+	Expression operator()(Expression _a) const
+	{
+		solAssert(arguments.empty(), "Attempted function application to non-function.");
+		return Expression(name, _a);
+	}
+
+	std::string const name;
+	std::vector<Expression> const arguments;
+
+private:
+	/// Manual constructor, should only be used by SolverInterface and this class itself.
+	Expression(std::string _name, std::vector<Expression> _arguments):
+		name(std::move(_name)), arguments(std::move(_arguments)) {}
+
+	explicit Expression(std::string _name):
+		Expression(std::move(_name), std::vector<Expression>{}) {}
+	Expression(std::string _name, Expression _arg):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
+	Expression(std::string _name, Expression _arg1, Expression _arg2):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
+};
+
+class SolverInterface
+{
+public:
+	virtual void reset() = 0;
+
+	virtual void push() = 0;
+	virtual void pop() = 0;
+
+	virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
+	{
+		// Subclasses should do something here
+		return Expression(std::move(_name), {});
+	}
+	virtual Expression newInteger(std::string _name)
+	{
+		// Subclasses should do something here
+		return Expression(std::move(_name), {});
+	}
+	virtual Expression newBool(std::string _name)
+	{
+		// Subclasses should do something here
+		return Expression(std::move(_name), {});
+	}
+
+	virtual void addAssertion(Expression const& _expr) = 0;
+
+	virtual std::pair<CheckResult, std::vector<std::string>>
+	check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
+};
+
+
+}
+}
+}