diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 1d1c83652b56..e8feeb386a01 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -484,7 +484,7 @@ impl Expr { /// `(typ) self`. pub fn cast_to(self, typ: Type) -> Self { - assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?}\n\n{:?}", self, typ); + assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?} ({:?})\n\n{:?}", self, self.typ, typ); if self.typ == typ { self } else if typ.is_bool() { 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/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index ec536a9c2f69..274c612e3003 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! this module handles intrinsics -use super::typ::pointee_type; +use super::typ::{self, pointee_type}; use super::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{ @@ -35,6 +35,11 @@ struct SizeAlign { align: Expr, } +enum VTableInfo { + Size, + Align, +} + impl<'tcx> GotocCtx<'tcx> { fn binop Expr>( &mut self, @@ -703,6 +708,8 @@ impl<'tcx> GotocCtx<'tcx> { assert!(self.place_ty(p).is_unit()); self.codegen_volatile_store(fargs, farg_types, loc) } + "vtable_size" => self.vtable_info(VTableInfo::Size, fargs, p, loc), + "vtable_align" => self.vtable_info(VTableInfo::Align, fargs, p, loc), "wrapping_add" => codegen_wrapping_op!(plus), "wrapping_mul" => codegen_wrapping_op!(mul), "wrapping_sub" => codegen_wrapping_op!(sub), @@ -1201,6 +1208,26 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place(p, e) } + fn vtable_info( + &mut self, + info: VTableInfo, + mut fargs: Vec, + place: &Place<'tcx>, + _loc: Location, + ) -> Stmt { + assert_eq!(fargs.len(), 1, "vtable intrinsics expects one raw pointer argument"); + let vtable_obj = fargs + .pop() + .unwrap() + .cast_to(self.codegen_ty_common_vtable().to_pointer()) + .dereference(); + let expr = match info { + VTableInfo::Size => vtable_obj.member(typ::VTABLE_SIZE_FIELD, &self.symbol_table), + VTableInfo::Align => vtable_obj.member(typ::VTABLE_ALIGN_FIELD, &self.symbol_table), + }; + self.codegen_expr_to_place(place, expr) + } + /// This function computes the size and alignment of a dynamically-sized type. /// The implementations follows closely the SSA implementation found in /// rustc_codegen_ssa::glue::size_and_align_of_dst. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 61fc615d5336..723fa4a36606 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -379,6 +379,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..ae6d871d9761 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -6,6 +6,7 @@ //! in [GotocCtx::codegen_place] below. use super::typ::TypeExt; +use crate::codegen_cprover_gotoc::codegen::typ::{pointee_type, std_pointee_type}; use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Location, Type}; @@ -360,31 +361,30 @@ impl<'tcx> GotocCtx<'tcx> { before.goto_expr }; - let inner_mir_typ_and_mut = base_type.builtin_deref(true).unwrap(); - let fat_ptr_mir_typ = if self.is_box_of_unsized(base_type) { - // If we have a box, its fat pointer typ is a pointer to the boxes inner type. - Some(self.tcx.mk_ptr(inner_mir_typ_and_mut)) - } else if self.is_ref_of_unsized(base_type) { - Some(before.mir_typ_or_variant.expect_type()) + let inner_mir_typ = std_pointee_type(base_type).unwrap(); + let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self.use_thin_pointer(inner_mir_typ) { + (before.fat_ptr_mir_typ, before.fat_ptr_goto_expr) } else { - before.fat_ptr_mir_typ + (Some(before.mir_typ_or_variant.expect_type()), Some(inner_goto_expr.clone())) }; - let fat_ptr_goto_expr = - if self.is_box_of_unsized(base_type) || self.is_ref_of_unsized(base_type) { - Some(inner_goto_expr.clone()) - } else { - before.fat_ptr_goto_expr - }; // Check that we have a valid trait or slice fat pointer 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(), + pointee_type(fat_ptr_mir_typ.unwrap()).unwrap().kind(), + ); + assert!( + self.use_fat_pointer(pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()), + "Unexpected type: {:?} -- {:?}", + fat_ptr.typ(), + fat_ptr_mir_typ, ); }; - let inner_mir_typ = inner_mir_typ_and_mut.ty; let expr = match inner_mir_typ.kind() { ty::Slice(_) | ty::Str | ty::Dynamic(..) => { inner_goto_expr.member("data", &self.symbol_table) @@ -547,13 +547,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/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 1035e96e830e..1a757860eeb6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -43,7 +43,7 @@ impl<'tcx> GotocCtx<'tcx> { let left_typ = self.operand_ty(left_op); let right_typ = self.operand_ty(left_op); assert_eq!(left_typ, right_typ, "Cannot compare pointers of different types"); - assert!(self.is_ref_of_unsized(left_typ)); + assert!(self.is_fat_pointer(left_typ)); if self.is_vtable_fat_pointer(left_typ) { // Codegen an assertion failure since vtable comparison is not stable. @@ -334,7 +334,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_unchecked_scalar_binop(op, e1, e2) } BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => { - if self.is_ref_of_unsized(self.operand_ty(e1)) { + if self.is_fat_pointer(self.operand_ty(e1)) { self.codegen_comparison_fat_ptr(op, e1, e2, loc) } else { self.codegen_comparison(op, e1, e2) @@ -628,11 +628,11 @@ impl<'tcx> GotocCtx<'tcx> { } // Cast between fat pointers - if self.is_ref_of_unsized(src_t) && self.is_ref_of_unsized(dst_t) { + if self.is_fat_pointer(src_t) && self.is_fat_pointer(dst_t) { return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_t); } - if self.is_ref_of_unsized(src_t) && self.is_ref_of_sized(dst_t) { + if self.is_fat_pointer(src_t) && !self.is_fat_pointer(dst_t) { return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_t); } @@ -760,14 +760,9 @@ impl<'tcx> GotocCtx<'tcx> { dst_mir_type, ) } else { - // Check that the source is either not a pointer, or a thin or a slice pointer - assert!( - pointee_type(src_mir_type) - .map_or(true, |p| self.use_thin_pointer(p) || self.use_slice_fat_pointer(p)) - ); - - // Sized to unsized cast - self.cast_sized_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type) + // Recursively cast the source expression into an unsized expression. + // This will include thin pointers, slices, and Adt. + self.cast_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type) } } @@ -1041,10 +1036,9 @@ impl<'tcx> GotocCtx<'tcx> { Some(dynamic_fat_ptr(dst_goto_type, data, vtable, &self.symbol_table)) } - /// Cast a sized object to an unsized object: the result of the cast will be - /// a fat pointer or an ADT with a nested fat pointer. Return the result of - /// the cast as Some(expr) and return None if no cast was required. - fn cast_sized_expr_to_unsized_expr( + /// Cast an object / thin pointer to a fat pointer or an ADT with a nested fat pointer. + /// Return the result of the cast as Some(expr) and return None if no cast was required. + fn cast_expr_to_unsized_expr( &mut self, src_goto_expr: Expr, src_mir_type: Ty<'tcx>, @@ -1054,19 +1048,6 @@ impl<'tcx> GotocCtx<'tcx> { return None; // no cast required, nothing to do } - // The src type will be sized, but the dst type may not be unsized. If - // the dst is an adt containing a pointer to a trait object nested - // within the adt, the trait object will be unsized and the pointer will - // be a fat pointer, but the adt (containing the fat pointer) will - // itself be sized. - assert!( - src_mir_type.is_sized(self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all()) - ); - - // The src type cannot be a pointer to a dynamic trait object, otherwise - // we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait - assert!(!self.is_vtable_fat_pointer(src_mir_type)); - match (src_mir_type.kind(), dst_mir_type.kind()) { (ty::Ref(..), ty::Ref(..)) => { self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type) @@ -1081,7 +1062,7 @@ impl<'tcx> GotocCtx<'tcx> { self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type) } (ty::Adt(..), ty::Adt(..)) => { - self.cast_sized_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type) + self.cast_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type) } (src_kind, dst_kind) => { unreachable!( @@ -1095,6 +1076,11 @@ impl<'tcx> GotocCtx<'tcx> { /// Cast a pointer to a sized object to a fat pointer to an unsized object. /// Return the result of the cast as Some(expr) and return None if no cast /// was required. + /// Note: This seems conceptually wrong. If we are converting sized to unsized, how come + /// source and destination can have the same type? Also, how come destination can be a thin + /// pointer? + /// TODO: Fix the cast code structure: + /// fn cast_sized_pointer_to_fat_pointer( &mut self, src_goto_expr: Expr, @@ -1106,6 +1092,10 @@ impl<'tcx> GotocCtx<'tcx> { return None; }; + // The src type cannot be a pointer to a dynamic trait object, otherwise + // we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait + assert!(!self.is_vtable_fat_pointer(src_mir_type)); + // extract pointee types from pointer types, panic if type is not a // pointer type. let src_pointee_type = pointee_type(src_mir_type).unwrap(); @@ -1192,10 +1182,10 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Cast a sized ADT to an unsized ADT (an ADT with a nested fat pointer). + /// Cast an ADT (sized or unsized) to an unsized ADT (an ADT with a nested fat pointer). /// Return the result of the cast as Some(expr) and return None if no cast /// was required. - fn cast_sized_adt_to_unsized_adt( + fn cast_adt_to_unsized_adt( &mut self, src_goto_expr: Expr, src_mir_type: Ty<'tcx>, 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..45f766e40f22 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -14,7 +14,7 @@ use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::print::FmtPrinter; use rustc_middle::ty::subst::InternalSubsts; use rustc_middle::ty::{ - self, AdtDef, FloatTy, GeneratorSubsts, Instance, IntTy, PolyFnSig, Ty, TyKind, UintTy, + self, AdtDef, FloatTy, GeneratorSubsts, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind, UintTy, VariantDef, VtblEntry, }; use rustc_middle::ty::{List, TypeFoldable}; @@ -38,6 +38,13 @@ use ty::layout::HasParamEnv; const UNIT_TYPE_EMPTY_STRUCT_NAME: &str = "Unit"; pub const FN_RETURN_VOID_VAR_NAME: &str = "VoidUnit"; +/// Name for the common vtable structure. +const COMMON_VTABLE_STRUCT_NAME: &str = "Kani::CommonVTable"; + +const VTABLE_DROP_FIELD: &str = "drop"; +pub const VTABLE_SIZE_FIELD: &str = "size"; +pub const VTABLE_ALIGN_FIELD: &str = "align"; + /// Map the never i.e. `!` type to an empty struct. /// The never type can appear as a function argument, e.g. in library/core/src/num/error.rs const NEVER_TYPE_EMPTY_STRUCT_NAME: &str = "Never"; @@ -417,39 +424,16 @@ impl<'tcx> GotocCtx<'tcx> { self.monomorphize(p.ty(self.current_fn().mir().local_decls(), self.tcx).ty) } - /// Is the MIR type an unsized type (i.e. one represented by a fat pointer?) + /// Is the MIR type an unsized type + /// Unsized types can represent: + /// 1- Types that rust cannot infer their type such as ForeignItems. + /// 2- Types that can only be accessed via FatPointer. pub fn is_unsized(&self, t: Ty<'tcx>) -> bool { !self .monomorphize(t) .is_sized(self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all()) } - /// Is the MIR type a ref of an unsized type (i.e. one represented by a fat pointer?) - pub fn is_ref_of_unsized(&self, t: Ty<'tcx>) -> bool { - match t.kind() { - ty::Ref(_, to, _) | ty::RawPtr(ty::TypeAndMut { ty: to, .. }) => self.is_unsized(*to), - _ => false, - } - } - - /// Is the MIR type a ref of an unsized type (i.e. one represented by a fat pointer?) - pub fn is_ref_of_sized(&self, t: Ty<'tcx>) -> bool { - match t.kind() { - ty::Ref(_, to, _) | ty::RawPtr(ty::TypeAndMut { ty: to, .. }) => !self.is_unsized(*to), - _ => false, - } - } - - /// Is the MIR type a box of an unsized type (i.e. one represented by a fat pointer?) - pub fn is_box_of_unsized(&self, t: Ty<'tcx>) -> bool { - if t.is_box() { - let boxed_t = self.monomorphize(t.boxed_ty()); - self.is_unsized(boxed_t) - } else { - false - } - } - /// Generates the type for a single field for a dynamic vtable. /// In particular, these fields are function pointers. fn trait_method_vtable_field_type( @@ -568,14 +552,9 @@ impl<'tcx> GotocCtx<'tcx> { /// Given a trait of type `t`, determine the fields of the struct that will implement its vtable. /// /// The order of fields (i.e., the layout of a vtable) is not guaranteed by the compiler. - /// We follow the order implemented by the compiler in compiler/rustc_codegen_ssa/src/meth.rs - /// `get_vtable`. + /// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`. fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec { - let mut vtable_base = vec![ - DatatypeComponent::field("drop", self.trait_vtable_drop_type(t)), - DatatypeComponent::field("size", Type::size_t()), - DatatypeComponent::field("align", Type::size_t()), - ]; + let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t)); if let ty::Dynamic(binder, _region) = t.kind() { // The virtual methods on the trait ref. Some auto traits have no methods. if let Some(principal) = binder.principal() { @@ -702,6 +681,23 @@ impl<'tcx> GotocCtx<'tcx> { self.ensure_struct(UNIT_TYPE_EMPTY_STRUCT_NAME, "()", |_, _| vec![]) } + /// The common VTable entries. + /// A VTable is an opaque type to the compiler, but they all follow the same structure. + /// The first three entries are always the following: + /// 1- Function pointer to drop in place. + /// 2- The size of the object. + /// 3- The alignment of the object. + /// We use this common structure to extract information out of a vtable. Since we don't have + /// any information about the original type, we use `void*` to encode the drop fn argument type. + pub fn codegen_ty_common_vtable(&mut self) -> Type { + self.ensure_struct(COMMON_VTABLE_STRUCT_NAME, COMMON_VTABLE_STRUCT_NAME, |_, _| { + let drop_type = + Type::code_with_unnamed_parameters(vec![Type::void_pointer()], Type::unit()) + .to_pointer(); + common_vtable_fields(drop_type) + }) + } + /// codegen for types. it finds a C type which corresponds to a rust type. /// that means [ty] has to be monomorphized. /// @@ -1697,7 +1693,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(); @@ -1870,21 +1866,50 @@ impl<'tcx> GotocCtx<'tcx> { } } -/// The mir type is a mir pointer type. +/// Return the datatype components for fields are present in every vtable struct. +/// +/// We follow the order from the `TyCtxt::::COMMON_VTABLE_ENTRIES`. +fn common_vtable_fields(drop_in_place: Type) -> Vec { + let fields: Vec = TyCtxt::COMMON_VTABLE_ENTRIES + .iter() + .map(|entry| match entry { + VtblEntry::MetadataDropInPlace => { + DatatypeComponent::field(VTABLE_DROP_FIELD, drop_in_place.clone()) + } + VtblEntry::MetadataSize => DatatypeComponent::field(VTABLE_SIZE_FIELD, Type::size_t()), + VtblEntry::MetadataAlign => { + DatatypeComponent::field(VTABLE_ALIGN_FIELD, Type::size_t()) + } + VtblEntry::Vacant | VtblEntry::Method(_) | VtblEntry::TraitVPtr(_) => { + unimplemented!("Entry shouldn't be common: {:?}", entry) + } + }) + .collect(); + assert_eq!(fields.len(), 3, "We expect only three common fields for every vtable."); + fields +} + +/// The mir type is a mir pointer type (Ref or RawPtr). +/// This will return false for all smart pointers. See is_std_pointer for a more complete check. pub fn is_pointer(mir_type: Ty) -> bool { - return matches!(mir_type.kind(), ty::Ref(..) | ty::RawPtr(..)); + return pointee_type(mir_type).is_some(); } -/// Extract from a mir pointer type the mir type of the value to which the -/// pointer points. -pub fn pointee_type(pointer_type: Ty) -> Option { - match pointer_type.kind() { +/// If given type is a Ref / Raw ref, return the pointee type. +pub fn pointee_type(mir_type: Ty) -> Option { + match mir_type.kind() { ty::Ref(_, pointee_type, _) => Some(*pointee_type), ty::RawPtr(ty::TypeAndMut { ty: pointee_type, .. }) => Some(*pointee_type), _ => None, } } +/// Extracts the pointee type if the given mir type is either a known smart pointer (Box, Rc, ..) +/// or a regular pointer. +pub fn std_pointee_type(mir_type: Ty) -> Option { + mir_type.builtin_deref(true).map(|tm| tm.ty) +} + /// This is a place holder function that should normalize the given type. /// /// TODO: We should normalize the type projection here. For more details, see @@ -1896,11 +1921,19 @@ fn normalize_type(ty: Ty) -> Ty { impl<'tcx> GotocCtx<'tcx> { /// A pointer to the mir type should be a thin pointer. /// Use thin pointer if the type is sized or if the resulting pointer has no metadata. + /// Note: Foreign items are unsized but it codegen as a thin pointer since there is no + /// metadata associated with it. pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool { // ptr_metadata_ty is not defined on all types, the projection of an associated type let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type); !self.is_unsized(mir_type) || metadata == self.tcx.types.unit } + + /// We use fat pointer if not thin pointer. + pub fn use_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { + !self.use_thin_pointer(mir_type) + } + /// A pointer to the mir type should be a slice fat pointer. /// We use a slice fat pointer if the metadata is the slice length (type usize). pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { @@ -1915,9 +1948,15 @@ impl<'tcx> GotocCtx<'tcx> { metadata != self.tcx.types.unit && metadata != self.tcx.types.usize } + /// Does the current mir represent a fat pointer (Raw pointer or ref) + /// TODO: Should we use `std_pointee_type` here? + /// + pub fn is_fat_pointer(&self, pointer_ty: Ty<'tcx>) -> bool { + pointee_type(pointer_ty).map_or(false, |pointee_ty| self.use_fat_pointer(pointee_ty)) + } + /// Check if the mir type already is a vtable fat pointer. pub fn is_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - self.is_ref_of_unsized(mir_type) - && self.use_vtable_fat_pointer(pointee_type(mir_type).unwrap()) + pointee_type(mir_type).map_or(false, |pointee_ty| self.use_vtable_fat_pointer(pointee_ty)) } } 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 635886a7cb8e..c7c1d5ce3464 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"] diff --git a/tests/kani/DynTrait/unsized_cast.rs b/tests/kani/DynTrait/unsized_cast.rs new file mode 100644 index 000000000000..1f107758a36b --- /dev/null +++ b/tests/kani/DynTrait/unsized_cast.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we can cast between two unsized objects. +use std::rc::Rc; + +trait Byte { + fn eq(&self, byte: u8) -> bool; +} + +impl Byte for u8 { + fn eq(&self, byte: u8) -> bool { + *self == byte + } +} + +fn all_zero(num: Box) -> bool { + num.eq(0x0) +} + +#[kani::proof] +fn check_box() { + let num: u8 = kani::any(); + kani::assume(num != 0); + let boxed: Box = Box::new(num); + assert!(!all_zero(boxed)); +} + +fn all_zero_ref(num: &dyn Byte) -> bool { + num.eq(0x0) +} + +#[kani::proof] +fn check_ref() { + let num: u8 = kani::any(); + kani::assume(num != 0); + let fat_ptr: &(dyn Byte + Sync) = # + assert!(!all_zero_ref(fat_ptr)); +} diff --git a/tests/kani/DynTrait/unsized_rc_cast_fixme.rs b/tests/kani/DynTrait/unsized_rc_cast_fixme.rs new file mode 100644 index 000000000000..8f48d8d73e2f --- /dev/null +++ b/tests/kani/DynTrait/unsized_rc_cast_fixme.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we can cast between two unsized objects. +//! This fix-me is derived from unsized_rc_cast.rs and it should be merged with the original test. +//! The issue https://github.com/model-checking/kani/issues/1528 tracks the fix for this testcase. +use std::rc::Rc; + +trait Byte { + fn eq(&self, byte: u8) -> bool; +} + +impl Byte for u8 { + fn eq(&self, byte: u8) -> bool { + *self == byte + } +} + +fn all_zero_rc(num: Rc) -> bool { + num.eq(0x0) +} + +#[kani::proof] +fn check_rc() { + let num: u8 = kani::any(); + kani::assume(num != 0); + let rc: Rc = Rc::new(num); + assert!(!all_zero_rc(rc)); +} diff --git a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs index 4fadabd92da2..3f86391824c1 100644 --- a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs +++ b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs @@ -2,6 +2,10 @@ // // Modifications Copyright Kani Contributors // See GitHub history for details. +// +// NOTE: The initial fix for this has been reverted from rustc. I'm keeping this test here so we +// will know when it has been reverted back. +// kani-check-fail //! Tests that check handling of opaque casts. Tests were adapted from the rustc repository.