Add a weekly Charon update job, and run the LLBC regression in the toolchain job - #4920
Merged
Merged
Conversation
…olchain job Charon tags `nightly-YYYY.MM.DD` almost daily, but nothing noticed the pin drifting: before model-checking#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 <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The LLBC update gates can accept failed Kani processes because expected-mode tests ignore their exit status.
Review effort: Balanced
Findings: 2
Open (2)
What changed in this PR
Adds automated weekly Charon updates and expands toolchain-upgrade validation to include the LLBC backend.
Changes:
- Adds Charon update, regression, PR, and failure-issue automation.
- Runs LLBC regression during toolchain upgrades.
| File | Description |
|---|---|
.github/workflows/charon-update.yml |
Defines the weekly update workflow. |
scripts/charon_update.sh |
Implements Charon update and reporting logic. |
scripts/toolchain_update.sh |
Adds LLBC regression to toolchain validation. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
This was referenced Sep 30, 2026
feliperodri
approved these changes
Sep 30, 2026
srivatsansamraj
pushed a commit
to srivatsansamraj/kani
that referenced
this pull request
Sep 30, 2026
…odel (model-checking#4924) With `-Z lean`, stop once the compiler has run instead of trying to link a goto model that the LLBC backend never writes. **The bug.** `kani-compiler` translates to LLBC under `-Z lean` and writes no goto program, but the driver still went on to link one for every harness. Every `kani file.rs -Zlean --print-llbc` therefore printed the LLBC and then ended with ``` error: Failed to canonicalize harness model .../test__...main.symtab.out: No such file or directory (os error 2) ``` and exit status 1, even when the translation had succeeded. On current main all 23 `tests/llbc` tests exit with status 1 this way. The llbc tests only compare output, so nothing noticed, but it also means a real failure of the LLBC backend cannot be told apart from success by exit status. **The fix.** With the LLBC backend there is nothing to link or verify, so the driver now stops after compilation, as `--only-codegen` does: `Project::try_new` creates no link jobs, and the standalone, `cargo kani` and autoharness entry points skip verification. A failing translation (a compiler panic, or Charon reporting errors) still exits with an error. Stopping early must not skip what the driver checks before verification (both from Copilot's review): the LLBC path still runs `determine_targets`, so a `--harness` filter that matches nothing (or a missing one under `--exact`) is still an error, and `--export-json` and `--sarif` are rejected with `-Z lean`, as they are with `--only-codegen`, since nothing would write the requested file. **Manual testing.** - `kani tests/llbc/basic0/test.rs -Zlean --print-llbc` prints the LLBC and exits 0 (was 1 with the error above). - A program that makes the LLBC translation panic still exits 1. - `kani -Z lean --harness typo` (also with `--exact`) and `cargo kani -Z lean --harness typo` fail with "Failed to match the following harness(es)"; a matching `--harness` succeeds. `-Z lean` with `--export-json` or `--sarif` is rejected as a conflict; the argument tests cover both. - All 23 llbc tests exit 0; checked with the compiletest flag from model-checking#4925. - `cargo test -p kani-driver` passes (105/105); the `expected` (487 passed, 0 failed) and `ui` (152/152) suites and `kani-llbc-regression.sh` pass; fmt and both CI clippy invocations are clean. model-checking#4925 makes `kani-llbc-regression.sh` check exit statuses, which is what Copilot pointed out on model-checking#4920; it is stacked on this one. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
srivatsansamraj
pushed a commit
to srivatsansamraj/kani
that referenced
this pull request
Sep 30, 2026
…cking#4925) **Stacked on model-checking#4924**: the first two commits are model-checking#4924 and drop out once it merges; only the last commit (`e251cab38`) is new here. Make `kani-llbc-regression.sh` fail an llbc test whose Kani invocation exits unsuccessfully, not only one whose output misses the expected lines. **Context.** Copilot pointed this out on model-checking#4920 ([1](model-checking#4920 (comment)), [2](model-checking#4920 (comment))): compiletest's `expected` mode (`run_expected_test`) only checks that the output contains the expected lines and ignores the exit status. That is what many `expected` tests need, since they pin the output of a failing verification. For the llbc suite it means a Kani run that prints the expected LLBC and then fails (Charon reporting errors, a driver error) still passes. `kani-llbc-regression.sh` is what CI's LLBC job runs, and what the toolchain and Charon update jobs in model-checking#4920 use to decide between a PR and an issue. **The change.** A new opt-in compiletest flag, `--require-success`, additionally fails an `expected` test whose Kani invocation exits unsuccessfully. `kani-llbc-regression.sh` passes it for the llbc suite. Other suites are unchanged. **Manual testing.** - Without model-checking#4924's fix, `--require-success` fails all 23 llbc tests (they all exit 1), while without the flag all 23 pass: the flag catches what the suite used to miss. - With model-checking#4924, all 23 pass with `--require-success`, and `kani-llbc-regression.sh` passes. - fmt and both CI clippy invocations are clean. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add a weekly job that tries to move the Charon pin to Charon's latest tag, and make the daily toolchain job also run the LLBC regression.
Context. Charon tags
nightly-YYYY.MM.DDalmost every day, but nothing noticed the pin drifting: before #4883 it was 2,176 commits behind, and catching up needed a patch forboxpatterns (removed from nightly Rust) and skipping Charon versions that could no longer be built on current toolchains at all. A weekly attempt would have surfaced each of those changes when it happened.The Charon job (
.github/workflows/charon-update.yml, Wednesdays 04:30 UTC and on demand) runsscripts/charon_update.sh, modelled on the CBMC and toolchain jobs:charonsubmodule to the latestnightly-*tag and runcargo update -p charon;kani-llbc-regression.sh, which covers everything Charon affects (the LLBC build, the-D warningsbuild, llbc clippy and the llbc suite); the fullkani-regression.shdoesn't build Charon, so it isn't needed here;charon-<tag>PR listing the merged Charon PRs since the current pin; the PR gets the full CI, includingcargo denyfor new licenses or git sources;charon-<tag>branch also stops the job.Most failures will need a person (printer changes break expected files, AST renames need code changes), so in practice this is often an early-warning issue with the Charon log attached rather than a ready-to-merge PR.
The toolchain job now runs
kani-llbc-regression.shafterkani-regression.sh, since the latter does not build the LLBC backend: a toolchain that only breaks it (as thebox-pattern removal did) went unnoticed until the PR's LLBC job.Manual testing (the workflow itself only runs on model-checking/kani, so I tested the script):
nightly-2026.09.29):next_step=none.nightly-2026.09.26in a test commit: the script moved it tonightly-2026.09.29,kani-llbc-regression.shpassed (llbc 22/22),next_step=create_pr, and the log section lists the merged PR with a comparison link.kani-llbc-regression.shand a mockedgh: no open issue givescreate_issue; an open issue that doesn't mention the tag givescomment_issue; one that does givesnone.shellcheckis clean on the new script andactionlinton both workflows.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.