diff --git a/.github/workflows/ci-test-fedora.yml b/.github/workflows/ci-test-fedora.yml index 8b490e74583..8644592288a 100644 --- a/.github/workflows/ci-test-fedora.yml +++ b/.github/workflows/ci-test-fedora.yml @@ -43,7 +43,7 @@ jobs: - name: Build p4c (Fedora Linux) run: | - ./bootstrap.sh -DCMAKE_BUILD_TYPE=RELEASE -DCMAKE_UNITY_BUILD=ON --build-generator "Ninja" + ./bootstrap.sh -DCMAKE_BUILD_TYPE=Release -DCMAKE_UNITY_BUILD=ON --build-generator "Ninja" cmake --build build -- -j $(nproc) - name: Run p4c tests (Fedora Linux) diff --git a/.github/workflows/ci-test-mac.yml b/.github/workflows/ci-test-mac.yml index a24f458a064..b06211f222d 100644 --- a/.github/workflows/ci-test-mac.yml +++ b/.github/workflows/ci-test-mac.yml @@ -51,7 +51,7 @@ jobs: - name: Build (MacOS) run: | source ~/.bash_profile - ./bootstrap.sh -DENABLE_GC=ON -DCMAKE_BUILD_TYPE=RELEASE \ + ./bootstrap.sh -DENABLE_GC=ON -DCMAKE_BUILD_TYPE=Release \ -DCMAKE_UNITY_BUILD=ON -DENABLE_TEST_TOOLS=ON --build-generator "Ninja" cmake --build build -- -j $(nproc) @@ -104,7 +104,7 @@ jobs: - name: Build (MacOS) run: | source ~/.bash_profile - ./bootstrap.sh -DENABLE_GC=ON -DCMAKE_BUILD_TYPE=RELEASE \ + ./bootstrap.sh -DENABLE_GC=ON -DCMAKE_BUILD_TYPE=Release \ -DCMAKE_UNITY_BUILD=ON -DENABLE_TEST_TOOLS=ON --build-generator "Ninja" cmake --build build -- -j $(nproc) diff --git a/backends/p4tools/cmake/Z3.cmake b/backends/p4tools/cmake/Z3.cmake new file mode 100644 index 00000000000..e2aea1a4554 --- /dev/null +++ b/backends/p4tools/cmake/Z3.cmake @@ -0,0 +1,71 @@ +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") + fetchcontent_declare( + z3 + GIT_REPOSITORY https://github.com/Z3Prover/z3.git + GIT_TAG z3-${P4TOOLS_Z3_VERSION} # 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") + 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) diff --git a/backends/p4tools/cmake/common.cmake b/backends/p4tools/cmake/common.cmake index 0cde58e8584..ed8f15de194 100644 --- a/backends/p4tools/cmake/common.cmake +++ b/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) diff --git a/backends/p4tools/cmake/z3.patch b/backends/p4tools/cmake/z3.patch new file mode 100644 index 00000000000..92b641ad04d --- /dev/null +++ b/backends/p4tools/cmake/z3.patch @@ -0,0 +1,25 @@ +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/backends/p4tools/common/CMakeLists.txt b/backends/p4tools/common/CMakeLists.txt index 480215b13dc..a5068fadbe2 100644 --- a/backends/p4tools/common/CMakeLists.txt +++ b/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,7 +42,7 @@ 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 @@ -49,7 +50,8 @@ target_link_libraries( 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} ) diff --git a/backends/p4tools/common/core/z3_solver.cpp b/backends/p4tools/common/core/z3_solver.cpp index e91c37efaf9..4827459883e 100644 --- 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 -#include - #include #include #include diff --git a/backends/p4tools/common/core/z3_solver.h b/backends/p4tools/common/core/z3_solver.h index 5f73a2493d4..f70b5018cef 100644 --- 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 +#include #include #include diff --git a/tools/ci-build.sh b/tools/ci-build.sh index 6a2bd78dc8d..d496611794a 100755 --- a/tools/ci-build.sh +++ b/tools/ci-build.sh @@ -243,7 +243,7 @@ CMAKE_FLAGS+="-DSTATIC_BUILD_WITH_DYNAMIC_STDLIB=${STATIC_BUILD_WITH_DYNAMIC_STD # Toggle the installation of the tools back end. CMAKE_FLAGS+="-DENABLE_TEST_TOOLS=${ENABLE_TEST_TOOLS} " # RELEASE should be default, but we want to make sure. -CMAKE_FLAGS+="-DCMAKE_BUILD_TYPE=RELEASE " +CMAKE_FLAGS+="-DCMAKE_BUILD_TYPE=Release " # Treat warnings as errors. CMAKE_FLAGS+="-DENABLE_WERROR=${ENABLE_WERROR} " # Enable sanitizers. diff --git a/tools/debian-build/packaging.conf b/tools/debian-build/packaging.conf index 4458efb4174..c4defeb356a 100644 --- a/tools/debian-build/packaging.conf +++ b/tools/debian-build/packaging.conf @@ -12,7 +12,7 @@ export CXXFLAGS="${CXXFLAGS} -O3" # Enable unity compilation. CONFOPT+="-DCMAKE_UNITY_BUILD=ON " # RELEASE should be default, but we want to make sure. -CONFOPT+="-DCMAKE_BUILD_TYPE=RELEASE " +CONFOPT+="-DCMAKE_BUILD_TYPE=Release " # The binaries we produce should not depend on system libraries. CONFOPT+="-DSTATIC_BUILD_WITH_DYNAMIC_GLIBC=ON " MAKE_DIST="cd ${P4C_DIR}/backends/ebpf && ./build_libbpf && mkdir -p ${P4C_DIR}/build && cd ${P4C_DIR}/build && cmake .. $CONFOPT && make && make dist"