diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index af7f47b60..796eb546d 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -1,6 +1,8 @@ set(sources CHCSmtLib2Interface.cpp CHCSmtLib2Interface.h + DLSolver.cpp + DLSolver.h Exceptions.h SMTLib2Interface.cpp SMTLib2Interface.h diff --git a/libsmtutil/DLSolver.cpp b/libsmtutil/DLSolver.cpp new file mode 100644 index 000000000..94befed68 --- /dev/null +++ b/libsmtutil/DLSolver.cpp @@ -0,0 +1,170 @@ +/* + 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 + +using namespace std; +using namespace solidity::smtutil; +using namespace solidity::util; + +DLSolver::DLSolver(std::optional _queryTimeout): + SolverInterface(_queryTimeout) +{ + reset(); +} + +void DLSolver::reset() +{ + m_graphs.clear(); + initGraphs(); +} + +void DLSolver::push() +{ + m_graphs.push_back(m_graphs.back()); +} + +void DLSolver::pop() +{ + smtAssert(!m_graphs.empty()); + m_graphs.pop_back(); + if (m_graphs.empty()) + initGraphs(); +} + +void DLSolver::declareVariable(string const& _name, SortPointer const& _sort) +{ + smtAssert(_sort, ""); + smtAssert(_sort->kind == Kind::Int); + + if (m_variables.count(_name)) + return; + + m_variables[_name] = uniqueId(); +} + +void DLSolver::addAssertion(Expression const& _expr) +{ + smtAssert(_expr.sort->kind == Kind::Bool); + smtAssert(_expr.name == "<="); + smtAssert(_expr.arguments.size() == 2); + + Expression const& lhs = _expr.arguments.at(0); + Expression const& rhs = _expr.arguments.at(1); + + smtAssert(lhs.sort->kind == Kind::Int); + smtAssert(lhs.name == "-"); + smtAssert(lhs.arguments.size() == 2); + + Expression const& a = lhs.arguments.at(0); + Expression const& b = lhs.arguments.at(1); + + smtAssert(a.sort->kind == Kind::Int); + smtAssert(a.arguments.empty()); + smtAssert(m_variables.count(a.name)); + + smtAssert(b.sort->kind == Kind::Int); + smtAssert(b.arguments.empty()); + smtAssert(m_variables.count(b.name)); + + smtAssert(rhs.sort->kind == Kind::Int); + smtAssert(rhs.arguments.empty()); + + bigint constK; + try + { + constK = bigint(rhs.name); + } + catch (...) + { + smtAssert(false); + } + + unsigned nodeA = m_variables.at(a.name); + unsigned nodeB = m_variables.at(b.name); + + std::map>& graph = m_graphs.back(); + + if (graph.count(nodeA) && graph.at(nodeA).count(nodeB)) + { + bigint oldK = graph.at(nodeA).at(nodeB); + if (oldK <= constK) + return; + } + + graph[nodeA][nodeB] = constK; +} + +pair> DLSolver::check(vector const& _expressionsToEvaluate) +{ + vector values; + + CheckResult result = solve(); + + if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) + { + // TODO model stuff + } + + return make_pair(result, values); +} + +CheckResult DLSolver::solve() +{ + smtAssert(!m_graphs.empty()); + std::map> const& graph = m_graphs.back(); + unsigned const nNodes = m_lastId; + + // ==== Bellman-Ford negative cycle detection ==== + + // 1. Single source shortest path + + //vector dist(nNodes, 0); + vector dist(nNodes, bigint(1) << 256); + + for (unsigned i = 0; i < nNodes; ++i) + for (auto const& [a, edges]: graph) + for (auto const& [b, k]: edges) + dist[b] = min(dist[b], dist[a] + k); + + // 2. Negative cycle detection + + bool neg = false; + for (auto const& [a, edges]: graph) + for (auto const& [b, k]: edges) + if (dist[b] > dist[a] + k) { + neg = true; + break; + } + + return neg ? CheckResult::UNSATISFIABLE : CheckResult::SATISFIABLE; +} + +void DLSolver::initGraphs() +{ + smtAssert(m_graphs.empty()); + m_graphs.push_back({ {} }); +} + +unsigned DLSolver::uniqueId() +{ + return m_lastId++; +} diff --git a/libsmtutil/DLSolver.h b/libsmtutil/DLSolver.h new file mode 100644 index 000000000..8e2163558 --- /dev/null +++ b/libsmtutil/DLSolver.h @@ -0,0 +1,61 @@ +/* + 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 + +namespace solidity::smtutil +{ + +class DLSolver: public SolverInterface +{ +public: + /// Noncopyable. + DLSolver(DLSolver const&) = delete; + DLSolver& operator=(DLSolver const&) = delete; + + DLSolver(std::optional _queryTimeout = {}); + + void reset() override; + + void push() override; + void pop() override; + + void declareVariable(std::string const& _name, SortPointer const& _sort) override; + + void addAssertion(Expression const& _expr) override; + std::pair> check(std::vector const& _expressionsToEvaluate) override; + +private: + CheckResult solve(); + void initGraphs(); + unsigned uniqueId(); + + // Stack of DL graphs and unique ids, + // used for incremental solving. + std::vector< + std::map> + > m_graphs; + + std::map m_variables; + + unsigned m_lastId = 0; +}; + +} diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 255218c15..164252214 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -62,6 +62,11 @@ set(liblangutil_sources ) detect_stray_source_files("${liblangutil_sources}" "liblangutil/") +set(libsmtutil_sources + libsmtutil/DLSolver.cpp +) +detect_stray_source_files("${libsmtutil_sources}" "libsmtutil/") + set(libsolidity_sources libsolidity/ABIDecoderTests.cpp libsolidity/ABIEncoderTests.cpp @@ -194,6 +199,7 @@ add_executable(soltest ${sources} ${contracts_sources} ${libsolutil_sources} ${liblangutil_sources} + ${libsmtutil_sources} ${libevmasm_sources} ${libyul_sources} ${libsolidity_sources} diff --git a/test/libsmtutil/DLSolver.cpp b/test/libsmtutil/DLSolver.cpp new file mode 100644 index 000000000..620a51066 --- /dev/null +++ b/test/libsmtutil/DLSolver.cpp @@ -0,0 +1,295 @@ +/* + 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 . +*/ + +#include + +#include + +using namespace std; +using namespace solidity::smtutil; + +namespace solidity::smtutil::test +{ + +BOOST_AUTO_TEST_SUITE(DLSolverTest) + +BOOST_AUTO_TEST_CASE(test_empty_sat) +{ + DLSolver solver; + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::SATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_basic_sat) +{ + DLSolver solver; + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + + Expression k2{"2", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + + solver.addAssertion(a - b <= k2); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::SATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_sat) +{ + DLSolver solver; + + // a <= b -> a - b <= 0 + // b <= c -> b - c <= 0 + // c <= a -> c - a <= 0 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k0{"0", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k0); + solver.addAssertion(b - c <= k0); + solver.addAssertion(c - a <= k0); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::SATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_basic_unsat) +{ + DLSolver solver; + + // a <= b -> a - b <= 0 + // b < a -> b - a < 0 -> b - a <= -1 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + + Expression k0{"0", {}, SortProvider::sintSort}; + Expression kMinus1{"-1", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + + solver.addAssertion(a - b <= k0); + solver.addAssertion(b - a <= kMinus1); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::UNSATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_unsat) +{ + DLSolver solver; + + // a <= b -> a - b <= 0 + // b <= c -> b - c <= 0 + // c < a -> c - a < 0 -> c - a <= -1 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k0{"0", {}, SortProvider::sintSort}; + Expression kMinus1{"-1", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k0); + solver.addAssertion(b - c <= k0); + solver.addAssertion(c - a <= kMinus1); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::UNSATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_unsat_reset_sat) +{ + DLSolver solver; + + // a <= b -> a - b <= 0 + // b <= c -> b - c <= 0 + // c < a -> c - a < 0 -> c - a <= -1 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k0{"0", {}, SortProvider::sintSort}; + Expression kMinus1{"-1", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k0); + solver.addAssertion(b - c <= k0); + solver.addAssertion(c - a <= kMinus1); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::UNSATISFIABLE); + + solver.reset(); + + auto [res2, model2] = solver.check({}); + BOOST_CHECK(res2 == CheckResult::SATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_incremental) +{ + DLSolver solver; + + // a <= b -> a - b <= 0 + // b <= c -> b - c <= 0 + // c < a -> c - a < 0 -> c - a <= -1 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k0{"0", {}, SortProvider::sintSort}; + Expression kMinus1{"-1", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k0); + solver.addAssertion(b - c <= k0); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::SATISFIABLE); + + solver.push(); + + solver.addAssertion(c - a <= kMinus1); + + auto [res2, model2] = solver.check({}); + BOOST_CHECK(res2 == CheckResult::UNSATISFIABLE); + + solver.pop(); + + auto [res3, model3] = solver.check({}); + BOOST_CHECK(res3 == CheckResult::SATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_complex) +{ + DLSolver solver; + + // a−b ≤ 2, b−c ≤ 3, c−a ≤ −7 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k2{"2", {}, SortProvider::sintSort}; + Expression k3{"3", {}, SortProvider::sintSort}; + Expression kMinus7{"-7", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k2); + solver.addAssertion(b - c <= k3); + solver.addAssertion(c - a <= kMinus7); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::UNSATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_complex2) +{ + DLSolver solver; + + // a−b ≤ 2, b−c ≤ 10, c−a ≤ −7 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k2{"2", {}, SortProvider::sintSort}; + Expression k10{"10", {}, SortProvider::sintSort}; + Expression kMinus7{"-7", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k2); + solver.addAssertion(b - c <= k10); + solver.addAssertion(c - a <= kMinus7); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::SATISFIABLE); +} + +BOOST_AUTO_TEST_CASE(test_triangle_complex2_incremental) +{ + DLSolver solver; + + // a−b ≤ 2, b−c ≤ 10, c−a ≤ −7 + + Expression a{"a", {}, SortProvider::sintSort}; + Expression b{"b", {}, SortProvider::sintSort}; + Expression c{"c", {}, SortProvider::sintSort}; + + Expression k2{"2", {}, SortProvider::sintSort}; + Expression k3{"3", {}, SortProvider::sintSort}; + Expression k10{"10", {}, SortProvider::sintSort}; + Expression kMinus7{"-7", {}, SortProvider::sintSort}; + + solver.declareVariable(a.name, a.sort); + solver.declareVariable(b.name, b.sort); + solver.declareVariable(c.name, c.sort); + + solver.addAssertion(a - b <= k2); + solver.addAssertion(c - a <= kMinus7); + + auto [res, model] = solver.check({}); + BOOST_CHECK(res == CheckResult::SATISFIABLE); + + solver.push(); + solver.addAssertion(b - c <= k3); + + auto [res2, model2] = solver.check({}); + BOOST_CHECK(res2 == CheckResult::UNSATISFIABLE); + + solver.pop(); + + solver.addAssertion(b - c <= k10); + auto [res3, model3] = solver.check({}); + BOOST_CHECK(res3 == CheckResult::SATISFIABLE); +} + + +BOOST_AUTO_TEST_SUITE_END() + +} // end namespaces