Introduce compiler timing script & CI job

.github/labeler.yml

@@ -5,9 +5,20 @@
 #
 # Note that we enable dot, so "**" matches all files in a folder
 
-Z-BenchCI:
+Z-EndToEndBenchCI:
 - any:
   - changed-files:
-    - any-glob-to-any-file: ['kani-compiler/**', 'kani-driver/src/call-*', 'cprover_bindings/**', 'library/**']
+    - any-glob-to-any-file: ['kani-compiler/**', 'kani-driver/src/call_*', 'cprover_bindings/**', 'library/**']
     - any-glob-to-any-file: ['rust-toolchain.toml', 'Cargo.lock']
     - any-glob-to-any-file: ['kani-dependencies']
+
+Z-CompilerBenchCI:
+- any:
+  # we want to run compiler benchmarks if:
+  - changed-files:
+    # any parts of the compiler change
+    - any-glob-to-any-file: ['kani-compiler/**', 'cprover_bindings/**', 'library/**']
+    # the way we call the compiler changes
+    - any-glob-to-any-file: ['kani-driver/src/call_cargo.rs', 'kani-driver/src/call_single_file.rs']
+    # or if our dependencies change
+    - any-glob-to-any-file: ['rust-toolchain.toml', 'Cargo.lock']

.github/workflows/bench-compiler.yml

@@ -0,0 +1,140 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Run performance benchmarks comparing the compiler performance of two different Kani versions.
+name: Kani Compiler Performance Benchmarks
+on:
+  push:
+    branches:
+      - 'main'
+  workflow_call:
+
+jobs:
+  compile-timer-short:
+    runs-on: ubuntu-24.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-24.04
+          kani_dir: old
+
+      - name: Set up Kani Dependencies (new variant)
+        uses: ./new/.github/actions/setup
+        with:
+          os: ubuntu-24.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: Build `compile-timer` in old
+        run: cd old/tools/compile-timer && cargo build --release
+      - name: Build `kani` in old
+        run: cd old && cargo build-dev --release
+
+      - name: Build `compile-timer` in new
+        run: cd new/tools/compile-timer && cargo build --release
+      - name: Build `kani` in new
+        run: cd new && cargo build-dev --release
+
+      - name: Run `compile-timer` on old
+        run: |
+          export PATH="${{ github.workspace }}/old/scripts:$PATH"
+          cd old/tests/perf && ../../target/release/compile-timer --out-path compile-times-old.json --ignore kani-lib --ignore display_trait --ignore s2n-quic
+      - name: Run `compile-timer` on new
+        run: |
+          export PATH="${{ github.workspace }}/new/scripts:$PATH"
+          cd new/tests/perf && ../../target/release/compile-timer --out-path compile-times-new.json --ignore kani-lib --ignore display_trait --ignore s2n-quic
+      - name: Run analysis between the two
+        run: ./new/target/release/compile-analyzer --path-pre old/tests/perf/compile-times-old.json --path-post new/tests/perf/compile-times-new.json --only-markdown --suite-name short >> "$GITHUB_STEP_SUMMARY"
+
+  compile-timer-long:
+    runs-on: ubuntu-24.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-24.04
+          kani_dir: old
+
+      - name: Set up Kani Dependencies (new variant)
+        uses: ./new/.github/actions/setup
+        with:
+          os: ubuntu-24.04
+          kani_dir: new
+
+      # Ensures that a PR changing the benchmarks will have the new benchmarks run 
+      # for both commits.
+      - name: Copy benchmarks from new to old
+        run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
+
+      - name: Build `compile-timer` in old
+        run: cd old/tools/compile-timer && cargo build --release
+      - name: Build `kani` in old
+        run: cd old && cargo build-dev --release
+
+      - name: Build `compile-timer` in new
+        run: cd new/tools/compile-timer && cargo build --release
+      - name: Build `kani` in new
+        run: cd new && cargo build-dev --release
+
+      - name: Run `compile-timer` on old
+        run: |
+          export PATH="${{ github.workspace }}/old/scripts:$PATH"
+          cd old/tests/perf/s2n-quic && ../../../target/release/compile-timer --out-path compile-times-old.json --also-visit quic/s2n-quic-core --also-visit quic/s2n-quic-platform --also-visit common/s2n-codec --skip-current
+      - name: Run `compile-timer` on new
+        run: |
+          export PATH="${{ github.workspace }}/new/scripts:$PATH"
+          cd new/tests/perf/s2n-quic && ../../../target/release/compile-timer --out-path compile-times-new.json --also-visit quic/s2n-quic-core --also-visit quic/s2n-quic-platform --also-visit common/s2n-codec --skip-current
+      - name: Run analysis between the two
+        run: ./new/target/release/compile-analyzer --path-pre old/tests/perf/s2n-quic/compile-times-old.json --path-post new/tests/perf/s2n-quic/compile-times-new.json --only-markdown --suite-name long >> "$GITHUB_STEP_SUMMARY"

