ci-pr-bench.yml

name: CI Benchmarks

on:
  pull_request:
    branches:
      - master

env:
  CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release

# cancel in-progress job when a new push is performed
concurrency:
  group: ci-pr-bench-${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  benchmark:
    name: Performance benchmarks
    strategy:
      matrix:
        # version: [4.12.0, 4.14.1]
        version: [4.14.1]


    runs-on: ubuntu-22.04

    steps:
    - uses: actions/checkout@v3
      with:
        fetch-depth: 100 # this is to make sure we obtain the target base commit

    - name: System dependencies (ubuntu)
      run: |
        sudo apt install build-essential libgmp-dev z3 opam cmake

    - name: Restore cached opam
      id: cache-opam-restore
      uses: actions/cache/restore@v4
      with:
        path: ~/.opam
        key: ${{ matrix.version }}

    - name: Setup opam
      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
      run: |
        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
        opam install --deps-only --yes ./cerberus-lib.opam
        opam switch create with_coq ${{ matrix.version }}
        eval $(opam env --switch=with_coq)
        opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
        opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
        opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
        opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
        opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git
        opam install --deps-only --yes ./cerberus-lib.opam ./cerberus-cheri.opam

    - name: Save cached opam
      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
      id: cache-opam-save
      uses: actions/cache/save@v4
      with:
        path: ~/.opam
        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}

    - name: Install python dependencies
      run: pip install tabulate

    - name: Install Cerberus
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cerberus-lib .
        opam pin --yes --no-action add cerberus .
        opam install --yes cerberus

    - name: Download cvc5 release
      uses: robinraju/release-downloader@v1
      with:
        repository: cvc5/cvc5
        tag: cvc5-1.1.2
        fileName: cvc5-Linux-static.zip

    - name: Unzip and install cvc5
      run: |
        unzip cvc5-Linux-static.zip
        chmod +x cvc5-Linux-static/bin/cvc5
        sudo cp cvc5-Linux-static/bin/cvc5 /usr/local/bin/

    - name: Install CN
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cn .
        opam install --yes cn ocamlformat.0.26.2

    - name: Set environment variables
      run: |
        echo "BASE_DATA=$(mktemp)" >> $GITHUB_ENV
        echo "PR_DATA=$(mktemp)" >> $GITHUB_ENV
        echo "COMMENT=$(mktemp)" >>  $GITHUB_ENV
        echo "BASE_SHA=$(echo ${{ github.event.pull_request.base.sha }} | cut -c1-8)" >> $GITHUB_ENV
        echo "HEAD_SHA=$(echo ${{ github.event.pull_request.head.sha }} | cut -c1-8)" >> $GITHUB_ENV

    - name: Run benchmark on PR
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh
        mv benchmark-data.json ${{ env.PR_DATA }}
        cd ..

    - name: Switch to target branch
      run: |
        git checkout ${{ github.event.pull_request.base.sha }}

    - name: Install Cerberus
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cerberus-lib .
        opam pin --yes --no-action add cerberus .
        opam install --yes cerberus

    - name: Install CN
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cn .
        opam install --yes cn ocamlformat.0.26.2

    - name: Run benchmark on baseline
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh; mv benchmark-data.json ${{ env.BASE_DATA }}
        cd ..

    - name: Compare results
      run: |
        echo 'Benchmark comparison for [`${{ env.HEAD_SHA }}`](${{ github.event.repository.html_url }}/commit/${{ github.event.pull_request.head.sha }}) (PR) vs [`${{ env.BASE_SHA }}`](${{ github.event.repository.html_url }}/commit/${{ github.event.pull_request.base.sha }}) (baseline).' >> ${{ env.COMMENT }}
        git checkout ${{ github.event.pull_request.head.sha }}
        tests/compare-benchmarks.py ${{ env.BASE_DATA }} ${{ env.PR_DATA }} >> ${{ env.COMMENT }}

    - name: 'Comment PR'
      uses: actions/github-script@v4.0.2
      with:
        github-token: ${{ secrets.GITHUB_TOKEN }}
        script: |
          github.issues.createComment({
            issue_number: context.issue.number,
            owner: context.repo.owner,
            repo: context.repo.repo,
            body: require('fs').readFileSync('${{ env.COMMENT }}').toString()
          });