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.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4cef0bc00e56951fd24a356eecafb053233cdf07..f8fe74130e06ac76814a9fae915c770676bca624 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -66,6 +66,7 @@ option(ENABLE_GPL "Enable GPL dependencies")
 #    > allows to detect if set by user (default: IGNORE)
 #    > 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_ASSERTIONS     "Enable assertions")
 cvc4_option(ENABLE_COMP_INC_TRACK
             "Enable optimizations for incremental SMT-COMP tracks")
@@ -154,7 +155,7 @@ endif()
 #       to cmake standards (first letter uppercase).
 set(BUILD_TYPES Production Debug Testing Competition)
 
-if(ENABLE_ASAN)
+if(ENABLE_ASAN OR ENABLE_UBSAN)
   set(CMAKE_BUILD_TYPE Debug)
 endif()
 
@@ -297,6 +298,11 @@ if(ENABLE_ASAN)
   add_check_c_cxx_flag("-fsanitize-recover=address")
 endif()
 
+if(ENABLE_UBSAN)
+  add_required_c_cxx_flag("-fsanitize=undefined")
+  add_definitions(-DCVC4_USE_UBSAN)
+endif()
+
 if(ENABLE_ASSERTIONS)
   add_definitions(-DCVC4_ASSERTIONS)
 else()

diff --git a/configure.sh b/configure.sh
index 244592aeef138c9ae4ea75a8d529e8f930ef6792..701744570de96caff2a922ba881e0fa68f2dcb60 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -44,6 +44,8 @@ The following flags enable optional features (disable with --no-<option name>).
   --unit-testing           support for unit testing
   --python2                prefer using Python 2 (also for Python bindings)
   --python3                prefer using Python 3 (also for Python bindings)
+  --asan                   build with ASan instrumentation
+  --ubsan                  build with UBSan instrumentation
 
 The following options configure parameterized features.
 
@@ -107,6 +109,7 @@ buildtype=default
 
 abc=default
 asan=default
+ubsan=default
 assertions=default
 best=default
 cadical=default
@@ -168,6 +171,9 @@ do
     --asan) asan=ON;;
     --no-asan) asan=OFF;;
 
+    --ubsan) ubsan=ON;;
+    --no-ubsan) ubsan=OFF;;
+
     --assertions) assertions=ON;;
     --no-assertions) assertions=OFF;;
 
@@ -348,6 +354,8 @@ cmake_opts=""
 
 [ $asan != default ] \
   && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
+[ $ubsan != default ] \
+  && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
 [ $assertions != default ] \
   && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
 [ $best != default ] \

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 080c817a43fe9f0ba535e5484eddee2cb167954b..0400a4e4d4a12da8007d2b614634643f54bcf822 100644 (file)
--- 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 fc149587bddad419cc07bc1cad9c7bd208a6f735..db0cd5cdee8d19d9f827075691c2e3b103b6f926 100644 (file)
--- 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 3b06a9e6a698bc5c13216dace9c34176cba8dbf4..82938adb9d58e7f2105d93c228499aafa14dd55c 100644 (file)
--- 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 e838988c9a5b0912eadedb5a05d77af3deadd872..3f5cfc0a0c51a0543cc9f52aa55b84e30ae1c347 100644 (file)
--- 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 8b63a9aa625f3a3c2ade0af8d38ac1d7cf2f66f4..4e11c0f36db94307db4697c8f70d24598addae22 100644 (file)
--- 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