diff options
| -rw-r--r-- | .travis.yml | 69 | ||||
| -rwxr-xr-x | .travis/klee.sh | 103 | ||||
| -rw-r--r-- | .travis/stp-r940-smtlib2.y.patch | 24 | ||||
| -rwxr-xr-x | .travis/stp.sh | 40 | ||||
| -rwxr-xr-x | .travis/testing-utils.sh | 40 |
5 files changed, 276 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 00000000..a5d7a06e --- /dev/null +++ b/.travis.yml @@ -0,0 +1,69 @@ +language: cpp +compiler: + - clang + - gcc +env: + ########################################################################### + # Configurations + # + # Each line in the "env" section represents a set of environmental variables + # pass to a build. Thus each line represents a different build + ########################################################################### + # FIXME: I want to enable assertions but I can't because Release+Asserts build fails + # Release builds + # FIXME: Enable when we want to test LLVM3.5 + #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + # FIXME: Do Debug+Asserts builds +cache: apt +before_install: + # Assume Travis image uses Ubuntu 12.04 LTS + - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' + - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' + - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' + - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' + - sudo add-apt-repository -y ppa:ubuntu-sdk-team/ppa + - sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test/ + - wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add - + # Needed for new libstdc++ and gcc4.8 + - sudo apt-get update + # FIXME: STP doesn't need everything from Boost! + - sudo apt-get install gcc-4.8 g++-4.8 libcap-dev cmake libboost-all-dev + # Make gcc4.8 the default gcc version + - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 20 + - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 20 + - sudo apt-get install llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev clang-3.4 + # Make Clang3.4 the default clang version (for building KLEE) + - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.4 20 + - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.4 20 + # Install lit (llvm-lit is not available) + - sudo pip install lit + # Gross! tools/klee/Makefile depends on "bc" + - sudo apt-get install bc + # Setup out of source build + - export KLEE_SRC=`pwd` + - cd ../ + - mkdir build + - cd build/ + - export BUILD_DIR=`pwd` + # Build STP + - mkdir stp + - cd stp + - ${KLEE_SRC}/.travis/stp.sh + - cd ../ +script: + # Get need utlities/libraries for testing KLEE + - mkdir test-utils/ + - cd test-utils/ + - ${KLEE_SRC}/.travis/testing-utils.sh + - cd ../ + # Build KLEE + - ${KLEE_SRC}/.travis/klee.sh diff --git a/.travis/klee.sh b/.travis/klee.sh new file mode 100755 index 00000000..0853d0e8 --- /dev/null +++ b/.travis/klee.sh @@ -0,0 +1,103 @@ +#!/bin/bash -x +# Make sure we exit if there is a failure +set -e + +# Travis doesn't seem to like this in the yaml file so put it here instead +[ "${LLVM_VERSION}" != "2.9" ] && sudo apt-get install llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} + +# Calculate LLVM branch name to retrieve missing files from +SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')" + +############################################################################### +# Select the compiler to use to generate LLVM bitcode +############################################################################### +if [ "${LLVM_VERSION}" != "2.9" ]; then + KLEE_CC=/usr/bin/clang-${LLVM_VERSION} + KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION} +else + # Just use pre-built llvm-gcc. + wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 || exit + tar -xjf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 + KLEE_CC=$(pwd)/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-gcc + KLEE_CXX=$(pwd)/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-g++ + export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu + export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu + + # Add symlinks to fix llvm-2.9-dev package so KLEE can configure properly + # Because of the way KLEE's configure script works this must be a relative + # symlink, **not** absolute! + sudo sh -c 'cd /usr/lib/llvm-2.9/build/ && ln -s ../ Release' + sudo sh -c 'cd /usr/lib/llvm-2.9/build/ && ln -s ../include include' +fi + +############################################################################### +# klee-uclibc +############################################################################### +if [ "${KLEE_UCLIBC}" -eq 1 ]; then + git clone --depth 1 git://github.com/klee/klee-uclibc.git + cd klee-uclibc + ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION} + make + KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --with-posix-runtime" + cd ../ +else + KLEE_UCLIBC_CONFIGURE_OPTION="" +fi + +############################################################################### +# KLEE +############################################################################### +mkdir klee +cd klee + +# Build KLEE +# 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 \ + --with-llvmcc=${KLEE_CC} \ + --with-llvmcxx=${KLEE_CXX} \ + --with-stp="${BUILD_DIR}/stp/build" \ + ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 + +############################################################################### +# Testing +############################################################################### + +############################################################################### +# Unit tests +############################################################################### +# The unittests makefile doesn't seem to have been packaged so get it from SVN +sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ +svn export http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \ + ../Makefile.unittest +sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ + + +make unittests ENABLE_SHARED=0 +RETURN="$?" + +############################################################################### +# lit tests +############################################################################### +# Note can't use ``make check`` because llvm-lit is not available +cd test +# The build system needs to generate this file before we can run lit +make lit.site.cfg +# Running is parallel is broken and there's no point on our "single core" VM anyway + +set +e # We want to let all the tests run before we exit +lit -v -j1 . +RETURN="${RETURN}$?" + +############################################################################### +# Result +############################################################################### +if [ "${RETURN}" != "00" ]; then + echo "Running tests failed" + exit 1 +fi diff --git a/.travis/stp-r940-smtlib2.y.patch b/.travis/stp-r940-smtlib2.y.patch new file mode 100644 index 00000000..212c0180 --- /dev/null +++ b/.travis/stp-r940-smtlib2.y.patch @@ -0,0 +1,24 @@ +diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y +index a94bd6c..5263bf5 100644 +--- a/src/parser/smtlib2.y ++++ b/src/parser/smtlib2.y +@@ -64,6 +64,7 @@ + FatalError(""); + return 1; + } ++ int yyerror(void* AssertsQuery, const char* s) { return yyerror(s); } + + ASTNode querysmt2; + ASTVec assertionsSMT2; +@@ -72,9 +73,10 @@ + #define YYMAXDEPTH 104857600 + #define YYERROR_VERBOSE 1 + #define YY_EXIT_FAILURE -1 +-#define YYPARSE_PARAM AssertsQuery + %} + ++%parse-param {void* AssertsQuery} ++ + %union { + unsigned uintval; /* for numerals in types. */ + //ASTNode,ASTVec diff --git a/.travis/stp.sh b/.travis/stp.sh new file mode 100755 index 00000000..94bbab4d --- /dev/null +++ b/.travis/stp.sh @@ -0,0 +1,40 @@ +#!/bin/bash -x + +# Make sure we exit if there is a failure +set -e + +if [ "${STP_VERSION}" == "UPSTREAM" ]; then + git clone --depth 1 git://github.com/stp/stp.git src + mkdir build + cd build + # Disabling building of shared libs is a workaround + cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF ../src + # Don't try to build stp executable, there's an issue with using gcc4.8 with boost libraries built with gcc4.6 + make libstp CopyPublicHeaders +elif [ "${STP_VERSION}" == "r940" ]; then + # Building the old "r940" version that for some reason we love so much! + git clone git://github.com/stp/stp.git src_build + mkdir build # This is actually the install directory + cd src_build/ + git checkout bc78d1f9f06fc095bd1ddad90eacdd1f05f64dae # r940 + + # Fixes for GCC + # We don't try to fix clang compilation because there too many things that need + # fixing and it isn't really r940 anymore if we start doing that + git config --global user.name "travis" + git config --global user.email "travis@travis.123" + git cherry-pick ece1a55fb367bd905078baca38476e35b4df06c3 + patch -p1 -i ${KLEE_SRC}/.travis/stp-r940-smtlib2.y.patch + + # Oh man this project is so broken. The binary build directory is missing + mkdir -p bin + + export CC=gcc + export CXX=g++ + ./scripts/configure --with-prefix=${BUILD_DIR}/stp/build --with-cryptominisat2 + echo "WARNING FORCING GCC TO BE USED TO COMPILE STP" + make OPTIMIZE=-O2 CFLAGS_M32= install +else + echo "Unsupported STP_VERSION" + exit 1 +fi diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh new file mode 100755 index 00000000..27bd420d --- /dev/null +++ b/.travis/testing-utils.sh @@ -0,0 +1,40 @@ +#!/bin/bash -x +# Make sure we exit if there is a failure +set -e + +if [ "${LLVM_VERSION}" != "2.9" ]; then + # Using LLVM3.4 all we need is vanilla GoogleTest :) + wget https://googletest.googlecode.com/files/gtest-1.7.0.zip + unzip gtest-1.7.0.zip + cd gtest-1.7.0/ + 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 +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` + cd "${KLEE_SRC}" + cd tools/ + svn export http://llvm.org/svn/llvm-project/llvm/branches/release_29/utils/unittest unittest + + # Now put the header files in the search path so building will succeed + sudo cp -r unittest/googletest/include/gtest /usr/include/ + + # We need the FileCheck and not utilites as well because they aren't in the llvm-2.9-dev package + for tool in FileCheck not; do + svn export http://llvm.org/svn/llvm-project/llvm/branches/release_29/utils/${tool} ${tool} + # Patch the Makefile so it will work in KLEE's build system + sed -i 's/^USEDLIBS.*$/LINK_COMPONENTS = support/' ${tool}/Makefile + done + + # Now hack the make file to build the unittest library and the FileCheck and not tools + sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += unittest FileCheck not' Makefile + + cd "${old_dir}" +fi + |