bench.yml

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
#
# Run performance benchmarks comparing two different Kani versions.
# This workflow takes much longer than other workflows, so we don't run it by default.
# This workflow will run when:
#  - Changes are pushed to 'main'.
#  - Triggered by another workflow
name: Kani Performance Benchmarks
on:
  push:
    branches:
      - 'main'
  workflow_call:

jobs:
  perf-benchcomp:
    runs-on: ubuntu-20.04
    steps:
      - name: Save push event HEAD and HEAD~ to environment variables
        if: ${{ github.event_name == 'push' }}
        run: |
          echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
          echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"

      - name: Save pull request HEAD and base to environment variables
        if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }}
        run: |
          echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
          echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"

      - name: Check out Kani (old variant)
        uses: actions/checkout@v4
        with:
          path: ./old
          ref: ${{ env.OLD_REF }}
          fetch-depth: 2

      - name: Check out Kani (new variant)
        uses: actions/checkout@v4
        with:
          path: ./new
          ref: ${{ env.NEW_REF }}
          fetch-depth: 1

      - name: Set up Kani Dependencies (old variant)
        uses: ./old/.github/actions/setup
        with:
          os: ubuntu-20.04
          kani_dir: old

      - name: Set up Kani Dependencies (new variant)
        uses: ./new/.github/actions/setup
        with:
          os: ubuntu-20.04
          kani_dir: new

      - name: Copy benchmarks from new to old
        run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/

      - name: Run benchcomp
        run: |
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            run
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            collate

      - name: Perf Regression Results Table
        run: |
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"

      - name: Run other visualizations
        run: |
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            visualize --except dump_markdown_results_table