From 627be34f407cf3e45186ed35f55a37f8e9e37fd0 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 23 May 2023 09:45:44 -0700 Subject: [PATCH] Switch to rustc's archive builder --- Cargo.lock | 7 -- kani-compiler/Cargo.toml | 3 +- .../src/codegen_cprover_gotoc/archive.rs | 91 ------------------- .../compiler_interface.rs | 6 +- .../src/codegen_cprover_gotoc/mod.rs | 1 - 5 files changed, 5 insertions(+), 103 deletions(-) delete mode 100644 kani-compiler/src/codegen_cprover_gotoc/archive.rs diff --git a/Cargo.lock b/Cargo.lock index 8cfba7c025ff..a73a76e141d9 100644 --- a/Cargo.lock +++ b/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", diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index f7730597eca6..55146532eb7f 100644 --- a/kani-compiler/Cargo.toml +++ b/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 = [] diff --git a/kani-compiler/src/codegen_cprover_gotoc/archive.rs b/kani-compiler/src/codegen_cprover_gotoc/archive.rs deleted file mode 100644 index 3909ca1135b2..000000000000 --- a/kani-compiler/src/codegen_cprover_gotoc/archive.rs +++ /dev/null @@ -1,91 +0,0 @@ -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -// Modifications Copyright Kani Contributors -// See GitHub history for details. -// This file is a heavily modified version of upstream rustc: -// compiler/rustc_codegen_cranelift/src/archive.rs - -//! Creation of ar archives like for the lib and staticlib crate type -//! We now call the ArchiveBuilder directly, so we don't bother trying to fit into the rustc's -//! `ArchiveBuilder`. -//! Note that once we update to a version newer than 2022-12-04 we should be able to remove the -//! logic here and use the compiler ArArchiveBuilder introduced here: -//! - -use rustc_session::Session; -use std::fs::File; -use std::path::{Path, PathBuf}; - -pub(crate) struct ArchiveBuilder<'a> { - sess: &'a Session, - use_gnu_style_archive: bool, - - // Don't use `HashMap` here, as the order is important. `rust.metadata.bin` must always be at - // the end of an archive for linkers to not get confused. - entries: Vec<(Vec, PathBuf)>, -} - -impl<'a> ArchiveBuilder<'a> { - pub fn add_file(&mut self, file: &Path) { - self.entries.push(( - file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(), - file.to_owned(), - )); - } - - pub fn build(&self, output: &Path) -> bool { - enum BuilderKind { - Bsd(ar::Builder), - Gnu(ar::GnuBuilder), - } - - let sess = self.sess; - - let mut builder = if self.use_gnu_style_archive { - BuilderKind::Gnu(ar::GnuBuilder::new( - File::create(&output).unwrap_or_else(|err| { - sess.fatal(&format!( - "error opening destination during archive building: {err}" - )); - }), - self.entries.iter().map(|(name, _)| name.clone()).collect(), - )) - } else { - BuilderKind::Bsd(ar::Builder::new(File::create(&output).unwrap_or_else(|err| { - sess.fatal(&format!("error opening destination during archive building: {err}")); - }))) - }; - - let entries = self.entries.iter().map(|(entry_name, file)| { - let data = std::fs::read(file).unwrap_or_else(|err| { - sess.fatal(&format!( - "error while reading object file during archive building: {err}" - )); - }); - (entry_name, data) - }); - - // Add all files - let mut any_members = false; - for (entry_name, data) in entries { - let header = ar::Header::new(entry_name.clone(), data.len() as u64); - match builder { - BuilderKind::Bsd(ref mut builder) => builder.append(&header, &mut &*data).unwrap(), - BuilderKind::Gnu(ref mut builder) => builder.append(&header, &mut &*data).unwrap(), - } - any_members = true; - } - - // Finalize archive - std::mem::drop(builder); - any_members - } - - pub fn new(sess: &'a Session) -> Self { - ArchiveBuilder { - sess, - use_gnu_style_archive: sess.target.archive_format == "gnu", - entries: vec![], - } - } -} diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 318334805283..910fe63924e5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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: `.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( diff --git a/kani-compiler/src/codegen_cprover_gotoc/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/mod.rs index da98c9f07030..7454d748d660 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/mod.rs +++ b/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;