Merge pull request #2504 from polgreen/docker_file_for_xen

Compiling Xen with CBMC: docker file "expensive regression test"

Author: tautschnig

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

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

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