about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2017-02-13 22:32:07 +0000
committerGitHub <noreply@github.com>2017-02-13 22:32:07 +0000
commit13d8b4cb78c81bff97501cbe586f0fd8f1adc4d2 (patch)
tree424398f1dac3f76b85592940b1af30f4fec14b99
parent950c823ddec56d59edb88e6ef81ba541aa5a34df (diff)
parent56afb17888a8330093e6691ae5bb1635b179431d (diff)
downloadklee-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.yml5
-rwxr-xr-x.travis/klee.sh19
-rwxr-xr-x.travis/metaSMT.sh6
-rw-r--r--.travis/sanitizer_flags.sh39
-rwxr-xr-x.travis/solvers.sh6
-rwxr-xr-x.travis/stp.sh7
-rw-r--r--Dockerfile4
-rw-r--r--Makefile.common10
-rw-r--r--lib/Support/MemoryUsage.cpp65
-rw-r--r--runtime/Runtest/Makefile6
-rw-r--r--test/CMakeLists.txt4
-rw-r--r--test/Makefile4
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 > $@