From a9fcfc531bda243b7b7cf30f2d6591d6430ac8b6 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 15:25:41 +0100 Subject: [PATCH] [TravisCI][CMake] Add `Z3_C_EXAMPLES_FORCE_CXX_LINKER` CMake option and propagate its value into the C API examples. This flag forces the C API examples to use the C++ compiler as the linker rather than the C compiler. This a workaround to avoid linking errors when building with UBSan. --- README-CMake.md | 1 + contrib/ci/scripts/build_z3_cmake.sh | 11 +++++++++++ examples/CMakeLists.txt | 21 +++++++++++++++++++-- examples/c/CMakeLists.txt | 11 +++++++++++ examples/maxsat/CMakeLists.txt | 10 ++++++++++ 5 files changed, 52 insertions(+), 2 deletions(-) diff --git a/README-CMake.md b/README-CMake.md index 605c14818..0d323e08f 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -270,6 +270,7 @@ The following useful options can be passed to CMake whilst configuring. * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors. If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors. +* ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh index 76fd0fb84..c1014d5d5 100755 --- a/contrib/ci/scripts/build_z3_cmake.sh +++ b/contrib/ci/scripts/build_z3_cmake.sh @@ -22,6 +22,7 @@ set -o pipefail : ${USE_LTO?"USE_LTO must be specified"} : ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} : ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} ADDITIONAL_Z3_OPTS=() @@ -105,6 +106,16 @@ fi # Set compiler flags source ${SCRIPT_DIR}/set_compiler_flags.sh +if [ "X${UBSAN_BUILD}" = "X1" ]; then + # HACK: When building with UBSan the C++ linker + # must be used to avoid the following linker errors. + # undefined reference to `__ubsan_vptr_type_cache' + # undefined reference to `__ubsan_handle_dynamic_type_cache_miss' + ADDITIONAL_Z3_OPTS+=( \ + '-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \ + ) +fi + # Sanity check if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then echo "Z3_SRC_DIR is invalid" diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index ba7f6ee59..338d2e4bb 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -7,6 +7,19 @@ else() set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") endif() +option(Z3_C_EXAMPLES_FORCE_CXX_LINKER + "Force C++ linker when building C example projects" OFF) + +if (Z3_C_EXAMPLES_FORCE_CXX_LINKER) + # HACK: This is a workaround for UBSan. + message(STATUS "Forcing C++ linker to be used when building example C projects") + set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG + "-DFORCE_CXX_LINKER=ON" + ) +else() + set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG "") +endif() + ################################################################################ # Build example project using libz3's C API as an external project ################################################################################ @@ -14,7 +27,9 @@ ExternalProject_Add(c_example DEPENDS libz3 # Configure step SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c" - CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + CMAKE_ARGS + "-DZ3_DIR=${CMAKE_BINARY_DIR}" + "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" # Build step ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" @@ -30,7 +45,9 @@ ExternalProject_Add(c_maxsat_example DEPENDS libz3 # Configure step SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/maxsat" - CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + CMAKE_ARGS + "-DZ3_DIR=${CMAKE_BINARY_DIR}" + "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" # Build step ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir" diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt index dd8fa6328..bac08e460 100644 --- a/examples/c/CMakeLists.txt +++ b/examples/c/CMakeLists.txt @@ -22,6 +22,17 @@ message(STATUS "Found Z3 ${Z3_VERSION_STRING}") message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(c_example test_capi.c) + +option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF) +if (FORCE_CXX_LINKER) + # This is a hack for avoiding UBSan linking errors + message(STATUS "Forcing use of C++ linker") + set_target_properties(c_example + PROPERTIES + LINKER_LANGUAGE CXX + ) +endif() + target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) diff --git a/examples/maxsat/CMakeLists.txt b/examples/maxsat/CMakeLists.txt index b48e167ea..019243ecf 100644 --- a/examples/maxsat/CMakeLists.txt +++ b/examples/maxsat/CMakeLists.txt @@ -25,6 +25,16 @@ add_executable(c_maxsat_example maxsat.c) target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_link_libraries(c_maxsat_example PRIVATE ${Z3_LIBRARIES}) +option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF) +if (FORCE_CXX_LINKER) + # This is a hack for avoiding UBSan linking errors + message(STATUS "Forcing use of C++ linker") + set_target_properties(c_maxsat_example + PROPERTIES + LINKER_LANGUAGE CXX + ) +endif() + if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") # On Windows we need to copy the Z3 libraries # into the same directory as the executable