Run every test program under ThreadSanitizer every night

.github/workflows/cppverify-sanitize.sh

@@ -1,49 +1,80 @@
 #!/bin/bash
-# Runs every Verify test program through a cpp-verify built with
-# -DCPPVERIFY_SANITIZER="address;undefined" and fails when a sanitizer reports
-# anything. Verdicts are not compared: the sanitizers slow the verifier, and
-# lit checks verdicts.
+# Runs every Verify test program that lit runs through a sanitized cpp-verify
+# and fails when a sanitizer reports anything. Verdicts are not compared: the
+# sanitizers slow the verifier, and lit checks verdicts.
 #
-# usage: cppverify-sanitize.sh BUILD_DIR [PARALLEL]
+# usage: cppverify-sanitize.sh BUILD_DIR address|thread [PARALLEL]
 #
-# LLVM's allocators poison memory in the instrumented code's copies of their
-# inline functions, which the uninstrumented libraries then use, so poisoning
-# by hand is off. Each program runs with two jobs, so the pool runs under the
+# address: a build with -DCPPVERIFY_SANITIZER="address;undefined". LLVM's
+# allocators poison memory in the instrumented code's copies of their inline
+# functions, which the uninstrumented libraries then use, so poisoning by
+# hand is off. Each program runs with two jobs, so the pool runs under the
 # sanitizers too.
+#
+# thread: a build with -DLLVM_USE_SANITIZER=Thread, which instruments LLVM,
+# Clang, the verifier, and the vendored Z3. Each program runs with four jobs
+# and a proof cache of its own, and a program whose tests race Z3 against
+# cvc5 runs on the race backend, so the pool, the cache, and the races run
+# concurrently. cppverify-tsan.supp lists the reports inside Z3 itself and
+# LLVM's crash handler.
 set -u
 BUILD=$1
-PARALLEL=${2:-$(nproc)}
+MODE=$2
+PARALLEL=${3:-$(nproc)}
 HERE=$(cd "$(dirname "$0")" && pwd)
 ROOT=$(cd "$HERE/../.." && pwd)
 TESTS=$ROOT/clang/test/Verify
 OUT=$(mktemp -d)
-export OUT TESTS
+export OUT TESTS MODE
 export CPPVERIFY=$BUILD/bin/cpp-verify
 export ASAN_OPTIONS=detect_leaks=0:allow_user_poisoning=0
 export UBSAN_OPTIONS=print_stacktrace=1
+export TSAN_OPTIONS="suppressions=$HERE/cppverify-tsan.supp second_deadlock_stack=1"
+
+# A runtime that hangs reports nothing, so a program without a result
+# within the time limit is reported too.
+case $MODE in
+  address) REPORT='ERROR: AddressSanitizer|runtime error:' ;;
+  thread) REPORT='WARNING: ThreadSanitizer|ERROR: ThreadSanitizer|ThreadSanitizer shadow stack' ;;
+  *) echo "unknown mode $MODE" >&2; exit 2 ;;
+esac
+REPORT="$REPORT|cppverify-sanitize: no result"
 
 run() {
-  local file=$1 name
+  local file=$1 name extra=()
   name=$(echo "${file#$TESTS/}" | tr / _)
-  timeout -k 60 900 "$CPPVERIFY" --timeout=5000 --jobs=2 "$file" -- \
+  grep -q '^// UNSUPPORTED: true' "$file" && return 0
+  if [ "$MODE" = thread ]; then
+    extra=(--jobs=4 "--proof-cache=$OUT/cache-$name")
+    if grep -q -E -- '--backend[= ]race' "$file" && command -v cvc5 > /dev/null; then
+      extra+=(--backend=race)
+    fi
+  else
+    extra=(--jobs=2)
+  fi
+  timeout -k 60 900 "$CPPVERIFY" --timeout=5000 "${extra[@]}" "$file" -- \
     "-I$TESTS/suite/Inputs" > "$OUT/$name.txt" 2>&1
+  local status=$?
+  if [ $status -eq 124 ] || [ $status -eq 137 ]; then
+    echo "cppverify-sanitize: no result within 900 s (status $status)" >> "$OUT/$name.txt"
+  fi
   return 0
 }
 export -f run
 
 find "$TESTS" -name '*.cpp' -not -path '*/Inputs/*' -print0 |
   xargs -0 -P "$PARALLEL" -I{} bash -c 'run "$1"' _ {}
 
