DL Solver

libsmtutil/CMakeLists.txt

@@ -1,6 +1,8 @@
 set(sources
 	CHCSmtLib2Interface.cpp
 	CHCSmtLib2Interface.h
+	DLSolver.cpp
+	DLSolver.h
 	Exceptions.h
 	SMTLib2Interface.cpp
 	SMTLib2Interface.h

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 <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsmtutil/DLSolver.h>
+
+#include <libsolutil/CommonData.h>
+#include <libsolutil/CommonIO.h>
+
+using namespace std;
+using namespace solidity::smtutil;
+using namespace solidity::util;
+
+DLSolver::DLSolver(std::optional<unsigned> _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<unsigned, std::map<unsigned, bigint>>& 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<CheckResult, vector<string>> DLSolver::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	vector<string> 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<unsigned, std::map<unsigned, bigint>> const& graph = m_graphs.back();
+	unsigned const nNodes = m_lastId;
+
+	// ==== Bellman-Ford negative cycle detection ====
+
+	// 1. Single source shortest path
+
+	//vector<bigint> dist(nNodes, 0);
+	vector<bigint> 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++;
+}

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 <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsmtutil/SolverInterface.h>
+
+namespace solidity::smtutil
+{
+
+class DLSolver: public SolverInterface
+{
+public:
+	/// Noncopyable.
+	DLSolver(DLSolver const&) = delete;
+	DLSolver& operator=(DLSolver const&) = delete;
+
+	DLSolver(std::optional<unsigned> _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<CheckResult, std::vector<std::string>> check(std::vector<Expression> 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<unsigned, std::map<unsigned, bigint>>
+	> m_graphs;
+
+	std::map<std::string, unsigned> m_variables;
+
+	unsigned m_lastId = 0;
+};
+
+}

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}

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 <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsmtutil/DLSolver.h>
+
+#include <boost/test/unit_test.hpp>
+
+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