.github/workflows/bench.yml → .github/workflows/bench-e2e.yml

@@ -6,7 +6,7 @@
 # This workflow will run when:
 #  - Changes are pushed to 'main'.
 #  - Triggered by another workflow
-name: Kani Performance Benchmarks
+name: Kani End-To-End Performance Benchmarks
 on:
   push:
     branches:

.github/workflows/extra_jobs.yml

@@ -43,9 +43,16 @@ jobs:
       with:
         dot: true
 
-  verification-bench:
-    name: Verification Benchmarks
+  end-to-end-bench:
+    name: End-to-End Benchmarks
     needs: auto-label
     permissions: {}
-    if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI') && github.event_name != 'merge_group' }}
-    uses: ./.github/workflows/bench.yml
+    if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-EndToEndBenchCI') && github.event_name != 'merge_group' }}
+    uses: ./.github/workflows/bench-e2e.yml
+
+  compiler-bench:
+    name: Compiler Benchmarks
+    needs: auto-label
+    permissions: {}
+    if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-CompilerBenchCI') && github.event_name != 'merge_group' }}
+    uses: ./.github/workflows/bench-compiler.yml

Cargo.lock

@@ -338,19 +338,19 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.39"
+version = "4.5.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fd60e63e9be68e5fb56422e397cf9baddded06dae1d2e523401542383bc72a9f"
+checksum = "40b6887a1d8685cebccf115538db5c0efe625ccac9696ad45c409d96566e910f"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.39"
+version = "4.5.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "89cc6392a1f72bbeb820d71f32108f61fdaf18bc526e1d23954168a67759ef51"
+checksum = "e0c66c08ce9f0c698cbce5c0279d0bb6ac936d8674174fe48f736533b964f59e"
 dependencies = [
  "anstream",
  "anstyle",
@@ -360,9 +360,9 @@ dependencies = [
 
 [[package]]
 name = "clap_derive"
-version = "4.5.32"
+version = "4.5.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09176aae279615badda0765c0c0b3f6ed53f4709118af73cf4655d85d1530cd7"
+checksum = "d2c7947ae4cc3d851207c1adb5b5e260ff0cca11446b1d6d1423788e442257ce"
 dependencies = [
  "heck",
  "proc-macro2",
@@ -403,6 +403,15 @@ dependencies = [
  "unicode-width 0.2.0",
 ]
 
+[[package]]
+name = "compile-timer"
+version = "0.1.0"
+dependencies = [
+ "clap",
+ "serde",
+ "serde_json",
+]
+
 [[package]]
 name = "compiletest"
 version = "0.0.0"

Cargo.toml

@@ -48,6 +48,7 @@ members = [
   "tools/build-kani",
   "tools/kani-cov",
   "tools/scanner",
+  "tools/compile-timer",
   "kani-driver",
   "kani-compiler",
   "kani_metadata",

kani-driver/src/call_cargo.rs

@@ -357,7 +357,13 @@ crate-type = ["lib"]
                     && t1.doc == t2.doc)
         }
 
+        let compile_start = std::time::Instant::now();
         let artifacts = self.run_build(cargo_cmd)?;
+        if std::env::var("TIME_COMPILER").is_ok() {
+            // conditionally print the compilation time for debugging & use by `compile-timer`
+            // doesn't just use the existing `--debug` flag because the number of prints significantly affects performance
+            println!("BUILT {} IN {:?}μs", target.name, compile_start.elapsed().as_micros());
+        }
         debug!(?artifacts, "run_build_target");
 
         // We generate kani specific artifacts only for the build target. The build target is

tools/benchcomp/benchcomp/visualizers/__init__.py

@@ -265,12 +265,17 @@ def _get_template():
             Scatterplot axis ranges are {{ d["scaled_metrics"][metric]["min_value"] }} (bottom/left) to {{ d["scaled_metrics"][metric]["max_value"] }} (top/right).
 
             {% endif -%}
+            <details> <summary>Breakdown by harness</summary>
+
             | Benchmark | {% for variant in d["variants"][metric] %} {{ variant }} |{% endfor %}
             | --- |{% for variant in d["variants"][metric] %} --- |{% endfor -%}
             {% for bench_name, bench_variants in benchmarks.items () %}
             | {{ bench_name }} {% for variant in d["variants"][metric] -%}
              | {{ bench_variants[variant] }} {% endfor %}|
             {%- endfor %}
+
+            </details>
+
             {% endfor -%}
             """)
 

tools/benchcomp/test/test_regression.py

@@ -477,18 +477,28 @@ def test_markdown_results_table(self):
                     ```
                     Scatterplot axis ranges are 5 (bottom/left) to 10 (top/right).
 
+                    <details> <summary>Breakdown by harness</summary>
+
                     | Benchmark |  variant_1 | variant_2 | ratio |
                     | --- | --- | --- | --- |
                     | bench_1 | 5 | 10 | **2.0** |
                     | bench_2 | 10 | 5 | 0.5 |
 
+                    </details>
+
+
                     ## success
 
+                    <details> <summary>Breakdown by harness</summary>
+
                     | Benchmark |  variant_1 | variant_2 | notes |
                     | --- | --- | --- | --- |
                     | bench_1 | True | True |  |
                     | bench_2 | True | False | regressed |
                     | bench_3 | False | True | newly passing |
+
+                    </details>
+
                     """))
 
 

