diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index fe43c977016e..80cafbbcd2a2 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 @@ -879,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. @@ -1260,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] @@ -1358,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 95b5c660bc67..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,7 +114,13 @@ fn postprocess_project( session.args.common_args.quiet, ); } - if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } + if session.args.only_codegen { + Ok(()) + } else if session.args.uses_llbc_backend() { + codegen_llbc_only(&project, &session) + } 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..22fec0a3d8ab 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -118,7 +118,13 @@ 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 { + Ok(()) + } else if session.args.uses_llbc_backend() { + codegen_llbc_only(&project, &session) + } else { + verify_project(project, session) + } } /// The main function for the `kani` command. @@ -164,7 +170,21 @@ fn standalone_main() -> Result<()> { (session, project) } }; - if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } + 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. 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 };