Skip to content

Commit

Permalink
Fix compilation errors
Browse files Browse the repository at this point in the history
Regression is still failing. Related changes:

- rust-lang/rust#99420
- rust-lang/rust#99495
- rust-lang/rust#99844
- rust-lang/rust#99058
  • Loading branch information
celinval committed Aug 8, 2022
1 parent 43f22a8 commit 81a692c
Show file tree
Hide file tree
Showing 9 changed files with 45 additions and 37 deletions.
50 changes: 27 additions & 23 deletions kani-compiler/src/codegen_cprover_gotoc/archive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use std::fs::File;
use std::io::{self, Read, Seek};
use std::path::{Path, PathBuf};

use rustc_codegen_ssa::back::archive::ArchiveBuilder;
use rustc_codegen_ssa::back::archive::{ArchiveBuilder, ArchiveBuilderBuilder};
use rustc_session::Session;

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

pub(crate) struct ArArchiveBuilder<'a> {
sess: &'a Session,
dst: PathBuf,
use_gnu_style_archive: bool,

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

impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
fn new(sess: &'a Session, output: &Path) -> Self {
ArArchiveBuilder {
sess,
dst: output.to_path_buf(),
use_gnu_style_archive: sess.target.archive_format == "gnu",
src_archives: vec![],
entries: vec![],
}
}

fn add_file(&mut self, file: &Path) {
self.entries.push((
file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
ArchiveEntry::File(file.to_owned()),
));
}

fn add_archive<F>(&mut self, archive_path: &Path, mut skip: F) -> std::io::Result<()>
where
F: FnMut(&str) -> bool + 'static,
{
fn add_archive(
&mut self,
archive_path: &Path,
mut skip: Box<dyn FnMut(&str) -> bool + 'static>,
) -> std::io::Result<()> {
let read_cache = ReadCache::new(std::fs::File::open(&archive_path)?);
let archive = ArchiveFile::parse(&read_cache).unwrap();
let archive_index = self.src_archives.len();
Expand All @@ -85,7 +75,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
Ok(())
}

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

let mut builder = if self.use_gnu_style_archive {
BuilderKind::Gnu(ar::GnuBuilder::new(
File::create(&self.dst).unwrap_or_else(|err| {
File::create(&output).unwrap_or_else(|err| {
sess.fatal(&format!(
"error opening destination during archive building: {}",
err
Expand All @@ -131,7 +121,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
entries.iter().map(|(name, _)| name.clone()).collect(),
))
} else {
BuilderKind::Bsd(ar::Builder::new(File::create(&self.dst).unwrap_or_else(|err| {
BuilderKind::Bsd(ar::Builder::new(File::create(&output).unwrap_or_else(|err| {
sess.fatal(&format!("error opening destination during archive building: {}", err));
})))
};
Expand All @@ -150,13 +140,27 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
std::mem::drop(builder);
any_members
}
}

fn inject_dll_import_lib(
&mut self,
pub(crate) struct ArArchiveBuilderBuilder;

impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box<dyn ArchiveBuilder<'a> + 'a> {
Box::new(ArArchiveBuilder {
sess,
use_gnu_style_archive: sess.target.archive_format == "gnu",
src_archives: vec![],
entries: vec![],
})
}

fn create_dll_import_lib(
&self,
_sess: &Session,
_lib_name: &str,
_dll_imports: &[rustc_session::cstore::DllImport],
_tmpdir: &rustc_data_structures::temp_dir::MaybeTempDir,
) {
_tmpdir: &Path,
) -> PathBuf {
unimplemented!("injecting dll imports is not supported");
}
}
8 changes: 8 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -376,6 +376,14 @@ impl<'tcx> GotocCtx<'tcx> {
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
}
GlobalAlloc::VTable(ty, trait_ref) => {
// This is similar to GlobalAlloc::Memory but the type is opaque to rust and it
// requires a bit more logic to get information about the allocation.
let alloc_id = self.tcx.vtable_allocation((ty, trait_ref));
let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
}
};
assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
let offset_addr = base_addr
Expand Down
11 changes: 3 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -380,7 +380,9 @@ impl<'tcx> GotocCtx<'tcx> {
if let Some(fat_ptr) = fat_ptr_goto_expr.clone() {
assert!(
fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table)
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table),
"Unexpected type: {:?}",
fat_ptr.typ()
);
};

Expand Down Expand Up @@ -547,13 +549,6 @@ impl<'tcx> GotocCtx<'tcx> {
self,
)
}
ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
before.goto_expr.cast_to(self.codegen_ty(ty)),
TypeOrVariant::Type(ty),
before.fat_ptr_goto_expr,
before.fat_ptr_mir_typ,
self,
),
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
| InstanceDef::DropGlue(_, Some(_))
| InstanceDef::Intrinsic(..)
| InstanceDef::FnPtrShim(..)
| InstanceDef::VtableShim(..)
| InstanceDef::VTableShim(..)
| InstanceDef::ReifyShim(..)
| InstanceDef::ClosureOnceShim { .. }
| InstanceDef::CloneShim(..) => {
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1697,7 +1697,7 @@ impl<'tcx> GotocCtx<'tcx> {
// For vtable shims, we need to modify fn(self, ...) to fn(self: *mut Self, ...),
// since the vtable functions expect a pointer as the first argument. See the comment
// and similar code in compiler/rustc_mir/src/shim.rs.
if let ty::InstanceDef::VtableShim(..) = self.current_fn().instance().def {
if let ty::InstanceDef::VTableShim(..) = self.current_fn().instance().def {
if let Some(self_param) = params.first() {
let ident = self_param.identifier();
let ty = self_param.typ().clone();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -214,8 +214,9 @@ impl CodegenBackend for GotocCodegenBackend {

// All this ultimately boils down to is emitting an `rlib` that contains just one file: `lib.rmeta`
use rustc_codegen_ssa::back::link::link_binary;
link_binary::<crate::codegen_cprover_gotoc::archive::ArArchiveBuilder<'_>>(
link_binary(
sess,
&crate::codegen_cprover_gotoc::archive::ArArchiveBuilderBuilder,
&codegen_results,
outputs,
)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,9 @@ use cbmc::InternedString;
use cbmc::{MachineModel, RoundingMode};
use kani_metadata::HarnessMetadata;
use kani_queries::{QueryDb, UserInput};
use rustc_data_structures::fx::FxHashMap;
use rustc_data_structures::owning_ref::OwningRef;
use rustc_data_structures::rustc_erase_owner;
use rustc_data_structures::stable_map::FxHashMap;
use rustc_data_structures::sync::MetadataRef;
use rustc_middle::mir::interpret::Allocation;
use rustc_middle::span_bug;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::{Stmt, Type};
use cbmc::InternedString;
use kani_metadata::{CallSite, PossibleMethodEntry, TraitDefinedMethod, VtableCtxResults};
use rustc_data_structures::stable_map::FxHashMap;
use rustc_data_structures::fx::FxHashMap;
use tracing::debug;

/// This structure represents data about the vtable that we construct
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-2022-07-19"
channel = "nightly-2022-08-02"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 81a692c

Please sign in to comment.