From 54449d5a9bd8e0de1a32aa35895f4edae51c5e45 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 11 Oct 2019 01:09:09 -0700 Subject: [PATCH] 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. --- CMakeLists.txt | 8 +++++++- configure.sh | 8 ++++++++ src/base/configuration.cpp | 2 ++ src/base/configuration.h | 2 ++ src/base/configuration_private.h | 6 ++++++ src/options/options_handler.cpp | 1 + src/theory/bv/bitblast/aig_bitblaster.h | 16 ++++++++++++++++ 7 files changed, 42 insertions(+), 1 deletion(-) 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-