build-and-test-Xen.yaml

name: Build Xen with CPROVER tools

on:
  pull_request:
    branches: [ develop ]

jobs:
  # This job takes approximately 33 minutes
  CompileXen:
    runs-on: ubuntu-20.04
    steps:
      - uses: actions/checkout@v4
        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 build-essential git 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 time ccache clang-10 clang++-10

      - name: Prepare ccache
        uses: actions/cache@v3
        with:
          path: .ccache
          key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-XEN
          restore-keys: |
            ${{ runner.os }}-20.04-make-clang-${{ github.ref }}
            ${{ runner.os }}-20.04-make-clang
      - 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/clang++' 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 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)
        
      - name: Check for goto-cc section in xen-syms binary
        run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"

      - name: Show goto-cc properties
        run:  $(pwd)/src/cbmc/cbmc --show-properties xen_4_13/xen/xen-syms

      - name: Show some goto-cc functions
        run:  $(pwd)/src/cbmc/cbmc --list-goto-functions xen_4_13/xen/xen-syms | grep "arch"