Stub linker to avoid missing symbols errors (#3858)

Kani compiler does not generate real object files when compiling a crate
and its dependencies for verification. Instead, the compiler generates
goto binaries. This can cause linking errors. Instead, stub it with
echo.

We should consider creating a stub linker instead, but echo will do it
for now.

Note that this change only applies to target artifacts, not those
compiled for the host, such as build dependencies and build scripts.

Resolves #3817 

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

Author: celinval

kani-driver/src/call_single_file.rs

@@ -181,6 +181,8 @@ impl KaniSession {
                 "-Z",
                 "mir-enable-passes=-RemoveStorageMarkers",
                 "--check-cfg=cfg(kani)",
+                // Do not invoke the linker since the compiler will not generate real object files
+                "-Clinker=echo",
             ]
             .map(OsString::from),
         );

tests/cargo-kani/issue-3817/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "issue-3817"
+version = "0.1.0"
+edition = "2024"
+description = "Issue with linking cdylib and another shared library"
+
+[lib]
+crate-type = ["cdylib", "rlib"]
+
+[dependencies]
+bzip2 = "0.5.0"
+
+[profile.release]
+lto = true

tests/cargo-kani/issue-3817/expected

@@ -0,0 +1,9 @@
+Checking harness check_unreachable_extern_fn...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_missing_extern_fn...
+Failed Checks: call to foreign "C" function `BZ2_bzCompressInit` is not currently supported by Kani.
+VERIFICATION:- FAILED
+
+Verification failed for - check_missing_extern_fn
+1 successfully verified harnesses, 1 failures, 2 total

tests/cargo-kani/issue-3817/src/lib.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani can compile a crate that depends on bzip, and the analysis will only
+//! fail if a missing symbol is reachable.
+
+use bzip2::Compression;
+use bzip2::read::BzEncoder;
+
+#[kani::proof]
+fn check_missing_extern_fn() {
+    // Call bzip compressor
+    let data: [u8; 10] = kani::any();
+    let compressor = BzEncoder::new(&data[..], Compression::best());
+    assert_eq!(compressor.total_in(), data.len().try_into().unwrap());
+}
+
+#[kani::proof]
+fn check_unreachable_extern_fn() {
+    let positive = kani::any_where(|v: &i8| *v > 0);
+    if positive == 0 {
+        // This should be unreachable so verification should succeed.
+        check_missing_extern_fn();
+    }
+}