Fix issue when linking rlib + another library type (#3576)

Invoking the native linker was overriding the `json` we create in Kani's
compiler. Thus, invoke the native linker first, then create the `json`
files.

Resolves #3569

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

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -403,13 +403,7 @@ impl CodegenBackend for GotocCodegenBackend {
     /// We need to emit `rlib` files normally if requested. Cargo expects these in some
     /// circumstances and sends them to subsequent builds with `-L`.
     ///
-    /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects.
-    /// What determines whether the native linker is invoked or not is the set of `crate_types`.
-    /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker.
-    ///
-    /// Thus, we manually build the rlib file including only the `rmeta` file.
-    ///
-    /// For cases where no metadata file was requested, we stub the file requested by writing the
+    /// For other crate types, we stub the file requested by writing the
     /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata.
     /// See <https://github.com/model-checking/kani/issues/2234> for more details.
     fn link(
@@ -419,6 +413,14 @@ impl CodegenBackend for GotocCodegenBackend {
         outputs: &OutputFilenames,
     ) -> Result<(), ErrorGuaranteed> {
         let requested_crate_types = &codegen_results.crate_info.crate_types;
+        // Create the rlib if one was requested.
+        if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) {
+            link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?;
+        }
+
+        // But override all the other outputs.
+        // Note: Do this after `link_binary` call, since it may write to the object files
+        // and override the json we are creating.
         for crate_type in requested_crate_types {
             let out_fname = out_filename(
                 sess,
@@ -428,10 +430,7 @@ impl CodegenBackend for GotocCodegenBackend {
             );
             let out_path = out_fname.as_path();
             debug!(?crate_type, ?out_path, "link");
-            if *crate_type == CrateType::Rlib {
-                // Emit the `rlib` that contains just one file: `<crate>.rmeta`
-                link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?
-            } else {
+            if *crate_type != CrateType::Rlib {
                 // Write the location of the kani metadata file in the requested compiler output file.
                 let base_filepath = outputs.path(OutputType::Object);
                 let base_filename = base_filepath.as_path();

tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml

@@ -0,0 +1,13 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "supported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle supported crate types"
+
+[lib]
+name = "lib"
+crate-type = ["cdylib", "rlib"]
+path = "../src/lib.rs"
+

tests/cargo-ui/supported-lib-types/cdylib-rlib/expected

@@ -0,0 +1,2 @@
+Checking harness check_ok...
+VERIFICATION:- SUCCESSFUL