diff --git a/Cargo.lock b/Cargo.lock index 390336c8fde8..a3f9bc2e50be 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -81,9 +81,9 @@ checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6" [[package]] name = "autocfg" -version = "1.3.0" +version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" +checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" [[package]] name = "bitflags" @@ -147,9 +147,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.18" +version = "4.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0956a43b323ac1afaffc053ed5c4b7c1f1800bacd1683c353aabbb752515dd3" +checksum = "7be5744db7978a28d9df86a214130d106a89ce49644cbc4e3f0c22c3fba30615" dependencies = [ "clap_builder", "clap_derive", @@ -157,9 +157,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.18" +version = "4.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d72166dd41634086d5803a47eb71ae740e61d84709c36f3c34110173db3961b" +checksum = "a5fbc17d3ef8278f55b282b2a2e75ae6f6c7d4bb70ed3d0382375104bfafdb4b" dependencies = [ "anstream", "anstyle", @@ -248,15 +248,6 @@ dependencies = [ "tracing", ] -[[package]] -name = "crc32fast" -version = "1.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a97769d94ddab943e4510d138150169a2758b5ef3eb191a9ee688de3e23ef7b3" -dependencies = [ - "cfg-if", -] - [[package]] name = "crossbeam-deque" version = "0.8.5" @@ -420,6 +411,12 @@ dependencies = [ "ahash", ] +[[package]] +name = "hashbrown" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" + [[package]] name = "heck" version = "0.5.0" @@ -437,12 +434,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.5.0" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68b900aa2f7301e21c36462b170ee99994de34dff39a4a6a528e80e7376d07e5" +checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" dependencies = [ "equivalent", - "hashbrown", + "hashbrown 0.15.0", ] [[package]] @@ -485,7 +482,6 @@ dependencies = [ "kani_metadata", "lazy_static", "num", - "object", "quote", "regex", "serde", @@ -573,9 +569,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.158" +version = "0.2.159" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d8adc4bb1803a324070e64a98ae98f38934d91957a99cfb3a43dcbc01bc56439" +checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5" [[package]] name = "linear-map" @@ -728,24 +724,11 @@ dependencies = [ "autocfg", ] -[[package]] -name = "object" -version = "0.36.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "084f1a5821ac4c651660a94a7153d27ac9d8a53736203f58b31945ded098070a" -dependencies = [ - "crc32fast", - "hashbrown", - "indexmap", - "memchr", - "wasmparser", -] - [[package]] name = "once_cell" -version = "1.19.0" +version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" +checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "os_info" @@ -915,23 +898,23 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.4" +version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0884ad60e090bf1345b93da0a5de8923c93884cd03f40dfcfddd3b4bee661853" +checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" dependencies = [ "bitflags", ] [[package]] name = "regex" -version = "1.10.6" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4219d74c6b67a3654a9fbebc4b419e22126d13d2f3c4a07ee0cb61ff79a79619" +checksum = "38200e5ee88914975b69f657f0801b6f6dccafd44fd9326302a4aaeecfacb1d8" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.4.7", - "regex-syntax 0.8.4", + "regex-automata 0.4.8", + "regex-syntax 0.8.5", ] [[package]] @@ -945,13 +928,13 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.7" +version = "0.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df" +checksum = "368758f23274712b504848e9d5a6f010445cc8b87a7cdb4d7cbee666c1288da3" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.8.4", + "regex-syntax 0.8.5", ] [[package]] @@ -962,9 +945,9 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" [[package]] name = "regex-syntax" -version = "0.8.4" +version = "0.8.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b" +checksum = "2b15c43186be67a4fd63bee50d0303afffcef381492ebe2c5d87f324e1b8815c" [[package]] name = "rustc-demangle" @@ -1067,9 +1050,9 @@ dependencies = [ [[package]] name = "serde_spanned" -version = "0.6.7" +version = "0.6.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb5b1b31579f3811bf615c144393417496f152e12ac8b7663bf664f4a815306d" +checksum = "87607cb1398ed59d48732e575a4c28a7a8ebf2454b964fe3f224f2afc07909e1" dependencies = [ "serde", ] @@ -1131,7 +1114,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e" dependencies = [ "cfg-if", - "hashbrown", + "hashbrown 0.14.5", "serde", ] @@ -1162,9 +1145,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.77" +version = "2.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed" +checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" dependencies = [ "proc-macro2", "quote", @@ -1173,9 +1156,9 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.12.0" +version = "3.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04cbcdd0c794ebb0d4cf35e88edd2f7d2c4c3e9a5a6dab322839b321c6a87a64" +checksum = "f0f2c9fc62d0beef6951ccffd757e241266a2c833136efbe35af6cd2567dca5b" dependencies = [ "cfg-if", "fastrand", @@ -1268,9 +1251,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.21" +version = "0.22.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b072cee73c449a636ffd6f32bd8de3a9f7119139aff882f44943ce2986dc5cf" +checksum = "4ae48d6208a266e853d946088ed816055e556cc6028c5e8e2b84d9fa5dd7c7f5" dependencies = [ "indexmap", "serde", @@ -1427,15 +1410,6 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" -[[package]] -name = "wasmparser" -version = "0.216.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcdee6bea3619d311fb4b299721e89a986c3470f804b6d534340e412589028e3" -dependencies = [ - "bitflags", -] - [[package]] name = "which" version = "6.0.3" @@ -1563,9 +1537,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.18" +version = "0.6.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68a9bda4691f099d435ad181000724da8e5899daa10713c2d432552b9ccd3a6f" +checksum = "36c1fec1a2bb5866f07c25f68c26e565c4c200aebb96d7e55710c19d3e8ac49b" dependencies = [ "memchr", ] diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9a4a0de43a34..9ca8d10f5275 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -28,11 +28,6 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} tracing-tree = "0.4.0" -[dependencies.object] -version = "0.36.2" -default-features = false -features = ["elf", "macho", "pe", "xcoff", "write", "wasm"] - # Future proofing: enable backend dependencies using feature. [features] default = ['cprover'] diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9ef8bdf314c2..2049a4159c29 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -24,20 +24,15 @@ use kani_metadata::artifact::convert_type; use kani_metadata::UnsupportedFeature; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; -use object::write::{self, StandardSegment, Symbol, SymbolSection}; -use object::{ - elf, pe, xcoff, Architecture, BinaryFormat, Endianness, FileFlags, SectionFlags, SectionKind, - SubArchitecture, SymbolFlags, SymbolKind, SymbolScope, +use rustc_codegen_ssa::back::archive::{ + ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, }; -use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER}; -use rustc_codegen_ssa::back::metadata::create_metadata_file_for_wasm; +use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; -use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; -use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::ty::TyCtxt; @@ -46,9 +41,8 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_session::Session; use rustc_smir::rustc_internal; -use rustc_span::sym; use rustc_target::abi::Endian; -use rustc_target::spec::{ef_avr_arch, PanicStrategy, RelocModel, Target}; +use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; @@ -61,7 +55,6 @@ use std::path::{Path, PathBuf}; use std::process::Command; use std::sync::{Arc, Mutex}; use std::time::Instant; -use tempfile::Builder as TempFileBuilder; use tracing::{debug, error, info}; pub type UnsupportedConstructs = FxHashMap>; @@ -229,292 +222,6 @@ impl GotocCodegenBackend { } } -// Copy of macho_object_build_version_for_target from -// rust/compiler/rustc_codegen_ssa/src/back/metadata.rs -fn macho_object_build_version_for_target(target: &Target) -> object::write::MachOBuildVersion { - /// The `object` crate demands "X.Y.Z encoded in nibbles as xxxx.yy.zz" - /// e.g. minOS 14.0 = 0x000E0000, or SDK 16.2 = 0x00100200 - fn pack_version((major, minor, patch): (u16, u8, u8)) -> u32 { - let (major, minor, patch) = (major as u32, minor as u32, patch as u32); - (major << 16) | (minor << 8) | patch - } - - let platform = - rustc_target::spec::current_apple_platform(target).expect("unknown Apple target OS"); - let min_os = rustc_target::spec::current_apple_deployment_target(target); - let (sdk_major, sdk_minor) = - rustc_target::spec::current_apple_sdk_version(platform).expect("unknown Apple target OS"); - - let mut build_version = object::write::MachOBuildVersion::default(); - build_version.platform = platform; - build_version.minos = pack_version(min_os); - build_version.sdk = pack_version((sdk_major, sdk_minor, 0)); - build_version -} - -// Copy of create_object_file from -// rust/compiler/rustc_codegen_ssa/src/back/metadata.rs -fn create_object_file(sess: &Session) -> Option> { - let endianness = match sess.target.options.endian { - Endian::Little => Endianness::Little, - Endian::Big => Endianness::Big, - }; - let (architecture, sub_architecture) = match &sess.target.arch[..] { - "arm" => (Architecture::Arm, None), - "aarch64" => ( - if sess.target.pointer_width == 32 { - Architecture::Aarch64_Ilp32 - } else { - Architecture::Aarch64 - }, - None, - ), - "x86" => (Architecture::I386, None), - "s390x" => (Architecture::S390x, None), - "mips" | "mips32r6" => (Architecture::Mips, None), - "mips64" | "mips64r6" => (Architecture::Mips64, None), - "x86_64" => ( - if sess.target.pointer_width == 32 { - Architecture::X86_64_X32 - } else { - Architecture::X86_64 - }, - None, - ), - "powerpc" => (Architecture::PowerPc, None), - "powerpc64" => (Architecture::PowerPc64, None), - "riscv32" => (Architecture::Riscv32, None), - "riscv64" => (Architecture::Riscv64, None), - "sparc" => (Architecture::Sparc32Plus, None), - "sparc64" => (Architecture::Sparc64, None), - "avr" => (Architecture::Avr, None), - "msp430" => (Architecture::Msp430, None), - "hexagon" => (Architecture::Hexagon, None), - "bpf" => (Architecture::Bpf, None), - "loongarch64" => (Architecture::LoongArch64, None), - "csky" => (Architecture::Csky, None), - "arm64ec" => (Architecture::Aarch64, Some(SubArchitecture::Arm64EC)), - // Unsupported architecture. - _ => return None, - }; - let binary_format = if sess.target.is_like_osx { - BinaryFormat::MachO - } else if sess.target.is_like_windows { - BinaryFormat::Coff - } else if sess.target.is_like_aix { - BinaryFormat::Xcoff - } else { - BinaryFormat::Elf - }; - - let mut file = write::Object::new(binary_format, architecture, endianness); - file.set_sub_architecture(sub_architecture); - if sess.target.is_like_osx { - if sess.target.llvm_target.starts_with("arm64e") { - file.set_macho_cpu_subtype(object::macho::CPU_SUBTYPE_ARM64E); - } - - file.set_macho_build_version(macho_object_build_version_for_target(&sess.target)) - } - if binary_format == BinaryFormat::Coff { - // Disable the default mangler to avoid mangling the special "@feat.00" symbol name. - let original_mangling = file.mangling(); - file.set_mangling(object::write::Mangling::None); - - let mut feature = 0; - - if file.architecture() == object::Architecture::I386 { - // When linking with /SAFESEH on x86, lld requires that all linker inputs be marked as - // safe exception handling compatible. Metadata files masquerade as regular COFF - // objects and are treated as linker inputs, despite containing no actual code. Thus, - // they still need to be marked as safe exception handling compatible. See #96498. - // Reference: https://docs.microsoft.com/en-us/windows/win32/debug/pe-format - feature |= 1; - } - - file.add_symbol(object::write::Symbol { - name: "@feat.00".into(), - value: feature, - size: 0, - kind: object::SymbolKind::Data, - scope: object::SymbolScope::Compilation, - weak: false, - section: object::write::SymbolSection::Absolute, - flags: object::SymbolFlags::None, - }); - - file.set_mangling(original_mangling); - } - let e_flags = match architecture { - Architecture::Mips => { - let arch = match sess.target.options.cpu.as_ref() { - "mips1" => elf::EF_MIPS_ARCH_1, - "mips2" => elf::EF_MIPS_ARCH_2, - "mips3" => elf::EF_MIPS_ARCH_3, - "mips4" => elf::EF_MIPS_ARCH_4, - "mips5" => elf::EF_MIPS_ARCH_5, - s if s.contains("r6") => elf::EF_MIPS_ARCH_32R6, - _ => elf::EF_MIPS_ARCH_32R2, - }; - - let mut e_flags = elf::EF_MIPS_CPIC | arch; - - // If the ABI is explicitly given, use it or default to O32. - match sess.target.options.llvm_abiname.to_lowercase().as_str() { - "n32" => e_flags |= elf::EF_MIPS_ABI2, - "o32" => e_flags |= elf::EF_MIPS_ABI_O32, - _ => e_flags |= elf::EF_MIPS_ABI_O32, - }; - - if sess.target.options.relocation_model != RelocModel::Static { - e_flags |= elf::EF_MIPS_PIC; - } - if sess.target.options.cpu.contains("r6") { - e_flags |= elf::EF_MIPS_NAN2008; - } - e_flags - } - Architecture::Mips64 => { - // copied from `mips64el-linux-gnuabi64-gcc foo.c -c` - elf::EF_MIPS_CPIC - | elf::EF_MIPS_PIC - | if sess.target.options.cpu.contains("r6") { - elf::EF_MIPS_ARCH_64R6 | elf::EF_MIPS_NAN2008 - } else { - elf::EF_MIPS_ARCH_64R2 - } - } - Architecture::Riscv32 | Architecture::Riscv64 => { - // Source: https://github.com/riscv-non-isa/riscv-elf-psabi-doc/blob/079772828bd10933d34121117a222b4cc0ee2200/riscv-elf.adoc - let mut e_flags: u32 = 0x0; - - // Check if compressed is enabled - // `unstable_target_features` is used here because "c" is gated behind riscv_target_feature. - if sess.unstable_target_features.contains(&sym::c) { - e_flags |= elf::EF_RISCV_RVC; - } - - // Set the appropriate flag based on ABI - // This needs to match LLVM `RISCVELFStreamer.cpp` - match &*sess.target.llvm_abiname { - "" | "ilp32" | "lp64" => (), - "ilp32f" | "lp64f" => e_flags |= elf::EF_RISCV_FLOAT_ABI_SINGLE, - "ilp32d" | "lp64d" => e_flags |= elf::EF_RISCV_FLOAT_ABI_DOUBLE, - "ilp32e" => e_flags |= elf::EF_RISCV_RVE, - _ => panic!("unknown RISC-V ABI name"), - } - - e_flags - } - Architecture::LoongArch64 => { - // Source: https://github.com/loongson/la-abi-specs/blob/release/laelf.adoc#e_flags-identifies-abi-type-and-version - let mut e_flags: u32 = elf::EF_LARCH_OBJABI_V1; - - // Set the appropriate flag based on ABI - // This needs to match LLVM `LoongArchELFStreamer.cpp` - match &*sess.target.llvm_abiname { - "ilp32s" | "lp64s" => e_flags |= elf::EF_LARCH_ABI_SOFT_FLOAT, - "ilp32f" | "lp64f" => e_flags |= elf::EF_LARCH_ABI_SINGLE_FLOAT, - "ilp32d" | "lp64d" => e_flags |= elf::EF_LARCH_ABI_DOUBLE_FLOAT, - _ => panic!("unknown LoongArch ABI name"), - } - - e_flags - } - Architecture::Avr => { - // Resolve the ISA revision and set - // the appropriate EF_AVR_ARCH flag. - ef_avr_arch(&sess.target.options.cpu) - } - Architecture::Csky => { - let e_flags = match sess.target.options.abi.as_ref() { - "abiv2" => elf::EF_CSKY_ABIV2, - _ => elf::EF_CSKY_ABIV1, - }; - e_flags - } - _ => 0, - }; - // adapted from LLVM's `MCELFObjectTargetWriter::getOSABI` - let os_abi = match sess.target.options.os.as_ref() { - "hermit" => elf::ELFOSABI_STANDALONE, - "freebsd" => elf::ELFOSABI_FREEBSD, - "solaris" => elf::ELFOSABI_SOLARIS, - _ => elf::ELFOSABI_NONE, - }; - let abi_version = 0; - // rustc implementation also does: - // add_gnu_property_note(&mut file, architecture, binary_format, endianness); - file.flags = FileFlags::Elf { os_abi, abi_version, e_flags }; - Some(file) -} - -// copy of create_wrapper_file from -// rust/compiler/rustc_codegen_ssa/src/back/metadata.rs -// without the MetadataPosition return value, which we don't need -fn create_wrapper_file(sess: &Session, section_name: String, data: &[u8]) -> Vec { - let Some(mut file) = create_object_file(sess) else { - if sess.target.is_like_wasm { - return create_metadata_file_for_wasm(sess, data, §ion_name); - } - - // Targets using this branch don't have support implemented here yet or - // they're not yet implemented in the `object` crate and will likely - // fill out this module over time. - return data.to_vec(); - }; - let section = if file.format() == BinaryFormat::Xcoff { - file.add_section(Vec::new(), b".info".to_vec(), SectionKind::Debug) - } else { - file.add_section( - file.segment_name(StandardSegment::Debug).to_vec(), - section_name.into_bytes(), - SectionKind::Debug, - ) - }; - match file.format() { - BinaryFormat::Coff => { - file.section_mut(section).flags = - SectionFlags::Coff { characteristics: pe::IMAGE_SCN_LNK_REMOVE }; - } - BinaryFormat::Elf => { - file.section_mut(section).flags = - SectionFlags::Elf { sh_flags: elf::SHF_EXCLUDE as u64 }; - } - BinaryFormat::Xcoff => { - // AIX system linker may aborts if it meets a valid XCOFF file in archive with no .text, no .data and no .bss. - file.add_section(Vec::new(), b".text".to_vec(), SectionKind::Text); - file.section_mut(section).flags = - SectionFlags::Xcoff { s_flags: xcoff::STYP_INFO as u32 }; - // Encode string stored in .info section of XCOFF. - // FIXME: The length of data here is not guaranteed to fit in a u32. - // We may have to split the data into multiple pieces in order to - // store in .info section. - let len: u32 = data.len().try_into().unwrap(); - let offset = file.append_section_data(section, &len.to_be_bytes(), 1); - // Add a symbol referring to the data in .info section. - file.add_symbol(Symbol { - name: "__aix_rust_metadata".into(), - value: offset + 4, - size: 0, - kind: SymbolKind::Unknown, - scope: SymbolScope::Compilation, - weak: false, - section: SymbolSection::Section(section), - flags: SymbolFlags::Xcoff { - n_sclass: xcoff::C_INFO, - x_smtyp: xcoff::C_HIDEXT, - x_smclas: xcoff::C_HIDEXT, - containing_csect: None, - }, - }); - } - _ => {} - }; - file.append_section_data(section, data, 1); - file.write().unwrap() -} - impl CodegenBackend for GotocCodegenBackend { fn provide(&self, providers: &mut Providers) { provide::provide(providers, &self.queries.lock().unwrap()); @@ -723,17 +430,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 = Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)); - let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); - let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); - let metadata = create_wrapper_file( - sess, - ".rmeta".to_string(), - codegen_results.metadata.raw_data(), - ); - let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME); - builder.add_file(&metadata); - builder.build(&out_path); + link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)? } else { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); @@ -749,6 +446,14 @@ impl CodegenBackend for GotocCodegenBackend { } } +struct ArArchiveBuilderBuilder; + +impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { + fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box { + Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)) + } +} + fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option { let attrs = KaniAttributes::for_def_id(tcx, def_id); attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)