Skip to content

Commit 45887b5

Browse files
committed
Fix compilation errors
Regression is still failing. Related changes: - rust-lang/rust#99420 - rust-lang/rust#99495 - rust-lang/rust#99844 - rust-lang/rust#99058
1 parent 0ae8eb0 commit 45887b5

File tree

9 files changed

+45
-37
lines changed

9 files changed

+45
-37
lines changed

kani-compiler/src/codegen_cprover_gotoc/archive.rs

Lines changed: 27 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ use std::fs::File;
2020
use std::io::{self, Read, Seek};
2121
use std::path::{Path, PathBuf};
2222

23-
use rustc_codegen_ssa::back::archive::ArchiveBuilder;
23+
use rustc_codegen_ssa::back::archive::{ArchiveBuilder, ArchiveBuilderBuilder};
2424
use rustc_session::Session;
2525

2626
use object::read::archive::ArchiveFile;
@@ -34,7 +34,6 @@ enum ArchiveEntry {
3434

3535
pub(crate) struct ArArchiveBuilder<'a> {
3636
sess: &'a Session,
37-
dst: PathBuf,
3837
use_gnu_style_archive: bool,
3938

4039
src_archives: Vec<File>,
@@ -44,27 +43,18 @@ pub(crate) struct ArArchiveBuilder<'a> {
4443
}
4544

4645
impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
47-
fn new(sess: &'a Session, output: &Path) -> Self {
48-
ArArchiveBuilder {
49-
sess,
50-
dst: output.to_path_buf(),
51-
use_gnu_style_archive: sess.target.archive_format == "gnu",
52-
src_archives: vec![],
53-
entries: vec![],
54-
}
55-
}
56-
5746
fn add_file(&mut self, file: &Path) {
5847
self.entries.push((
5948
file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
6049
ArchiveEntry::File(file.to_owned()),
6150
));
6251
}
6352

