Build Z3 from source instead of downloading precompiled binaries. (#4697

) * Build Z3 from source for P4Tools. Signed-off-by: fruffy <fruffy@nyu.edu> * Review comments. Signed-off-by: fruffy <fruffy@nyu.edu> asdsa Signed-off-by: fruffy <fruffy@nyu.edu> --------- Signed-off-by: fruffy <fruffy@nyu.edu>
p4lang · Oct 31, 2024 · 8ba0201 · 8ba0201
1 parent 3feffe0
commit 8ba0201
Show file tree

Hide file tree

Showing 7 changed files with 100 additions and 53 deletions.
diff --git a/backends/p4tools/common/CMakeLists.txt b/backends/p4tools/common/CMakeLists.txt
@@ -1,6 +1,6 @@
 # Handle the Z3 installation with this macro. Users have the option to supply their own Z3.
 include(${P4C_SOURCE_DIR}/cmake/Z3.cmake)
-p4tools_obtain_z3()
+obtain_z3()
 
 # Generate version information.
 configure_file(version.h.in version.h)
@@ -42,16 +42,17 @@ add_library(p4tools-common OBJECT ${P4C_TOOLS_COMMON_SOURCES})
 
 target_link_libraries(
   p4tools-common
-  # We export Z3' with the common library.
-  PUBLIC ${P4TOOLS_Z3_LIB}
+  # We export Z3 with the common library.
+  PUBLIC ${Z3_LIB}
     # For Abseil includes.
   PRIVATE frontend
 )
 
 target_include_directories(
   p4tools-common
-  # We export Z3's includes with the common library.
-  SYSTEM BEFORE PUBLIC ${P4TOOLS_Z3_INCLUDE_DIR}
+  # We also export Z3's includes with the common library.
+  # This is necessary because the z3 target itself does not export its includes.
+  SYSTEM BEFORE PUBLIC ${Z3_INCLUDE_DIR}
 )
 
 # Add control-plane-specific extensions.

diff --git a/backends/p4tools/common/core/z3_solver.cpp b/backends/p4tools/common/core/z3_solver.cpp
@@ -1,8 +1,5 @@
 #include "backends/p4tools/common/core/z3_solver.h"
 
-#include <z3++.h>
-#include <z3_api.h>
-
 #include <algorithm>
 #include <cstdint>
 #include <exception>

diff --git a/backends/p4tools/common/core/z3_solver.h b/backends/p4tools/common/core/z3_solver.h
@@ -2,6 +2,7 @@
 #define BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 
 #include <z3++.h>
+#include <z3.h>
 
 #include <cstddef>
 #include <iosfwd>

diff --git a/backends/tofino/CMakeLists.txt b/backends/tofino/CMakeLists.txt
@@ -4,7 +4,7 @@ MESSAGE("-- Adding p4c-barefoot")
 include(${CMAKE_CURRENT_SOURCE_DIR}/cmake/spdlog.cmake)
 include(${P4C_SOURCE_DIR}/cmake/Z3.cmake)
 
-p4tools_obtain_z3()
+obtain_z3()
 
 set (BFN_P4C_SOURCE_DIR ${PROJECT_SOURCE_DIR}/backends/tofino)
 

diff --git a/backends/tofino/bf-p4c/CMakeLists.txt b/backends/tofino/bf-p4c/CMakeLists.txt
@@ -90,14 +90,14 @@ add_definitions("-DRESOURCES_SCHEMA_VERSION=\"${RESOURCES_SCHEMA_VERSION}\"")
 
 include_directories(${BFN_P4C_SOURCE_DIR}
   ${CMAKE_CURRENT_SOURCE_DIR}
-  ${Boost_INCLUDE_DIRS} ${LIBDYNHASH_INCLUDE_DIR} ${P4TOOLS_Z3_INCLUDE_DIR} )
+  ${Boost_INCLUDE_DIRS} ${LIBDYNHASH_INCLUDE_DIR} ${Z3_INCLUDE_DIR} )
 # The generated code for protobuf has an excessive number of warnings so we
 # include the build directory as a system directory
 include_directories(SYSTEM ${P4C_BINARY_DIR}/control-plane)
 set (HAVE_LIBBOOST_GRAPH 1)
-message(STATUS "Z3_LIBRARY value: ${P4TOOLS_Z3_LIB}")
+message(STATUS "Z3_LIBRARY value: ${Z3_LIB}")
 
-set (P4C_LIB_DEPS "${P4C_LIB_DEPS};${Boost_GRAPH_LIBRARY};${LIBDYNHASH_LIBRARY};${P4TOOLS_Z3_LIB}")
+set (P4C_LIB_DEPS "${P4C_LIB_DEPS};${Boost_GRAPH_LIBRARY};${LIBDYNHASH_LIBRARY};${Z3_LIB}")
 set (P4C_LIB_DEPS ${P4C_LIB_DEPS} PARENT_SCOPE)
 
 add_subdirectory(logging)

