Add support for ThreadSanitizer instrumentation (#3467)

This commit adds support for compiling CVC4 with ThreadSanitizer
instrumentation. This is useful for debugging issues when CVC4 is used
in a multi-threaded context (e.g. #3292).

6 files changed, 41 insertions, 2 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 294286e30..fbdd05c95 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -68,6 +68,7 @@ option(ENABLE_GPL "Enable GPL dependencies")
 #    > only necessary for options set for build types
 cvc4_option(ENABLE_ASAN           "Enable ASAN build")
 cvc4_option(ENABLE_UBSAN          "Enable UBSan build")
+cvc4_option(ENABLE_TSAN           "Enable TSan build")
 cvc4_option(ENABLE_ASSERTIONS     "Enable assertions")
 cvc4_option(ENABLE_COMP_INC_TRACK
             "Enable optimizations for incremental SMT-COMP tracks")
@@ -156,7 +157,7 @@ endif()
 #       to cmake standards (first letter uppercase).
 set(BUILD_TYPES Production Debug Testing Competition)
 
-if(ENABLE_ASAN OR ENABLE_UBSAN)
+if(ENABLE_ASAN OR ENABLE_UBSAN OR ENABLE_TSAN)
   set(CMAKE_BUILD_TYPE Debug)
 endif()
 
@@ -302,6 +303,14 @@ if(ENABLE_UBSAN)
   add_definitions(-DCVC4_USE_UBSAN)
 endif()
 
+if(ENABLE_TSAN)
+  # -fsanitize=thread requires CMAKE_REQUIRED_FLAGS to be explicitely set,
+  # otherwise the -fsanitize=thread check will fail while linking.
+  set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
+  add_required_c_cxx_flag("-fsanitize=thread")
+  unset(CMAKE_REQUIRED_FLAGS)
+endif()
+
 if(ENABLE_ASSERTIONS)
   add_definitions(-DCVC4_ASSERTIONS)
 else()
@@ -542,7 +551,9 @@ print_config("Replay               :" ENABLE_REPLAY)
 print_config("Statistics           :" ENABLE_STATISTICS)
 print_config("Tracing              :" ENABLE_TRACING)
 message("")
-print_config("Asan                 :" ENABLE_ASAN)
+print_config("ASan                 :" ENABLE_ASAN)
+print_config("UBSan                :" ENABLE_UBSAN)
+print_config("TSan                 :" ENABLE_TSAN)
 print_config("Coverage (gcov)      :" ENABLE_COVERAGE)
 print_config("Profiling (gprof)    :" ENABLE_PROFILING)
 print_config("Unit tests           :" ENABLE_UNIT_TESTING)
diff --git a/configure.sh b/configure.sh
index 701744570..5763fa7ce 100755
--- a/configure.sh
+++ b/configure.sh
@@ -46,6 +46,7 @@ The following flags enable optional features (disable with --no-<option name>).
   --python3                prefer using Python 3 (also for Python bindings)
   --asan                   build with ASan instrumentation
   --ubsan                  build with UBSan instrumentation
+  --tsan                   build with TSan instrumentation
 
 The following options configure parameterized features.
 
@@ -110,6 +111,7 @@ buildtype=default
 abc=default
 asan=default
 ubsan=default
+tsan=default
 assertions=default
 best=default
 cadical=default
@@ -174,6 +176,9 @@ do
     --ubsan) ubsan=ON;;
     --no-ubsan) ubsan=OFF;;
 
+    --tsan) tsan=ON;;
+    --no-tsan) tsan=OFF;;
+
     --assertions) assertions=ON;;
     --no-assertions) assertions=OFF;;
 
@@ -356,6 +361,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
 [ $ubsan != default ] \
   && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
+[ $tsan != default ] \
+  && cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
 [ $assertions != default ] \
   && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
 [ $best != default ] \
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 0400a4e4d..fb4d94f9d 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -86,6 +86,8 @@ bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
 
 bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
 
+bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }
+
 bool Configuration::isCompetitionBuild() {
   return IS_COMPETITION_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index db0cd5cde..60cdd5a9c 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -67,6 +67,8 @@ public:
 
   static bool isUbsanBuild();
 
+  static bool isTsanBuild();
+
   static bool isCompetitionBuild();
 
   static std::string getPackageName();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 82938adb9..f3e76d53b 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -178,6 +178,22 @@ namespace CVC4 {
 #define IS_UBSAN_BUILD false
 #endif /* CVC4_USE_UBSAN */
 
+#define IS_TSAN_BUILD false
+
+// GCC test
+#if defined(__SANITIZE_THREAD__)
+#undef IS_TSAN_BUILD
+#define IS_TSAN_BUILD true
+#endif /* defined(__SANITIZE_THREAD__) */
+
+// Clang test
+#if defined(__has_feature)
+#if __has_feature(thread_sanitizer)
+#undef IS_TSAN_BUILD
+#define IS_TSAN_BUILD true
+#endif /* __has_feature(thread_sanitizer) */
+#endif /* defined(__has_feature) */
+
 }/* CVC4 namespace */
 
 #endif /* CVC4__CONFIGURATION_PRIVATE_H */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 9fd49864b..d4194d456 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -2108,6 +2108,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("profiling", Configuration::isProfilingBuild());
   print_config_cond("asan", Configuration::isAsanBuild());
   print_config_cond("ubsan", Configuration::isUbsanBuild());
+  print_config_cond("tsan", Configuration::isTsanBuild());
   print_config_cond("competition", Configuration::isCompetitionBuild());
   
   std::cout << std::endl;