diff --git a/.github/workflows/bench-compiler.yml b/.github/workflows/bench-compiler.yml index f94195479cc..0b30110c6ad 100644 --- a/.github/workflows/bench-compiler.yml +++ b/.github/workflows/bench-compiler.yml @@ -20,8 +20,11 @@ jobs: run: | echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV" echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV" + # Note: in reusable workflows, github.event_name and github.event are + # those of the caller; when invoked from bench-pr.yml this is a + # pull_request event. - name: Save pull request HEAD and base to environment variables - if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }} + if: ${{ github.event_name == 'pull_request' }} 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" @@ -83,8 +86,11 @@ jobs: run: | echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV" echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV" + # Note: in reusable workflows, github.event_name and github.event are + # those of the caller; when invoked from bench-pr.yml this is a + # pull_request event. - name: Save pull request HEAD and base to environment variables - if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }} + if: ${{ github.event_name == 'pull_request' }} 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" diff --git a/.github/workflows/bench-e2e.yml b/.github/workflows/bench-e2e.yml index 987420379af..bc2db84b52f 100644 --- a/.github/workflows/bench-e2e.yml +++ b/.github/workflows/bench-e2e.yml @@ -25,8 +25,11 @@ jobs: echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV" echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV" + # Note: in reusable workflows, github.event_name and github.event are + # those of the caller; when invoked from bench-pr.yml this is a + # pull_request event. - name: Save pull request HEAD and base to environment variables - if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }} + if: ${{ github.event_name == 'pull_request' }} 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" diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml new file mode 100644 index 00000000000..d68534a54ff --- /dev/null +++ b/.github/workflows/bench-pr.yml @@ -0,0 +1,40 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# Run the performance benchmark workflows for pull requests that carry the +# corresponding Z-*BenchCI label (applied automatically by the labeler in +# extra_jobs.yml based on the changed files, or manually). +# +# This runs on `pull_request` (not `pull_request_target`) on purpose: the +# benchmark workflows build and execute the code proposed in the pull +# request, which must not happen in the trusted `pull_request_target` +# context (actions/checkout v6.1.0/v5.1.0/v4.4.0 refuse to do so; see +# https://github.blog/changelog/2026-06-18-safer-pull_request_target-defaults-for-github-actions-checkout/). +# +# Note on the `labeled` trigger: labels added by the auto-labeler do not +# re-trigger this workflow (events created with the default GITHUB_TOKEN +# never trigger new workflow runs), so on freshly opened pull requests the +# benchmarks only start with the next push to the pull request. Manually +# adding the label triggers them immediately. + +name: Kani Benchmarks +permissions: + contents: read +on: + pull_request: + types: [opened, synchronize, reopened, labeled] + +concurrency: + group: ${{ github.workflow }}-${{ github.event.pull_request.number }} + cancel-in-progress: true + +jobs: + end-to-end-bench: + name: End-to-End Benchmarks + if: ${{ contains(github.event.pull_request.labels.*.name, 'Z-EndToEndBenchCI') }} + uses: ./.github/workflows/bench-e2e.yml + + compiler-bench: + name: Compiler Benchmarks + if: ${{ contains(github.event.pull_request.labels.*.name, 'Z-CompilerBenchCI') }} + uses: ./.github/workflows/bench-compiler.yml diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index 352d6ded22d..b6c8600de45 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -44,14 +44,8 @@ jobs: with: dot: true - end-to-end-bench: - name: End-to-End Benchmarks - needs: auto-label - 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 - if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-CompilerBenchCI') && github.event_name != 'merge_group' }} - uses: ./.github/workflows/bench-compiler.yml + # Note: the label-gated benchmark workflows (bench-pr.yml) used to be + # invoked from here, but they build and run the code proposed in the pull + # request, which must not happen in this workflow's trusted + # `pull_request_target` context. They now trigger on `pull_request` + # events directly.