blob: 5c7147c6b30df08dd1c3e5bd7ab9b7ebeee797ba (
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
130
131
132
133
134
|
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 \
SOLVERS=STP:Z3 \
STP_VERSION=2.1.0 \
DISABLE_ASSERTIONS=0 \
ENABLE_OPTIMIZED=1 \
KLEE_UCLIBC=klee_uclibc_v1.0.0 \
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 && \
( wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key | apt-key add - ) && \
echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /' >> /etc/apt/sources.list.d/z3.list && \
apt-get update
# 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 \
MetaSMT.mk \
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/Install SMT solvers (use TravisCI script)
RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.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-${LLVM_VERSION}/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
|
