Stop after codegen with -Z lean instead of failing to link a goto model - #4924
Merged
feliperodri merged 2 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 bypass harness validation and silently ignore requested verification output files.
Review effort: Balanced
Findings: 1
Open (2)
What changed in this PR
Stops LLBC (-Z lean) runs after compilation instead of attempting unavailable goto-model linking and verification.
Changes:
- Detects LLBC backend usage centrally.
- Skips goto linking and verification for standalone, Cargo, and autoharness flows.
- Preserves compiler translation errors.
| File | Description |
|---|---|
kani-driver/src/args/mod.rs |
Adds LLBC backend detection. |
kani-driver/src/project.rs |
Avoids creating LLBC link jobs. |
kani-driver/src/main.rs |
Stops standard flows after LLBC compilation. |
kani-driver/src/autoharness/mod.rs |
Stops autoharness after LLBC compilation. |
💡 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>
feliperodri
approved these changes
Sep 30, 2026
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.
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-compilertranslates to LLBC under-Z leanand writes no goto program, but the driver still went on to link one for every harness. Everykani file.rs -Zlean --print-llbctherefore printed the LLBC and then ended withand exit status 1, even when the translation had succeeded. On current main all 23
tests/llbctests 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-codegendoes:Project::try_newcreates no link jobs, and the standalone,cargo kaniand 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--harnessfilter that matches nothing (or a missing one under--exact) is still an error, and--export-jsonand--sarifare 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-llbcprints the LLBC and exits 0 (was 1 with the error above).kani -Z lean --harness typo(also with--exact) andcargo kani -Z lean --harness typofail with "Failed to match the following harness(es)"; a matching--harnesssucceeds.-Z leanwith--export-jsonor--sarifis rejected as a conflict; the argument tests cover both.cargo test -p kani-driverpasses (105/105); theexpected(487 passed, 0 failed) andui(152/152) suites andkani-llbc-regression.shpass; fmt and both CI clippy invocations are clean.#4925 makes
kani-llbc-regression.shcheck exit statuses, which is what Copilot pointed out on #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.