Merge remote-tracking branch 'upstream/main' into codegen-ordering

Author: feliperodri

.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"

.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"

.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

.github/workflows/extra_jobs.yml

@@ -40,18 +40,12 @@ jobs:
 
     - name: Label PR
       id: labeler
-      uses: actions/labeler@v6
+      uses: actions/labeler@v7
       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.

.github/workflows/kani.yml

@@ -82,7 +82,7 @@ jobs:
         # Retry on infra-driven failures (spot preemption / runner shutdown).
         # The script itself bounds per-test wall time, so functional regressions
         # surface as normal test failures and are not retried indefinitely.
-        uses: nick-fields/retry@v3
+        uses: nick-fields/retry@v4
         with:
           timeout_minutes: 180
           max_attempts: 2