Continuous docker

integration/linux/Dockerfile

@@ -0,0 +1,8 @@
+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 bc \
+        libgtk2.0-dev libyajl-dev sudo time libelf-dev openssl libssl-dev

integration/linux/Makefile

@@ -0,0 +1,2 @@
+all:
+	bash -x ./compile_linux_via_docker.sh

integration/linux/compile_linux_one_line_scan.sh

@@ -0,0 +1,37 @@
+#!/bin/bash
+#
+# build linux with the goto-gcc compiler
+
+# abort on failure, and show what we're doing
+set -ex
+
+# locate the script to be able to call related scripts
+SCRIPT="$(readlink -e "$0")"
+SCRIPTDIR="$(dirname "$SCRIPT")"
+
+# make sure we work from the correct directory
+pushd "$SCRIPTDIR"
+
+# make tools available in PATH
+export PATH=$PATH:$(readlink -e bin)
+
+# configure build before we move on
+pushd linux
+make x86_64_defconfig
+make kvmconfig
+popd
+
+make -C x86_64_defconfig
+make -C kvmconfig
+
+# build linux with the goto-gcc compiler
+declare -i COMPILE_STATUS=0
+# for now, do not consider Werror, to do so, add '--extra-cflags -Wno-error'
+one-line-scan \
+    --no-analysis --trunc-existing \
+    -o CPROVER-linux -j $(($(nproc)/4)) -- \
+    make -C linux all -j $(nproc) -k -B || COMPILE_STATUS=$?
+
+popd
+
+exit $COMPILE_STATUS

integration/linux/compile_linux_via_docker.sh

