Skip to content

Commit 6d4edc8

Browse files
authored
Merge branch 'main' into final-cache
2 parents 75ba271 + 6fa4467 commit 6d4edc8

192 files changed

Lines changed: 6038 additions & 1514 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.github/actions/setup/action.yml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,5 +37,7 @@ runs:
3737
run: |
3838
cd ${{ inputs.kani_dir }}
3939
git config --global --add safe.directory $(pwd)
40-
git submodule update --init --depth 1
40+
# Workaround for occasionally failing to copy a file in s2n-quic that we
41+
# don't actually care about
42+
GIT_LFS_SKIP_SMUDGE=1 git submodule update --init --depth 1
4143
shell: bash

.github/workflows/bench-compiler.yml

Lines changed: 7 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
#
44
# Run performance benchmarks comparing the compiler performance of two different Kani versions.
55
name: Kani Compiler Performance Benchmarks
6+
permissions:
7+
contents: read
68
on:
79
push:
810
branches:
@@ -24,31 +26,19 @@ jobs:
2426
echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
2527
echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
2628
- name: Check out Kani (old variant)
27-
uses: actions/checkout@v5
29+
uses: actions/checkout@v6
2830
with:
2931
path: ./old
3032
ref: ${{ env.OLD_REF }}
3133
fetch-depth: 2
3234

3335
- name: Check out Kani (new variant)
34-
uses: actions/checkout@v5
36+
uses: actions/checkout@v6
3537
with:
3638
path: ./new
3739
ref: ${{ env.NEW_REF }}
3840
fetch-depth: 1
3941

40-
- name: Cache Kani build artifacts
41-
uses: Swatinem/rust-cache@v2
42-
with:
43-
cache-on-failure: true
44-
shared-key: "kani-rust-cache-bench"
45-
workspaces: |
46-
new
47-
new/tools/compile-timer
48-
old
49-
old/tools/compile-timer
50-
cache-directories: "~/.rustup"
51-
5242
- name: Set up Kani Dependencies (old variant)
5343
uses: ./old/.github/actions/setup
5444
with:
@@ -100,31 +90,19 @@ jobs:
10090
echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
10191
10292
- name: Check out Kani (old variant)
103-
uses: actions/checkout@v5
93+
uses: actions/checkout@v6
10494
with:
10595
path: ./old
10696
ref: ${{ env.OLD_REF }}
10797
fetch-depth: 2
10898

10999
- name: Check out Kani (new variant)
110-
uses: actions/checkout@v5
100+
uses: actions/checkout@v6
111101
with:
112102
path: ./new
113103
ref: ${{ env.NEW_REF }}
114104
fetch-depth: 1
115105

116-
- name: Cache Kani build artifacts
117-
uses: Swatinem/rust-cache@v2
118-
with:
119-
cache-on-failure: true
120-
shared-key: "kani-rust-cache-bench"
121-
workspaces: |
122-
new
123-
new/tools/compile-timer
124-
old
125-
old/tools/compile-timer
126-
cache-directories: "~/.rustup"
127-
128106
- name: Set up Kani Dependencies (old variant)
129107
uses: ./old/.github/actions/setup
130108
with:
@@ -161,4 +139,4 @@ jobs:
161139
export PATH="${{ github.workspace }}/new/scripts:$PATH"
162140
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
163141
- name: Run analysis between the two
164-
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"
142+
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-e2e.yml

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77
# - Changes are pushed to 'main'.
88
# - Triggered by another workflow
99
name: Kani End-To-End Performance Benchmarks
10+
permissions:
11+
contents: read
1012
on:
1113
push:
1214
branches:
@@ -30,14 +32,14 @@ jobs:
3032
echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
3133
3234
- name: Check out Kani (old variant)
33-
uses: actions/checkout@v5
35+
uses: actions/checkout@v6
3436
with:
3537
path: ./old
3638
ref: ${{ env.OLD_REF }}
3739
fetch-depth: 2
3840

