diff options
-rw-r--r-- | .travis.yml | 9 | ||||
-rwxr-xr-x | .travis/install-llvm-and-runtime-compiler.sh | 16 | ||||
-rwxr-xr-x | .travis/install-tcmalloc.sh | 23 | ||||
-rwxr-xr-x | .travis/klee.sh | 28 | ||||
-rwxr-xr-x | .travis/stp.sh | 60 | ||||
-rwxr-xr-x | .travis/testing-utils.sh | 12 | ||||
-rwxr-xr-x | .travis/z3.sh | 9 |
7 files changed, 106 insertions, 51 deletions
diff --git a/.travis.yml b/.travis.yml index cd2a9771..3d01b506 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,6 +82,12 @@ env: - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg= +matrix: + include: + - os: osx + osx_image: xcode8.2 + env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0 USE_CMAKE=1 + addons: apt: sources: @@ -103,7 +109,8 @@ before_install: # We assume the Travis image uses Ubuntu 14.04 LTS ########################################################################### # Update package information - - sudo apt-get update + - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi + - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap andreamattavelli/klee; fi ########################################################################### # Set up out of source build directory ########################################################################### diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh index 1068d158..de6f9bbd 100755 --- a/.travis/install-llvm-and-runtime-compiler.sh +++ b/.travis/install-llvm-and-runtime-compiler.sh @@ -1,13 +1,14 @@ #!/bin/bash -x set -ev -sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev -if [ "${LLVM_VERSION}" != "2.9" ]; then + if [ "${LLVM_VERSION}" != "2.9" ]; then sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_VERSION} 20 sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_VERSION} 20 -else + else # Get llvm-gcc. We don't bother installing it wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 tar -xjf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 @@ -27,4 +28,13 @@ else export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu llvm-gcc/bin/llvm-gcc test.c -o hello_world ./hello_world + fi +else # OSX + # NOTE: We should not easily generalize, since we need the corresponding support of bottled formulas + if [ "${LLVM_VERSION}" == "3.4" ]; then + brew install llvm34 + else + echo "Error: Requested to install LLVM ${LLVM_VERSION} on macOS, which is not supported" + exit 1 + fi fi diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh index 5a86380b..a0d825e1 100755 --- a/.travis/install-tcmalloc.sh +++ b/.travis/install-tcmalloc.sh @@ -1,12 +1,19 @@ #!/bin/bash -x set -ev -if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then - # Get tcmalloc release - wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz - tar xfz gperftools-2.4.tar.gz - cd gperftools-2.4 - ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc --enable-minimal --prefix=/usr - make - sudo make install +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then + # Get tcmalloc release + wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz + tar xfz gperftools-2.4.tar.gz + cd gperftools-2.4 + ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc --enable-minimal --prefix=/usr + make + sudo make install + fi +else # OSX + if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then + echo "Error: Requested to install TCMalloc on macOS, which is not supported" + exit 1 + fi fi diff --git a/.travis/klee.sh b/.travis/klee.sh index 61806df3..a2efc70d 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -10,8 +10,13 @@ SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')" # Select the compiler to use to generate LLVM bitcode ############################################################################### if [ "${LLVM_VERSION}" != "2.9" ]; then + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then KLEE_CC=/usr/bin/clang-${LLVM_VERSION} KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION} + else # OSX + KLEE_CC=/usr/local/bin/clang-${LLVM_VERSION} + KLEE_CXX=/usr/local/bin/clang++-${LLVM_VERSION} + fi else # Just use pre-built llvm-gcc downloaded earlier KLEE_CC=${BUILD_DIR}/llvm-gcc/bin/llvm-gcc @@ -117,6 +122,17 @@ fi source ${KLEE_SRC}/.travis/sanitizer_flags.sh ############################################################################### +# Handling LLVM configuration +############################################################################### +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + LLVM_CONFIG="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" + LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION}/build" +else # OSX + LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}" + LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)" +fi + +############################################################################### # KLEE ############################################################################### mkdir klee @@ -139,7 +155,7 @@ if [ "X${USE_CMAKE}" == "X1" ]; then CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ cmake \ - -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \ + -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \ -DLLVMCC="${KLEE_CC}" \ -DLLVMCXX="${KLEE_CXX}" \ ${KLEE_STP_CONFIGURE_OPTION} \ @@ -160,8 +176,8 @@ else # Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged # and is missing the shared library that was supposed to be built that the build # system will try to use by default. - ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ - --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \ + ${KLEE_SRC}/configure --with-llvmsrc=${LLVM_BUILD_DIR} \ + --with-llvmobj=${LLVM_BUILD_DIR} \ --with-llvmcc=${KLEE_CC} \ --with-llvmcxx=${KLEE_CXX} \ ${KLEE_STP_CONFIGURE_OPTION} \ @@ -234,14 +250,14 @@ if [ ${COVERAGE} -eq 1 ]; then cd zcov #these files are not where zcov expects them to be after install so we move them - sudo cp js/sorttable.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sorttable.js - sudo cp js/sourceview.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sourceview.js + sudo cp js/sorttable.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sorttable.js + sudo cp js/sourceview.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sourceview.js sudo cp style.css /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/style.css #install zcov dependency sudo apt-get install -y enscript -#update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause +#update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause #a segmentation fault in v4.6 sudo apt-get install -y ggcov sudo rm /usr/bin/gcov diff --git a/.travis/stp.sh b/.travis/stp.sh index 4cc55c62..412f7613 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -1,46 +1,54 @@ #!/bin/bash -x +# TODO: For OSX we can prepare bottled formulas for STP and minisat + # Make sure we exit if there is a failure 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` + # 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` + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then CFLAGS="${SANITIZER_C_FLAGS}" \ CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ cmake -DCMAKE_INSTALL_PREFIX=/usr .. - make - sudo make install - cd ../../ - - # Build STP - git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src - mkdir build - 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 + else # OSX CFLAGS="${SANITIZER_C_FLAGS}" \ CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src + cmake -DCMAKE_INSTALL_PREFIX=/usr/local .. + fi + make + sudo make install + cd ../../ + + # Build STP + git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src + mkdir build + 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 - make >> "${STP_LOG}" 2>&1 + set +e # Do not exit if build fails because we need to display the log + make >> "${STP_LOG}" 2>&1 else - echo "No STP_VERSION given or empty" - exit 1 + echo "No STP_VERSION given or empty" + exit 1 fi # Only show build output if something went wrong to keep log output short if [ $? -ne 0 ]; then - echo "Build error" - cat "${STP_LOG}" + echo "Build error" + cat "${STP_LOG}" fi diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh index 3d52457f..29295be2 100755 --- a/.travis/testing-utils.sh +++ b/.travis/testing-utils.sh @@ -18,11 +18,16 @@ if [ "${LLVM_VERSION}" != "2.9" ]; then cmake . make # Normally I wouldn't do something like this but hey we're running on a temporary virtual machine, so who cares? - sudo cp lib* /usr/lib/ - sudo cp -r include/gtest /usr/include + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + sudo cp lib* /usr/lib/ + sudo cp -r include/gtest /usr/include + else # OSX + sudo cp lib* /usr/local/lib/ + sudo cp -r include/gtest /usr/local/include + fi else # LLVM2.9 on the other hand is a pain - + # We need the version of GoogleTest used in LLVM2.9 # This is a hack old_dir=`pwd` @@ -45,4 +50,3 @@ else cd "${old_dir}" fi - diff --git a/.travis/z3.sh b/.travis/z3.sh index 10d6be80..f8ae6e0b 100755 --- a/.travis/z3.sh +++ b/.travis/z3.sh @@ -3,12 +3,15 @@ # Make sure we exit if there is a failure set -e -# 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 -# Should we install libz3-dbg too? -sudo apt-get -y install libz3 libz3-dev +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + # Should we install libz3-dbg too? + sudo apt-get -y install libz3 libz3-dev +else # OSX + brew install z3 +fi |