diff --git a/cmake/Z3.cmake b/cmake/Z3.cmake
@@ -1,10 +1,13 @@
-macro(p4tools_obtain_z3)
-  option(TOOLS_USE_PREINSTALLED_Z3 "Look for a preinstalled version of Z3 instead of installing a prebuilt binary using FetchContent." OFF)
+macro(obtain_z3)
+  option(USE_PREINSTALLED_Z3 "Look for a preinstalled version of Z3 instead of installing a prebuilt binary using FetchContent." OFF)
 
-  if(TOOLS_USE_PREINSTALLED_Z3)
+  if(USE_PREINSTALLED_Z3)
     # We need a fairly recent version of Z3.
     set(Z3_MIN_VERSION "4.8.14")
-    # But 4.12+ is currently broken with libGC
+    # Anything above 4.12+ does not work with libGC and causes crashes. The reason is
+    # that malloc_usable_size() does not seem to be supported in libgc.
+    # /~https://github.com/Z3Prover/z3/blob/b0fef6429fb29a33eb14adf9a61353b59f0f7fd0/src/util/memory_manager.cpp#L319
+    # Without being able to patch Z3 we have to limit the maximum version.
     set(Z3_MAX_VERSION_EXCL "4.12")
     find_package(Z3 ${Z3_MIN_VERSION} REQUIRED)
 
@@ -15,54 +18,71 @@ macro(p4tools_obtain_z3)
       message(FATAL_ERROR "The Z3 version has to be lower than ${Z3_MAX_VERSION_EXCL} (the latter currently does no work with libGC). Has ${Z3_VERSION_STRING}.")
     endif()
     # Set variables for later consumption.
-    set(P4TOOLS_Z3_LIB z3::z3)
-    set(P4TOOLS_Z3_INCLUDE_DIR ${Z3_INCLUDE_DIR})
+    set(Z3_LIB z3::z3)
+    set(Z3_INCLUDE_DIR ${Z3_INCLUDE_DIR})
   else()
     # Pull in a specific version of Z3 and link against it.
-    set(P4TOOLS_Z3_VERSION "4.11.2")
-    message("Fetching Z3 version ${P4TOOLS_Z3_VERSION} for P4Tools...")
-
-    # Determine platform to fetch pre-built Z3
-    if (CMAKE_HOST_SYSTEM_PROCESSOR STREQUAL "x86_64")
-      set(Z3_ARCH "x64")
-      if (APPLE)
-        set(Z3_PLATFORM_SUFFIX "osx-10.16")
-        set(Z3_ZIP_HASH "a56b6c40d9251a963aabe1f15731dd88ad1cb801d0e7b16e45f8b232175e165c")
-      elseif (UNIX)
-        set(Z3_PLATFORM_SUFFIX "glibc-2.31")
-        set(Z3_ZIP_HASH "9d0f70e61e82b321f35e6cad1343615d2dead6f2c54337a24293725de2900fb6")
-      else()
-        message(FATAL_ERROR "Unsupported system platform")
-      endif()
-    elseif(CMAKE_HOST_SYSTEM_PROCESSOR STREQUAL "arm64")
-      set(Z3_ARCH "arm64")
-      if (APPLE)
-        set(Z3_PLATFORM_SUFFIX "osx-11.0")
-        set(Z3_ZIP_HASH "c021f381fa3169b1f7fb3b4fae81a1d1caf0dd8aa4aa773f4ab9d5e28c6657a4")
-      else()
-        message(FATAL_ERROR "Unsupported system platform")
-      endif()
-    else()
-      message(FATAL_ERROR "Unsupported system processor")
-    endif()
+    set(Z3_VERSION "4.13.0")
+    message(STATUS "Fetching Z3 version ${Z3_VERSION}...")
 
+    # Unity builds do not work for Protobuf...
+    set(CMAKE_UNITY_BUILD_PREV ${CMAKE_UNITY_BUILD})
+    set(CMAKE_UNITY_BUILD OFF)
     # Print out download state while setting up Z3.
     set(FETCHCONTENT_QUIET_PREV ${FETCHCONTENT_QUIET})
     set(FETCHCONTENT_QUIET OFF)
