Add support for UBSan instrumentation (#3382)

This commit adds support for compiling CVC4 with UBSan instrumentation.
The commit also adds a dummy version of `AigBitblaster`. Previously,
when CVC4 was built without ABC, `AigBitblaster` was not fully defined
(the class was declared but the implementation was not being compiled).
This lead to missing RTTI information when compiling with UBSan
instrumentation.

5 files changed, 27 insertions, 0 deletions

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 080c817a4..0400a4e4d 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -84,6 +84,8 @@ bool Configuration::isProfilingBuild() {
 
 bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
 
+bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
+
 bool Configuration::isCompetitionBuild() {
   return IS_COMPETITION_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index fc149587b..db0cd5cde 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -65,6 +65,8 @@ public:
 
   static bool isAsanBuild();
 
+  static bool isUbsanBuild();
+
   static bool isCompetitionBuild();
 
   static std::string getPackageName();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 3b06a9e6a..82938adb9 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -172,6 +172,12 @@ namespace CVC4 {
 #  endif /* __has_feature(address_sanitizer) */
 #endif /* defined(__has_feature) */
 
+#ifdef CVC4_USE_UBSAN
+#define IS_UBSAN_BUILD true
+#else /* CVC4_USE_UBSAN */
+#define IS_UBSAN_BUILD false
+#endif /* CVC4_USE_UBSAN */
+
 }/* CVC4 namespace */
 
 #endif /* CVC4__CONFIGURATION_PRIVATE_H */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e838988c9..3f5cfc0a0 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -2107,6 +2107,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("coverage", Configuration::isCoverageBuild());
   print_config_cond("profiling", Configuration::isProfilingBuild());
   print_config_cond("asan", Configuration::isAsanBuild());
+  print_config_cond("ubsan", Configuration::isUbsanBuild());
   print_config_cond("competition", Configuration::isCompetitionBuild());
   
   std::cout << std::endl;
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 8b63a9aa6..4e11c0f36 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -38,6 +38,8 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+#ifdef CVC4_USE_ABC
+
 class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 {
  public:
@@ -108,7 +110,21 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   Statistics d_statistics;
 };
 
+#else /* CVC4_USE_ABC */
+
+/**
+ * Dummy version of the AigBitblaster class that cannot be instantiated s.t. we
+ * can declare `std::unique_ptr<AigBitblaster>` without ABC.
+ */
+class AigBitblaster : public TBitblaster<Abc_Obj_t*>
+{
+  AigBitblaster() = delete;
+};
+
+#endif /* CVC4_USE_ABC */
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
+
 #endif  //  CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H