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

4 files changed, 21 insertions, 0 deletions

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;