Allow loading Z3 dynamically at runtime.

.circleci/config.yml

@@ -466,7 +466,7 @@ jobs:
     <<: *build_ubuntu2004
     environment:
       MAKEFLAGS: -j 10
-      CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -DSOLC_LINK_STATIC=1 -DUSE_CVC4=OFF -DUSE_Z3=OFF
+      CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -DUSE_Z3_DLOPEN=ON -DUSE_CVC4=OFF -DSOLC_STATIC_STDLIBS=ON
     steps:
       - checkout
       - run: *run_build

CMakeLists.txt

@@ -22,6 +22,7 @@ if (IS_BIG_ENDIAN)
 endif()
 
 option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms" OFF)
+option(SOLC_STATIC_STDLIBS "Link solc against static versions of libgcc and libstdc++ on supported platforms" OFF)
 
 # Setup cccache.
 include(EthCcache)
@@ -51,8 +52,27 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 include(EthOptions)
 configure_project(TESTS)
 
-find_package(Z3 4.6.0)
+find_package(Z3 4.8.0)
-if (${Z3_FOUND})
+if(${USE_Z3_DLOPEN})
+  add_definitions(-DHAVE_Z3)
+  add_definitions(-DHAVE_Z3_DLOPEN)
+  find_package(Python3 COMPONENTS Interpreter)
+  if(${Z3_FOUND})
+    get_target_property(Z3_HEADER_HINTS z3::libz3 INTERFACE_INCLUDE_DIRECTORIES)
+  endif()
+  find_path(Z3_HEADER_PATH z3.h HINTS ${Z3_HEADER_HINTS})
+  if(Z3_HEADER_PATH)
+    set(Z3_FOUND TRUE)
+  else()
+    message(SEND_ERROR "Dynamic loading of Z3 requires Z3 headers to be present at build time.")
+  endif()
+  if(NOT ${Python3_FOUND})
+    message(SEND_ERROR "Dynamic loading of Z3 requires Python 3 to be present at build time.")
+  endif()
+  if(${SOLC_LINK_STATIC})
+    message(SEND_ERROR "solc cannot be linked statically when dynamically loading Z3.")
+  endif()
+elseif (${Z3_FOUND})
   add_definitions(-DHAVE_Z3)
   message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
 endif()

Changelog.md

@@ -7,6 +7,7 @@ Language Features:
  * Wasm backend: Add ``i32.select`` and ``i64.select`` instructions.
 
 Compiler Features:
+ * Build System: Optionally support dynamic loading of Z3 and use that mechanism for Linux release builds.
  * Code Generator: Avoid memory allocation for default value if it is not used.
  * SMTChecker: Report struct values in counterexamples from CHC engine.
  * SMTChecker: Support early returns in the CHC engine.

cmake/EthCompilerSettings.cmake

@@ -209,6 +209,9 @@ endif()
 
 # SMT Solvers integration
 option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON)
+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)
 
 if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))

docs/installing-solidity.rst

@@ -312,7 +312,7 @@ The following are dependencies for all builds of Solidity:
 +-----------------------------------+-------------------------------------------------------+
 | `Git`_                            | Command-line tool for retrieving source code.         |
 +-----------------------------------+-------------------------------------------------------+
-| `z3`_ (version 4.6+, Optional)    | For use with SMT checker.                             |
+| `z3`_ (version 4.8+, Optional)    | For use with SMT checker.                             |
 +-----------------------------------+-------------------------------------------------------+
 | `cvc4`_ (Optional)                | For use with SMT checker.                             |
 +-----------------------------------+-------------------------------------------------------+

libsmtutil/CMakeLists.txt

@@ -24,10 +24,25 @@ else()
   set(cvc4_SRCS)
 endif()
 
+if (${USE_Z3_DLOPEN})
+  file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h)
+  set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp)
+  add_custom_command(
+    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})
 target_link_libraries(smtutil PUBLIC solutil Boost::boost)
 
-if (${Z3_FOUND})
+if (${USE_Z3_DLOPEN})
+  target_include_directories(smtutil PUBLIC ${Z3_HEADER_PATH})
+  target_link_libraries(smtutil PUBLIC ${CMAKE_DL_LIBS})
+elseif (${Z3_FOUND})
   target_link_libraries(smtutil PUBLIC z3::libz3)
 endif()
 

libsmtutil/SMTPortfolio.cpp

