Add an option to skip codegen (#4002)

This PR adds a new unstable option, `--no-codegen`, that can be used for
running Kani, just to check if the code compiles, i.e. similar to
running `cargo check`. This is useful as a lightweight check for
compilation errors including code under `#[cfg(kani)]`.

This is implemented through passing rustc's `-Zno-codegen` option, which
is what `cargo check` passes to `rustc`.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <cmzech@amazon.com>

Author: zhassan-aws

Cargo.toml

@@ -73,6 +73,8 @@ exclude = [
   "tests/script-based-pre/build-cache-dirty/target/new_dep",
   "tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std",
   "tests/script-based-pre/kani_lib_dep",
+  "tests/script-based-pre/no_codegen",
+  "tests/script-based-pre/no_codegen_error",
 ]
 
 [workspace.lints.clippy]

kani-driver/src/args/mod.rs

@@ -242,6 +242,11 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub only_codegen: bool,
 
+    /// Run Kani without codegen. Useful for quick feedback on whether the code would compile successfully (similar to `cargo check`).
+    /// This feature is unstable and requires `-Z unstable-options` to be used
+    #[arg(long, hide_short_help = true)]
+    pub no_codegen: bool,
+
     /// Specify the value used for loop unwinding in CBMC
     #[arg(long)]
     pub default_unwind: Option<u32>,
@@ -660,6 +665,12 @@ impl ValidateArgs for VerificationArgs {
             UnstableFeature::UnstableOptions,
         )?;
 
+        self.common_args.check_unstable(
+            self.no_codegen,
+            "--no-codegen",
+            UnstableFeature::UnstableOptions,
+        )?;
+
         self.common_args.check_unstable(
             self.jobs.is_some(),
             "--jobs",

kani-driver/src/call_single_file.rs

@@ -182,6 +182,11 @@ impl KaniSession {
             .map(OsString::from),
         );
 
+        if self.args.no_codegen {
+            flags.push("-Z".into());
+            flags.push("no-codegen".into());
+        }
+
         if let Some(seed_opt) = self.args.randomize_layout {
             flags.push("-Z".into());
             flags.push("randomize-layout".into());

kani-driver/src/project.rs

@@ -6,7 +6,7 @@
 
 use crate::metadata::from_json;
 use crate::session::KaniSession;
-use crate::util::crate_name;
+use crate::util::{crate_name, info_operation};
 use anyhow::{Context, Result};
 use kani_metadata::{
     ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, artifact::convert_type,
@@ -177,6 +177,13 @@ impl Artifact {
 /// be collected from the project.
 pub fn cargo_project(session: &mut KaniSession, keep_going: bool) -> Result<Project> {
     let outputs = session.cargo_build(keep_going)?;
+    if session.args.no_codegen {
+        info_operation(
+            "info:",
+            "Compilation succeeded up until codegen. Skipping codegen because of `--no-codegen` option. Rerun without `--no-codegen` to perform codegen.",
+        );
+        return Ok(Project::default());
+    }
     let outdir = outputs.outdir.canonicalize()?;
     // For the MIR Linker we know there is only one metadata per crate. Use that in our favor.
     let metadata =

tests/script-based-pre/no_codegen/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "no_codegen"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

tests/script-based-pre/no_codegen/config.yml

@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: run.sh
+expected: expected
+exit_code: 0

tests/script-based-pre/no_codegen/expected

@@ -0,0 +1 @@
+info: Compilation succeeded up until codegen. Skipping codegen because of `--no-codegen` option. Rerun without `--no-codegen` to perform codegen.

tests/script-based-pre/no_codegen/run.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+rm -rf target
+
+# Test the behavior of the `--no-codegen` option
+cargo kani --no-codegen -Zunstable-options
+
+# Ensure no goto binaries (*.out) are generated
+[[ -z $(find target -name "*.out") ]] || {
+    echo "ERROR: Found goto binaries (*.out) in target directory"
+    exit 1
+}

tests/script-based-pre/no_codegen/src/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the behavior of Kani's `--no-codegen` option
+
+#[kani::proof]
+fn main() {
+    let x: u8 = kani::any();
+    if x < 100 {
+        assert!(x < 101);
+    } else {
+        assert!(x > 99);
+    }
+}

tests/script-based-pre/no_codegen_error/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "no_codegen_error"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]