about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--.travis.yml9
-rwxr-xr-x.travis/install-llvm-and-runtime-compiler.sh16
-rwxr-xr-x.travis/install-tcmalloc.sh23
-rwxr-xr-x.travis/klee.sh28
-rwxr-xr-x.travis/stp.sh60
-rwxr-xr-x.travis/testing-utils.sh12
-rwxr-xr-x.travis/z3.sh9
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