@@ -42,7 +42,7 @@ SMTPortfolio::SMTPortfolio(
 {
 	m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
 #ifdef HAVE_Z3
-	if (_enabledSolvers.z3)
+	if (_enabledSolvers.z3 && Z3Interface::available())
 		m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
 #endif
 #ifdef HAVE_CVC4

libsmtutil/Z3Interface.cpp

@@ -21,12 +21,23 @@
 #include <libsolutil/CommonData.h>
 #include <libsolutil/CommonIO.h>
 
-#include <z3_api.h>
+#ifdef HAVE_Z3_DLOPEN
+#include <libsmtutil/Z3Loader.h>
+#endif
 
 using namespace std;
 using namespace solidity::smtutil;
 using namespace solidity::util;
 
+bool Z3Interface::available()
+{
+#ifdef HAVE_Z3_DLOPEN
+	return Z3Loader::get().available();
+#else
+	return true;
+#endif
+}
+
 Z3Interface::Z3Interface(std::optional<unsigned> _queryTimeout):
 	SolverInterface(_queryTimeout),
 	m_solver(m_context)

libsmtutil/Z3Interface.h

@@ -30,6 +30,8 @@ class Z3Interface: public SolverInterface, public boost::noncopyable
 public:
 	Z3Interface(std::optional<unsigned> _queryTimeout = {});
 
+	static bool available();
+
 	void reset() override;
 
 	void push() override;

libsmtutil/Z3Loader.cpp

@@ -0,0 +1,70 @@
+/*
+	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/Z3Loader.h>
+#include <libsmtutil/Exceptions.h>
+#include <z3.h>
+#include <z3_version.h>
+#include <vector>
+
+#ifndef _GNU_SOURCE
+#define _GNU_SOURCE
+#endif
+#include <dlfcn.h>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::smtutil;
+
+Z3Loader const& Z3Loader::get()
+{
+	static Z3Loader z3;
+	return z3;
+}
+
+void* Z3Loader::loadSymbol(char const* _name) const
+{
+	smtAssert(m_handle, "Attempted to use dynamically loaded Z3, even though it is not available.");
+	void* sym = dlsym(m_handle, _name);
+	smtAssert(sym, string("Symbol \"") + _name + "\" not found in libz3.so");
+	return sym;
+}
+
+bool Z3Loader::available() const
+{
+	if (m_handle == nullptr)
+		return false;
+	unsigned major = 0;
+	unsigned minor = 0;
+	unsigned build = 0;
+	unsigned rev = 0;
+	Z3_get_version(&major, &minor, &build, &rev);
+	return major == Z3_MAJOR_VERSION && minor == Z3_MINOR_VERSION;
+}
+
+Z3Loader::Z3Loader()
+{
+	string libname{"libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION)};
+	m_handle = dlmopen(LM_ID_NEWLM, libname.c_str(), RTLD_NOW);
+}
+
+Z3Loader::~Z3Loader()
+{
+	if (m_handle)
+		dlclose(m_handle);
+}

libsmtutil/Z3Loader.h

@@ -0,0 +1,38 @@
+/*
+	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
+
+namespace solidity::smtutil
+{
+
+class Z3Loader
+{
+public:
+	Z3Loader(Z3Loader const&) = delete;
+	Z3Loader& operator=(Z3Loader const&) = delete;
+	static Z3Loader const& get();
+	void* loadSymbol(char const* _name) const;
+	bool available() const;
+private:
+	Z3Loader();
+	~Z3Loader();
+	void* m_handle = nullptr;
+};
+
+}

libsmtutil/genz3wrapper.py

@@ -0,0 +1,99 @@
+#!/usr/bin/env python3
+# ------------------------------------------------------------------------------
+# 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/>
+#------------------------------------------------------------------------------
+#
+# Script that generates a dlsym-wrapper for Z3 from the header files.
+# Expects all Z3 headers as arguments and outputs the wrapper code to stdout.
+
+import sys
+import re
+
+# Patterns to match Z3 API entry point definitions.
+def_pat = re.compile(" *def_API(.*)")
+extradef_pat = re.compile(" *extra_API(.*)")
+# Pattern to extract name and arguments from the above.
+def_args_pat = re.compile("\('([^']*)'[^\(\)]*\((.*)\)\s*\)")
+# Pattern to extract a list of arguments from the above.
+arg_list_pat = re.compile("[^\(]*\([^\)]*\)[, ]*")
+
+def generateEntryPoint(line, args):
+    m = def_args_pat.match(args)
+    if not m:
+        raise Exception('Could not parse entry point definition: ' + line)
+    name = m.group(1)
+    num_args = len(arg_list_pat.findall(m.group(2)))
+    arglist = ', '.join(f"_{i}" for i in range(num_args))
+    paramlist = ', '.join(f"ArgType<&{name}, {i}> _{i}" for i in range(num_args))
+    print(f'ResultType<&{name}> Z3_API {name}({paramlist})')
+    print('{')
+    print(f'\tstatic auto sym = reinterpret_cast<decltype(&{name})>(Z3Loader::get().loadSymbol(\"{name}\"));')
+    print(f'\treturn sym({arglist});')
+    print('}')
+
+
+print(r"""// This file is auto-generated from genz3wrapper.py
+#include <libsmtutil/Z3Loader.h>
+#include <tuple>
+#include <z3.h>
+
+namespace
+{
+
+template<typename T>
+struct FunctionTrait;
+
+template<typename R, typename... Args>
+struct FunctionTrait<R(*)(Args...)>
+{
+    using ResultType = R;
+    template<unsigned N>
+    using ArgType = std::tuple_element_t<N, std::tuple<Args...>>;
+};
+
+template<auto F>
+using ResultType = typename FunctionTrait<decltype(F)>::ResultType;
+
+template<auto F, unsigned N>
+using ArgType = typename FunctionTrait<decltype(F)>::template ArgType<N>;
+
+}
+
+using namespace solidity;
+using namespace solidity::smtutil;
+
+extern "C"
+{
+
+void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
+{
+    static auto sym = reinterpret_cast<decltype(&Z3_set_error_handler)>(Z3Loader::get().loadSymbol("Z3_set_error_handler"));
+    sym(c, h);
+}
+""")
+
+for header in sys.argv[1:]:
+    with open(header, 'r') as f:
+        for line in f:
+            line = line.strip('\r\n\t ')
+            m = def_pat.match(line)
+            if m:
+                generateEntryPoint(line, m.group(1).strip('\r\n\t '))
+            m = extradef_pat.match(line)
+            if m:
+                generateEntryPoint(line, m.group(1).strip('\r\n\t '))
+
+print('}')

libsolidity/formal/BMC.cpp

@@ -23,6 +23,10 @@
 
 #include <libsmtutil/SMTPortfolio.h>
 
+#ifdef HAVE_Z3_DLOPEN
+#include <z3_version.h>
+#endif
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
@@ -83,7 +87,10 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			m_outerErrorReporter.warning(
 				8084_error,
 				SourceLocation(),
-				"BMC analysis was not possible since no integrated SMT solver (Z3 or CVC4) was found."
+				"BMC analysis was not possible since no SMT solver (Z3 or CVC4) was found."
+#ifdef HAVE_Z3_DLOPEN
+				" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
+#endif
 			);
 		}
 	}

libsolidity/formal/CHC.cpp

@@ -34,6 +34,10 @@
 
 #include <boost/range/adaptor/reversed.hpp>
 
+#ifdef HAVE_Z3_DLOPEN
+#include <z3_version.h>
+#endif
+
 #include <queue>
 
 using namespace std;
@@ -58,7 +62,9 @@ CHC::CHC(
 	m_queryTimeout(_timeout)
 {
 	bool usesZ3 = _enabledSolvers.z3;
-#ifndef HAVE_Z3
+#ifdef HAVE_Z3
+	usesZ3 = usesZ3 && Z3Interface::available();
+#else
 	usesZ3 = false;
 #endif
 	if (!usesZ3)
@@ -88,16 +94,19 @@ void CHC::analyze(SourceUnit const& _source)
 	}
 
 	bool ranSolver = true;
-#ifndef HAVE_Z3
+	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
-	ranSolver = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get())->unhandledQueries().empty();
+		ranSolver = smtLibInterface->unhandledQueries().empty();
-#endif
 	if (!ranSolver && !m_noSolverWarning)
 	{
 		m_noSolverWarning = true;
 		m_outerErrorReporter.warning(
 			3996_error,
 			SourceLocation(),
+#ifdef HAVE_Z3_DLOPEN
+			"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
+#else
 			"CHC analysis was not possible since no integrated z3 SMT solver was found."
+#endif
 		);
 	}
 	else
@@ -762,7 +771,7 @@ void CHC::resetSourceAnalysis()
 
 	bool usesZ3 = false;
 #ifdef HAVE_Z3
-	usesZ3 = m_enabledSolvers.z3;
+	usesZ3 = m_enabledSolvers.z3 && Z3Interface::available();
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.

libsolidity/formal/ModelChecker.cpp

@@ -17,6 +17,9 @@
 // SPDX-License-Identifier: GPL-3.0
 
 #include <libsolidity/formal/ModelChecker.h>
+#ifdef HAVE_Z3
+#include <libsmtutil/Z3Interface.h>
+#endif
 
 using namespace std;
 using namespace solidity;
@@ -63,7 +66,7 @@ solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
 {
 	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
 #ifdef HAVE_Z3
-	available.z3 = true;
+	available.z3 = solidity::smtutil::Z3Interface::available();
 #endif
 #ifdef HAVE_CVC4
 	available.cvc4 = true;

solc/CMakeLists.txt

@@ -20,4 +20,9 @@ if(SOLC_LINK_STATIC AND UNIX AND NOT APPLE)
 		LINK_SEARCH_START_STATIC ON
 		LINK_SEARCH_END_STATIC ON
 	)
+elseif(SOLC_STATIC_STDLIBS AND UNIX AND NOT APPLE)
+	set_target_properties(
+		solc PROPERTIES
+		LINK_FLAGS "-static-libgcc -static-libstdc++"
+	)
 endif()