3941
- name: Check out Kani (new variant)
40-
uses: actions/checkout@v5
42+
uses: actions/checkout@v6
4143
with:
4244
path: ./new
4345
ref: ${{ env.NEW_REF }}

.github/workflows/cargo-update.yml

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,14 @@ permissions:
1515

1616
jobs:
1717
create-cargo-update-pr:
18+
# This workflow is restricted to the main repository (model-checking/kani) to prevent
19+
# unnecessary PRs being created in forks. The cargo update action should only run in
20+
# the main repository context.
21+
if: github.repository == 'model-checking/kani'
1822
runs-on: ubuntu-22.04
1923
steps:
2024
- name: Checkout Kani
21-
uses: actions/checkout@v5
25+
uses: actions/checkout@v6
2226

2327
- name: Setup Kani Dependencies
2428
uses: ./.github/actions/setup
@@ -37,7 +41,7 @@ jobs:
3741
git diff
3842
fi
3943
- name: Create Pull Request
40-
uses: peter-evans/create-pull-request@v7
44+
uses: peter-evans/create-pull-request@v8
4145
with:
4246
commit-message: Upgrade cargo dependencies to ${{ env.today }}
4347
branch: cargo-update-${{ env.today }}

.github/workflows/cbmc-latest.yml

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@
55
name: >-
66
Nightly: CBMC Latest
77
8+
permissions:
9+
contents: read
10+
811
on:
912
schedule:
1013
- cron: "0 9 * * *" # Run this every day at 9 AM UTC (4 AM ET/1 AM PT)
@@ -19,10 +22,10 @@ jobs:
1922
runs-on: ${{ matrix.os }}
2023
strategy:
2124
matrix:
22-
os: [macos-13, ubuntu-22.04, ubuntu-24.04]
25+
os: [macos-15-intel, ubuntu-22.04, ubuntu-24.04]
2326
steps:
2427
- name: Checkout Kani under "kani"
25-
uses: actions/checkout@v5
28+
uses: actions/checkout@v6
2629
with:
2730
path: kani
2831

@@ -33,7 +36,7 @@ jobs:
3336
kani_dir: 'kani'
3437

3538
- name: Checkout CBMC under "cbmc"
36-
uses: actions/checkout@v5
39+
uses: actions/checkout@v6
3740
with:
3841
repository: diffblue/cbmc
3942
path: cbmc
@@ -64,7 +67,7 @@ jobs:
6467
runs-on: ubuntu-24.04
6568
steps:
6669
- name: Checkout Kani under "kani"
67-
uses: actions/checkout@v5
70+
uses: actions/checkout@v6
6871
with:
6972
path: kani
7073

@@ -79,7 +82,7 @@ jobs:
7982
run: cargo build-dev -- --release
8083

8184
- name: Checkout CBMC under "cbmc"
82-
uses: actions/checkout@v5
85+
uses: actions/checkout@v6
8386
with:
8487
repository: diffblue/cbmc
8588
path: cbmc

.github/workflows/cbmc-update.yml

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,15 @@ permissions:
1515
pull-requests: write
1616

1717
jobs:
18-
create-cargo-update-pr:
18+
create-cbmc-update-pr:
19+
# This workflow is restricted to the main repository (model-checking/kani) to prevent
20+
# unnecessary PRs being created in forks. The CBMC update action should only run in
21+
# the main repository context.
22+
if: github.repository == 'model-checking/kani'
1923
runs-on: ubuntu-22.04
2024
steps:
2125
- name: Checkout Kani
22-
uses: actions/checkout@v5
26+
uses: actions/checkout@v6
2327

