[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

@@ -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.
 

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"

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"

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})
 

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