From b74f8e7f763cbd6812e58ad07f383107de36ca8c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 12:06:53 +0000 Subject: [PATCH 1/3] Stop after codegen with `-Z lean` instead of failing to link a goto model 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 --- kani-driver/src/args/mod.rs | 6 +++++ kani-driver/src/autoharness/mod.rs | 6 ++++- kani-driver/src/main.rs | 12 ++++++++-- kani-driver/src/project.rs | 38 ++++++++++++++++++------------ 4 files changed, 44 insertions(+), 18 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index fe43c977016e..43dd0ed7d939 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -471,6 +471,12 @@ impl NumThreads { } impl VerificationArgs { + /// Whether the LLBC backend (`-Z lean`) replaces the CBMC one. It writes no goto program, so + /// there is nothing to link or verify: Kani stops once the compiler has run. + pub fn uses_llbc_backend(&self) -> bool { + self.common_args.unstable_features.contains(UnstableFeature::Lean) + } + pub fn restrict_vtable(&self) -> bool { self.common_args.unstable_features.contains(UnstableFeature::RestrictVtable) && !self.no_restrict_vtable diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 95b5c660bc67..d1000055625c 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -114,7 +114,11 @@ fn postprocess_project( session.args.common_args.quiet, ); } - if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } + if session.args.only_codegen || session.args.uses_llbc_backend() { + Ok(()) + } else { + verify_project(project, session) + } } /// Print automatic harness metadata to the terminal. diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 7492ada70908..dbbd2dd51ba5 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -118,7 +118,11 @@ fn cargokani_main(input_args: Vec) -> Result<()> { } let project = project::cargo_project(&mut session, false)?; - if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } + if session.args.only_codegen || session.args.uses_llbc_backend() { + Ok(()) + } else { + verify_project(project, session) + } } /// The main function for the `kani` command. @@ -164,7 +168,11 @@ fn standalone_main() -> Result<()> { (session, project) } }; - if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } + if session.args.only_codegen || session.args.uses_llbc_backend() { + Ok(()) + } else { + verify_project(project, session) + } } /// Run verification on the given project. diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 3e2bfb04d2a2..0f1c0978d636 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -122,21 +122,29 @@ impl Project { cargo_metadata: Option, ) -> Result { // For each harness (test or proof) from each metadata, read the path for the goto - // SymTabGoto file. Use that path to find all the other artifacts. - let link_jobs = metadata - .iter() - .flat_map(|crate_metadata| { - crate_metadata.test_harnesses.iter().chain(crate_metadata.proof_harnesses.iter()) - }) - .map(|harness| { - let model_path = harness.goto_file.as_ref().expect("Expected a model file"); - let input = model_path.canonicalize().with_context(|| { - format!("Failed to canonicalize harness model {}", model_path.display()) - })?; - let output = convert_type(&input, SymTabGoto, Goto); - Ok(LinkJob { input, output }) - }) - .collect::>>()?; + // SymTabGoto file. Use that path to find all the other artifacts. The LLBC backend writes + // no goto files, so there is nothing to link. + let link_jobs = if session.args.uses_llbc_backend() { + vec![] + } else { + metadata + .iter() + .flat_map(|crate_metadata| { + crate_metadata + .test_harnesses + .iter() + .chain(crate_metadata.proof_harnesses.iter()) + }) + .map(|harness| { + let model_path = harness.goto_file.as_ref().expect("Expected a model file"); + let input = model_path.canonicalize().with_context(|| { + format!("Failed to canonicalize harness model {}", model_path.display()) + })?; + let output = convert_type(&input, SymTabGoto, Goto); + Ok(LinkJob { input, output }) + }) + .collect::>>()? + }; let build_artifacts = |link_job: &LinkJob| -> Result> { let symtab_out = Artifact { path: link_job.input.clone(), typ: SymTabGoto }; From 2f805922718db879c86aafb53c1cff0a2e2c6397 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 12:39:16 +0000 Subject: [PATCH 2/3] Keep `-Z lean`'s harness checks and reject output files it cannot write 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 #4924 and #4925. Co-authored-by: Kiro --- kani-driver/src/args/mod.rs | 26 ++++++++++++++++++++++++++ kani-driver/src/autoharness/mod.rs | 6 ++++-- kani-driver/src/main.rs | 16 ++++++++++++++-- 3 files changed, 44 insertions(+), 4 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 43dd0ed7d939..80cafbbcd2a2 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -885,6 +885,24 @@ impl ValidateArgs for VerificationArgs { "Conflicting options: --sarif isn't compatible with --only-codegen.", )); } + // The LLBC backend stops after codegen too (see `uses_llbc_backend`), so the same + // holds for it: nothing would write the requested file. + if self.uses_llbc_backend() { + for (requested, option) in [ + (self.sarif.is_some(), "--sarif"), + (self.export_json.is_some(), "--export-json"), + ] { + if requested { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + format!( + "Conflicting options: {option} isn't compatible with {}.", + UnstableFeature::Lean.as_argument_string() + ), + )); + } + } + } // Neither code-generation-only mode runs verification, so there is nothing to export. // `--only-codegen` would otherwise succeed without writing the file the user asked for, // and `--no-codegen` would write a document describing a run that never happened. @@ -1266,6 +1284,10 @@ mod tests { "kani file.rs -Z unstable-options --export-json out.json --no-codegen", ErrorKind::ArgumentConflict, ); + expect_validation_error( + "kani file.rs -Z unstable-options -Z lean --export-json out.json", + ErrorKind::ArgumentConflict, + ); } #[test] @@ -1364,6 +1386,10 @@ mod tests { "kani file.rs --sarif out.sarif --only-codegen", ErrorKind::ArgumentConflict, ); + expect_validation_error( + "kani file.rs -Z lean --sarif out.sarif", + ErrorKind::ArgumentConflict, + ); } #[test] diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index d1000055625c..1472b8844876 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -16,7 +16,7 @@ use crate::list::output::output_list_results; use crate::project::{Project, standalone_project, std_project}; use crate::session::KaniSession; use crate::util::warning; -use crate::{InvocationType, print_kani_version, project, verify_project}; +use crate::{InvocationType, codegen_llbc_only, print_kani_version, project, verify_project}; use anyhow::Result; use comfy_table::Table as PrettyTable; use kani_metadata::{AutoHarnessSkipReason, HarnessMetadata, KaniMetadata}; @@ -114,8 +114,10 @@ fn postprocess_project( session.args.common_args.quiet, ); } - if session.args.only_codegen || session.args.uses_llbc_backend() { + if session.args.only_codegen { Ok(()) + } else if session.args.uses_llbc_backend() { + codegen_llbc_only(&project, &session) } else { verify_project(project, session) } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index dbbd2dd51ba5..22fec0a3d8ab 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -118,8 +118,10 @@ fn cargokani_main(input_args: Vec) -> Result<()> { } let project = project::cargo_project(&mut session, false)?; - if session.args.only_codegen || session.args.uses_llbc_backend() { + if session.args.only_codegen { Ok(()) + } else if session.args.uses_llbc_backend() { + codegen_llbc_only(&project, &session) } else { verify_project(project, session) } @@ -168,13 +170,23 @@ fn standalone_main() -> Result<()> { (session, project) } }; - if session.args.only_codegen || session.args.uses_llbc_backend() { + if session.args.only_codegen { Ok(()) + } else if session.args.uses_llbc_backend() { + codegen_llbc_only(&project, &session) } else { verify_project(project, session) } } +/// Finish a run of the LLBC backend (`-Z lean`), which stops after codegen: there is nothing to +/// link or verify. Still reject `--harness` filters that match nothing, as `verify_project` does: +/// the compiler only filters its metadata and would silently translate no harness. +pub(crate) fn codegen_llbc_only(project: &Project, session: &KaniSession) -> Result<()> { + session.determine_targets(project.get_all_harnesses())?; + Ok(()) +} + /// Run verification on the given project. fn verify_project(project: Project, session: KaniSession) -> Result<()> { debug!(?project, "verify_project"); From e251cab3816580076a71337ef6bda57a6c53dfb2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 12:06:53 +0000 Subject: [PATCH 3/3] Make the LLBC regression require Kani to exit successfully 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 --- scripts/kani-llbc-regression.sh | 4 +++- tools/compiletest/src/common.rs | 4 ++++ tools/compiletest/src/main.rs | 4 ++++ tools/compiletest/src/runtest.rs | 3 +++ 4 files changed, 14 insertions(+), 1 deletion(-) diff --git a/scripts/kani-llbc-regression.sh b/scripts/kani-llbc-regression.sh index b82dd1b9a34b..391a43ce4776 100755 --- a/scripts/kani-llbc-regression.sh +++ b/scripts/kani-llbc-regression.sh @@ -34,8 +34,10 @@ echo "-----------------------------" suite="llbc" mode="expected" echo "Check compiletest suite=$suite mode=$mode" +# `--require-success`: the LLBC tests only pin output, and Kani can print the expected LLBC and +# still fail afterwards (e.g. when Charon reports errors), which would otherwise go unnoticed. cargo run -p compiletest --quiet -- --suite $suite --mode $mode \ - --quiet --no-fail-fast + --quiet --no-fail-fast --require-success echo echo "All Kani llbc regression tests completed successfully." diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index 0ff106c92de3..cbd8f2f9b474 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -153,6 +153,10 @@ pub struct Config { /// relevant expectations. pub fix_expected: bool, + /// Whether an `expected` test also requires Kani to exit successfully. By default only the + /// output is checked, since many `expected` tests pin the output of a failing verification. + pub require_success: bool, + /// Whether we should measure and limit the time of a test. pub time_opts: Option, diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index d965073b816e..a2c363e925d9 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -95,6 +95,8 @@ pub fn parse_config(args: Vec) -> Config { .optopt("", "timeout", "the timeout for each test in seconds", "TIMEOUT") .optflag("", "no-fail-fast", "run all tests regardless of failure") .optflag("", "dry-run", "don't actually run the tests") + .optflag("", "require-success", + "in `expected` mode, also fail a test whose Kani invocation exits unsuccessfully") .optflag("", "fix-expected", "override all expected files that did not match the output. Tests will NOT fail when there is a mismatch") .optflag("", "report-time", @@ -177,6 +179,7 @@ pub fn parse_config(args: Vec) -> Config { fail_fast: !matches.opt_present("no-fail-fast"), dry_run: matches.opt_present("dry-run"), fix_expected: matches.opt_present("fix-expected"), + require_success: matches.opt_present("require-success"), timeout, time_opts: matches .opt_present("report-time") @@ -202,6 +205,7 @@ pub fn log_config(config: &Config) { logv(c, format!("fail-fast: {:?}", config.fail_fast)); logv(c, format!("dry-run: {:?}", config.dry_run)); logv(c, format!("fix-expected: {:?}", config.fix_expected)); + logv(c, format!("require-success: {:?}", config.require_success)); logv( c, format!( diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 38ed5a0ad70d..82526b5d3e45 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -494,6 +494,9 @@ impl TestCx<'_> { self.testpaths.file.parent().unwrap().join("expected") }; self.verify_output(&proc_res, &expected_path); + if self.config.require_success && !proc_res.status.success() { + self.fatal_proc_rec("test failed: Kani exited unsuccessfully", &proc_res); + } } /// Runs Kani in coverage mode on the test file specified by `self.testpaths.file`.