64-
fn add_archive<F>(&mut self, archive_path: &Path, mut skip: F) -> std::io::Result<()>
65-
where
66-
F: FnMut(&str) -> bool + 'static,
67-
{
53+
fn add_archive(
54+
&mut self,
55+
archive_path: &Path,
56+
mut skip: Box<dyn FnMut(&str) -> bool + 'static>,
57+
) -> std::io::Result<()> {
6858
let read_cache = ReadCache::new(std::fs::File::open(&archive_path)?);
6959
let archive = ArchiveFile::parse(&read_cache).unwrap();
7060
let archive_index = self.src_archives.len();
@@ -85,7 +75,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
8575
Ok(())
8676
}
8777

88-
fn build(mut self) -> bool {
78+
fn build(mut self: Box<Self>, output: &Path) -> bool {
8979
enum BuilderKind {
9080
Bsd(ar::Builder<File>),
9181
Gnu(ar::GnuBuilder<File>),
@@ -122,7 +112,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
122112

123113
let mut builder = if self.use_gnu_style_archive {
124114
BuilderKind::Gnu(ar::GnuBuilder::new(
125-
File::create(&self.dst).unwrap_or_else(|err| {
115+
File::create(&output).unwrap_or_else(|err| {
126116
sess.fatal(&format!(
127117
"error opening destination during archive building: {}",
128118
err
@@ -131,7 +121,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
131121
entries.iter().map(|(name, _)| name.clone()).collect(),
132122
))
133123
} else {
134-
BuilderKind::Bsd(ar::Builder::new(File::create(&self.dst).unwrap_or_else(|err| {
124+
BuilderKind::Bsd(ar::Builder::new(File::create(&output).unwrap_or_else(|err| {
135125
sess.fatal(&format!("error opening destination during archive building: {}", err));
136126
})))
137127
};
@@ -150,13 +140,27 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
150140
std::mem::drop(builder);
151141
any_members
152142
}
143+
}
153144

154-
fn inject_dll_import_lib(
155-
&mut self,
145+
pub(crate) struct ArArchiveBuilderBuilder;
146+
147+
impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
148+
fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box<dyn ArchiveBuilder<'a> + 'a> {
149+
Box::new(ArArchiveBuilder {
150+
sess,
151+
use_gnu_style_archive: sess.target.archive_format == "gnu",
152+
src_archives: vec![],
153+
entries: vec![],
154+
})
155+
}
156+
157+
fn create_dll_import_lib(
158+
&self,
159+
_sess: &Session,
156160
_lib_name: &str,
157161
_dll_imports: &[rustc_session::cstore::DllImport],
158-
_tmpdir: &rustc_data_structures::temp_dir::MaybeTempDir,
159-
) {
162+
_tmpdir: &Path,
163+
) -> PathBuf {
160164
unimplemented!("injecting dll imports is not supported");
161165
}
162166
}

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -379,6 +379,14 @@ impl<'tcx> GotocCtx<'tcx> {
379379
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
380380
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
381381
}
382+
GlobalAlloc::VTable(ty, trait_ref) => {
383+
// This is similar to GlobalAlloc::Memory but the type is opaque to rust and it
384+
// requires a bit more logic to get information about the allocation.
385+
let alloc_id = self.tcx.vtable_allocation((ty, trait_ref));
386+
let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
387+
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
388+
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
389+
}
382390
};
383391
assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
384392
let offset_addr = base_addr

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -380,7 +380,9 @@ impl<'tcx> GotocCtx<'tcx> {
380380
if let Some(fat_ptr) = fat_ptr_goto_expr.clone() {
381381
assert!(
382382
fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)
383-
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table)
383+
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table),
384+
"Unexpected type: {:?}",
385+
fat_ptr.typ()
384386
);
385387
};
386388

@@ -547,13 +549,6 @@ impl<'tcx> GotocCtx<'tcx> {
547549
self,
548550
)
549551
}
550-
ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
551-
before.goto_expr.cast_to(self.codegen_ty(ty)),
552-
TypeOrVariant::Type(ty),
553-
before.fat_ptr_goto_expr,
554-
before.fat_ptr_mir_typ,
555-
self,
556-
),
557552
}
558553
}
559554

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
595595
| InstanceDef::DropGlue(_, Some(_))
596596
| InstanceDef::Intrinsic(..)
597597
| InstanceDef::FnPtrShim(..)
598-
| InstanceDef::VtableShim(..)
598+
| InstanceDef::VTableShim(..)
599599
| InstanceDef::ReifyShim(..)
600600
| InstanceDef::ClosureOnceShim { .. }
601601
| InstanceDef::CloneShim(..) => {

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1697,7 +1697,7 @@ impl<'tcx> GotocCtx<'tcx> {
16971697
// For vtable shims, we need to modify fn(self, ...) to fn(self: *mut Self, ...),
16981698
// since the vtable functions expect a pointer as the first argument. See the comment
16991699
// and similar code in compiler/rustc_mir/src/shim.rs.
1700-
if let ty::InstanceDef::VtableShim(..) = self.current_fn().instance().def {
1700+
if let ty::InstanceDef::VTableShim(..) = self.current_fn().instance().def {
17011701
if let Some(self_param) = params.first() {
17021702
let ident = self_param.identifier();
17031703
let ty = self_param.typ().clone();

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,8 +214,9 @@ impl CodegenBackend for GotocCodegenBackend {
214214

215215
// All this ultimately boils down to is emitting an `rlib` that contains just one file: `lib.rmeta`
216216
use rustc_codegen_ssa::back::link::link_binary;
217-
link_binary::<crate::codegen_cprover_gotoc::archive::ArArchiveBuilder<'_>>(
217+
link_binary(
218218
sess,
219+
&crate::codegen_cprover_gotoc::archive::ArArchiveBuilderBuilder,
219220
&codegen_results,
220221
outputs,
221222
)

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,9 @@ use cbmc::InternedString;
2323
use cbmc::{MachineModel, RoundingMode};
2424
use kani_metadata::HarnessMetadata;
2525
use kani_queries::{QueryDb, UserInput};
26+
use rustc_data_structures::fx::FxHashMap;
2627
use rustc_data_structures::owning_ref::OwningRef;
2728
use rustc_data_structures::rustc_erase_owner;
28-
use rustc_data_structures::stable_map::FxHashMap;
2929
use rustc_data_structures::sync::MetadataRef;
3030
use rustc_middle::mir::interpret::Allocation;
3131
use rustc_middle::span_bug;

kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
2020
use cbmc::goto_program::{Stmt, Type};
2121
use cbmc::InternedString;
2222
use kani_metadata::{CallSite, PossibleMethodEntry, TraitDefinedMethod, VtableCtxResults};
23-
use rustc_data_structures::stable_map::FxHashMap;
23+
use rustc_data_structures::fx::FxHashMap;
2424
use tracing::debug;
2525

2626
/// This structure represents data about the vtable that we construct

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2022-07-19"
5+
channel = "nightly-2022-08-02"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)