From f4604024eaa5ee34b9ec997a46598e3afd2aa59a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 07:41:08 +0000 Subject: [PATCH] Add a weekly Charon update job, and run the LLBC regression in the toolchain job Charon tags `nightly-YYYY.MM.DD` almost daily, but nothing noticed the pin drifting: before #4883 it was 2,176 commits behind, and catching up needed a patch for `box` patterns removed from nightly Rust and skipping Charon versions that could no longer be built at all. `charon-update.yml` (weekly, and on demand) runs the new `scripts/charon_update.sh`, modelled on the CBMC and toolchain jobs. It moves the `charon` submodule to the latest tag, runs `cargo update -p charon`, and runs `kani-llbc-regression.sh`, which covers everything Charon affects (the LLBC build, the `-D warnings` build, llbc clippy and the llbc suite). If that passes, the job opens a PR that lists the merged Charon PRs; the PR then gets the full CI, including `cargo deny`. If it fails, the job files an "Automatic Charon upgrade failed" issue, or comments on it when one is already open. Because the tag changes nearly every day, a single rolling issue takes the place of one issue per version; a tag the issue already mentions is not retried. `toolchain_update.sh` now also runs `kani-llbc-regression.sh`: the LLBC backend (and with it Charon) is not built by `kani-regression.sh`, so a toolchain that only breaks it went unnoticed until the PR's LLBC job. Co-authored-by: Kiro --- .github/workflows/charon-update.yml | 93 +++++++++++++++++++++++++++ scripts/charon_update.sh | 99 +++++++++++++++++++++++++++++ scripts/toolchain_update.sh | 4 +- 3 files changed, 195 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/charon-update.yml create mode 100755 scripts/charon_update.sh diff --git a/.github/workflows/charon-update.yml b/.github/workflows/charon-update.yml new file mode 100644 index 000000000000..70ad28901c1a --- /dev/null +++ b/.github/workflows/charon-update.yml @@ -0,0 +1,93 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +name: Attempt Charon update + +on: + schedule: + - cron: "30 4 * * Wed" # Run this every Wednesday at 04:30 UTC + workflow_dispatch: # Allow manual dispatching for a custom branch / tag. + +permissions: + checks: write + contents: write + issues: write + pull-requests: write + +jobs: + create-charon-update-pr: + # This workflow is restricted to the main repository (model-checking/kani) to prevent + # unnecessary PRs being created in forks. The Charon update action should only run in + # the main repository context. + if: github.repository == 'model-checking/kani' + runs-on: ubuntu-22.04 + steps: + - name: Checkout Kani + uses: actions/checkout@v6 + + - name: Setup Kani Dependencies + uses: ./.github/actions/setup + with: + os: ubuntu-22.04 + + - name: Update the Charon pin and determine next step + env: + GH_TOKEN: ${{ github.token }} + run: ./scripts/charon_update.sh + + - name: Clean untracked files + run: git clean -f + + - name: Create Pull Request + id: create_pr + if: ${{ env.next_step == 'create_pr' }} + uses: peter-evans/create-pull-request@v8 + with: + commit-message: Upgrade Charon from ${{ env.current_charon }} to ${{ env.next_charon }} + branch: charon-${{ env.next_charon }} + delete-branch: true + title: 'Automatic upgrade of Charon from ${{ env.current_charon }} to ${{ env.next_charon }}' + body: | + Update the Charon pin (used by the LLBC backend) from ${{ env.current_charon }} to its + latest tag, ${{ env.next_charon }}. Only the `charon` submodule and `Cargo.lock` change. + `kani-llbc-regression.sh` passed in the + [automated run](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}). + + ${{ env.charon_log }} + + - name: Point the open failure issue to the PR + if: ${{ steps.create_pr.outputs.pull-request-number && env.failure_issue != '' }} + env: + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ steps.create_pr.outputs.pull-request-number }} + run: | + gh issue comment "$failure_issue" --body \ + "Charon $next_charon passes the LLBC regression: see #$PR_NUMBER." + + - name: Create Issue + if: ${{ env.next_step == 'create_issue' }} + uses: dacbd/create-issue-action@main + with: + token: ${{ github.token }} + # Keep in sync with `failure_title` in scripts/charon_update.sh. + title: 'Automatic Charon upgrade failed' + body: | + Updating Charon from ${{ env.current_charon }} to ${{ env.next_charon }} requires + source changes: `kani-llbc-regression.sh` failed in the + [automated run](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}). + + This issue stays open across Charon tags: later failing attempts add a comment here + rather than filing a new issue. Close it once the pin is updated. + + ${{ env.charon_log }} + + - name: Comment on the open failure issue + if: ${{ env.next_step == 'comment_issue' }} + env: + GH_TOKEN: ${{ github.token }} + BODY: | + Updating Charon from ${{ env.current_charon }} to ${{ env.next_charon }} failed as well: + [automated run](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}). + + ${{ env.charon_log }} + run: gh issue comment "$failure_issue" --body "$BODY" diff --git a/scripts/charon_update.sh b/scripts/charon_update.sh new file mode 100755 index 000000000000..804278fce193 --- /dev/null +++ b/scripts/charon_update.sh @@ -0,0 +1,99 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# This script is part of our CI nightly job to bump the Charon pin (the `charon` submodule, used by +# the LLBC backend) to Charon's latest `nightly-*` tag. It updates the submodule and `Cargo.lock`, +# runs the LLBC regression, and tells the workflow what to do next via `$GITHUB_ENV`: +# +# - `next_step=create_pr`: the bump passed `kani-llbc-regression.sh`; open a PR; +# - `next_step=create_issue`: it failed and no failure issue is open; file one; +# - `next_step=comment_issue`: it failed and the failure issue (`failure_issue`) is open; add a +# comment for the new tag instead of filing another issue; +# - `next_step=none`: nothing to do (already at the latest tag, the PR branch exists, or the open +# failure issue already mentions this tag). +# +# Charon tags nearly every day, so failures are tracked in a single rolling issue rather than one +# per tag. + +set -eu + +failure_title="Automatic Charon upgrade failed" +charon_url=$(git config -f .gitmodules submodule.charon.url) + +current_commit=$(git ls-tree HEAD charon | awk '{print $3}') +# Only accept tags of the expected shape: the name ends up in branch names, titles and commands. +next_tag=$(git ls-remote --tags --refs "$charon_url" 'nightly-*' | sed 's#.*refs/tags/##' | \ + grep -E '^nightly-[0-9]{4}\.[0-9]{2}\.[0-9]{2}$' | sort | tail -1) +if [ -z "$next_tag" ]; then + echo "No nightly-YYYY.MM.DD tag found at $charon_url" + exit 1 +fi +# Fetch the tag with enough history to relate it to the current pin. +git -C charon fetch --quiet --filter=tree:0 "$charon_url" "refs/tags/$next_tag:refs/tags/$next_tag" +next_commit=$(git -C charon rev-parse "$next_tag^{commit}") +current_tag=$(git -C charon describe --tags --exact-match "$current_commit" 2>/dev/null || true) +current_name=${current_tag:-${current_commit:0:10}} +{ + echo "current_charon=$current_name" + echo "current_charon_commit=$current_commit" + echo "next_charon=$next_tag" + echo "next_charon_commit=$next_commit" +} >> "$GITHUB_ENV" + +echo "------ Start upgrade ------" +echo "- current: $current_name ($current_commit)" +echo "- next: $next_tag ($next_commit)" +echo "---------------------------" + +failure_issue=$(gh issue list --state open --search "\"$failure_title\" in:title" \ + --json number,title --jq ".[] | select(.title == \"$failure_title\") | .number" | head -1) +echo "failure_issue=$failure_issue" >> "$GITHUB_ENV" + +if [ "$next_commit" = "$current_commit" ]; then + echo "Skip update: already at $next_tag" + echo "next_step=none" >> "$GITHUB_ENV" + exit 0 +fi +if git ls-remote --exit-code origin "charon-$next_tag" > /dev/null; then + echo "Skip update: found existing branch charon-$next_tag" + echo "next_step=none" >> "$GITHUB_ENV" + exit 0 +fi +if [ -n "$failure_issue" ] && \ + gh issue view "$failure_issue" --json body,comments --jq '.body, .comments[].body' | \ + grep -qF "$next_tag"; then + echo "Skip update: issue #$failure_issue already reports $next_tag" + echo "next_step=none" >> "$GITHUB_ENV" + exit 0 +fi + +# The (first-parent, i.e. merged-PR) log of the update, for the PR or issue, capped so that the +# text stays well below GitHub's size limit for issue and PR bodies. +max_log=200 +log=$(git -C charon log --oneline --first-parent "$current_commit..$next_commit") +count=$(echo "$log" | wc -l) +EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64) +{ + echo "charon_log<<$EOF" + echo "Full comparison: https://github.com/AeneasVerif/charon/compare/$current_commit...$next_commit" + echo + echo "$log" | head -n "$max_log" | \ + sed 's#^\([0-9a-f]*\) #https://github.com/AeneasVerif/charon/commit/\1 #' + if [ "$count" -gt "$max_log" ]; then + echo "... and $((count - max_log)) more" + fi + echo "$EOF" +} >> "$GITHUB_ENV" + +git -C charon checkout --quiet "$next_commit" +cargo update -p charon +git diff --stat + +if ./scripts/kani-llbc-regression.sh; then + echo "next_step=create_pr" >> "$GITHUB_ENV" +elif [ -n "$failure_issue" ]; then + echo "next_step=comment_issue" >> "$GITHUB_ENV" +else + echo "next_step=create_issue" >> "$GITHUB_ENV" +fi diff --git a/scripts/toolchain_update.sh b/scripts/toolchain_update.sh index 2140ca340337..cf649df72dc3 100755 --- a/scripts/toolchain_update.sh +++ b/scripts/toolchain_update.sh @@ -56,7 +56,9 @@ then cd .. rm -rf rust.git - if ! ./scripts/kani-regression.sh ; then + # `kani-regression.sh` does not build the LLBC backend (and with it Charon), so a toolchain that + # only breaks the LLBC backend would otherwise go unnoticed until the PR's LLBC job. + if ! ./scripts/kani-regression.sh || ! ./scripts/kani-llbc-regression.sh ; then echo "next_step=create_issue" >> $GITHUB_ENV fi else