From 6bd09ba9d561221c2daf16d68f56fd15dbf339e5 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 May 2022 17:22:47 +0200 Subject: [PATCH] smt solver --- tools/CMakeLists.txt | 3 + tools/solsmt.cpp | 225 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 228 insertions(+) create mode 100644 tools/solsmt.cpp diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 83a869579..7415e0d01 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -53,3 +53,6 @@ install(TARGETS yul-phaser DESTINATION "${CMAKE_INSTALL_BINDIR}") add_executable(satsolver satsolver-main.cpp) target_link_libraries(satsolver PUBLIC solidity range-v3 Boost::boost Boost::program_options) + +add_executable(solsmt solsmt.cpp) +target_link_libraries(solsmt PRIVATE smtutil solutil range-v3 Boost::boost Boost::program_options) diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp new file mode 100644 index 000000000..7b8afd03c --- /dev/null +++ b/tools/solsmt.cpp @@ -0,0 +1,225 @@ +/* + 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 + +#include +#include +#include +#include + +#include +#include +#include +#include +#include + +using namespace std; +using namespace solidity; +using namespace solidity::util; +using namespace solidity::langutil; +using namespace solidity::smtutil; + +struct SMTLib2Expression +{ + variant> data; + + string toString() const + { + return std::visit(GenericVisitor{ + [](string_view const& _sv) { return string{_sv}; }, + [](vector const& _subExpr) { + vector formatted; + for (auto const& item: _subExpr) + formatted.emplace_back(item.toString()); + return "(" + joinHumanReadable(formatted, " ") + ")"; + } + }, data); + } +}; + +class SMTLib2Parser +{ +public: + SMTLib2Parser(string_view const& _data): m_data(_data) {} + + SMTLib2Expression parseExpression() + { + skipWhitespace(); + // TODO This does not check if there is trailing data after the closing ')' + if (token() == '(') + { + advance(); + vector subExpressions; + while (token() != 0 && token() != ')') + { + subExpressions.emplace_back(parseExpression()); + skipWhitespace(); + } + if (token() == ')') + advance(); + return {subExpressions}; + } + else + return {parseToken()}; + } + + string_view remainingInput() const + { + return m_data.substr(m_pos); + } + +private: + string_view parseToken() + { + skipWhitespace(); + size_t start = m_pos; + while (m_pos < m_data.size()) + { + char c = token(); + if (langutil::isWhiteSpace(c) || c == '(' || c == ')') + break; + advance(); + } + return m_data.substr(start, m_pos - start); + } + + void skipWhitespace() + { + while (isWhiteSpace(token())) + advance(); + } + + char token() + { + return m_pos < m_data.size() ? m_data[m_pos] : 0; + } + void advance() { m_pos++;} + + size_t m_pos = 0; + string_view const m_data; +}; + +namespace +{ + +string_view command(SMTLib2Expression const& _expr) +{ + vector const& items = get>(_expr.data); + solAssert(!items.empty()); + solAssert(holds_alternative(items.front().data)); + return get(items.front().data); +} + +// TODO If we want to return rational here, we need smtutil::Expression to support rationals... +u256 parseRational(string_view _atom) +{ + if (_atom.size() >= 3 && _atom.at(_atom.size() - 1) == '0' && _atom.at(_atom.size() - 2) == '.') + return parseRational(_atom.substr(0, _atom.size() - 2)); + else + return u256(_atom); +} + +smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr) +{ + return std::visit(GenericVisitor{ + [](string_view const& _atom) { + if (isDigit(_atom.front()) || _atom.front() == '.') + return Expression(parseRational(_atom)); + else + // TODO should be real, but internally, we use ints. + return Expression(string(_atom), {}, SortProvider::intSort()); + }, + [&](vector const& _subExpr) { + set boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"}; + vector arguments; + for (size_t i = 1; i < _subExpr.size(); i++) + arguments.emplace_back(toSMTUtilExpression(_subExpr[i])); + string_view op = get(_subExpr.front().data); + return Expression( + string(op), + move(arguments), + contains(boolOperators, op) ? + SortProvider::boolSort : + SortProvider::intSort() + ); + } + }, _expr.data); +} + +} + +int main(int argc, char** argv) +{ + if (argc != 2) + { + cout << "Usage: solsmt " << endl; + return -1; + } + + string input = readFileAsString(argv[1]); + string_view inputToParse = input; + + BooleanLPSolver solver; + while (!inputToParse.empty()) + { + //cout << line << endl; + SMTLib2Parser parser(inputToParse); + //cout << " -> " << parser.parseExpression().toString() << endl; + SMTLib2Expression expr = parser.parseExpression(); + inputToParse = parser.remainingInput(); + vector const& items = get>(expr.data); + string_view cmd = command(expr); + if (cmd == "set-info") + continue; // ignore + else if (cmd == "declare-fun") + { + solAssert(items.size() == 4); + string variableName = string{get(items[1].data)}; + solAssert(get>(items[2].data).empty()); + string_view type = get(items[3].data); + solAssert(type == "Real" || type == "Bool"); + // TODO should be real, but we call it int... + SortPointer sort = type == "Real" ? SortProvider::intSort() : SortProvider::boolSort; + solver.declareVariable(variableName, move(sort)); + } + else if (cmd == "assert") + { + solAssert(items.size() == 2); + solver.addAssertion(toSMTUtilExpression(items[1])); + } + else if (cmd == "set-logic") + { + // ignore - could check the actual logic. + } + else if (cmd == "check-sat") + { + auto&& [result, model] = solver.check({}); + if (result == CheckResult::SATISFIABLE) + cout << "(sat)" << endl; + else if (result == CheckResult::UNSATISFIABLE) + cout << "(unsat)" << endl; + else + cout << "(unknown)" << endl; + } + else if (cmd == "exit") + return 0; + else + solAssert(false, "Unknown instruction: " + string(cmd)); + } + + return 0; +}