@@ -0,0 +1,127 @@
+#!/bin/bash
+
+# abort on failure, and show what we're doing
+set -ex
+
+# locate the script to be able to call related scripts
+SCRIPT="$(readlink -e "$0")"
+SCRIPTDIR="$(dirname "$SCRIPT")"
+
+DOCKERFILE=$(readlink -e "$SCRIPTDIR"/Dockerfile)
+
+# make sure we have what we need
+assert_environment()
+{
+    if ! command -v docker &> /dev/null
+    then
+        echo "error: docker not found, abort"
+        exit 1
+    fi
+
+    if [ ! -r $DOCKERFILE ]
+    then
+        echo "error: cannot read Dockerfile $DOCKERFILE, abort"
+        exit 1
+    fi
+
+    # test whether we can build the container and run a simple command
+    pushd "$SCRIPTDIR"/../..
+    scripts/run_in_container.sh "$DOCKERFILE" ls integration/linux
+    popd
+}
+
+# get a recent copy of one-line-scan
+get_one_line_scan ()
+{
+    rm -rf one-line-scan
+    git clone https://github.com/awslabs/one-line-scan.git
+}
+
+# get a local copy of the linux repository, and jump to origin/master
+get_and_update_linux ()
+{
+    [ -d linux ] || git clone https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux
+    pushd linux
+    git fetch origin
+    git checkout origin/master
+    popd
+}
+
+# setup CBMC to be used in one-line-scan
+setup_cbmc_in_container ()
+{
+    pushd "$SCRIPTDIR"/../..
+    scripts/run_in_container.sh "$DOCKERFILE" make -C src minisat2-download
+    scripts/run_in_container.sh "$DOCKERFILE" make -C src -j$(nproc)
+    popd
+}
+
+# setup PATH to have all tools
+setup_PATH ()
+{
+    mkdir -p bin
+    pushd bin
+    rm -rf ./*
+
+    # create all links we might need
+    ln -s ../../../src/goto-cc/goto-cc goto-ar
+    ln -s ../../../src/goto-cc/goto-cc goto-as
+    ln -s ../../../src/goto-cc/goto-cc goto-diff
+    ln -s ../../../src/goto-cc/goto-cc goto-gcc
+    ln -s ../../../src/goto-cc/goto-cc goto-ld
+
+    ln -s ../one-line-scan/one-line-scan one-line-scan
+
+    # actually update the PATH variable
+    export PATH=$PATH:$(readlink -e .)
+
+    popd
+}
+
+compile_linux_in_container ()
+{
+    pushd "$SCRIPTDIR"/../..
+
+    pwd
+
+    # make sure we start fresh
+    scripts/run_in_container.sh "$DOCKERFILE" make -C integration/linux/linux clean
+
+    # build linux with the goto-gcc compiler
+    declare -i COMPILE_STATUS=0
+    scripts/run_in_container.sh "$DOCKERFILE" integration/linux/compile_linux_one_line_scan.sh || COMPILE_STATUS=$?
+
+    popd
+
+    return $COMPILE_STATUS
+}
+
+# steps to execute
+
+assert_environment
+
+get_one_line_scan
+
+get_and_update_linux
+
+setup_cbmc_in_container
+
+# setup path
+setup_PATH
+
+# compile linux
+declare -i COMPILE_STATUS
+COMPILE_STATUS=0
+compile_linux_in_container || COMPILE_STATUS=$?
+
+# evaluate
+if [ "$COMPILE_STATUS" -eq 0 ]
+then
+  echo "SUCCESS: Compilation of linux succeeded"
+else
+  echo -n "FAILED: Compilation of Linux failed."
+  echo -n " The build log can be found in"
+  echo " CPROVER-linux/build.log"
+fi
+
+exit $COMPILE_STATUS

integration/xen/Dockerfile

@@ -6,10 +6,3 @@ RUN apt-get update && apt-get --no-install-recommends -y install \
         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
-ADD scripts /tmp/cbmc/scripts
-RUN ./docker_compile_xen.sh
-VOLUME /tmp/cbmc
-VOLUME /tmp/xen_compilation

integration/xen/Makefile

@@ -1,9 +1,2 @@
-CONTAINER_ID = xen_build_container
-IMAGE_ID = xen_image
-
 all:
-	if docker ps -a | grep -wq $(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
+	bash -x ./compile_xen_via_docker.sh

integration/xen/compile_xen_one_line_scan.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+#
+# build xen with the goto-gcc compiler
+
+# abort on failure, and show what we're doing
+set -ex
+
+# locate the script to be able to call related scripts
+SCRIPT="$(readlink -e "$0")"
+SCRIPTDIR="$(dirname "$SCRIPT")"
+
+# make sure we work from the correct directory
+pushd "$SCRIPTDIR"
+
+# make tools available in PATH
+export PATH=$PATH:$(readlink -e bin)
+
+# build xen with the goto-gcc compiler
+declare -i COMPILE_STATUS=0
+one-line-scan \
+    --no-analysis --trunc-existing \
+    --extra-cflags -Wno-error \
+    -o CPROVER-xen -j $(($(nproc)/4)) -- \
+    make -C xen xen -j $(nproc) -k -B || COMPILE_STATUS=$?
+
+popd
+
+exit $COMPILE_STATUS

integration/xen/compile_xen_via_docker.sh

@@ -0,0 +1,127 @@
+#!/bin/bash
+
+# abort on failure, and show what we're doing
+set -ex
+
+# locate the script to be able to call related scripts
+SCRIPT="$(readlink -e "$0")"
+SCRIPTDIR="$(dirname "$SCRIPT")"
+
+DOCKERFILE=$(readlink -e "$SCRIPTDIR"/Dockerfile)
+
+# make sure we have what we need
+assert_environment()
+{
+    if ! command -v docker &> /dev/null
+    then
+        echo "error: docker not found, abort"
+        exit 1
+    fi
+
+    if [ ! -r $DOCKERFILE ]
+    then
+        echo "error: cannot read Dockerfile $DOCKERFILE, abort"
+        exit 1
+    fi
+
+    # test whether we can build the container and run a simple command
+    pushd "$SCRIPTDIR"/../..
+    scripts/run_in_container.sh "$DOCKERFILE" ls integration/xen
+    popd
+}
+
+# get a recent copy of one-line-scan
+get_one_line_scan ()
+{
+    rm -rf one-line-scan
+    git clone https://github.com/awslabs/one-line-scan.git
+}
+
+# get a local copy of the xen repository, and jump to origin/master
+get_and_update_xen ()
+{
+    [ -d xen ] || git clone git://xenbits.xen.org/xen.git
+    pushd xen
+    git fetch origin
+    git checkout origin/master
+    popd
+}
+
+# setup CBMC to be used in one-line-scan
+setup_cbmc_in_container ()
+{
+    pushd "$SCRIPTDIR"/../..
+    scripts/run_in_container.sh "$DOCKERFILE" make -C src minisat2-download
+    scripts/run_in_container.sh "$DOCKERFILE" make -C src -j$(nproc)
+    popd
+}
+
+# setup PATH to have all tools
+setup_PATH ()
+{
+    mkdir -p bin
+    pushd bin
+    rm -rf ./*
+
+    # create all links we might need
+    ln -s ../../../src/goto-cc/goto-cc goto-ar
+    ln -s ../../../src/goto-cc/goto-cc goto-as
+    ln -s ../../../src/goto-cc/goto-cc goto-diff
+    ln -s ../../../src/goto-cc/goto-cc goto-gcc
+    ln -s ../../../src/goto-cc/goto-cc goto-ld
+
+    ln -s ../one-line-scan/one-line-scan one-line-scan
+
+    # actually update the PATH variable
+    export PATH=$PATH:$(readlink -e .)
+
+    popd
+}
+
+compile_xen_in_container ()
+{
+    pushd "$SCRIPTDIR"/../..
+
+    pwd
+
+    # make sure we start fresh
+    scripts/run_in_container.sh "$DOCKERFILE" make -C integration/xen/xen clean
+
+    # build xen with the goto-gcc compiler
+    declare -i COMPILE_STATUS=0
+    scripts/run_in_container.sh "$DOCKERFILE" integration/xen/compile_xen_one_line_scan.sh || COMPILE_STATUS=$?
+
+    popd
+
+    return $COMPILE_STATUS
+}
+
+# steps to execute
+
+assert_environment
+
+get_one_line_scan
+
+get_and_update_xen
+
+setup_cbmc_in_container
+
+# setup path
+setup_PATH
+
+# compile xen
+declare -i COMPILE_STATUS
+COMPILE_STATUS=0
+compile_xen_in_container || COMPILE_STATUS=$?
+
+# evaluate
+if [ "$COMPILE_STATUS" -eq 0 ]
+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 " CPROVER-xen/build.log"
+fi
+
+exit $COMPILE_STATUS