Skip to content

Commit

Permalink
Use link_binary instead and remove impl of metadata loader
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval committed Sep 24, 2024
1 parent 3d8d6a5 commit dd3c5cf
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 22 deletions.
34 changes: 13 additions & 21 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,16 +24,15 @@ use kani_metadata::artifact::convert_type;
use kani_metadata::UnsupportedFeature;
use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
use kani_metadata::{AssignsContract, CompilerArtifactStub};
use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER};
use rustc_codegen_ssa::back::metadata::create_wrapper_file;
use rustc_codegen_ssa::back::archive::{
ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER,
};
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::creader::MetadataLoaderDyn;
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;
Expand All @@ -56,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<InternedString, Vec<Location>>;
Expand Down Expand Up @@ -225,10 +223,6 @@ impl GotocCodegenBackend {
}

impl CodegenBackend for GotocCodegenBackend {
fn metadata_loader(&self) -> Box<MetadataLoaderDyn> {
Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader)
}

fn provide(&self, providers: &mut Providers) {
provide::provide(providers, &self.queries.lock().unwrap());
}
Expand Down Expand Up @@ -436,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: `<crate>.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, _metadata_position) = 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);
Expand All @@ -462,6 +446,14 @@ impl CodegenBackend for GotocCodegenBackend {
}
}

struct ArArchiveBuilderBuilder;

impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box<dyn ArchiveBuilder + 'a> {
Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER))
}
}

fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<InternalDefId> {
let attrs = KaniAttributes::for_def_id(tcx, def_id);
attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-09-17"
channel = "nightly-2024-09-20"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit dd3c5cf

Please sign in to comment.