Add performance regression comparison in CI (#2362)

.github/workflows/kani.yml

@@ -226,3 +226,53 @@ jobs:
           if-no-files-found: error
           # Aggressively short retention: we don't really need these
           retention-days: 3
+
+  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 "OLD_REF=${{ github.event.push.after }}" | tee -a "$GITHUB_ENV"
+          echo "NEW_REF=$(git rev-parse ${{ github.event.push.after }}~)" | tee -a "$GITHUB_ENV"
+
+      - name: Save pull request HEAD and base to environment variables
+        if: ${{ github.event_name == 'pull_request' }}
+        run: |
+          echo "OLD_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
+          echo "NEW_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
+
+      - name: Checkout Kani (pull request HEAD)
+        uses: actions/checkout@v3
+        with:
+          path: ./pr
+          ref: ${{ env.NEW_REF }}
+
+      - name: Checkout Kani (pull request base)
+        uses: actions/checkout@v3
+        with:
+          path: ./base
+          ref: ${{ env.OLD_REF }}
+
+      - name: Setup Kani Dependencies (pull request base)
+        uses: ./base/.github/actions/setup
+        with:
+          os: ubuntu-20.04
+          kani_dir: base
+
+      - name: Setup Kani Dependencies (pull request HEAD)
+        uses: ./pr/.github/actions/setup
+        with:
+          os: ubuntu-20.04
+          kani_dir: pr
+
+      - name: Build Kani (pull request HEAD)
+        run: pushd pr && cargo build-dev
+
+      - name: Build Kani (pull request base)
+        run: pushd base && cargo build-dev
+
+      - name: Run benchcomp
+        run: |
+          pr/tools/benchcomp/bin/benchcomp \
+            --config pr/tools/benchcomp/configs/perf-regression.yaml

tools/benchcomp/benchcomp/entry/run.py

@@ -57,7 +57,8 @@ def __call__(self):
 
         if self.copy_benchmarks_dir:
             shutil.copytree(
-                self.directory, self.working_copy, ignore_dangling_symlinks=True)
+                self.directory, self.working_copy,
+                ignore_dangling_symlinks=True, symlinks=True)
 
         try:
             subprocess.run(

tools/benchcomp/benchcomp/visualizers/utils.py

@@ -3,6 +3,7 @@
 
 
 import dataclasses
+import logging
 import typing
 
 import benchcomp.visualizers
@@ -82,7 +83,7 @@ def __call__(self, results):
                 new = bench["variants"][new_variant]["metrics"][self.metric]
 
                 if has_regressed(old, new):
-                    logging.warining(
+                    logging.warning(
                         "Benchmark '%s' regressed on metric '%s' (%s -> %s)",
                         bench_name, self.metric, old, new)
                     ret = True

tools/benchcomp/configs/README.md

@@ -0,0 +1,4 @@
+Example Benchcomp Configurations
+================================
+
+The files in this directory can be passed to benchcomp's -c/--config flag.

tools/benchcomp/configs/perf-regression.yaml

@@ -0,0 +1,39 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Run the Kani perf suite twice, erroring out on regression. This config
+# file is primarily intended to be used in CI, because it assumes that
+# there are two Kani checkouts in the 'base' and 'pr' directories;
+# benchcomp compares the performance of these two checkouts.
+
+variants:
+  kani_pr:
+    config:
+      directory: pr
+      command_line: PATH=$(realpath pr/scripts):$PATH scripts/kani-perf.sh
+      env:
+        RUST_TEST_THREADS: "1"
+  kani_base:
+    config:
+      directory: base
+      command_line: PATH=$(realpath base/scripts):$PATH scripts/kani-perf.sh
+      env:
+        RUST_TEST_THREADS: "1"
+
+run:
+  suites:
+    kani_perf:
+      parser:
+        module: kani_perf
+      variants: [kani_base, kani_pr]
+
+visualize:
+  - type: error_on_regression
+    variant_pairs: [[kani_base, kani_pr]]
+    checks:
+      - metric: success
+        test: "lambda old, new: False if not old else not new"
+      - metric: solver_runtime
+        test: "lambda old, new: False if new < 2 else new/old > 1.1"
+      - metric: symex_runtime
+        test: "lambda old, new: False if new < 2 else new/old > 1.1"