Use our own Z3 if available

Author: artemdinaburg

Dockerfile

@@ -52,7 +52,7 @@ RUN mkdir -p /cache && ./pkgman.py \
   --exclude_libcxx \
   "--additional_paths=${BOOTSTRAP}/cmake/bin" \
   "--repository_path=${LIBRARIES}" \
-  "--packages=llvm" && \
+  "--packages=z3,llvm" && \
   rm -rf build && mkdir build && \
   rm -rf sources && mkdir sources && rm -rf /cache
 
@@ -71,7 +71,7 @@ RUN mkdir -p /cache && ./pkgman.py \
   --verbose \
   "--additional_paths=${BOOTSTRAP}/cmake/bin:${LIBRARIES}/llvm/bin" \
   "--repository_path=${LIBRARIES}" \
-  "--packages=cmake,google,xed,z3" && \
+  "--packages=cmake,google,xed" && \
   rm -rf build && mkdir build && \
   rm -rf sources && mkdir sources && rm -rf /cache
 

pkgman.py

@@ -115,6 +115,13 @@ def main():
   print(("Repository path: " + args.repository_path))
 
   if "llvm" in packages_to_install:
+    if "z3" not in packages_to_install:
+      properties["llvm_has_z3"] = False
+    else:
+      properties["llvm_has_z3"] = True
+      # ensure "z3" is always first to install
+      packages_to_install.remove("z3")
+      packages_to_install.insert(0, "z3")
     if sys.platform == "win32":
       supported_llvm_version_list = [501]
     else:

pkgman/installers/common.py

@@ -558,6 +558,20 @@ def common_installer_llvm(properties):
       print(" x Failed to patch LLVM")
       return False
 
+  if int(properties["llvm_version"]) <= 1000:
+    print(" i Fixing LLVM's FindZ3.cmake")
+    fz3_location = os.path.realpath(os.path.join(llvm_root_folder, "cmake", "modules", "FindZ3.cmake"))
+    have_fz3 = os.path.exists(fz3_location)
+    if have_fz3:
+      src_file = os.path.join(PATCHES_DIR, "FindZ3.cmake")
+      # overwrite the bad FindZ3.cmake with our version
+      shutil.copyfile(src_file, fz3_location)
+
+      src_file = os.path.join(PATCHES_DIR, "testz3.cpp")
+      tz3_location = os.path.realpath(os.path.join(llvm_root_folder, "cmake", "modules", "testz3.cpp"))
+      shutil.copyfile(src_file, tz3_location)
+
+
   # create the build directory and compile the package
   llvm_build_path = os.path.realpath(os.path.join("build", "llvm-" + str(properties["llvm_version"])))
   if not os.path.isdir(llvm_build_path):
@@ -582,7 +596,12 @@ def common_installer_llvm(properties):
   cmake_command = ["cmake"] + get_env_compiler_settings() + get_cmake_build_type(debug) + ["-DCMAKE_INSTALL_PREFIX=" + destination_path,
                                                                                            "-DCMAKE_CXX_STANDARD="+cppstd, "-DLLVM_TARGETS_TO_BUILD=" + arch_list,
                                                                                            "-DLLVM_ENABLE_RTTI=ON", "-DLLVM_INCLUDE_EXAMPLES=OFF",
-                                                                                           "-DLLVM_INCLUDE_TESTS=OFF", "-DLLVM_ENABLE_Z3_SOLVER=OFF"]
+                                                                                           "-DLLVM_INCLUDE_TESTS=OFF"]
+
+  if properties["llvm_has_z3"]:
+    cmake_command += ["-DLLVM_ENABLE_Z3_SOLVER=ON", "-DLLVM_Z3_INSTALL_DIR=" + os.path.join(repository_path, "z3")]
+  else:
+    cmake_command += ["-DLLVM_ENABLE_Z3_SOLVER=OFF"]
 
   if properties["ccache"]:
     print(" i Enabling ccache on /cache ... ")
@@ -644,9 +663,7 @@ def common_installer_z3(properties):
       return False
 
   cmake_command = ["cmake"] + get_env_compiler_settings() + get_cmake_build_type(debug) + get_cmake_generator()
