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 single file and all its dependencies,
with the smalles configuration possible.

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

Signed-off-by: Norbert Manthey <[email protected]>

Author: nmanthey

.github/workflows/build-and-test-Linux.yaml

@@ -0,0 +1,75 @@
+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 coreutils  build-essential gcc git make flex bison software-properties-common curl python
+          sudo apt-get install --no-install-recommends -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config
+          sudo apt-get install --no-install-recommends -y libgtk2.0-dev libyajl-dev sudo time ccache
+          sudo apt-get install --no-install-recommends -y automake bc libssl-dev dkms libelf-dev libudev-dev libpci-dev libiberty-dev autoconf 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: Get one-line-scan
+        run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git
+
+      - name: Get Linux v5.10
+        run: git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10
+
+      - name: Prepare compile a part of the kernel with CBMC via one-line-scan
+        run: |
+          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++
+
+      - name: Compile Linux with CBMC via one-line-scan, and check for goto-cc section
+        run: |
+          ls
+          make -C linux_5_10 allnoconfig
+          make -C linux_5_10 kvm_guest.config
+          make -C linux_5_10 bzImage -j $(nproc)
+          du -h . --max-depth=1
+          rm "linux_5_10/arch/x86/kernel/kvm.o"
+          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 --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C linux_5_10 bzImage -j $(nproc) -k || true
+          du -h . --max-depth=1
+        
+      - name: Check for faulty input
+        run: ls CPROVER/faultyInput/* || true
+
+      - name: Check for goto-cc section in a created file
+        run: objdump -h linux_5_10/arch/x86/kernel/kvm.o | grep "goto-cc"