2428
- name: Setup Kani Dependencies
2529
uses: ./.github/actions/setup
@@ -65,7 +69,7 @@ jobs:
6569
6670
- name: Create Pull Request
6771
if: ${{ env.next_step == 'create_pr' }}
68-
uses: peter-evans/create-pull-request@v7
72+
uses: peter-evans/create-pull-request@v8
6973
with:
7074
commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}
7175
branch: cbmc-${{ env.CBMC_LATEST }}
@@ -75,7 +79,7 @@ jobs:
7579
Upgrade CBMC to its latest release.
7680
7781
- name: Create Issue
78-
if: ${{ env.next_step == 'create_issue' && github.repository_owner == 'model-checking' }}
82+
if: ${{ env.next_step == 'create_issue' }}
7983
uses: dacbd/create-issue-action@main
8084
with:
8185
token: ${{ github.token }}

.github/workflows/deny.yml

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55
# 2. Checks Rust-Sec registry for security advisories.
66

77
name: Cargo Deny
8+
permissions:
9+
contents: read
810
on:
911
pull_request:
1012
merge_group:
@@ -17,12 +19,12 @@ jobs:
1719
audit:
1820
runs-on: ubuntu-latest
1921
steps:
20-
- uses: actions/checkout@v5
22+
- uses: actions/checkout@v6
2123
with:
2224
submodules: recursive
23-
- name: Install rustup
24-
run: ./scripts/setup/install_rustup.sh
2525
- uses: EmbarkStudios/cargo-deny-action@v2
26+
env:
27+
RUSTUP_TOOLCHAIN: stable
2628
with:
2729
arguments: --all-features --workspace
2830
command-arguments: -s

.github/workflows/extra_jobs.yml

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@
1818
# See https://github.com/actions/labeler?tab=readme-ov-file#recommended-permissions for more details.
1919

2020
name: Kani Extra
21+
permissions:
22+
contents: read
2123
on:
2224
pull_request_target:
2325
merge_group:
@@ -27,32 +29,29 @@ jobs:
2729
auto-label:
2830
name: Auto Label
2931
permissions:
30-
contents: read
3132
pull-requests: write
3233
outputs:
3334
all-labels: ${{ steps.labeler.outputs.all-labels }}
3435
new-labels: ${{ steps.labeler.outputs.new-labels }}
3536
runs-on: ubuntu-latest
3637
steps:
3738
- name: Checkout Kani
38-
uses: actions/checkout@v5
39+
uses: actions/checkout@v6
3940

4041
- name: Label PR
4142
id: labeler
42-
uses: actions/labeler@v5
43+
uses: actions/labeler@v6
4344
with:
4445
dot: true
4546

4647
end-to-end-bench:
4748
name: End-to-End Benchmarks
4849
needs: auto-label
49-
permissions: {}
5050
if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-EndToEndBenchCI') && github.event_name != 'merge_group' }}
5151
uses: ./.github/workflows/bench-e2e.yml
5252

5353
compiler-bench:
5454
name: Compiler Benchmarks
5555
needs: auto-label
56-
permissions: {}
5756
if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-CompilerBenchCI') && github.event_name != 'merge_group' }}
5857
uses: ./.github/workflows/bench-compiler.yml

.github/workflows/format-check.yml

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
# Copyright Kani Contributors
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33
name: Kani Format Check
4+
permissions:
5+
contents: read
46
on:
57
pull_request:
68
merge_group:
@@ -15,7 +17,7 @@ jobs:
1517
runs-on: ubuntu-latest
1618
steps:
1719
- name: Checkout Kani
18-
uses: actions/checkout@v5
20+
uses: actions/checkout@v6
1921

2022
- name: Execute copyright check
2123
run: ./scripts/ci/run-copyright-check.sh
@@ -34,7 +36,7 @@ jobs:
3436
runs-on: ubuntu-24.04
3537
steps:
3638
- name: Checkout Kani
37-
uses: actions/checkout@v5
39+
uses: actions/checkout@v6
3840

3941
- name: Setup Kani Dependencies
4042
uses: ./.github/actions/setup

0 commit comments

Comments
 (0)