From f4f80cea2b5eef8d9c43b27e78b3ee9afd9474c4 Mon Sep 17 00:00:00 2001
From: Joshua Liebow-Feeser <joshlf@users.noreply.github.com>
Date: Fri, 23 Feb 2024 06:42:50 -0800
Subject: [PATCH] [ci] Automatically roll pinned Kani version (#931)

Makes progress on #929
---
 .github/workflows/ci.yml                      |  3 +-
 .../roll-pinned-toolchain-versions.yml        | 32 ++++++++++++++++++-
 2 files changed, 33 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 217db76767..d827af6136 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -321,7 +321,8 @@ jobs:
           # Go back to testing all features once the Kani GitHub Action supports
           # specifying a particular toolchain.
           args: "--package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks"
-          # TODO(#929): Either roll this automatically or don't pin.
+          # This version is automatically rolled by
+          # `roll-pinned-toolchain-versions.yml`.
           kani-version: 0.46.0
 
   check_fmt:
diff --git a/.github/workflows/roll-pinned-toolchain-versions.yml b/.github/workflows/roll-pinned-toolchain-versions.yml
index b0ca0695f5..5336a7966a 100644
--- a/.github/workflows/roll-pinned-toolchain-versions.yml
+++ b/.github/workflows/roll-pinned-toolchain-versions.yml
@@ -17,7 +17,7 @@ on:
 permissions: read-all
 
 jobs:
-  roll:
+  roll_rust:
     runs-on: ubuntu-latest
     strategy:
       matrix:
@@ -105,3 +105,33 @@ jobs:
           branch: roll-pinned-${{ matrix.toolchain }}-toolchain-to-${{ env.ZC_VERSION_FOR_BRANCH_NAME }}
           push-to-fork: google-pr-creation-bot/zerocopy
           token: ${{ secrets.GOOGLE_PR_CREATION_BOT_TOKEN }}
+  roll_kani:
+    runs-on: ubuntu-latest
+    name: Roll pinned Kani version
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4.1.1
+        with:
+          ref: main
+          persist-credentials: false
+      - run: |
+          set -eo pipefail
+
+          # NOTE: If this is failing, try adding the `cargo add` command on a
+          # separate line to see its output. As is, we pipe stdout and stderr to
+          # `grep`, which will eat any error messages.
+          KANI_LATEST=$(cargo add --dry-run kani-verifier 2>&1 | grep -oh '[0-9]\+\.[0-9]\+\.[0-9]\+')
+          echo "ZC_KANI_LATEST=$KANI_LATEST" >> $GITHUB_ENV
+
+          # Update the `kani-version:` argument in-place.
+          sed -i -E -e "s/^( *kani-version:)( [0-9]+\.[0-9]+\.[0-9]+)/\1 $KANI_LATEST/" .github/workflows/ci.yml
+      - name: Submit PR
+        uses: peter-evans/create-pull-request@b1ddad2c994a25fbc81a28b3ec0e368bb2021c50 # v6.0.0
+        with:
+          commit-message: "[ci] Roll pinned Kani version"
+          author: Google PR Creation Bot <github-pull-request-creation-bot@google.com>
+          committer: Google PR Creation Bot <github-pull-request-creation-bot@google.com>
+          title: "[ci] Roll pinned Kani version"
+          branch: roll-pinned-kani-to-${{ env.ZC_KANI_LATEST }}
+          push-to-fork: google-pr-creation-bot/zerocopy
+          token: ${{ secrets.GOOGLE_PR_CREATION_BOT_TOKEN }}