diff options
Diffstat (limited to '.travis')
| -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 |
4 files changed, 207 insertions, 0 deletions
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 + |