Stop after codegen with -Z lean instead of failing to link a goto model

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]

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.

kani-driver/src/main.rs

@@ -118,7 +118,13 @@ fn cargokani_main(input_args: Vec<OsString>) -> 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.

kani-driver/src/project.rs

@@ -122,21 +122,29 @@ impl Project {
         cargo_metadata: Option<cargo_metadata::Metadata>,
     ) -> Result<Self> {
         // 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::<Result<Vec<_>>>()?;
+        // 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::<Result<Vec<_>>>()?
+        };
 
         let build_artifacts = |link_job: &LinkJob| -> Result<Vec<Artifact>> {
             let symtab_out = Artifact { path: link_job.input.clone(), typ: SymTabGoto };