Experimental mechanism for loading Z3 dynamically at runtime.

.circleci/config.yml

@@ -469,7 +469,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 -DSOLC_LINK_STATIC=OFF -DUSE_Z3_DLLOAD=ON -DUSE_CVC4=OFF -DUSE_Z3=OFF '-DCMAKE_EXE_LINKER_FLAGS="-static-libgcc -static-libstdc++"'
     steps:
       - checkout
       - run: *run_build

CMakeLists.txt

@@ -51,10 +51,16 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 include(EthOptions)
 configure_project(TESTS)
 
-find_package(Z3 4.6.0)
-if (${Z3_FOUND})
+if(${USE_Z3_DLLOAD})
   add_definitions(-DHAVE_Z3)
-  message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
+  add_definitions(-DHAVE_Z3_DLLOAD)
+  set(Z3_FOUND TRUE)
+else()
+  find_package(Z3 4.6.0)
+  if (${Z3_FOUND})
+    add_definitions(-DHAVE_Z3)
+    message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
+  endif()
 endif()
 
 find_package(CVC4 QUIET)

cmake/EthCompilerSettings.cmake

@@ -204,6 +204,7 @@ endif()
 
 # SMT Solvers integration
 option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON)
+option(USE_Z3_DLLOAD "Dynamically load the Z3 SMT solver instead of linking against it." OFF)
 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"))

libsmtutil/CMakeLists.txt

@@ -27,7 +27,10 @@ endif()
 add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
 target_link_libraries(smtutil PUBLIC solutil Boost::boost)
 
-if (${Z3_FOUND})
+if (${USE_Z3_DLLOAD})
+  add_subdirectory(z3)
+  target_link_libraries(smtutil PUBLIC z3wrapper)
+elseif (${Z3_FOUND})
   target_link_libraries(smtutil PUBLIC z3::libz3)
 endif()
 

libsmtutil/SMTPortfolio.cpp

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

libsmtutil/Z3Interface.cpp

@@ -21,12 +21,23 @@
 #include <libsolutil/CommonData.h>
 #include <libsolutil/CommonIO.h>
 
-#include <z3_api.h>
+#ifdef HAVE_Z3_DLLOAD
+#include <Z3Loader.h>
+#endif
 
 using namespace std;
 using namespace solidity::smtutil;
 using namespace solidity::util;
 
+bool Z3Interface::available()
+{
+#ifdef HAVE_Z3_DLLOAD
+	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/z3/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_library(z3wrapper STATIC wrapper.cpp Z3Loader.cpp)
+target_include_directories(z3wrapper SYSTEM PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
+target_link_libraries(z3wrapper PUBLIC ${CMAKE_DL_LIBS})

libsmtutil/z3/Z3Loader.cpp

@@ -0,0 +1,38 @@
+#include <Z3Loader.h>
+#include <stdexcept>
+#include <z3.h>
+
+Z3Loader const& Z3Loader::get()
+{
+	static Z3Loader z3;
+	return z3;
+}
+void* Z3Loader::loadSymbol(const char* _name) const
+{
+	if (!m_handle)
+		throw std::runtime_error("Attempted to use dynamically loaded Z3, even though it is not available.");
+	void* sym = dlsym(m_handle, _name);
+	if (!sym)
+		throw std::runtime_error(std::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 > 4 || (major == 4 && minor >= 6));
+}
+
+Z3Loader::Z3Loader(): m_handle(dlmopen(LM_ID_NEWLM, "libz3.so", RTLD_NOW))
+{
+}
+Z3Loader::~Z3Loader()
+{
+	dlclose(m_handle);
+}

libsmtutil/z3/Z3Loader.h

@@ -0,0 +1,13 @@
+#include <dlfcn.h>
+
+class Z3Loader
+{
+public:
+	static Z3Loader const& get();
+	void* loadSymbol(const char* _name) const;
+	bool available() const;
+private:
+	Z3Loader();
+	~Z3Loader();
+	void* m_handle = nullptr;
+};

libsmtutil/z3/genwrapper.py

@@ -0,0 +1,81 @@
+#!/usr/bin/env python
+
+import os
+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 m:
+    name = m.group(1)
+    num_args = len(arg_list_pat.findall(m.group(2)))
+    arglist = ''
+    paramlist = ''
+    for i in range(num_args):
+      if i != 0:
+        arglist += ', '
+        paramlist += ', '
+      arglist += '_' + str(i)
+      paramlist += 'ArgType<&' + name + ', ' + str(i) + '> _' + str(i)
+    print('ResultType<&' + name + '> Z3_API ' + name + '(' + paramlist + ')')
+    print('{')
+    print('\t' + 'static auto sym = reinterpret_cast<decltype(&' + name + ')>(Z3Loader::get().loadSymbol(\"' + name + '\"));')
+    print('\treturn sym(' + arglist + ');')
+    print('}')
+  else:
+    raise Exception('Could not parse entry point definition: ' + line)
+
+print(r"""// This file is auto-generated from genwrapper.py
+#include <z3.h>
+#include <tuple>
+#include <Z3Loader.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)>::ArgType<N>;
+
+}
+
+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('}\n')