workflow: fix xen

.github/workflows/README.md

@@ -1,4 +1,4 @@
-# CBMC packages
+# CBMC packages 
 
 This project builds installation packages for the tip of the develop
 branch for MacOS, Windows, and Ubuntu.

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

@@ -0,0 +1,39 @@
+name: Build and Test Xen
+
+on:
+  pull_request:
+    branches: [ develop ]
+
+jobs:
+  CompileXen:
+    runs-on: ubuntu-18.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 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
+      - 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: 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: 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"

.github/workflows/pull-request-checks.yaml

@@ -176,3 +176,38 @@ jobs:
       - uses: actions/checkout@v2
       - name: Check for unused irep ids
         run: ./scripts/string_table_check.sh
+
+  CompileXen:
+    runs-on: ubuntu-18.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 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
+    - 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 https://github.com/awslabs/one-line-scan.git
+    - 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
+      run: |
+        ls
+        pwd
+        ls src/*
+        ln -sf src/goto-cc/goto-cc src/goto-cc/goto-ld
+        ln -sf src/goto-cc/goto-cc src/goto-cc/goto-as
+        ln -sf src/goto-cc/goto-cc src/goto-cc/goto-g++
+        PATH=$PATH:src/cbmc:src/goto-cc one-line-scan/one-line-scan --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k