1 files changed, 218 insertions, 0 deletions
diff --git a/scripts/build/klee.sh b/scripts/build/klee.sh
new file mode 100755
index 00000000..2b68dd7e
--- /dev/null
+++ b/scripts/build/klee.sh
@@ -0,0 +1,218 @@
+#!/bin/bash -x
+# Compile KLEE
+# Make sure we exit if there is a failure
+set -e
+
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+: ${SOLVERS?"Solvers must be specified"}
+if [[ -z "${KLEE_UCLIBC}" ]]; then
+  echo "KLEE_UCLIBC must be specified: 0 or branch/tag"
+  exit 1
+fi
+if [[ -z "${KLEE_SRC}" ]]; then
+  # Assumeption: this build script is part of the KLEE source tree
+  KLEE_SRC="${DIR}/../.."
+fi
+
+CMAKE_PREFIX_PATH=""
+###############################################################################
+# Handling LLVM configuration
+###############################################################################
+if [[ "$TRAVIS_OS_NAME" = "linux" ]] ; then
+  LLVM_CONFIG="${LLVM_BIN}/llvm-config"
+  LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION_SHORT}/build"
+  KLEE_CC="${LLVM_BIN}/clang"
+  KLEE_CXX="${LLVM_BIN}/clang++"
+elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
+  LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}"
+  LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)"
+  KLEE_CC="/usr/local/bin/clang-${LLVM_VERSION}"
+  KLEE_CXX="/usr/local/bin/clang++-${LLVM_VERSION}"
+else
+  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
+  exit 1
+fi
+
+###############################################################################
+# klee-uclibc
+###############################################################################
+if [ "${KLEE_UCLIBC}" != "0" ]; then
+    KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH="${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" -DENABLE_POSIX_RUNTIME=TRUE)
+else
+    KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE)
+fi
+
+COVERAGE_FLAGS=""
+if [ ${COVERAGE} -eq 1 ]; then
+    COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage'
+fi
+
+
+###############################################################################
+# Handle setting up solver configure flags for KLEE
+###############################################################################
+SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g')
+
+# Set CMake configure options
+KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=OFF)
+KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=OFF)
+KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=OFF)
+for solver in ${SOLVER_LIST}; do
+  echo "Setting CMake configuration option for ${solver}"
+  case ${solver} in
+  STP)
+    KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=TRUE -DSTP_DIR="${BASE}/stp-${STP_VERSION}-install")
+    ;;
+  Z3)
+    echo "Z3"
+    KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=TRUE)
+    if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+    	KLEE_Z3_CONFIGURE_OPTION+=(-DZ3_INCLUDE_DIRS="${BASE}/z3-${Z3_VERSION}-install/include" -DZ3_LIBRARIES="${BASE}/z3-${Z3_VERSION}-install/lib/libz3.so")
+    fi
+    ;;
+  metaSMT)
+    echo "metaSMT"
+    if [ "X${METASMT_DEFAULT}" == "X" ]; then
+      METASMT_DEFAULT=STP
+    fi
+    KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR="${BASE}/metaSMT/build" -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}")
+    ;;
+  *)
+    echo "Unknown solver ${solver}"
+    exit 1
+  esac
+done
+
+###############################################################################
+# Handle additional configure flags
+###############################################################################
+
+TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
+if [[ "$TCMALLOC_OPTION" != "0" ]] ; then
+  if [[ ! -z "${CMAKE_PREFIX_PATH}" ]]; then
+    CMAKE_PREFIX_PATH+=":"
+  fi
+  CMAKE_PREFIX_PATH="${CMAKE_PREFIX_PATH}$BASE/tcmalloc-install"
+fi
+
+###############################################################################
+# KLEE
+###############################################################################
+KLEE_BUILD="${BASE}/klee_build${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX}"
+mkdir -p "${KLEE_BUILD}"
+cd "${KLEE_BUILD}"
+GTEST_SRC_DIR="${BASE}/googletest-release-${GTEST_VERSION}/"
+if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
+  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE"
+else
+  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE"
+fi
+
+if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
+  CMAKE_BUILD_TYPE="RelWithDebInfo"
+else
+  CMAKE_BUILD_TYPE="Debug"
+fi
+
+# TODO: We should support Ninja too
+# Configure KLEE
+echo "CXXFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}\" \
+CFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}\" \
+LDFLAGS=\"${COVERAGE_LDFLAGS} ${SANITIZER_LD_FLAGS}\" \
+cmake \
+  -DLLVM_CONFIG_BINARY=\"${LLVM_CONFIG}\" \
+  -DLLVMCC=\"${KLEE_CC}\" \
+  -DLLVMCXX=\"${KLEE_CXX}\" \
+  ${KLEE_STP_CONFIGURE_OPTION[@]} \
+  ${KLEE_Z3_CONFIGURE_OPTION[@]} \
+  ${KLEE_METASMT_CONFIGURE_OPTION[@]} \
+  ${KLEE_UCLIBC_CONFIGURE_OPTION[@]} \
+  ${TCMALLOC_OPTION[@]} \
+  -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
+  -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
+  ${KLEE_ASSERTS_OPTION[@]} \
+  -DENABLE_UNIT_TESTS=TRUE \
+  -DENABLE_SYSTEM_TESTS=TRUE \
+  -DLIT_ARGS=\"-v\" \
+  ${SANITIZER_CMAKE_C_COMPILER[@]} \
+  ${SANITIZER_CMAKE_CXX_COMPILER[@]} \
+  -DCMAKE_PREFIX_PATH=${CMAKE_PREFIX_PATH} \
+  ${KLEE_SRC}" > "${KLEE_BUILD}/.build_command"
+source "${KLEE_BUILD}/.build_command"
+make -j$(nproc)
+
+###############################################################################
+# Prepare Coverage functionality
+###############################################################################
+coverage_setup()
+{
+  # TODO Remove it and put it to the proper package install section
+  apt update && apt -y --no-install-recommends install lcov
+  # Zero coverage for any file, e.g. previous tests
+  lcov --directory . --no-external --zerocounters
+  # Create a baseline by capturing any file used for compilation, no execution yet
+  lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --initial --output-file coverage_base.info
+  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info
+  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info
+}
+
+coverageup()
+{
+  # Create report
+  # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped)
+  lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --output-file coverage.info
+  # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests)
+  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info
+  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info
+  # Combine baseline and measured coverage
+  lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info
+  # Debug info
+  lcov --rc lcov_branch_coverage=1 --list coverage_all.info
+  # Uploading report to CodeCov
+  bash <(curl -s https://codecov.io/bash) -R "${KLEE_SRC}" -X gcov -y "${KLEE_SRC}/.codecov.yml" -f coverage_all.info -F $1
+}
+
+COVERAGE=${COVERAGE:=0}
+
+###############################################################################
+# Unit tests
+###############################################################################
+# Prepare coverage information if COVERAGE is set
+if [ ${COVERAGE} -eq 1 ]; then
+  coverage_setup
+fi
+make unittests
+
+# Generate and upload coverage if COVERAGE is set
+if [ ${COVERAGE} -eq 1 ]; then
+  coverageup "unittests"
+fi
+
+###############################################################################
+# lit tests
+###############################################################################
+if [ ${COVERAGE} -eq 1 ]; then
+  coverage_setup
+fi
+make systemtests
+
+# If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
+if [ "X${SOLVERS}" == "XmetaSMT" ]; then
+  metasmt_default=$(to_lower $METASMT_DEFAULT) # klee_opts and kleaver_opts use lowercase
+  available_metasmt_backends="btor stp z3 yices2 cvc4"
+  for backend in $available_metasmt_backends; do
+    if [ "X${metasmt_default}" != "X$backend" ]; then
+      if [ "$backend" == "cvc4" ]; then
+        for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done &
+      fi
+      lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/
+    fi
+  done
+fi
+
+# Generate and upload coverage if COVERAGE is set
+if [ ${COVERAGE} -eq 1 ]; then
+  coverageup "systemtests"
+fi