Add TravisCI testing infrastructure files.

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
+