+
+    set(Z3_BUILD_LIBZ3_SHARED OFF CACHE BOOL "Build libz3 as a shared library if true, otherwise build a static library")
+    set(Z3_INCLUDE_GIT_HASH OFF CACHE BOOL "Include git hash in version output")
+    set(Z3_INCLUDE_GIT_DESCRIBE OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_TEST_EXECUTABLES OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_SAVE_CLANG_OPTIMIZATION_RECORDS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_ENABLE_TRACING_FOR_NON_DEBUG OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_ENABLE_EXAMPLE_TARGETS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_DOTNET_BINDINGS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_PYTHON_BINDINGS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_JAVA_BINDINGS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_JULIA_BINDINGS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_DOCUMENTATION OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_ALWAYS_BUILD_DOCS OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_API_LOG_SYNC OFF CACHE BOOL "Include git describe output in version output")
+    set(Z3_BUILD_EXECUTABLE OFF CACHE BOOL "Include git describe output in version output")
     fetchcontent_declare(
       z3
-      URL /~https://github.com/Z3Prover/z3/releases/download/z3-${P4TOOLS_Z3_VERSION}/z3-${P4TOOLS_Z3_VERSION}-${Z3_ARCH}-${Z3_PLATFORM_SUFFIX}.zip
-      URL_HASH SHA256=${Z3_ZIP_HASH}
-      USES_TERMINAL_DOWNLOAD TRUE
+      GIT_REPOSITORY /~https://github.com/Z3Prover/z3.git
+      GIT_TAG z3-4.13.3 # 4.13.0
       GIT_PROGRESS TRUE
+      GIT_SHALLOW TRUE
+      # We need to patch because the Z3 CMakeLists.txt also adds an uinstall target.
+      # This leads to a namespace clash.
+      PATCH_COMMAND
+        git apply ${P4C_SOURCE_DIR}/cmake/z3.patch || git apply
+        ${P4C_SOURCE_DIR}/cmake/z3.patch -R --check && echo
+        "Patch does not apply because the patch was already applied."
     )
-    fetchcontent_makeavailable(z3)
+    fetchcontent_makeavailable_but_exclude_install(z3)
+
+    # Suppress warnings for all Z3 targets.
+    get_all_targets(Z3_BUILD_TARGETS ${z3_SOURCE_DIR})
+    foreach(target ${Z3_BUILD_TARGETS})
+        # Do not suppress warnings for Z3 library targets that are aliased.
+        get_target_property(target_type ${target} TYPE)
+        if (NOT ${target_type} STREQUAL "INTERFACE_LIBRARY" AND NOT ${target_type} STREQUAL "UTILITY")
+          target_compile_options(${target} PRIVATE "-Wno-error" "-w")
+          # Z3 does not add its own include directories for compilation, which can lead to conflicts.
+          target_include_directories(${target} BEFORE PRIVATE ${z3_SOURCE_DIR}/src)
+      endif()
+    endforeach()
+
+    # Reset temporary variable modifications.
+    set(CMAKE_UNITY_BUILD ${CMAKE_UNITY_BUILD_PREV})
     set(FETCHCONTENT_QUIET ${FETCHCONTENT_QUIET_PREV})
-    message("Done with setting up Z3 for P4Tools.")
 
     # Other projects may also pull in Z3.
-    # We have to make sure we only include our local version with P4Tools.
-    set(P4TOOLS_Z3_LIB ${z3_SOURCE_DIR}/bin/libz3${CMAKE_STATIC_LIBRARY_SUFFIX})
-    set(P4TOOLS_Z3_INCLUDE_DIR ${z3_SOURCE_DIR}/include)
+    # We have to make sure we only include our local version.
+    set(Z3_LIB libz3)
+    set(Z3_INCLUDE_DIR ${z3_SOURCE_DIR}/src/api ${z3_SOURCE_DIR}/src/api/c++)
   endif()
-endmacro(p4tools_obtain_z3)
+
+  message(STATUS "Done with setting up Z3.")
+endmacro(obtain_z3)
diff --git a/cmake/z3.patch b/cmake/z3.patch
@@ -0,0 +1,28 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 79708764..18af2183 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -446,7 +446,7 @@ configure_file(
+
+ # Target needs to be declared before the components so that they can add
+ # dependencies to this target so they can run their own custom uninstall rules.
+-add_custom_target(uninstall
++add_custom_target(z3_uninstall
+   COMMAND
+   "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+   COMMENT "Uninstalling..."
+diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
+index 8c6bfc7e..fb3226b8 100644
+--- a/src/util/memory_manager.cpp
++++ b/src/util/memory_manager.cpp
+@@ -31,6 +31,10 @@ Copyright (c) 2015 Microsoft Corporation
+
+ #define SIZE_T_ALIGN 2
+
++// malloc_usable_size() currently does not work with BDWGC which is used by P4C. We disable it.
++// FIXME: Find a way to patch BDWGC to allow malloc_usable_size() to work.
++#undef HAS_MALLOC_USABLE_SIZE
++
+ // The following two function are automatically generated by the mk_make.py script.
+ // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
+ // For example, rational.h contains