From 3ff5259b1936da3a7b84caaee3c7d9ed9a712bcd Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@amazon.de>
Date: Mon, 8 Jul 2019 15:56:52 +0200
Subject: [PATCH 1/3] docker: add generic run script

This script allows to run commands inside a Docker container easily.
The current directory, as well as the home directory are mounted inside
the container, and the user id of the calling user is used, or, in case
sudo is specified, the root user will be chosen.

This way, file write operations inside the container can be visible to
the outside, which allows to debug more easily, e.g. build failures.
---
 scripts/run_in_container.sh | 45 +++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100755 scripts/run_in_container.sh

diff --git a/scripts/run_in_container.sh b/scripts/run_in_container.sh
new file mode 100755
index 00000000000..3e4370cac4a
--- /dev/null
+++ b/scripts/run_in_container.sh
@@ -0,0 +1,45 @@
+#!/usr/bin/env bash
+#
+# Copyright Norbert Manthey, 2019
+
+# Run commands inside container
+#
+# Usage:
+# ./scripts/run_in_container "<path>/Dockerfile" command with args
+#
+# In case the environment variable CONTAINER is set already, the value of that
+# variable will be used as the image to use. Otherwise, the provided Dockerfile
+# will be used to create the image to be used in this script.
+
+set -ex
+DOCKERFILE="$1"  # Dockerfile
+shift
+
+USER_FLAGS="-e USER="$(id -u)" -u=$(id -u)"
+
+# disable getting the source again
+if [ -z "$1" ] || [ "$1" = "sudo" ]
+then
+	USER_FLAGS=""
+	shift
+fi
+
+if [ ! -r "$DOCKERFILE" ]
+then
+	echo "cannot find $DOCKERFILE (in $(readlink -e .)), abort"
+	exit 1
+fi
+
+DOCKERFILE_DIR=$(dirname "$DOCKERFILE")
+CONTAINER="${CONTAINER:-}"
+[ -n "$CONTAINER" ] || CONTAINER=$(docker build -q -f "$DOCKERFILE" "$DOCKERFILE_DIR")
+
+echo "running in container: $CONTAINER"
+
+docker run \
+  -t \
+  $USER_FLAGS \
+  -v $HOME:$HOME \
+  -v $(pwd):$(pwd) \
+  -w $(pwd) \
+  "$CONTAINER" "$@"

From cca54e92e1ea57873e49b83f56c000d90996d321 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@amazon.de>
Date: Mon, 8 Jul 2019 15:59:46 +0200
Subject: [PATCH 2/3] docker: improve xen files

The existing solution to build Xen did not allow to easily retrieve
the build artifacts after the build, not files that allow to work
on bug fixes in the tool chain. The new approach builds Xen inside
the CBMC tree, so that all files are available afterwards.

Note, CBMC is also build within the container, so that the relevant
tools can be used inside the container as well.
---
 integration/xen/Dockerfile                   |   7 -
 integration/xen/Makefile                     |   9 +-
 integration/xen/compile_xen_one_line_scan.sh |  28 ++++
 integration/xen/compile_xen_via_docker.sh    | 127 +++++++++++++++++++
 integration/xen/docker_compile_xen.sh        |  34 -----
 5 files changed, 156 insertions(+), 49 deletions(-)
 create mode 100755 integration/xen/compile_xen_one_line_scan.sh
 create mode 100755 integration/xen/compile_xen_via_docker.sh
 delete mode 100755 integration/xen/docker_compile_xen.sh

diff --git a/integration/xen/Dockerfile b/integration/xen/Dockerfile
index e4b487826b3..65182882701 100644
--- a/integration/xen/Dockerfile
+++ b/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
diff --git a/integration/xen/Makefile b/integration/xen/Makefile
index b2c5e05c563..2b7995b121e 100644
--- a/integration/xen/Makefile
+++ b/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
diff --git a/integration/xen/compile_xen_one_line_scan.sh b/integration/xen/compile_xen_one_line_scan.sh
new file mode 100755
index 00000000000..3c561fe9f47
--- /dev/null
+++ b/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
diff --git a/integration/xen/compile_xen_via_docker.sh b/integration/xen/compile_xen_via_docker.sh
new file mode 100755
index 00000000000..7a42a68835b
--- /dev/null
+++ b/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
diff --git a/integration/xen/docker_compile_xen.sh b/integration/xen/docker_compile_xen.sh
deleted file mode 100755
index 945ec7be3af..00000000000
--- a/integration/xen/docker_compile_xen.sh
+++ /dev/null
@@ -1,34 +0,0 @@
-#/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

From a15047b0870f1154c2a155ddd10666c1098d48a5 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@amazon.de>
Date: Mon, 8 Jul 2019 16:02:16 +0200
Subject: [PATCH 3/3] docker: add files to compile Linux

We are interested in being able to compile the Linux kernel with
goto-gcc. To not be required to have all tools available on a local
machine, this change provides a docker setup that allows to build
the Linux kernel natively, as well as with goto-gcc via the
wrapper one-line-scan.

Similarly to the Xen tooling, the build files, as well as logs and
files for debugging are accessible after the run is complete.
---
 integration/linux/Dockerfile                  |   8 ++
 integration/linux/Makefile                    |   2 +
 .../linux/compile_linux_one_line_scan.sh      |  37 +++++
 integration/linux/compile_linux_via_docker.sh | 127 ++++++++++++++++++
 4 files changed, 174 insertions(+)
 create mode 100644 integration/linux/Dockerfile
 create mode 100644 integration/linux/Makefile
 create mode 100755 integration/linux/compile_linux_one_line_scan.sh
 create mode 100755 integration/linux/compile_linux_via_docker.sh

diff --git a/integration/linux/Dockerfile b/integration/linux/Dockerfile
new file mode 100644
index 00000000000..4f7f36949ab
--- /dev/null
+++ b/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
diff --git a/integration/linux/Makefile b/integration/linux/Makefile
new file mode 100644
index 00000000000..0b108dbec84
--- /dev/null
+++ b/integration/linux/Makefile
@@ -0,0 +1,2 @@
+all:
+	bash -x ./compile_linux_via_docker.sh
diff --git a/integration/linux/compile_linux_one_line_scan.sh b/integration/linux/compile_linux_one_line_scan.sh
new file mode 100755
index 00000000000..18f66654446
--- /dev/null
+++ b/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
diff --git a/integration/linux/compile_linux_via_docker.sh b/integration/linux/compile_linux_via_docker.sh
new file mode 100755
index 00000000000..a153131643e
--- /dev/null
+++ b/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