Make the LLBC regression require Kani to exit successfully

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 };

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."

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<TestTimeOptions>,
 

tools/compiletest/src/main.rs

@@ -95,6 +95,8 @@ pub fn parse_config(args: Vec<String>) -> 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<String>) -> 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!(

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`.