Add opensmt2 interface

CMakeLists.txt

@@ -100,6 +100,12 @@ if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
   \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
 endif()
 
+find_package(OSMT2 QUIET)
+if (${OSMT2_FOUND})
+  add_definitions(-DHAVE_OSMT2)
+  message("OpenSMT2 SMT solver found. This enables optional SMT-based Yul optimizations with OpenSMT2.")
+endif()
+
 add_subdirectory(libsolutil)
 add_subdirectory(liblangutil)
 add_subdirectory(libsmtutil)

cmake/EthCompilerSettings.cmake

@@ -224,6 +224,7 @@ if(UNIX AND NOT APPLE)
 	option(USE_Z3_DLOPEN "Dynamically load the Z3 SMT solver instead of linking against it." OFF)
 endif()
 option(USE_CVC4 "Allow compiling with CVC4 SMT solver integration" ON)
+option(USE_OSMT2 "Allow compiling with OpenSMT2 SMT solver integration" ON)
 
 if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
 	option(USE_LD_GOLD "Use GNU gold linker" ON)

cmake/FindOSMT2.cmake

@@ -0,0 +1,27 @@
+if (USE_OSMT2)
+	find_path(OSMT2_INCLUDE_DIR opensmt/opensmt2.h)
+	find_library(OSMT2_LIBRARY NAMES opensmt2)
+    include(FindPackageHandleStandardArgs)
+	find_package_handle_standard_args(OSMT2 DEFAULT_MSG OSMT2_LIBRARY OSMT2_INCLUDE_DIR)
+	if(OSMT2_FOUND)
+		# OSMT2 depends on GMP.
+		# We can assume that GMP is present on the system,
+        # so we quietly try to find it and link against it, if it is present.
+        find_package(GMP QUIET)
+
+		set(OSMT2_LIBRARIES ${OSMT2_LIBRARY})
+
+        if (GMP_FOUND)
+			set(OSMT2_LIBRARIES ${OSMT2_LIBRARIES} GMP::GMP)
+        endif ()
+
+		if (NOT TARGET OSMT2::OSMT2)
+			add_library(OSMT2::OSMT2 UNKNOWN IMPORTED)
+			set_property(TARGET OSMT2::OSMT2 PROPERTY IMPORTED_LOCATION ${OSMT2_LIBRARY})
+			set_property(TARGET OSMT2::OSMT2 PROPERTY INTERFACE_LINK_LIBRARIES ${OSMT2_LIBRARIES})
+			set_property(TARGET OSMT2::OSMT2 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${OSMT2_INCLUDE_DIR})
+        endif()
+    endif()
+else()
+	set(OSMT2_FOUND FALSE)
+endif()

libsmtutil/CMakeLists.txt

@@ -24,19 +24,13 @@ else()
   set(cvc4_SRCS)
 endif()
 
-if (${USE_Z3_DLOPEN})
+if (${OSMT2_FOUND})
-  file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h)
+  set(osmt2_SRCS OpenSMT2Interface.cpp OpenSMT2Interface.h)
-  set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp)
+else()
-  add_custom_command(
+  set(osmt2_SRCS)
-    OUTPUT ${Z3_WRAPPER}
-    COMMAND ${Python3_EXECUTABLE} genz3wrapper.py ${Z3_HEADERS} > ${Z3_WRAPPER}
-    DEPENDS ${Z3_HEADERS} genz3wrapper.py
-    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
-  )
-  set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h)
 endif()
 
-add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
+add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS} ${osmt2_SRCS})
 target_link_libraries(smtutil PUBLIC solutil Boost::boost)
 
 if (${USE_Z3_DLOPEN})
@@ -49,3 +43,7 @@ endif()
 if (${CVC4_FOUND})
   target_link_libraries(smtutil PUBLIC CVC4::CVC4)
 endif()
+
+if (${OSMT2_FOUND})
+  target_link_libraries(smtutil PUBLIC OSMT2::OSMT2)
+endif()

libsmtutil/OpenSMT2Interface.cpp