-reports=$(grep -l -E 'ERROR: AddressSanitizer|runtime error:' "$OUT"/*.txt)
-programs=$(find "$TESTS" -name '*.cpp' -not -path '*/Inputs/*' | wc -l)
+reports=$(grep -l -E "$REPORT" "$OUT"/*.txt)
+programs=$(find "$TESTS" -name '*.cpp' -not -path '*/Inputs/*' -exec grep -L '^// UNSUPPORTED: true' {} + | wc -l)
 if [ -z "$reports" ]; then
-  echo "no reports in $programs programs"
+  echo "$MODE: no reports in $programs programs"
   exit 0
 fi
 for report in $reports; do
   echo "=== $(basename "$report" .txt)"
-  grep -m1 -A40 -E 'ERROR: AddressSanitizer|runtime error:' "$report"
+  grep -m1 -A40 -E "$REPORT" "$report"
 done
-echo "reports in $(echo "$reports" | wc -l) of $programs programs"
+echo "$MODE: reports in $(echo "$reports" | wc -l) of $programs programs"
 mkdir -p sanitizer-reports && cp $reports sanitizer-reports/
 exit 1

.github/workflows/cppverify-sanitizers.yml

@@ -3,9 +3,10 @@ name: CppVerify sanitizers
 # Every night, the verifier's own code (clang/lib/Verify and cpp-verify) is
 # built with AddressSanitizer and UndefinedBehaviorSanitizer
 # (-DCPPVERIFY_SANITIZER), beside an uninstrumented LLVM, Clang, and Z3, and
-# every Verify test program runs through it (cppverify-sanitize.sh). A
-# sanitizer report fails the job and uploads the outputs. A pull request that
-# changes this setup runs it too.
+# LLVM, Clang, the verifier, and Z3 together with ThreadSanitizer
+# (-DLLVM_USE_SANITIZER=Thread); every Verify test program runs through each
+# (cppverify-sanitize.sh). A sanitizer report fails the job and uploads the
+# outputs. A pull request that changes this setup runs it too.
 
 on:
   schedule:
@@ -15,6 +16,9 @@ on:
     paths:
       - .github/workflows/cppverify-sanitizers.yml
       - .github/workflows/cppverify-sanitize.sh
+      - .github/workflows/cppverify-tsan.supp
+      - clang/cmake/modules/CppVerifyZ3.cmake
+      - clang/tools/cpp-verify/ShadowStackGuard.cpp
   workflow_dispatch:
 
 permissions:
@@ -81,10 +85,86 @@ jobs:
       - name: Run every test program
         run: |
           build/bin/cpp-verify --version
-          .github/workflows/cppverify-sanitize.sh build
+          .github/workflows/cppverify-sanitize.sh build address
 
       - uses: actions/upload-artifact@v4
         if: failure()
         with:
           name: sanitizer-reports
           path: sanitizer-reports/
+
+  tsan:
+    name: ThreadSanitizer
+    runs-on: ubuntu-24.04
+    timeout-minutes: 355
+    env:
+      CCACHE_DIR: ${{ github.workspace }}/.ccache
+      CCACHE_MAXSIZE: 4G
+      CCACHE_COMPRESS: "1"
+    steps:
+      - name: Free disk space
+        run: sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install build tools and cvc5
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ninja-build ccache clang-18 llvm-18 libclang-rt-18-dev
+          curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \
+            "https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION/cvc5-Linux-x86_64-static.zip"
+          unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5"
+          dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH"
+
+      - uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ccache-linux-tsan-${{ github.sha }}
+          restore-keys: ccache-linux-tsan-
+
+      # LLVM, Clang, the verifier, and the vendored Z3 are all instrumented:
+      # TSan sees the synchronization of instrumented code only. Clang would
+      # take the libstdc++ of the image's newest GCC, 14.2, whose timed mutex
+      # cannot wait on a steady clock under TSan (GCC PR 121496), as Z3's
+      # timer does; GCC 13's waits with pthread_mutex_clocklock, which TSan
+      # intercepts.
+      - name: Configure
+        run: |
+          cmake -S llvm -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DCMAKE_C_COMPILER=clang-18 \
+            -DCMAKE_CXX_COMPILER=clang++-18 \
+            -DCMAKE_C_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 \
+            -DCMAKE_CXX_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 \
+            -DLLVM_ENABLE_PROJECTS=clang \
+            -DLLVM_TARGETS_TO_BUILD=Native \
+            -DCPPVERIFY_VENDOR_Z3=ON \
+            -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF \
+            -DLLVM_ENABLE_ASSERTIONS=ON \
+            -DLLVM_USE_SANITIZER=Thread \
+            -DLLVM_CCACHE_BUILD=ON
+
+      - name: Build
+        run: ninja -C build cpp-verify
+
+      - uses: actions/cache/save@v4
+        if: always()
+        with:
+          path: .ccache
+          key: ccache-linux-tsan-${{ github.sha }}
+
+      # Two programs at once, each with four jobs; llvm-symbolizer names the
+      # frames of a report.
+      - name: Run every test program
+        run: |
+          build/bin/cpp-verify --version
+          PATH=/usr/lib/llvm-18/bin:$PATH \
+            .github/workflows/cppverify-sanitize.sh build thread 2
+
+      - uses: actions/upload-artifact@v4
+        if: failure()
+        with:
+          name: tsan-reports
+          path: sanitizer-reports/

.github/workflows/cppverify-tsan.supp

@@ -0,0 +1,23 @@
+# ThreadSanitizer suppressions for cppverify-sanitize.sh in thread mode: data
+# races inside Z3 4.13.4 itself, and LLVM's crash handler. Each names a
+# function of Z3 or LLVM that the verifier does not call itself.
+#
+# Every Z3 command context, which pattern inference makes for each quantified
+# query, sets the global verbose stream (util.cpp) without a lock.
+race:set_verbose_stream
+# Z3's statistics read its global allocation counters without the lock its
+# allocator updates them under (memory_manager.cpp).
+race:get_memory_statistics
+# A check's timeout handler sets its flag from Z3's timer thread without
+# synchronization, and Z3_interrupt, which may be called from any thread,
+# reads it (cancel_eh.h).
+race:cancel_eh
+# A nested Z3 timer locks the timer pool's mutex while the outer timer holds
+# its state's mutex, and the pool hands a free state to a new timer by
+# locking the state's mutex under its own. A state is free only once its
+# timer has released it, so the two orders never meet; TSan relates the
+# recycled states (scoped_timer.cpp).
+deadlock:scoped_timer
+# LLVM prints a backtrace after a fatal signal, which is not
+# async-signal-safe; only crash_report_url.cpp crashes on purpose.
+signal:PrintStackTraceSignalHandler

clang/cmake/modules/CppVerifyZ3.cmake

@@ -26,6 +26,33 @@ set(CPPVERIFY_Z3_SOURCE_DIR "" CACHE PATH "Path to a Z3 source tree (overrides t
 get_filename_component(CPPVERIFY_REPO_ROOT
   "${CMAKE_CURRENT_LIST_DIR}/../../.." ABSOLUTE)
 
+# Z3's timer waits on a std::timed_mutex until a steady_clock time. Under
+# ThreadSanitizer libstdc++ 14.1 to 14.3 and 15.1 to 15.2 declare that wait
+# without the member it calls (GCC PR 121496), so Z3 would fail to compile.
+function(cppverify_z3_check_tsan_library)
+  include(CheckCXXSourceCompiles)
+  set(CMAKE_TRY_COMPILE_TARGET_TYPE STATIC_LIBRARY)
+  set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
+  check_cxx_source_compiles([[
+#include <chrono>
+#include <mutex>
+bool wait(std::timed_mutex &m) {
+  return m.try_lock_until(std::chrono::steady_clock::now());
+}
+]] CPPVERIFY_TSAN_TIMED_MUTEX_WAIT)
+  if(NOT CPPVERIFY_TSAN_TIMED_MUTEX_WAIT)
+    unset(CPPVERIFY_TSAN_TIMED_MUTEX_WAIT CACHE)
+    message(FATAL_ERROR
+      "Under ThreadSanitizer this C++ library cannot compile "
+      "std::timed_mutex::try_lock_until with a steady_clock time, which the "
+      "vendored Z3 uses: libstdc++ 14.1 to 14.3 and 15.1 to 15.2 have this "
+      "bug (GCC PR 121496), fixed in 14.4 and 15.3. Select another GCC "
+      "installation for C and C++, with Clang for example "
+      "-DCMAKE_C_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 "
+      "-DCMAKE_CXX_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13.")
+  endif()
+endfunction()
+
 # Build vendored Z3 as an isolated ExternalProject rather than add_subdirectory.
 #
 # Why ExternalProject and not add_subdirectory: Z3's CMake declares a library
@@ -74,6 +101,30 @@ function(cppverify_z3_build_external)
       list(APPEND _forward "-D${_var}:STRING=${_value}")
     endif()
   endforeach()
+  # So are the flags it was configured with, which the cache keeps without
+  # LLVM's own: one that selects the C++ library, as --gcc-install-dir= or
+  # -stdlib= does, must reach every object linked together.
+  set(_z3_C_flags "$CACHE{CMAKE_C_FLAGS}")
+  set(_z3_CXX_flags "$CACHE{CMAKE_CXX_FLAGS}")
+  set(_z3_EXE_LINKER_flags "$CACHE{CMAKE_EXE_LINKER_FLAGS}")
+  # Under ThreadSanitizer Z3 is instrumented too, so that its accesses are
+  # checked and its synchronization is seen.
+  if(LLVM_USE_SANITIZER MATCHES "Thread")
+    cppverify_z3_check_tsan_library()
+    set(_z3_tsan "-fsanitize=thread -fno-omit-frame-pointer")
+    if(CMAKE_CXX_COMPILER_ID MATCHES "Clang")
+      string(APPEND _z3_tsan " -gline-tables-only")
+    endif()
+    string(APPEND _z3_C_flags " ${_z3_tsan}")
+    string(APPEND _z3_CXX_flags " ${_z3_tsan}")
+    string(APPEND _z3_EXE_LINKER_flags " -fsanitize=thread")
+  endif()
+  foreach(_kind C CXX EXE_LINKER)
+    string(STRIP "${_z3_${_kind}_flags}" _flags)
+    if(_flags)
+      list(APPEND _forward "-DCMAKE_${_kind}_FLAGS:STRING=${_flags}")
+    endif()
+  endforeach()
 
   ExternalProject_Add(cppverify_z3_ep
     ${_src_args}

clang/lib/Verify/CMakeLists.txt

@@ -114,6 +114,16 @@ if(CPPVERIFY_SANITIZER)
   endif()
 endif()
 
+# ThreadSanitizer records each instrumented call on a shadow stack of 64 Ki
+# frames that it does not bound. The counterexample checker nests up to
+# CertifyLimits::Frames (50000) evaluations, several frames each, and
+# overflowed it into the runtime's own memory. Its accesses stay checked;
+# only its frames are missing from reported stacks.
+if(_cppverify_sanitizers MATCHES "thread" OR LLVM_USE_SANITIZER MATCHES "Thread")
+  set_source_files_properties(Backend/Certify.cpp PROPERTIES
+    COMPILE_OPTIONS -fno-sanitize-thread-func-entry-exit)
+endif()
+
 target_include_directories(clangVerify PUBLIC
   ${CMAKE_CURRENT_SOURCE_DIR}
   ${CMAKE_CURRENT_SOURCE_DIR}/Driver

clang/tools/cpp-verify/CMakeLists.txt

@@ -12,8 +12,20 @@ if(_cppverify_sanitize_flags)
   set(_cppverify_pch_reuse DISABLE_PCH_REUSE)
 endif()
 
+# Under ThreadSanitizer, a nesting deeper than its shadow stack holds stops
+# the run with its stack instead of corrupting the runtime.
+set(LLVM_OPTIONAL_SOURCES ShadowStackGuard.cpp)
+set(_cppverify_shadow_stack_guard)
+if((_cppverify_sanitize_flags MATCHES "thread" OR
+    LLVM_USE_SANITIZER MATCHES "Thread") AND NOT APPLE)
+  set(_cppverify_shadow_stack_guard ShadowStackGuard.cpp)
+  set_source_files_properties(ShadowStackGuard.cpp PROPERTIES
+    COMPILE_OPTIONS -fno-sanitize=thread SKIP_PRECOMPILE_HEADERS ON)
+endif()
+
 add_clang_tool(cpp-verify
   Main.cpp
+  ${_cppverify_shadow_stack_guard}
   ${_cppverify_pch_reuse}
   )
 
@@ -32,4 +44,9 @@ endif()
 if(_cppverify_sanitize_flags)
   target_compile_options(cpp-verify PRIVATE ${_cppverify_sanitize_flags})
   target_link_options(cpp-verify PRIVATE ${_cppverify_sanitize_flags})
+endif()
+
+if(_cppverify_shadow_stack_guard)
+  target_link_options(cpp-verify PRIVATE
+    -Wl,--wrap=__tsan_func_entry,--wrap=__tsan_func_exit)
 endif()

clang/tools/cpp-verify/ShadowStackGuard.cpp

@@ -0,0 +1,38 @@
+// ThreadSanitizer builds only, without instrumentation, linked with
+// --wrap=__tsan_func_entry,--wrap=__tsan_func_exit. TSan records each
+// thread's calls on a shadow stack of 64 Ki frames that it does not bound, so
+// a deeper nesting overwrites the runtime's own memory, and the run crashes
+// or hangs at random later. This stops it at the limit with its stack.
+
+#include <cstdio>
+#include <sanitizer/common_interface_defs.h>
+#include <unistd.h>
+
+extern "C" void __real___tsan_func_entry(void *CallerPC);
+extern "C" void __real___tsan_func_exit();
+
+namespace {
+thread_local unsigned long Depth;
+// Interceptors push a frame too.
+constexpr unsigned long MaxDepth = 64 * 1024 - 64;
+} // namespace
+
+extern "C" void __wrap___tsan_func_entry(void *CallerPC) {
+  if (++Depth == MaxDepth) {
+    char Message[160];
+    int Length = std::snprintf(
+        Message, sizeof Message,
+        "cpp-verify: ThreadSanitizer shadow stack full: %lu nested calls\n",
+        Depth);
+    if (write(STDERR_FILENO, Message, Length) < 0)
+      _exit(1);
+    __sanitizer_print_stack_trace();
+    _exit(1);
+  }
+  __real___tsan_func_entry(CallerPC);
+}
+
+extern "C" void __wrap___tsan_func_exit() {
+  --Depth;
+  __real___tsan_func_exit();
+}