Refactor SMTLib parser to separate file

libsmtutil/CHCSmtLib2Interface.cpp

@@ -18,6 +18,8 @@
 
 #include <libsmtutil/CHCSmtLib2Interface.h>
 
+#include <libsmtutil/SMTLibParser.h>
+
 #include <libsolutil/Keccak256.h>
 #include <libsolutil/StringUtils.h>
 #include <libsolutil/Visitor.h>
@@ -251,22 +253,8 @@ std::string CHCSmtLib2Interface::createQueryAssertion(std::string name) {
 	return "(assert\n(forall " + forall() + "\n" +	"(=> " + name + " false)))";
 }
 
-std::string CHCSmtLib2Interface::SMTLib2Expression::toString() const
-{
-	return std::visit(GenericVisitor{
-			[](std::string const& _sv) { return _sv; },
-			[](std::vector<SMTLib2Expression> const& _subExpr) {
-				std::vector<std::string> formatted;
-				for (auto const& item: _subExpr)
-					formatted.emplace_back(item.toString());
-				return "(" + joinHumanReadable(formatted, " ") + ")";
-			}
-	}, data);
-}
-
 namespace
 {
-	using SMTLib2Expression = CHCSmtLib2Interface::SMTLib2Expression;
 	bool isNumber(std::string const& _expr)
 	{
 		for (char c: _expr)
@@ -275,114 +263,6 @@ namespace
 		return true;
 	}
 
-	bool isAtom(SMTLib2Expression const & expr)
-	{
-		return std::holds_alternative<std::string>(expr.data);
-	}
-
-	std::string const& asAtom(SMTLib2Expression const& expr)
-	{
-		solAssert(isAtom(expr));
-		return std::get<std::string>(expr.data);
-	}
-
-	auto const& asSubExpressions(SMTLib2Expression const& expr)
-	{
-		solAssert(!isAtom(expr));
-		return std::get<SMTLib2Expression::args_t>(expr.data);
-	}
-
-	auto& asSubExpressions(SMTLib2Expression& expr)
-	{
-		solAssert(!isAtom(expr));
-		return std::get<SMTLib2Expression::args_t>(expr.data);
-	}
-
-	class SMTLib2Parser
-	{
-	public:
-		SMTLib2Parser(std::istream& _input):
-				m_input(_input),
-				m_token(static_cast<char>(m_input.get()))
-		{}
-
-		SMTLib2Expression parseExpression()
-		{
-			skipWhitespace();
-			if (token() == '(')
-			{
-				advance();
-				skipWhitespace();
-				std::vector<SMTLib2Expression> subExpressions;
-				while (token() != 0 && token() != ')')
-				{
-					subExpressions.emplace_back(parseExpression());
-					skipWhitespace();
-				}
-				solAssert(token() == ')');
-				// simulate whitespace because we do not want to read the next token
-				// since it might block.
-				m_token = ' ';
-				return {std::move(subExpressions)};
-			}
-			else
-				return {parseToken()};
-		}
-
-		bool isEOF()
-		{
-			skipWhitespace();
-			return m_input.eof();
-		}
-
-	private:
-		std::string parseToken()
-		{
-			std::string result;
-
-			skipWhitespace();
-			bool isPipe = token() == '|';
-			if (isPipe)
-				advance();
-			while (token() != 0)
-			{
-				char c = token();
-				if (isPipe && c == '|')
-				{
-					advance();
-					break;
-				}
-				else if (!isPipe && (isWhiteSpace(c) || c == '(' || c == ')'))
-					break;
-				result.push_back(c);
-				advance();
-			}
-			return result;
-		}
-
-		void skipWhitespace()
-		{
-			while (isWhiteSpace(token()))
-				advance();
-		}
-
-		char token() const
-		{
-			return m_token;
-		}
-
-		void advance()
-		{
-			m_token = static_cast<char>(m_input.get());
-			if (token() == ';')
-				while (token() != '\n' && token() != 0)
-					m_token = static_cast<char>(m_input.get());
-		}
-
-		std::istream& m_input;
-		char m_token = 0;
-	};
-
 	class SMTLibTranslationContext
 	{
 		SMTLib2Interface const& m_smtlib2Interface;

libsmtutil/CHCSmtLib2Interface.h

@@ -32,13 +32,6 @@ namespace solidity::smtutil
 class CHCSmtLib2Interface: public CHCSolverInterface
 {
 public:
-	struct SMTLib2Expression
-	{
-		using args_t = std::vector<SMTLib2Expression>;
-		std::variant<std::string, args_t> data;
-
-		std::string toString() const;
-	};
 
 	explicit CHCSmtLib2Interface(
 		std::map<util::h256, std::string> const& _queryResponses = {},

libsmtutil/CMakeLists.txt

@@ -4,6 +4,8 @@ set(sources
 	Exceptions.h
 	SMTLib2Interface.cpp
 	SMTLib2Interface.h
+	SMTLibParser.cpp
+	SMTLibParser.h
 	SolverInterface.h
 	Sorts.cpp
 	Sorts.h

libsmtutil/SMTLibParser.cpp

@@ -0,0 +1,77 @@
+#include <libsmtutil/SMTLibParser.h>
+
+#include <liblangutil/Common.h>
+
+#include <libsolutil/Visitor.h>
+#include <libsolutil/StringUtils.h>
+
+
+using namespace solidity::langutil;
+using namespace solidity::smtutil;
+
+std::string SMTLib2Expression::toString() const {
+	return std::visit(solidity::util::GenericVisitor{
+			[](std::string const& _sv) { return _sv; },
+			[](std::vector<SMTLib2Expression> const& _subExpr) {
+				std::vector<std::string> formatted;
+				for (auto const& item: _subExpr)
+					formatted.emplace_back(item.toString());
+				return "(" + solidity::util::joinHumanReadable(formatted, " ") + ")";
+			}
+	}, data);
+}
+
+SMTLib2Expression SMTLib2Parser::parseExpression() {
+	skipWhitespace();
+	if (token() == '(')
+	{
+		advance();
+		skipWhitespace();
+		std::vector<SMTLib2Expression> subExpressions;
+		while (token() != 0 && token() != ')')
+		{
+			subExpressions.emplace_back(parseExpression());
+			skipWhitespace();
+		}
+		solAssert(token() == ')');
+		// simulate whitespace because we do not want to read the next token
+		// since it might block.
+		m_token = ' ';
+		return {std::move(subExpressions)};
+	} else
+		return {parseToken()};
+}
+
+std::string SMTLib2Parser::parseToken() {
+	std::string result;
+
+	skipWhitespace();
+	bool isPipe = token() == '|';
+	if (isPipe)
+		advance();
+	while (token() != 0)
+	{
+		char c = token();
+		if (isPipe && c == '|')
+		{
+			advance();
+			break;
+		} else if (!isPipe && (isWhiteSpace(c) || c == '(' || c == ')'))
+			break;
+		result.push_back(c);
+		advance();
+	}
+	return result;
+}
+
+void SMTLib2Parser::advance() {
+	m_token = static_cast<char>(m_input.get());
+	if (token() == ';')
+		while (token() != '\n' && token() != 0)
+			m_token = static_cast<char>(m_input.get());
+}
+
+void SMTLib2Parser::skipWhitespace() {
+	while (isWhiteSpace(token()))
+		advance();
+}

libsmtutil/SMTLibParser.h

@@ -0,0 +1,88 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <liblangutil/Exceptions.h>
+
+#include <iostream>
+#include <string>
+#include <variant>
+#include <vector>
+
+namespace solidity::smtutil
+{
+
+struct SMTLib2Expression {
+	using args_t = std::vector<SMTLib2Expression>;
+	std::variant<std::string, args_t> data;
+
+	std::string toString() const;
+};
+
+inline bool isAtom(SMTLib2Expression const & expr)
+{
+	return std::holds_alternative<std::string>(expr.data);
+}
+
+inline std::string const& asAtom(SMTLib2Expression const& expr)
+{
+	solAssert(isAtom(expr));
+	return std::get<std::string>(expr.data);
+}
+
+inline auto const& asSubExpressions(SMTLib2Expression const& expr)
+{
+	solAssert(!isAtom(expr));
+	return std::get<SMTLib2Expression::args_t>(expr.data);
+}
+
+inline auto& asSubExpressions(SMTLib2Expression& expr)
+{
+	solAssert(!isAtom(expr));
+	return std::get<SMTLib2Expression::args_t>(expr.data);
+}
+
+class SMTLib2Parser {
+public:
+	SMTLib2Parser(std::istream& _input) :
+			m_input(_input),
+			m_token(static_cast<char>(m_input.get())) {}
+
+	SMTLib2Expression parseExpression();
+
+	bool isEOF() {
+		skipWhitespace();
+		return m_input.eof();
+	}
+
+private:
+	std::string parseToken();
+
+	void skipWhitespace();
+
+	char token() const {
+		return m_token;
+	}
+
+	void advance();
+
+	std::istream& m_input;
+	char m_token = 0;
+};
+}