From 81a692c146ff5155e774444658b8e70f5d5829b6 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 8 Aug 2022 23:54:11 +0000 Subject: [PATCH] Fix compilation errors Regression is still failing. Related changes: - https://github.com/rust-lang/rust/pull/99420 - https://github.com/rust-lang/rust/pull/99495 - https://github.com/rust-lang/rust/pull/99844 - https://github.com/rust-lang/rust/pull/99058 --- .../src/codegen_cprover_gotoc/archive.rs | 50 ++++++++++--------- .../codegen_cprover_gotoc/codegen/operand.rs | 8 +++ .../codegen_cprover_gotoc/codegen/place.rs | 11 ++-- .../codegen/statement.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 2 +- .../compiler_interface.rs | 3 +- .../codegen_cprover_gotoc/context/goto_ctx.rs | 2 +- .../context/vtable_ctx.rs | 2 +- rust-toolchain.toml | 2 +- 9 files changed, 45 insertions(+), 37 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/archive.rs b/kani-compiler/src/codegen_cprover_gotoc/archive.rs index 53df0135766d..5dff2f87171d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/archive.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/archive.rs @@ -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; @@ -34,7 +34,6 @@ enum ArchiveEntry { pub(crate) struct ArArchiveBuilder<'a> { sess: &'a Session, - dst: PathBuf, use_gnu_style_archive: bool, src_archives: Vec, @@ -44,16 +43,6 @@ 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(), @@ -61,10 +50,11 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> { )); } - fn add_archive(&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 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(); @@ -85,7 +75,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> { Ok(()) } - fn build(mut self) -> bool { + fn build(mut self: Box, output: &Path) -> bool { enum BuilderKind { Bsd(ar::Builder), Gnu(ar::GnuBuilder), @@ -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 @@ -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)); }))) }; @@ -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 + '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"); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 8cc6bb5c9d3e..e350e1c44896 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index e062dbfd5aa0..e315bbeff346 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -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() ); }; @@ -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, - ), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 6ba72e589b51..d517dd3633bc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -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(..) => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ddc8fce5b297..e7d30a96ee6a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -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(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 90c229228879..168cb9dde52a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -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::>( + link_binary( sess, + &crate::codegen_cprover_gotoc::archive::ArArchiveBuilderBuilder, &codegen_results, outputs, ) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index d1b999f9d59a..1fdce9b9034d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -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; diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs index a1e829b9b398..98e78ed2b5fd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs @@ -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 diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a1e7f9af086c..c919f519e96e 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"]