diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-02-13 22:32:07 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-02-13 22:32:07 +0000 |
commit | 13d8b4cb78c81bff97501cbe586f0fd8f1adc4d2 (patch) | |
tree | 424398f1dac3f76b85592940b1af30f4fec14b99 | |
parent | 950c823ddec56d59edb88e6ef81ba541aa5a34df (diff) | |
parent | 56afb17888a8330093e6691ae5bb1635b179431d (diff) | |
download | klee-13d8b4cb78c81bff97501cbe586f0fd8f1adc4d2.tar.gz |
Merge pull request #506 from delcypher/travis_asan_ubsan
Modify scripts and a test to allow ASan/UBSan builds.
-rw-r--r-- | .travis.yml | 5 | ||||
-rwxr-xr-x | .travis/klee.sh | 19 | ||||
-rwxr-xr-x | .travis/metaSMT.sh | 6 | ||||
-rw-r--r-- | .travis/sanitizer_flags.sh | 39 | ||||
-rwxr-xr-x | .travis/solvers.sh | 6 | ||||
-rwxr-xr-x | .travis/stp.sh | 7 | ||||
-rw-r--r-- | Dockerfile | 4 | ||||
-rw-r--r-- | Makefile.common | 10 | ||||
-rw-r--r-- | lib/Support/MemoryUsage.cpp | 65 | ||||
-rw-r--r-- | runtime/Runtest/Makefile | 6 | ||||
-rw-r--r-- | test/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/Makefile | 4 |
12 files changed, 161 insertions, 14 deletions
diff --git a/.travis.yml b/.travis.yml index 435d5139..a0b5e7ae 100644 --- a/.travis.yml +++ b/.travis.yml @@ -38,7 +38,6 @@ env: #- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 #- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 USE_CMAKE=1 - # TODO: Add ASan build # TODO: Add coverage build # TODO: Add Doxygen build @@ -47,6 +46,10 @@ env: - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 - LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_CMAKE=1 USE_TCMALLOC=0 ASAN_BUILD=1 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_CMAKE=0 USE_TCMALLOC=0 ASAN_BUILD=1 + # TODO: Port all configurations below to CMake build system # Test we can still build with Z3 in the old build sytem diff --git a/.travis/klee.sh b/.travis/klee.sh index 8db724ac..61806df3 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -112,6 +112,11 @@ else fi ############################################################################### +# Handle Sanitizer flags +############################################################################### +source ${KLEE_SRC}/.travis/sanitizer_flags.sh + +############################################################################### # KLEE ############################################################################### mkdir klee @@ -131,7 +136,8 @@ if [ "X${USE_CMAKE}" == "X1" ]; then CMAKE_BUILD_TYPE="Debug" fi # Compute CMake build type - CXXFLAGS="${COVERAGE_FLAGS}" \ + CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ + CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ cmake \ -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \ -DLLVMCC="${KLEE_CC}" \ @@ -163,11 +169,12 @@ else ${KLEE_METASMT_CONFIGURE_OPTION} \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ ${TCMALLOC_OPTION} \ - CXXFLAGS="${COVERAGE_FLAGS}" - make \ - DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 + CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ + CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ + LDFLAGS="${SANITIZER_LD_FLAGS}" + make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 fi ############################################################################### diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh index 7195ceb0..6376c4bc 100755 --- a/.travis/metaSMT.sh +++ b/.travis/metaSMT.sh @@ -8,6 +8,12 @@ git clone git://github.com/hoangmle/metaSMT.git cd metaSMT git clone git://github.com/agra-uni-bremen/dependencies.git +source ${KLEE_SRC}/.travis/sanitizer_flags.sh +if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then + echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented" + exit 1 +fi + # Bootstrap export BOOST_ROOT=/usr sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack diff --git a/.travis/sanitizer_flags.sh b/.travis/sanitizer_flags.sh new file mode 100644 index 00000000..4d3dce2c --- /dev/null +++ b/.travis/sanitizer_flags.sh @@ -0,0 +1,39 @@ +# This file is meant to be included by shell scripts +# that need to do a sanitized build. + +# Users of this script can use this variable +# to detect if a Sanitized build was enabled. +IS_SANITIZED_BUILD=0 + +# AddressSanitizer +if [ "X${ASAN_BUILD}" == "X1" ]; then + echo "Using ASan" + ASAN_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer" + ASAN_C_FLAGS="${ASAN_CXX_FLAGS}" + ASAN_LD_FLAGS="${ASAN_CXX_FLAGS}" + IS_SANITIZED_BUILD=1 +else + echo "Not using ASan" + ASAN_CXX_FLAGS="" + ASAN_C_FLAGS="" + ASAN_LD_FLAGS="" +fi + +# Undefined Behaviour Sanitizer +if [ "X${UBSAN_BUILD}" == "X1" ]; then + echo "Using UBSan" + UBSAN_CXX_FLAGS="-fsanitize=undefined" + UBSAN_C_FLAGS="${UBSAN_CXX_FLAGS}" + UBSAN_LD_FLAGS="${UBSAN_CXX_FLAGS}" + IS_SANITIZED_BUILD=1 +else + echo "Not using UBSan" + UBSAN_CXX_FLAGS="" + UBSAN_C_FLAGS="" + UBSAN_LD_FLAGS="" +fi + +# Set variables to be used by clients. +SANITIZER_CXX_FLAGS="${ASAN_CXX_FLAGS} ${UBSAN_CXX_FLAGS}" +SANITIZER_C_FLAGS="${ASAN_C_FLAGS} ${UBSAN_C_FLAGS}" +SANITIZER_LD_FLAGS="${ASAN_LD_FLAGS} ${UBSAN_LD_FLAGS}" diff --git a/.travis/solvers.sh b/.travis/solvers.sh index d64c1077..04f3276f 100755 --- a/.travis/solvers.sh +++ b/.travis/solvers.sh @@ -16,6 +16,12 @@ for solver in ${SOLVER_LIST}; do cd ../ ;; Z3) + # FIXME: Move this into its own script + source ${KLEE_SRC}/.travis/sanitizer_flags.sh + if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then + echo "Error: Requested Sanitized build but Z3 being used is not sanitized" + exit 1 + fi echo "Z3" # Should we install libz3-dbg too? sudo apt-get -y install libz3 libz3-dev diff --git a/.travis/stp.sh b/.travis/stp.sh index 53b7b6bc..4cc55c62 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -6,12 +6,17 @@ set -e STP_LOG="$(pwd)/stp-build.log" if [ "x${STP_VERSION}" != "x" ]; then + # Get Sanitizer flags + source ${KLEE_SRC}/.travis/sanitizer_flags.sh + # Build minisat git clone https://github.com/stp/minisat cd minisat mkdir build cd build MINISAT_DIR=`pwd` + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ cmake -DCMAKE_INSTALL_PREFIX=/usr .. make sudo make install @@ -23,6 +28,8 @@ if [ "x${STP_VERSION}" != "x" ]; then cd build # Disabling building of shared libs is a workaround. # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src set +e # Do not exit if build fails because we need to display the log diff --git a/Dockerfile b/Dockerfile index 747cbef8..d42b09c8 100644 --- a/Dockerfile +++ b/Dockerfile @@ -14,7 +14,9 @@ ENV LLVM_VERSION=3.4 \ KLEE_SRC=/home/klee/klee_src \ COVERAGE=0 \ BUILD_DIR=/home/klee/klee_build \ - USE_CMAKE=1 + USE_CMAKE=1 \ + ASAN_BUILD=0 \ + UBSAN_BUILD=0 RUN apt-get update && \ apt-get -y --no-install-recommends install \ diff --git a/Makefile.common b/Makefile.common index a6ce34fb..0eb741ea 100644 --- a/Makefile.common +++ b/Makefile.common @@ -80,8 +80,14 @@ endif # For metaSMT include $(PROJ_SRC_ROOT)/MetaSMT.mk -# If building KLEE with the Sanitizers don't build the runtime with it -# because KLEE doesn't know how to handle it. +# When building the runtime filter out unwanted flags. +# that add instrumentatation because KLEE can't handle this. ifneq ("X$(MODULE_NAME)$(BYTECODE_LIBRARY)X","XX") + # Sanitizer flags. CFLAGS := $(filter-out -fsanitize=%,$(CFLAGS)) + # Coverag flags. + CFLAGS := $(filter-out -fprofile-arcs,$(CFLAGS)) + CFLAGS := $(filter-out -ftest-coverage,$(CFLAGS)) + CFLAGS := $(filter-out -coverage,$(CFLAGS)) + CFLAGS := $(filter-out --coverage,$(CFLAGS)) endif diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp index d141593a..f1757ad3 100644 --- a/lib/Support/MemoryUsage.cpp +++ b/lib/Support/MemoryUsage.cpp @@ -22,9 +22,74 @@ #include <malloc/malloc.h> #endif +// ASan Support +// +// When building with ASan the `mallinfo()` function is intercepted and always +// reports zero so we can't use that to report KLEE's memory usage. Instead we +// will use ASan's public interface to query how much memory has been +// allocated. +// +// Unfortunately the interface is dependent on the compiler version. It is also +// unfortunate that the way to detect compilation with ASan differs between +// compilers. The preprocessor code below tries to determine if ASan is enabled +// and if so which interface should be used. +// +// If ASan is enabled the `KLEE_ASAN_BUILD` macro will be defined other it will +// be undefined. If `KLEE_ASAN_BUILD` is defined then the +// `ASAN_GET_ALLOCATED_MEM_FUNCTION` macro will defined to the name of the ASan +// function that can be called to get memory allocation + +// Make sure we start with the macro being undefined. +#undef KLEE_ASAN_BUILD + +// Clang and ASan +#if defined(__has_feature) +# if __has_feature(address_sanitizer) +# if __has_include("sanitizer/allocator_interface.h") +# include <sanitizer/allocator_interface.h> + // Modern interface +# define ASAN_GET_ALLOCATED_MEM_FUNCTION __sanitizer_get_current_allocated_bytes +# else +# include <sanitizer/asan_interface.h> + // Deprecated interface. +# define ASAN_GET_ALLOCATED_MEM_FUNCTION __asan_get_current_allocated_bytes +# endif /* has_include("sanitizer/allocator_interface.h") */ +# define KLEE_ASAN_BUILD +# endif /* __has_feature(address_sanitizer) */ +#endif /* defined(__has_feature) */ + +// For GCC and ASan +#ifndef KLEE_ASAN_BUILD +# if defined(__SANITIZE_ADDRESS__) + // HACK: GCC doesn't ship `allocator_interface.h` or `asan_interface.h` so + // just provide the proto-types here. + extern "C" { + size_t __sanitizer_get_current_allocated_bytes(); + size_t __asan_get_current_allocated_bytes(); // Deprecated. + } + // HACK: Guess which function to use based on GCC version +# if __GNUC__ > 4 + // Tested with gcc 5.2, 5.4, and 6.2.1 + // Modern interface +# define ASAN_GET_ALLOCATED_MEM_FUNCTION __sanitizer_get_current_allocated_bytes +# else + // Tested with gcc 4.8 and 4.9 + // Deprecated interface +# define ASAN_GET_ALLOCATED_MEM_FUNCTION __asan_get_current_allocated_bytes +# endif +# define KLEE_ASAN_BUILD +# endif /* defined(__SANITIZE_ADDRESS__) */ +#endif /* ndef KLEE_ASAN_BUILD */ + using namespace klee; size_t util::GetTotalMallocUsage() { +#ifdef KLEE_ASAN_BUILD + // When building with ASan on Linux `mallinfo()` just returns 0 so use ASan runtime + // function instead to get used memory. + return ASAN_GET_ALLOCATED_MEM_FUNCTION(); +#endif + #ifdef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H size_t value = 0; MallocExtension::instance()->GetNumericProperty( diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile index 82e21345..1de3281b 100644 --- a/runtime/Runtest/Makefile +++ b/runtime/Runtest/Makefile @@ -56,8 +56,14 @@ ifeq ($(HOST_OS), $(filter $(HOST_OS), DragonFly Linux FreeBSD GNU/kFreeBSD GNU) endif ifeq ($(HOST_OS), $(filter $(HOST_OS), Linux GNU GNU/kFreeBSD)) + ifeq (-fsanitize=address,$(filter -fsanitize=address,$(CXXFLAGS))) + # When building with ASan the library will have undefined symbols into + # ASan's runtime. We want to allow this and not fail the build. + $(warning Allowing undefined symbols in $(LIBRARYNAME) due to ASan build) + else # Don't allow unresolved symbols. LLVMLibsOptions += -Wl,--no-undefined + endif endif ifeq ($(HOST_OS), Linux) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 9f565444..a2a46e2a 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -13,8 +13,8 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") # is shared by both build systems. set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") -set(NATIVE_CC "${CMAKE_C_COMPILER} -I ${CMAKE_SOURCE_DIR}/include") -set(NATIVE_CXX "${CMAKE_CXX_COMPILER} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") if (ENABLE_KLEE_UCLIBC) set(ENABLE_UCLIBC 1) diff --git a/test/Makefile b/test/Makefile index c96ae889..a2d95056 100644 --- a/test/Makefile +++ b/test/Makefile @@ -74,7 +74,7 @@ lit.site.cfg: lit.site.cfg.in -e "s#@HAVE_SELINUX@#$(HAVE_SELINUX)#g" \ -e "s#@ENABLE_STP@#$(ENABLE_STP)#g" \ -e "s#@ENABLE_Z3@#$(ENABLE_Z3)#g" \ - -e "s#@NATIVE_CC@#$(CC) -I$(PROJ_SRC_ROOT)/include#g" \ - -e "s#@NATIVE_CXX@#$(CXX) -I$(PROJ_SRC_ROOT)/include#g" \ + -e "s#@NATIVE_CC@#$(CC) $(CFLAGS) -I$(PROJ_SRC_ROOT)/include#g" \ + -e "s#@NATIVE_CXX@#$(CXX) $(CXXFLAGS) -I$(PROJ_SRC_ROOT)/include#g" \ -e "s#@LIB_KLEE_RUN_TEST_PATH@#$(SharedLibDir)/$(SharedPrefix)kleeRuntest$(SHLIBEXT)#g" \ $(PROJ_SRC_DIR)/lit.site.cfg.in > $@ |