Make the LLBC regression require Kani to exit successfully - #4925
Merged
feliperodri merged 3 commits intoSep 30, 2026
Merged
Conversation
…odel With `-Z lean`, `kani-compiler` translates to LLBC and writes no goto program, but the driver still went on to link one for every harness and failed: every `kani file.rs -Zlean --print-llbc` printed the LLBC and then ended with "error: Failed to canonicalize harness model ....symtab.out: No such file or directory" and exit status 1, even when the translation had succeeded. The llbc tests only compare output, so nothing noticed. With the LLBC backend there is nothing to link or verify, so stop once the compiler has run, as `--only-codegen` does. A failing translation (a compiler panic, or Charon reporting errors) still exits with an error. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
LLBC early returns can report success while silently omitting requested JSON or SARIF output files.
Review effort: Balanced
Findings: 1
Open (1)
What changed in this PR
Ensures LLBC regressions require successful Kani execution, building on the stacked LLBC codegen-only fix.
Changes:
- Adds compiletest’s opt-in
--require-successflag. - Enables the flag for LLBC regression tests.
- Stops LLBC-backed driver paths before linking or verification.
| File | Description |
|---|---|
tools/compiletest/src/runtest.rs |
Checks Kani’s exit status when requested. |
tools/compiletest/src/main.rs |
Parses and logs the new flag. |
tools/compiletest/src/common.rs |
Adds the configuration field. |
scripts/kani-llbc-regression.sh |
Requires successful LLBC test invocations. |
kani-driver/src/project.rs |
Skips nonexistent goto link jobs for LLBC. |
kani-driver/src/main.rs |
Stops LLBC runs after compilation. |
kani-driver/src/autoharness/mod.rs |
Skips LLBC autoharness verification. |
kani-driver/src/args/mod.rs |
Adds LLBC backend detection. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Stopping after codegen with `-Z lean` skipped `determine_targets`, which is where the driver rejects a `--harness` filter that matches nothing (and missing filters under `--exact`); the compiler only filters its metadata, so `kani -Z lean --harness typo` exited successfully having translated no harness. Run `determine_targets` on the LLBC path too. It also made `--export-json` and `--sarif` succeed without writing the requested file, since only `verify_project` writes them. Reject both with `-Z lean`, as `--only-codegen` already does for them, and cover the new conflicts in the argument tests. Both from Copilot's review of model-checking#4924 and model-checking#4925. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
compiletest's `expected` mode only checks that the output contains the expected lines, which is what many `expected` tests need: 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, and so would `kani-llbc-regression.sh`, which CI's LLBC job and the toolchain and Charon update jobs rely on. Add an opt-in `--require-success` flag that additionally fails an `expected` test whose Kani invocation exits unsuccessfully, and pass it for the llbc suite. Other suites are unchanged. Checked: with the previous commit reverted, all 23 llbc tests fail with `--require-success` (and all pass without it); with it, all pass. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
llbc-require-success
branch
from
September 30, 2026 12:41
7823b62 to
e251cab
Compare
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>
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.
Stacked on #4924: the first two commits are #4924 and drop out once it merges; only the last commit (
e251cab38) is new here.Make
kani-llbc-regression.shfail an llbc test whose Kani invocation exits unsuccessfully, not only one whose output misses the expected lines.Context. Copilot pointed this out on #4920 (1, 2): compiletest's
expectedmode (run_expected_test) only checks that the output contains the expected lines and ignores the exit status. That is what manyexpectedtests 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.shis what CI's LLBC job runs, and what the toolchain and Charon update jobs in #4920 use to decide between a PR and an issue.The change. A new opt-in compiletest flag,
--require-success, additionally fails anexpectedtest whose Kani invocation exits unsuccessfully.kani-llbc-regression.shpasses it for the llbc suite. Other suites are unchanged.Manual testing.
-Z leaninstead of failing to link a goto model #4924's fix,--require-successfails all 23 llbc tests (they all exit 1), while without the flag all 23 pass: the flag catches what the suite used to miss.-Z leaninstead of failing to link a goto model #4924, all 23 pass with--require-success, andkani-llbc-regression.shpasses.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.