From b74f8e7f763cbd6812e58ad07f383107de36ca8c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 12:06:53 +0000 Subject: [PATCH 1/2] 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/2] 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");