Disable MIR inlining when stubbing is enabled

kani-driver/src/call_cargo.rs

@@ -88,6 +88,7 @@ crate-type = ["lib"]
         // In theory, these could be passed just to the local crate rather than all crates,
         // but the `cargo build` command we use for building `std` doesn't allow you to pass `rustc`
         // arguments, so we have to pass them through the environment variable instead.
+        rustc_args.extend(self.kani_rustc_local_flags());
         rustc_args.push(encode_as_rustc_arg(&self.kani_compiler_local_flags()));
 
         // Ignore global assembly, since `compiler_builtins` has some.
@@ -238,6 +239,7 @@ crate-type = ["lib"]
                     .arg("--") // Add this delimiter so we start passing args to rustc and not Cargo
                     .env("RUSTC", &self.kani_compiler)
                     .pass_rustc_args(&rustc_args, PassTo::AllCrates)
+                    .pass_rustc_args(&self.kani_rustc_local_flags(), PassTo::OnlyLocalCrate)
                     .pass_rustc_arg(encode_as_rustc_arg(&kani_pkg_args), PassTo::OnlyLocalCrate)
                     // This is only required for stable but is a no-op for nightly channels
                     .env("RUSTC_BOOTSTRAP", "1")

kani-driver/src/call_single_file.rs

@@ -66,6 +66,7 @@ impl KaniSession {
 
         let lib_path = lib_folder().unwrap();
         let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
+        rustc_args.extend(self.kani_rustc_local_flags());
         rustc_args.push(file.into());
         rustc_args.push("--out-dir".into());
         rustc_args.push(RustcArg::from(outdir.as_os_str()));
@@ -121,6 +122,19 @@ impl KaniSession {
         flags
     }
 
+    /// The rustc arguments that should be passed only to the local crate being compiled.
+    /// Dependencies skip codegen, so passing these to them would only force recompilation.
+    pub fn kani_rustc_local_flags(&self) -> Vec<RustcArg> {
+        let mut flags = vec![];
+        // The MIR inliner copies a stubbed function into its callers, where the stub pass
+        // cannot replace it.
+        if self.args.is_stubbing_enabled() {
+            flags.push("-Z".into());
+            flags.push("inline-mir=no".into());
+        }
+        flags
+    }
+
     /// The `kani-compiler`-specific arguments that should be passed only to the local crate
     /// being compiled.
     pub fn kani_compiler_local_flags(&self) -> Vec<KaniArg> {

tests/cargo-kani/stubbing-inlined-function/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "stubbing-inlined-function"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+# Enable the MIR inliner for the crate under verification.
+[profile.dev]
+opt-level = 2
+
+[package.metadata.kani.unstable]
+stubbing = true

tests/cargo-kani/stubbing-inlined-function/check_stub_inlined_function.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/stubbing-inlined-function/src/lib.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This tests that stubs are applied to calls the MIR inliner would inline when
+//! building with cargo.
+
+fn target() -> u32 {
+    1
+}
+
+fn caller() -> u32 {
+    target()
+}
+
+fn stub() -> u32 {
+    2
+}
+
+#[kani::proof]
+#[kani::stub(target, stub)]
+fn check_stub_inlined_function() {
+    assert_eq!(caller(), 2);
+}

tests/kani/Stubbing/stub_inlined_function.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+// compile-flags: -Copt-level=2
+//
+//! This tests that stubs are applied to calls the MIR inliner would inline.
+
+fn target() -> u32 {
+    1
+}
+
+fn caller() -> u32 {
+    target()
+}
+
+fn stub() -> u32 {
+    2
+}
+
+#[kani::proof]
+#[kani::stub(target, stub)]
+fn check_stub_inlined_function() {
+    assert_eq!(caller(), 2);
+}