diff options
| -rw-r--r-- | CMakeLists.txt | 8 | ||||
| -rwxr-xr-x | configure.sh | 8 | ||||
| -rw-r--r-- | src/base/configuration.cpp | 2 | ||||
| -rw-r--r-- | src/base/configuration.h | 2 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 6 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 1 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.h | 16 |
7 files changed, 42 insertions, 1 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 4cef0bc00..f8fe74130 100644 --- 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 244592aee..701744570 100755 --- 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 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 |