From af1acaba640593a8b065e2ad2bd78f09adbd981a Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Fri, 11 Aug 2023 17:59:52 +0200 Subject: [PATCH] Refactor SMTLib parser to separate file --- libsmtutil/CHCSmtLib2Interface.cpp | 124 +---------------------------- libsmtutil/CHCSmtLib2Interface.h | 7 -- libsmtutil/CMakeLists.txt | 2 + libsmtutil/SMTLibParser.cpp | 77 ++++++++++++++++++ libsmtutil/SMTLibParser.h | 88 ++++++++++++++++++++ 5 files changed, 169 insertions(+), 129 deletions(-) create mode 100644 libsmtutil/SMTLibParser.cpp create mode 100644 libsmtutil/SMTLibParser.h diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 154158a1e..b84ba2750 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -18,6 +18,8 @@ #include +#include + #include #include #include @@ -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 const& _subExpr) { - std::vector 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(expr.data); - } - - std::string const& asAtom(SMTLib2Expression const& expr) - { - solAssert(isAtom(expr)); - return std::get(expr.data); - } - - auto const& asSubExpressions(SMTLib2Expression const& expr) - { - solAssert(!isAtom(expr)); - return std::get(expr.data); - } - - auto& asSubExpressions(SMTLib2Expression& expr) - { - solAssert(!isAtom(expr)); - return std::get(expr.data); - } - - class SMTLib2Parser - { - public: - SMTLib2Parser(std::istream& _input): - m_input(_input), - m_token(static_cast(m_input.get())) - {} - - SMTLib2Expression parseExpression() - { - skipWhitespace(); - if (token() == '(') - { - advance(); - skipWhitespace(); - std::vector 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(m_input.get()); - if (token() == ';') - while (token() != '\n' && token() != 0) - m_token = static_cast(m_input.get()); - } - - std::istream& m_input; - char m_token = 0; - }; - class SMTLibTranslationContext { SMTLib2Interface const& m_smtlib2Interface; diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index 99100d663..03d10ed28 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -32,13 +32,6 @@ namespace solidity::smtutil class CHCSmtLib2Interface: public CHCSolverInterface { public: - struct SMTLib2Expression - { - using args_t = std::vector; - std::variant data; - - std::string toString() const; - }; explicit CHCSmtLib2Interface( std::map const& _queryResponses = {}, diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index 120996219..a5402d59a 100644 --- a/libsmtutil/CMakeLists.txt +++ b/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 diff --git a/libsmtutil/SMTLibParser.cpp b/libsmtutil/SMTLibParser.cpp new file mode 100644 index 000000000..cfc922dc6 --- /dev/null +++ b/libsmtutil/SMTLibParser.cpp @@ -0,0 +1,77 @@ +#include + +#include + +#include +#include + + +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 const& _subExpr) { + std::vector 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 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(m_input.get()); + if (token() == ';') + while (token() != '\n' && token() != 0) + m_token = static_cast(m_input.get()); +} + +void SMTLib2Parser::skipWhitespace() { + while (isWhiteSpace(token())) + advance(); +} diff --git a/libsmtutil/SMTLibParser.h b/libsmtutil/SMTLibParser.h new file mode 100644 index 000000000..f34bb66be --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include + +#include +#include +#include +#include + +namespace solidity::smtutil +{ + +struct SMTLib2Expression { + using args_t = std::vector; + std::variant data; + + std::string toString() const; +}; + +inline bool isAtom(SMTLib2Expression const & expr) +{ + return std::holds_alternative(expr.data); +} + +inline std::string const& asAtom(SMTLib2Expression const& expr) +{ + solAssert(isAtom(expr)); + return std::get(expr.data); +} + +inline auto const& asSubExpressions(SMTLib2Expression const& expr) +{ + solAssert(!isAtom(expr)); + return std::get(expr.data); +} + +inline auto& asSubExpressions(SMTLib2Expression& expr) +{ + solAssert(!isAtom(expr)); + return std::get(expr.data); +} + +class SMTLib2Parser { +public: + SMTLib2Parser(std::istream& _input) : + m_input(_input), + m_token(static_cast(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; +}; +}