Create workflow Kani Extra for checks that run conditionally on labels (

#2837)

The "Auto Label" workflow correctly label our PRs; however, this action
do not trigger a PR 'labeled' workflow. To automatically do that, we now
changed the CI structure to have a new workflow with extra jobs that are
conditional to labels and files being modified.

This new workflow starts by triggering the auto-label job. The benchmark
workflow is only triggered if after the auto-label job, the PR has a
Z-BenchCI label.

This also means that the benchmark workflow will now run after any
update to a PR that has the 'Z-BenchCI' label.

Resolves #2606

.github/workflows/bench.yml

@@ -1,21 +1,20 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Run performance benchmarks comparing two different Kani versions.
+# This workflow takes much longer than other workflows, so we don't run it by default.
+# This workflow will run when:
+# - Changes are pushed to 'main'.
+# - Triggered by another workflow
 name: Kani Performance Benchmarks
 on:
  push:
  branches:
  - 'main'
- pull_request:
- types:
- - labeled
+ workflow_call:
 
 jobs:
  perf-benchcomp:
- if: ${{ github.event_name == 'push' 
- || (github.event_name == 'pull_request' 
- && github.event.action == 'labeled'
- && github.event.label.name == 'Z-BenchCI')
- }}
  runs-on: ubuntu-20.04
  steps:
  - name: Save push event HEAD and HEAD~ to environment variables
@@ -25,7 +24,7 @@ jobs:
  echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
 
  - name: Save pull request HEAD and base to environment variables
- if: ${{ github.event_name == 'pull_request' }}
+ 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"

.github/workflows/extra_jobs.yml

@@ -0,0 +1,49 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Workflow that execute jobs based on the files that were changed or some label configuration.
+#
+# The first job in this workflow will auto label the PR, while the following jobs will conditionally
+# run according to the auto-label result.
+#
+# This workflow runs on `pull_request_target` because the labeler needs extra write permission.
+# Thus, we keep this job minimal, and the only actions used are from the same verified publisher.
+#
+# Other jobs should not require extra permissions, so be careful when adding new jobs to not propagate write
+# permissions.
+#
+# Note that this also means that the workflow version run is the one currently in `main`,
+# not the one from the PR. This is only relevant if a PR is changing this workflow.
+#
+# See <https://github.com/actions/labeler/issues/121> for more details.
+
+name: Kani Extra
+on: pull_request_target
+
+jobs:
+ # Keep this job minimal since it requires extra permission
+ auto-label:
+ name: Auto Label
+ permissions:
+ contents: read
+ pull-requests: write
+ outputs:
+ all-labels: ${{ steps.labeler.outputs.all-labels }}
+ new-labels: ${{ steps.labeler.outputs.new-labels }}
+ runs-on: ubuntu-latest
+ steps:
+ - name: Checkout Kani
+ uses: actions/checkout@v3
+
+ - name: Label PR
+ id: labeler
+ uses: actions/labeler@v4
+ with:
+ dot: true
+
+ verification-bench:
+ name: Verification Benchmarks
+ needs: auto-label
+ permissions: {}
+ if: contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI')
+ uses: ./.github/workflows/bench.yml