Switch to rustc's archive builder

Cargo.lock

@@ -98,12 +98,6 @@ version = "1.0.71"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8"
 
-[[package]]
-name = "ar"
-version = "0.9.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d67af77d68a931ecd5cbd8a3b5987d63a1d1d1278f7f6a60ae33db485cdebb69"
-
 [[package]]
 name = "atty"
 version = "0.2.14"
@@ -558,7 +552,6 @@ dependencies = [
 name = "kani-compiler"
 version = "0.28.0"
 dependencies = [
- "ar",
  "atty",
  "clap",
  "cprover_bindings",

kani-compiler/Cargo.toml

@@ -9,7 +9,6 @@ license = "MIT OR Apache-2.0"
 publish = false
 
 [dependencies]
-ar = { version = "0.9.0", optional = true }
 atty = "0.2.14"
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = { version = "4.1.3", features = ["cargo"] }
@@ -34,7 +33,7 @@ tracing-tree = "0.2.2"
 # Future proofing: enable backend dependencies using feature.
 [features]
 default = ['cprover']
-cprover = ['ar', 'cbmc', 'libc', 'num', 'object', 'serde',
+cprover = ['cbmc', 'libc', 'num', 'object', 'serde',
     'serde_json', "strum", "strum_macros"]
 write_json_symtab = []
 

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -3,7 +3,6 @@
 
 //! This file contains the code necessary to interface with the compiler backend
 
-use crate::codegen_cprover_gotoc::archive::ArchiveBuilder;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::is_proof_harness;
@@ -24,6 +23,9 @@ use kani_metadata::CompilerArtifactStub;
 use kani_metadata::UnsupportedFeature;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
 use kani_queries::{QueryDb, ReachabilityType, UserInput};
+use rustc_codegen_ssa::back::archive::{
+    get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder,
+};
 use rustc_codegen_ssa::back::metadata::create_wrapper_file;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
@@ -338,7 +340,7 @@ impl CodegenBackend for GotocCodegenBackend {
             debug!(?crate_type, ?out_path, "link");
             if *crate_type == CrateType::Rlib {
                 // Emit the `rlib` that contains just one file: `<crate>.rmeta`
-                let mut builder = ArchiveBuilder::new(sess);
+                let mut builder = Box::new(ArArchiveBuilder::new(sess, get_native_object_symbols));
                 let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap();
                 let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps);
                 let (metadata, _metadata_position) = create_wrapper_file(

kani-compiler/src/codegen_cprover_gotoc/mod.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-mod archive;
 mod codegen;
 mod compiler_interface;
 mod context;