@@ -24,16 +24,15 @@ use kani_metadata::artifact::convert_type;
2424use kani_metadata:: UnsupportedFeature ;
2525use kani_metadata:: { ArtifactType , HarnessMetadata , KaniMetadata } ;
2626use kani_metadata:: { AssignsContract , CompilerArtifactStub } ;
27- use rustc_codegen_ssa:: back:: archive:: { ArArchiveBuilder , ArchiveBuilder , DEFAULT_OBJECT_READER } ;
28- use rustc_codegen_ssa:: back:: metadata:: create_wrapper_file;
27+ use rustc_codegen_ssa:: back:: archive:: {
28+ ArArchiveBuilder , ArchiveBuilder , ArchiveBuilderBuilder , DEFAULT_OBJECT_READER ,
29+ } ;
30+ use rustc_codegen_ssa:: back:: link:: link_binary;
2931use rustc_codegen_ssa:: traits:: CodegenBackend ;
3032use rustc_codegen_ssa:: { CodegenResults , CrateInfo } ;
3133use rustc_data_structures:: fx:: { FxHashMap , FxIndexMap } ;
32- use rustc_data_structures:: temp_dir:: MaybeTempDir ;
3334use rustc_errors:: { ErrorGuaranteed , DEFAULT_LOCALE_RESOURCE } ;
3435use rustc_hir:: def_id:: { DefId as InternalDefId , LOCAL_CRATE } ;
35- use rustc_metadata:: creader:: MetadataLoaderDyn ;
36- use rustc_metadata:: fs:: { emit_wrapper_file, METADATA_FILENAME } ;
3736use rustc_metadata:: EncodedMetadata ;
3837use rustc_middle:: dep_graph:: { WorkProduct , WorkProductId } ;
3938use rustc_middle:: ty:: TyCtxt ;
@@ -56,7 +55,6 @@ use std::path::{Path, PathBuf};
5655use std:: process:: Command ;
5756use std:: sync:: { Arc , Mutex } ;
5857use std:: time:: Instant ;
59- use tempfile:: Builder as TempFileBuilder ;
6058use tracing:: { debug, error, info} ;
6159
6260pub type UnsupportedConstructs = FxHashMap < InternedString , Vec < Location > > ;
@@ -225,10 +223,6 @@ impl GotocCodegenBackend {
225223}
226224
227225impl CodegenBackend for GotocCodegenBackend {
228- fn metadata_loader ( & self ) -> Box < MetadataLoaderDyn > {
229- Box :: new ( rustc_codegen_ssa:: back:: metadata:: DefaultMetadataLoader )
230- }
231-
232226 fn provide ( & self , providers : & mut Providers ) {
233227 provide:: provide ( providers, & self . queries . lock ( ) . unwrap ( ) ) ;
234228 }
@@ -436,17 +430,7 @@ impl CodegenBackend for GotocCodegenBackend {
436430 debug ! ( ?crate_type, ?out_path, "link" ) ;
437431 if * crate_type == CrateType :: Rlib {
438432 // Emit the `rlib` that contains just one file: `<crate>.rmeta`
439- let mut builder = Box :: new ( ArArchiveBuilder :: new ( sess, & DEFAULT_OBJECT_READER ) ) ;
440- let tmp_dir = TempFileBuilder :: new ( ) . prefix ( "kani" ) . tempdir ( ) . unwrap ( ) ;
441- let path = MaybeTempDir :: new ( tmp_dir, sess. opts . cg . save_temps ) ;
442- let ( metadata, _metadata_position) = create_wrapper_file (
443- sess,
444- ".rmeta" . to_string ( ) ,
445- codegen_results. metadata . raw_data ( ) ,
446- ) ;
447- let metadata = emit_wrapper_file ( sess, & metadata, & path, METADATA_FILENAME ) ;
448- builder. add_file ( & metadata) ;
449- builder. build ( & out_path) ;
433+ link_binary ( sess, & ArArchiveBuilderBuilder , & codegen_results, outputs) ?
450434 } else {
451435 // Write the location of the kani metadata file in the requested compiler output file.
452436 let base_filepath = outputs. path ( OutputType :: Object ) ;
@@ -462,6 +446,14 @@ impl CodegenBackend for GotocCodegenBackend {
462446 }
463447}
464448
449+ struct ArArchiveBuilderBuilder ;
450+
451+ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
452+ fn new_archive_builder < ' a > ( & self , sess : & ' a Session ) -> Box < dyn ArchiveBuilder + ' a > {
453+ Box :: new ( ArArchiveBuilder :: new ( sess, & DEFAULT_OBJECT_READER ) )
454+ }
455+ }
456+
465457fn contract_metadata_for_harness ( tcx : TyCtxt , def_id : DefId ) -> Option < InternalDefId > {
466458 let attrs = KaniAttributes :: for_def_id ( tcx, def_id) ;
467459 attrs. interpret_for_contract_attribute ( ) . map ( |( _, id, _) | id)
0 commit comments