@@ -0,0 +1,182 @@
+/*
+	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/OpenSMT2Interface.h>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+OpenSMT2Interface::OpenSMT2Interface():
+	m_opensmt(make_unique<Opensmt>(qf_lia, "OpenSMT")),
+	m_logic(m_opensmt->getLIALogic()),
+	m_solver(m_opensmt->getMainSolver())
+{
+}
+
+void OpenSMT2Interface::reset()
+{
+}
+
+void OpenSMT2Interface::push()
+{
+	m_solver.push();
+}
+
+void OpenSMT2Interface::pop()
+{
+	m_solver.pop();
+}
+
+void OpenSMT2Interface::declareVariable(string const& _name, SortPointer const& _sort)
+{
+	smtAssert(_sort, "");
+	m_variables[_name] = m_logic.mkVar(openSMT2Sort(*_sort), _name.c_str());
+}
+
+void OpenSMT2Interface::addAssertion(Expression const& _expr)
+{
+	m_solver.insertFormula(toOpenSMT2Expr(_expr));
+}
+
+pair<CheckResult, vector<string>> OpenSMT2Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	CheckResult result;
+	vector<string> values;
+
+	sstat res = m_solver.check();
+	if (res == s_True)
+		result = CheckResult::SATISFIABLE;
+	else if (res == s_False)
+		result = CheckResult::UNSATISFIABLE;
+	else if (res == s_Undef)
+		result = CheckResult::UNKNOWN;
+	else
+		result = CheckResult::ERROR;
+
+	if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
+	{
+		for (Expression const& e: _expressionsToEvaluate)
+			values.push_back(m_solver.getValue(toOpenSMT2Expr(e)).val);
+	}
+
+	return make_pair(result, values);
+}
+
+PTRef OpenSMT2Interface::toOpenSMT2Expr(Expression const& _expr)
+{
+	// Variable
+	if (_expr.arguments.empty() && m_variables.count(_expr.name))
+		return m_variables.at(_expr.name);
+
+	vector<PTRef> arguments;
+	for (auto const& arg: _expr.arguments)
+		arguments.push_back(toOpenSMT2Expr(arg));
+
+	try
+	{
+		string const& n = _expr.name;
+		// Function application
+		if (!arguments.empty() && m_variables.count(_expr.name))
+			smtAssert(false, "Not implemented.");
+		// Literal
+		else if (arguments.empty())
+		{
+			if (n == "true")
+				return m_logic.getTerm_true();
+			else if (n == "false")
+				return m_logic.getTerm_false();
+			else if (auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort))
+				return m_logic.mkVar(openSMT2Sort(*sortSort->inner), n.c_str());
+			else
+				try
+				{
+					return m_logic.mkConst(n.c_str());
+				}
+				catch (std::exception const& _e)
+				{
+					smtAssert(false, _e.what());
+				}
+		}
+
+		smtAssert(_expr.hasCorrectArity(), "");
+		if (n == "ite")
+			return m_logic.mkIte(arguments[0], arguments[1], arguments[2]);
+		else if (n == "not")
+			return m_logic.mkNot(arguments[0]);
+		else if (n == "and")
+			return m_logic.mkAnd(arguments[0], arguments[1]);
+		else if (n == "or")
+			return m_logic.mkOr(arguments[0], arguments[1]);
+		else if (n == "implies")
+			return m_logic.mkImpl(arguments[0], arguments[1]);
+		else if (n == "=")
+			return m_logic.mkEq(arguments[0], arguments[1]);
+		else if (n == "<")
+			return m_logic.mkNumLt(arguments[0], arguments[1]);
+		else if (n == "<=")
+			return m_logic.mkNumLeq(arguments[0], arguments[1]);
+		else if (n == ">")
+			return m_logic.mkNumGt(arguments[0], arguments[1]);
+		else if (n == ">=")
+			return m_logic.mkNumGeq(arguments[0], arguments[1]);
+		else if (n == "+")
+			return m_logic.mkNumPlus(arguments[0], arguments[1]);
+		else if (n == "-")
+			return m_logic.mkNumMinus(arguments[0], arguments[1]);
+		else if (n == "*")
+			return m_logic.mkNumTimes(arguments[0], arguments[1]);
+		else if (n == "/")
+			return m_logic.mkNumDiv(arguments[0], arguments[1]);
+		else if (n == "mod")
+			smtAssert(false, "Not implemented.");
+		else
+			smtAssert(false, "Not implemented.");
+
+		smtAssert(false, "");
+	}
+	catch (std::exception const& _e)
+	{
+		smtAssert(false, _e.what());
+	}
+
+	smtAssert(false, "");
+}
+
+SRef OpenSMT2Interface::openSMT2Sort(Sort const& _sort)
+{
+	switch (_sort.kind)
+	{
+	case Kind::Bool:
+		return m_logic.getSort_bool();
+	case Kind::Int:
+		return m_logic.getSort_num();
+	default:
+		smtAssert(false, "Not implemented.");
+	}
+	smtAssert(false, "");
+}
+
+vector<SRef> OpenSMT2Interface::openSMT2Sort(vector<SortPointer> const& _sorts)
+{
+	vector<SRef> opensmt2Sorts;
+	for (auto const& _sort: _sorts)
+		opensmt2Sorts.push_back(openSMT2Sort(*_sort));
+	return opensmt2Sorts;
+}

libsmtutil/OpenSMT2Interface.h

@@ -0,0 +1,55 @@
+/*
+	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>
+#include <boost/noncopyable.hpp>
+
+#include <opensmt/opensmt2.h>
+
+namespace solidity::smtutil
+{
+
+class OpenSMT2Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+	OpenSMT2Interface();
+
+	void reset() override;
+
+	void push() override;
+	void pop() override;
+
+	void declareVariable(std::string const&, SortPointer const&) override;
+
+	void addAssertion(Expression const& _expr) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+
+private:
+	PTRef toOpenSMT2Expr(Expression const& _expr);
+	SRef openSMT2Sort(Sort const& _sort);
+	std::vector<SRef> openSMT2Sort(std::vector<SortPointer> const& _sorts);
+
+	std::unique_ptr<Opensmt> m_opensmt;
+	LIALogic& m_logic;
+	MainSolver& m_solver;
+	std::map<std::string, PTRef> m_variables;
+};
+
+}