From 507766ed45a34afca25d44b1dee4e242bce5cc93 Mon Sep 17 00:00:00 2001 From: Elizabeth Polgreen Date: Fri, 29 Jun 2018 09:20:45 +0000 Subject: [PATCH] Docker file to compile Xen To create docker file, run "make" in integration/xen. The Docker file will build CBMC, download Xen upstream version, and one-line-scan, and then attempt to build Xen using goto-cc. --- integration/xen/Dockerfile | 14 +++++++++++ integration/xen/Makefile | 9 +++++++ integration/xen/docker_compile_xen.sh | 34 +++++++++++++++++++++++++++ 3 files changed, 57 insertions(+) create mode 100644 integration/xen/Dockerfile create mode 100644 integration/xen/Makefile create mode 100755 integration/xen/docker_compile_xen.sh diff --git a/integration/xen/Dockerfile b/integration/xen/Dockerfile new file mode 100644 index 0000000000..4b59e3dc6f --- /dev/null +++ b/integration/xen/Dockerfile @@ -0,0 +1,14 @@ +FROM ubuntu:16.04 + +RUN apt-get update && apt-get --no-install-recommends -y install \ + build-essential gcc git make flex bison \ + software-properties-common libwww-perl python \ + bin86 gdb bcc liblzma-dev python-dev gettext iasl \ + uuid-dev libncurses5-dev libncursesw5-dev pkg-config \ + libgtk2.0-dev libyajl-dev sudo time + +ADD integration/xen/docker_compile_xen.sh docker_compile_xen.sh +ADD src /tmp/cbmc/src +RUN ./docker_compile_xen.sh +VOLUME /tmp/cbmc +VOLUME /tmp/xen_compilation diff --git a/integration/xen/Makefile b/integration/xen/Makefile new file mode 100644 index 0000000000..0586098c69 --- /dev/null +++ b/integration/xen/Makefile @@ -0,0 +1,9 @@ +CONTAINER_ID = xen_build_container +IMAGE_ID = xen_image + +all: + if docker ps | grep -q ^$(CONTAINER_ID) ; then \ + docker rm xen_build_container ; \ + fi + cd ../../ && docker build -t $(IMAGE_ID) -f integration/xen/Dockerfile . + docker run -i -t --name $(CONTAINER_ID) $(IMAGE_ID) /bin/bash diff --git a/integration/xen/docker_compile_xen.sh b/integration/xen/docker_compile_xen.sh new file mode 100755 index 0000000000..945ec7be3a --- /dev/null +++ b/integration/xen/docker_compile_xen.sh @@ -0,0 +1,34 @@ +#/bin/bash + +set -e + +cd /tmp/cbmc/src + +make minisat2-download +make -j$(nproc) + +mkdir /tmp/xen_compilation +cd /tmp/xen_compilation +ln -s /tmp/cbmc/src/goto-cc/goto-cc goto-ld +ln -s /tmp/cbmc/src/goto-cc/goto-cc goto-gcc +ln -s /tmp/cbmc/src/goto-cc/goto-cc goto-diff + +git clone https://github.com/awslabs/one-line-scan.git + +git clone git://xenbits.xen.org/xen.git + +export PATH=$(pwd)/one-line-scan/configuration:$PATH +export PATH=$(pwd):$PATH + +cd xen +if one-line-scan \ + --no-analysis --trunc-existing \ + --extra-cflags -Wno-error \ + -o CPROVER -j $(($(nproc)/4)) -- make xen -j$(nproc) +then + echo "SUCCESS: Compilation of Xen succeeded" +else + echo -n "FAILED: Compilation of Xen failed." + echo -n " The build log can be found in" + echo " /tmp/xen_compilation/xen/CPROVER/build.log" +fi