[CONTRACTS] Check side effect of loop contracts during instrumentation #9428
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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@v4 | |
| with: | |
| save-always: true | |
| 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 -j4 | |
| - 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 4 -- 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" |