blob: d9fdd02de125f52f579d55b929d93c794af410ff (
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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
FROM ubuntu:14.04
MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk>
# FIXME: Docker doesn't currently offer a way to
# squash the layers from within a Dockerfile so
# the resulting image is unnecessarily large!
ENV LLVM_VERSION=3.4 \
STP_VERSION=UPSTREAM \
DISABLE_ASSERTIONS=0 \
ENABLE_OPTIMIZED=1 \
KLEE_UCLIBC=1 \
KLEE_SRC=/home/klee/klee_src \
COVERAGE=0 \
BUILD_DIR=/home/klee/klee_build
RUN apt-get update && \
apt-get -y --no-install-recommends install \
clang-${LLVM_VERSION} \
llvm-${LLVM_VERSION} \
llvm-${LLVM_VERSION}-dev \
llvm-${LLVM_VERSION}-runtime \
llvm \
libcap-dev \
git \
subversion \
cmake \
make \
libboost-program-options-dev \
python3 \
python3-dev \
python3-pip \
perl \
flex \
bison \
libncurses-dev \
zlib1g-dev \
patch \
wget \
unzip \
binutils && \
pip3 install -U lit tabulate && \
update-alternatives --install /usr/bin/python python /usr/bin/python3 50
# Create ``klee`` user for container with password ``klee``.
# and give it password-less sudo access (temporarily so we can use the TravisCI scripts)
RUN useradd -m klee && \
echo klee:klee | chpasswd && \
cp /etc/sudoers /etc/sudoers.bak && \
echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER klee
WORKDIR /home/klee
# Copy across source files needed for build
RUN mkdir ${KLEE_SRC}
ADD configure \
LICENSE.TXT \
Makefile \
Makefile.* \
README.md \
TODO.txt \
${KLEE_SRC}/
ADD .travis ${KLEE_SRC}/.travis/
ADD autoconf ${KLEE_SRC}/autoconf/
ADD docs ${KLEE_SRC}/docs/
ADD include ${KLEE_SRC}/include/
ADD lib ${KLEE_SRC}/lib/
ADD runtime ${KLEE_SRC}/runtime/
ADD scripts ${KLEE_SRC}/scripts/
ADD test ${KLEE_SRC}/test/
ADD tools ${KLEE_SRC}/tools/
ADD unittests ${KLEE_SRC}/unittests/
ADD utils ${KLEE_SRC}/utils/
# Set klee user to be owner
RUN sudo chown --recursive klee: ${KLEE_SRC}
# Create build directory
RUN mkdir -p ${BUILD_DIR}
# Build STP (use TravisCI script)
RUN cd ${BUILD_DIR} && mkdir stp && cd stp && ${KLEE_SRC}/.travis/stp.sh
# Install testing utils (use TravisCI script)
RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \
${KLEE_SRC}/.travis/testing-utils.sh
# FIXME: This is a nasty hack so KLEE's configure and build finds
# LLVM's headers file, libraries and tools
RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \
sudo ln -s /usr/bin/llvm-config /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-config && \
sudo ln -s /usr/bin/llvm-dis /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-dis && \
sudo ln -s /usr/bin/llvm-as /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-as && \
sudo ln -s /usr/bin/llvm-link /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-link && \
sudo ln -s /usr/bin/llvm-ar /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-ar && \
sudo ln -s /usr/bin/opt /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/opt && \
sudo ln -s /usr/bin/lli /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/lli && \
sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/include && \
sudo ln -s /usr/include/llvm-${LLVM_VERSION}/llvm /usr/lib/llvm-${LLVM_VERSION}/build/include/llvm && \
sudo ln -s /usr/include/llvm-c-${LLVM_VERSION}/llvm-c /usr/lib/llvm-${LLVM_VERSION}/build/include/llvm-c && \
for static_lib in /usr/lib/llvm-3.4/lib/*.a ; do sudo ln -s ${static_lib} /usr/lib/`basename ${static_lib}`; done
# FIXME: This is **really gross**. The Official Ubuntu LLVM packages don't ship
# with ``FileCheck`` or the ``not`` tools so we have to hack building these
# into KLEE's build system in order for the tests to pass
RUN cd ${KLEE_SRC}/tools && \
for tool in FileCheck not; do \
svn export \
http://llvm.org/svn/llvm-project/llvm/branches/release_34/utils/${tool} ${tool} ; \
sed -i 's/^USEDLIBS.*$/LINK_COMPONENTS = support/' ${tool}/Makefile; \
done && \
sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile
# FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist
RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \
sudo ln -s /usr/bin/clang++ /usr/bin/clang++-${LLVM_VERSION}
# Build KLEE (use TravisCI script)
RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/klee.sh
# Revoke password-less sudo and Set up sudo access for the ``klee`` user so it
# requires a password
USER root
RUN mv /etc/sudoers.bak /etc/sudoers && \
echo 'klee ALL=(root) ALL' >> /etc/sudoers
USER klee
# Add KLEE binary directory to PATH
RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc
|