tools/compile-timer/Cargo.toml

@@ -0,0 +1,24 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "compile-timer"
+version = "0.1.0"
+edition = "2024"
+license = "MIT OR Apache-2.0"
+
+[dependencies]
+clap = { version = "4.5.40", features = ["derive"] }
+serde = {version = "1.0.219", features = ["derive"]}
+serde_json = "1.0.140"
+
+[[bin]]
+name = "compile-timer"
+path = "src/compile-timer.rs"
+
+[[bin]]
+name = "compile-analyzer"
+path = "src/compile-analyzer.rs"
+
+[lints]
+workspace = true

tools/compile-timer/README.md

@@ -0,0 +1,19 @@
+# Compile-Timer
+This is a simple script for timing the Kani compiler's end-to-end performance on crates.
+
+## Setup
+You can run it by first compiling Kani (with `cargo build-dev --release` in the project root), then building this script (with `cargo build --release` in this `compile-timer` directory). This will build new `compile-timer` & `compile-analyzer` binaries in `kani/target/release`. 
+
+## Recording Compiler Times with `compile-timer`
+After doing that, you should make sure you have Kani on your $PATH (see instructions [here](https://model-checking.github.io/kani/build-from-source.html#adding-kani-to-your-path)) after which you can run `compile-timer --out-path [OUT_JSON_FILE]` in any directory to profile the compiler's performance on it.
+
+By default, the script recursively goes into directories and will use `cargo kani` to profile any Rust projects it encounters (which it determines by looking for a `Cargo.toml`). You can tell it to ignore specific subtrees by passing in the `--ignore [DIR_NAME]` flag.
+
+## Visualizing Compiler Times with `compile-analyzer`
+`compile-timer` itself will have some debug output including each individual run's time and aggregates for each crate.
+
+`compile-analyzer` is specifically for comparing performance across multiple commits. 
+
+Once you've run `compile-timer` on both commits, you can run `compile-analyzer --path-pre [FIRST_JSON_FILE] --path-post [SECOND_JSON_FILE]` to see the change in performance going from the first to second commit. 
+
+By default, `compile-analyzer` will just print to the console, but if you specify the `--only-markdown` option, it's output will be formatted for GitHub flavored markdown (as is useful in CI).