From 4b46a0a60354419971e35ed3ac744953030da495 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@amazon.de>
Date: Thu, 18 Mar 2021 12:36:29 +0100
Subject: [PATCH 1/2] linux: add compilation script

Script the steps required to build linux, so that they can also be
executed locally.

Signed-off-by: Norbert Manthey <nmanthey@amazon.de>

Signed-off-by: Norbert Manthey <nmanthey@amazon.de>
---
 integration/linux/compile_linux.sh | 86 ++++++++++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100755 integration/linux/compile_linux.sh

diff --git a/integration/linux/compile_linux.sh b/integration/linux/compile_linux.sh
new file mode 100755
index 00000000000..b80c146ba72
--- /dev/null
+++ b/integration/linux/compile_linux.sh
@@ -0,0 +1,86 @@
+#!/bin/bash
+
+# Fail on errors
+# set -e # not for now
+
+# Show steps we execute
+set -x
+
+# This script needs to operate in the root directory of the CBMC repository
+SCRIPT=$(readlink -e "$0")
+readonly SCRIPT
+SCRIPTDIR=$(dirname "$SCRIPT")
+readonly SCRIPTDIR
+cd "$SCRIPTDIR/../.."
+
+# Build CBMC tools
+make -C src minisat2-download
+make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-diff.dir -j$(nproc)
+
+# Get one-line-scan, if we do not have it already
+[ -d one-line-scan ] || git clone https://github.com/awslabs/one-line-scan.git one-line-scan
+
+# Get Linux v5.10, if we do not have it already
+[ -d linux_5_10 ] || git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10
+
+# Prepare compile a part of the kernel with CBMC via one-line-scan
+ln -s goto-cc src/goto-cc/goto-ld
+ln -s goto-cc src/goto-cc/goto-as
+ln -s goto-cc src/goto-cc/goto-g++
+
+
+configure_linux ()
+{
+  pushd linux_5_10
+
+  cat > kvm-config <<EOF
+CONFIG_64BIT=y
+CONFIG_X86_64=y
+CONFIG_HIGH_RES_TIMERS=y
+CONFIG_MULTIUSER=y
+CONFIG_NET=y
+CONFIG_VIRTUALIZATION=y
+CONFIG_HYPERVISOR_GUEST=y
+CONFIG_PARAVIRT=y
+CONFIG_KVM_GUEST=y
+CONFIG_KVM=y
+CONFIG_KVM_INTEL=y
+CONFIG_KVM_AMD=y
+EOF
+  # use the configuration from the generated file
+  export KCONFIG_ALLCONFIG=kvm-config
+
+  # ... and use it during configuration
+  make allnoconfig
+  popd
+}
+
+# Configure kernel, and compile all of it
+configure_linux
+make -C linux_5_10 bzImage -j $(nproc)
+
+# Clean files we want to be able to re-compile
+find linux_5_10/arch/x86/kvm/ -name "*.o" -delete
+
+# Compile Linux with CBMC via one-line-scan, and check for goto-cc section
+# Re-Compile with goto-cc, and measure disk space
+declare -i STATUS=0
+du -h --max-depth=1
+one-line-scan/one-line-scan \
+    --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc \
+    --cbmc \
+    --no-analysis \
+    --trunc-existing \
+    --extra-cflags -Wno-error \
+    -o CPROVER -j 5 -- \
+    make -C linux_5_10 bzImage -j $(nproc) || STATUS=$?
+du -h --max-depth=1
+
+# Check for faulty input
+ls CPROVER/faultyInput/* || true
+
+# Check for produced output in the files we deleted above
+objdump -h linux_5_10/arch/x86/kvm/x86.o | grep "goto-cc" || STATUS=$?
+
+# Propagate failures
+exit "$STATUS"

From 1fbfd5e314cad9b27181bc2f052f8cb8d2120b5f Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@amazon.de>
Date: Thu, 4 Mar 2021 17:27:06 +0100
Subject: [PATCH 2/2] linuxci: test compiling linux

Similarly to Xen, CBMC should be able to compile the linux kernel. As
compiling the full kernel is very time consuming, and with CBMC also
space consuming, only compile a core part all its dependencies, with
the smalles configuration possible. For this core part, we select the
KVM hypervisor.

Once this is working, the configuration, as well as targets to be
compiled can be increased.

When the linuxci fails, we want to be able to easily understand the
failure. The used one-line-scan tool already captures input files that
cannot be handled by goto-cc. Hence, also archives these files for easy
access in the web UI.

Signed-off-by: Norbert Manthey <nmanthey@amazon.de>
---
 .github/workflows/build-and-test-Linux.yaml | 53 +++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 .github/workflows/build-and-test-Linux.yaml

diff --git a/.github/workflows/build-and-test-Linux.yaml b/.github/workflows/build-and-test-Linux.yaml
new file mode 100644
index 00000000000..e1c916dd4f5
--- /dev/null
+++ b/.github/workflows/build-and-test-Linux.yaml
@@ -0,0 +1,53 @@
+name: Build Linux partially with CPROVER tools
+
+on:
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  CompileLinux:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+      - name: Install Packages
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
+          sudo apt-get install --no-install-recommends -y libssl-dev libelf-dev libudev-dev libpci-dev libiberty-dev autoconf
+          sudo apt-get install --no-install-recommends -y gawk jq
+
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-make-${{ github.ref }}-${{ github.sha }}-KERNEL
+          restore-keys: |
+            ${{ runner.os }}-20.04-make-${{ github.ref }}
+            ${{ runner.os }}-20.04-make
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build CBMC tools
+        run: |
+          make -C src minisat2-download
+          make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-diff.dir -j2
+      - name: Print ccache stats
+        run: ccache -s
+
+      - name: Run (Docker Based) Linux Build test
+        run: integration/linux/compile_linux.sh
+
+      - uses: actions/upload-artifact@v2
+        with:
+          name: CPROVER-faultyInput
+          path: CPROVER/faultyInput/*