From 1ffda389d8d20c212884b8a669ebb4cb24f1fa01 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 18 Nov 2016 21:42:57 +0000 Subject: Fix `Feature/MemoryLimit.c` test when building KLEE with ASan. When building with ASan the `mallinfo()` function is intercepted. However the currently implementation is just a stub that always returns 0. So instead use the public API of the sanitizer runtime to get the amount of currently allocated memory when KLEE is built with ASan. Unfortunately it appears that the way to detect building with ASan differs between Clang and GCC. There was also a sanitizer runtime API change too. This was tested with * Clang 3.4, 3.5, and 3.9.0 * GCC 4.8, 4.9, 5.2, 5.4 and, 6.2.1. --- lib/Support/MemoryUsage.cpp | 65 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) 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 #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 + // Modern interface +# define ASAN_GET_ALLOCATED_MEM_FUNCTION __sanitizer_get_current_allocated_bytes +# else +# include + // 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( -- cgit 1.4.1 From 1ffef7b5a0bf78bd4b4a31c626f20e150229d814 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 20 Nov 2016 15:29:26 +0000 Subject: [TravisCI] Modify TravisCI/Docker build scripts to support doing ASan/UBSan builds of KLEE. Two configurations (one for each build system) have been added to TravisCI to do an ASan build. --- .travis.yml | 5 ++++- .travis/klee.sh | 19 +++++++++++++------ .travis/metaSMT.sh | 6 ++++++ .travis/sanitizer_flags.sh | 39 +++++++++++++++++++++++++++++++++++++++ .travis/solvers.sh | 6 ++++++ .travis/stp.sh | 7 +++++++ Dockerfile | 4 +++- 7 files changed, 78 insertions(+), 8 deletions(-) create mode 100644 .travis/sanitizer_flags.sh 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 @@ -111,6 +111,11 @@ else TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc") fi +############################################################################### +# Handle Sanitizer flags +############################################################################### +source ${KLEE_SRC}/.travis/sanitizer_flags.sh + ############################################################################### # 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 \ -- cgit 1.4.1 From 5454dd510f7414989440988c3df85d9bef6852c2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 20 Nov 2016 18:31:35 +0000 Subject: Fix the Autoconf/Makefile build system when building with coverage flags. The old build system stupidly propagates flags for the host C compiler into the flags for the C bitcode compiler leading to unwanted instrumentation being added to KLEE's runtime. --- Makefile.common | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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 -- cgit 1.4.1 From f420cbee41ff68f8229b70e8b3ee9e1f13ed670f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 19 Jan 2017 10:33:18 +0000 Subject: Teach both build systems to pass the user provided CXXFLAGS and CFLAGS when using the native compiler in system tests. This fixes the `libkleeruntest` tests when building with ASan. --- test/CMakeLists.txt | 4 ++-- test/Makefile | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) 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 > $@ -- cgit 1.4.1 From 56afb17888a8330093e6691ae5bb1635b179431d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 19 Jan 2017 11:32:43 +0000 Subject: In legacy build system fix building libkleeRuntest when building with ASan. --- runtime/Runtest/Makefile | 6 ++++++ 1 file changed, 6 insertions(+) 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) -- cgit 1.4.1