Skip to content

Remove the overflow checks for wrapping_offset (#3589) #641

Remove the overflow checks for wrapping_offset (#3589)

Remove the overflow checks for wrapping_offset (#3589) #641

Workflow file for this run

# 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