xen-cbmc: fix ci script

This script has been broken, and not been picked up in CI until now.

This change fixes the script, as well as makes sure that the relevant
steps are executed, and the resulting build artefacts have the required
goto-cc section in them.

This CI script has been refered to as part of the paper:
"Using model checking tools to triage the severity of security bugs in
the Xen hypervisor", that has been presented at FMCAD 2020.

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

Author: nmanthey

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

@@ -1,26 +1,45 @@
-name: Build and Test Xen
+name: Build Xen with CPROVER tools
 
-on: [push]
+on:
+  pull_request:
+    branches: [ develop ]
 
 jobs:
-  Linux:
-
+  CompileXen:
     runs-on: ubuntu-18.04
-
     steps:
-    - name: Install Packages
-      run: sudo apt-get install coreutils \
-        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
+      - 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 install -y coreutils  build-essential gcc git make flex bison software-properties-common libwww-perl python
+          sudo apt-get install -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config
+          sudo apt-get install -y libgtk2.0-dev libyajl-dev sudo time
+
+      - name: Build CBMC tools
+        run: |
+          make -C src minisat2-download
+          make -C src cbmc.dir goto-cc.dir goto-diff.dir
+
+      - name: Get one-line-scan
+        run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git
 
-    - uses: actions/checkout@v1
+      - name: Get Xen 4.13
+        run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 && pwd
 
-    - name: build CBMC tools
-      run: make -C src minisat2-download
-      run: make -C src cbmc.dir goto-cc.dir goto-diff.dir
+      - name: Prepare compile Xen 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: get Xen 4.13
-      run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0
+      - name: Compile Xen with CBMC via one-line-scan, and check for goto-cc section
+        run: 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 xen_4_13 xen -j $(nproc) -k || true
+        
+      - name: Check for goto-cc section in xen-syms binary
+        run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"