about summary refs log tree commit diff homepage
path: root/.travis/klee.sh
blob: 012262c6b8b9e847ff4fa87fcbcf526060021bdd (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
#!/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 \
    DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
    ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
    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