Create workflow Kani Extra for checks that run conditionally on labels (rust-lang#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 rust-lang#2606

Author: celinval

.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