-  cmake_command += ["-DCMAKE_CXX_STANDARD=11",
-                    "-DCMAKE_CXX_EXTENSIONS=ON",
-                    "-DZ3_BUILD_LIBZ3_SHARED=False",
+  cmake_command += ["-DZ3_BUILD_LIBZ3_SHARED=False",
                     "-DZ3_ENABLE_EXAMPLE_TARGETS=False",
                     "-DZ3_BUILD_DOCUMENTATION=False",
                     "-DZ3_BUILD_EXECUTABLE=True",

pkgman/patches/FindZ3.cmake

@@ -0,0 +1,105 @@
+INCLUDE(CheckCXXSourceRuns)
+
+# Function to check Z3's version
+function(check_z3_version z3_include z3_lib)
+  # Get lib path
+  get_filename_component(z3_lib_path ${z3_lib} PATH)
+
+  # Try to find a threading module in case Z3 was built with threading support.
+  # Threads are required elsewhere in LLVM, but not marked as required here because
+  # Z3 could have been compiled without threading support.
+  find_package(Threads)
+  set(z3_link_libs "-lz3" "${CMAKE_THREAD_LIBS_INIT}")
+
+  try_run(
+    Z3_RETURNCODE
+    Z3_COMPILED
+    ${CMAKE_BINARY_DIR}
+    ${CMAKE_SOURCE_DIR}/cmake/modules/testz3.cpp
+    COMPILE_DEFINITIONS -I"${z3_include}"
+    LINK_LIBRARIES -L${z3_lib_path} ${z3_link_libs}
+    RUN_OUTPUT_VARIABLE SRC_OUTPUT
+  )
+
+  if(Z3_COMPILED)
+    string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
+           z3_version "${SRC_OUTPUT}")
+    set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
+  endif()
+endfunction(check_z3_version)
+
+# Looking for Z3 in LLVM_Z3_INSTALL_DIR
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+  NO_DEFAULT_PATH
+  PATHS ${LLVM_Z3_INSTALL_DIR}/include
+  PATH_SUFFIXES libz3 z3
+  )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+  NO_DEFAULT_PATH
+  PATHS ${LLVM_Z3_INSTALL_DIR}
+  PATH_SUFFIXES lib bin
+  )
+
+# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+  PATH_SUFFIXES libz3 z3
+  )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+  PATH_SUFFIXES lib bin
+  )
+
+# Searching for the version of the Z3 library is a best-effort task
+unset(Z3_VERSION_STRING)
+
+# First, try to check it dynamically, by compiling a small program that
+# prints Z3's version
+if(Z3_INCLUDE_DIR AND Z3_LIBRARIES)
+  # We do not have the Z3 binary to query for a version. Try to use
+  # a small C++ program to detect it via the Z3_get_version() API call.
+  check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES})
+endif()
+
+# If the dynamic check fails, we might be cross compiling: if that's the case,
+# check the version in the headers, otherwise, fail with a message
+if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
+                              Z3_INCLUDE_DIR AND
+                              EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
+  # TODO: print message warning that we couldn't find a compatible lib?
+
+  # Z3 4.8.1+ has the version is in a public header.
+  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
+       z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*")
+  string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1"
+         Z3_MAJOR "${z3_version_str}")
+
+  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
+       z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
+  string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1"
+         Z3_MINOR "${z3_version_str}")
+
+  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
+       z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
+  string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1"
+         Z3_BUILD "${z3_version_str}")
+
+  set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})
+  unset(z3_version_str)
+endif()
+
+if(NOT Z3_VERSION_STRING)
+  # Give up: we are unable to obtain a version of the Z3 library. Be
+  # conservative and force the found version to 0.0.0 to make version
+  # checks always fail.
+  set(Z3_VERSION_STRING "0.0.0")
+endif()
+
+# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
+# all listed variables are TRUE
+include(FindPackageHandleStandardArgs)
+FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
+                                  REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
+                                  VERSION_VAR Z3_VERSION_STRING)
+
+mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)

pkgman/patches/testz3.cpp

@@ -0,0 +1,8 @@
+#include <assert.h>
+#include <z3.h>
+int main() {
+  unsigned int major, minor, build, rev;
+  Z3_get_version(&major, &minor, &build, &rev);
+  printf("%u.%u.%u", major, minor, build);
+  return 0;
+}