Build Z3 from source for P4Tools.

backends/p4tools/cmake/Z3.cmake

@@ -0,0 +1,85 @@
+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)
+
+  if(TOOLS_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
+    set(Z3_MAX_VERSION_EXCL "4.12")
+    find_package(Z3 ${Z3_MIN_VERSION} REQUIRED)
+
+    if(NOT DEFINED Z3_VERSION_STRING OR ${Z3_VERSION_STRING} VERSION_LESS ${Z3_MIN_VERSION})
+      message(FATAL_ERROR "The minimum required Z3 version is ${Z3_MIN_VERSION}. Has ${Z3_VERSION_STRING}.")
+    endif()
+    if(${Z3_VERSION_STRING} VERSION_GREATER_EQUAL ${Z3_MAX_VERSION_EXCL})
+      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})
+  else()
+    # Pull in a specific version of Z3 and link against it.
+    set(P4TOOLS_Z3_VERSION "4.13.0")
+    message(STATUS "Fetching Z3 version ${P4TOOLS_Z3_VERSION} for P4Tools...")
+
+    # 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
+      GIT_REPOSITORY https://github.com/Z3Prover/z3.git
+      GIT_TAG 51fcb10b2ff0e4496a3c0c2ed7c32f0876c9ee49 # 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 ${P4TOOLS_SOURCE_DIR}/cmake/z3.patch || git apply
+        ${P4TOOLS_SOURCE_DIR}/cmake/z3.patch -R --check && echo
+        "Patch does not apply because the patch was already applied."
+    )
+    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")
+          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})
+
+    # Other projects may also pull in Z3.
+    # We have to make sure we only include our local version with P4Tools.
+    set(P4TOOLS_Z3_LIB libz3)
+    set(P4TOOLS_Z3_INCLUDE_DIR ${z3_SOURCE_DIR}/src/api ${z3_SOURCE_DIR}/src/api/c++)
+  endif()
+
+  message(STATUS "Done with setting up Z3 for P4Tools.")
+endmacro(p4tools_obtain_z3)

backends/p4tools/cmake/common.cmake

@@ -13,71 +13,3 @@ function(add_p4tools_executable target source)
   install(TARGETS ${target} RUNTIME DESTINATION ${P4C_RUNTIME_OUTPUT_DIRECTORY})
 endfunction(add_p4tools_executable)
 
-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)
-
-  if(TOOLS_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
-    set(Z3_MAX_VERSION_EXCL "4.12")
-    find_package(Z3 ${Z3_MIN_VERSION} REQUIRED)
-
-    if(NOT DEFINED Z3_VERSION_STRING OR ${Z3_VERSION_STRING} VERSION_LESS ${Z3_MIN_VERSION})
-      message(FATAL_ERROR "The minimum required Z3 version is ${Z3_MIN_VERSION}. Has ${Z3_VERSION_STRING}.")
-    endif()
-    if(${Z3_VERSION_STRING} VERSION_GREATER_EQUAL ${Z3_MAX_VERSION_EXCL})
-      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})
-  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()
-
-    # Print out download state while setting up Z3.
-    set(FETCHCONTENT_QUIET_PREV ${FETCHCONTENT_QUIET})
-    set(FETCHCONTENT_QUIET OFF)
-    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_PROGRESS TRUE
-    )
-    fetchcontent_makeavailable(z3)
-    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)
-  endif()
-endmacro(p4tools_obtain_z3)

backends/p4tools/cmake/z3.patch

@@ -0,0 +1,38 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index ba3ec7bce..7ca1894fd 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -446,13 +446,13 @@ 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
+-  COMMAND
+-  "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+-  COMMENT "Uninstalling..."
+-  USES_TERMINAL
+-  VERBATIM
+-)
++# add_custom_target(uninstall
++#   COMMAND
++#   "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
++#   COMMENT "Uninstalling..."
++#   USES_TERMINAL
++#   VERBATIM
++# )
+
+ ################################################################################
+ # CMake build file locations
+diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
+index 290881ba5..a3db94d7a 100644
+--- a/src/util/memory_manager.cpp
++++ b/src/util/memory_manager.cpp
+@@ -29,6 +29,8 @@ Copyright (c) 2015 Microsoft Corporation
+ # define malloc_usable_size _msize
+ #endif
+
++#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

backends/p4tools/common/CMakeLists.txt

@@ -1,4 +1,5 @@
 # Handle the Z3 installation with this macro. Users have the option to supply their own Z3.
+include(Z3)
 p4tools_obtain_z3()
 
 # Generate version information.
@@ -41,15 +42,16 @@ add_library(p4tools-common OBJECT ${P4C_TOOLS_COMMON_SOURCES})
 
 target_link_libraries(
   p4tools-common
-  # We export Z3' with the common library.
+  # We export Z3 with the common library.
   PUBLIC ${P4TOOLS_Z3_LIB}
     # For Abseil includes.
   PRIVATE frontend
 )
 
 target_include_directories(
   p4tools-common
-  # We export Z3's includes with the common library.
+  # 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 ${P4TOOLS_Z3_INCLUDE_DIR}
 )
 

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>

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>

frontends/common/parser_options.cpp

@@ -48,6 +48,8 @@ const char *p4_14includePath = CONFIG_PKGDATADIR "/p4_14include";
 
 using namespace P4::literals;
 
+bool isSystemFile(cstring file) { return file.startsWith(p4includePath); }
+
 void ParserOptions::closeFile(FILE *file) {
     if (file == nullptr) {
         return;

frontends/common/parser_options.h

@@ -36,6 +36,9 @@ namespace P4 {
 extern const char *p4includePath;
 extern const char *p4_14includePath;
 
+/// Try to guess whether a file is a "system" file
+bool isSystemFile(cstring filename);
+
 /// Base class for compiler options.
 /// This class contains the options for the front-ends.
 /// Each back-end should subclass this file.

frontends/p4/toP4/toP4.cpp

@@ -46,18 +46,15 @@ void ToP4::end_apply(const IR::Node *) {
               "inconsistent vectorSeparator");
 }
 
-// Try to guess whether a file is a "system" file
-bool ToP4::isSystemFile(cstring file) {
-    if (noIncludes) return false;
-    if (file.startsWith(p4includePath)) return true;
-    return false;
-}
-
-cstring ToP4::ifSystemFile(const IR::Node *node) {
-    if (!node->srcInfo.isValid()) return nullptr;
+std::optional<cstring> ToP4::ifSystemFile(const IR::Node *node) {
+    if (!node->srcInfo.isValid() || noIncludes) {
+        return std::nullopt;
+    }
     auto sourceFile = node->srcInfo.getSourceFile();
-    if (isSystemFile(sourceFile)) return sourceFile;
-    return nullptr;
+    if (isSystemFile(sourceFile)) {
+        return sourceFile;
+    }
+    return std::nullopt;
 }
 
 namespace {
@@ -153,17 +150,17 @@ bool ToP4::preorder(const IR::P4Program *program) {
     dump(2);
     for (auto a : program->objects) {
         // Check where this declaration originates
-        cstring sourceFile = ifSystemFile(a);
-        if (!a->is<IR::Type_Error>() &&  // errors can come from multiple files
-            sourceFile != nullptr) {
+        auto sourceFileOpt = ifSystemFile(a);
+        // Errors can come from multiple files
+        if (!a->is<IR::Type_Error>() && sourceFileOpt.has_value()) {
             /* FIXME -- when including a user header file (sourceFile !=
              * mainFile), do we want to emit an #include of it or not?  Probably
              * not when translating from P4-14, as that would create a P4-16
              * file that tries to include a P4-14 header.  Unless we want to
              * allow converting headers independently (is that even possible?).
              * For now we ignore mainFile and don't emit #includes for any
              * non-system header */
-
+            auto sourceFile = sourceFileOpt.value();
             if (includesEmitted.find(sourceFile) == includesEmitted.end()) {
                 if (sourceFile.startsWith(p4includePath)) {
                     const char *p = sourceFile.c_str() + strlen(p4includePath);
@@ -691,7 +688,7 @@ bool ToP4::preorder(const IR::Type_Error *d) {
     dump(1);
     bool first = true;
     for (auto a : *d->getDeclarations()) {
-        if (ifSystemFile(a->getNode()))
+        if (ifSystemFile(a->getNode()).has_value())
             // only print if not from a system file
             continue;
         if (!first) {

frontends/p4/toP4/toP4.h

@@ -17,6 +17,8 @@ limitations under the License.
 #ifndef P4_TOP4_TOP4_H_
 #define P4_TOP4_TOP4_H_
 
+#include <optional>
+
 #include "frontends/common/resolveReferences/resolveReferences.h"
 #include "ir/ir.h"
 #include "ir/visitor.h"
@@ -72,9 +74,9 @@ class ToP4 : public Inspector, ResolutionContext {
         BUG_CHECK(!listTerminators.empty(), "Empty listTerminators");
         listTerminators.pop_back();
     }
-    bool isSystemFile(cstring file);
-    cstring ifSystemFile(const IR::Node *node);  // return file containing node if system file
-    // dump node IR tree up to depth - in the form of a comment
+    /// @returns the file that contains the node, if the node is part of a system file.
+    std::optional<cstring> ifSystemFile(const IR::Node *node);
+    /// dump node IR tree up to depth - in the form of a comment
     void dump(unsigned depth, const IR::Node *node = nullptr, unsigned adjDepth = 0);
     unsigned curDepth() const;