diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 8eb60a541de5..eed226cc42c2 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -712,26 +712,23 @@ impl<'tcx> GotocCtx<'tcx> { } } - fn codegen_vtable_drop_in_place(&self) -> Expr { - // TODO: The following still needs to be done for the destructor (drop_in_place method), but before that - // the right type for drop_in_place needs to be set in typ.rs in codegen_ty_ref method as well. - // Atm we pass a nullpointer instead (Type::empty().pointer(ctx.ptr_width()).null() in vtable_base) - // This is sound, because CBMC will give a pointer error if we ever actually use it. - // - // let drop_instance = - // Instance::resolve_drop_in_place(ctx.tcx, operand_type); - // let drop_method_name = self.symbol_name(drop_instance); - // let drop_inst_type = - // drop_instance.ty(self.tcx, ty::ParamEnv::reveal_all()); - // let drop_irep = data::Variable { - // data: drop_method_name.clone(), - // typ: self.codegen_ty(drop_inst_type), - // // typ: output_type, - // location: data::Irep::nil(), - // } - // .to_expr() - // .address_of(); - Type::void_pointer().null() + /// Generate a function pointer to drop_in_place for entry into the vtable + fn codegen_vtable_drop_in_place( + &mut self, + ty: Ty<'tcx>, + trait_ty: &'tcx ty::TyS<'tcx>, + ) -> Expr { + let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty); + let drop_sym_name = self.symbol_name(drop_instance); + let drop_sym = self.symbol_table.lookup(&drop_sym_name).unwrap().clone(); + + // The drop instance has the concrete object type, for consistency with + // type codegen we need the trait type for the function parameter. + let trait_fn_ty = + Type::code_with_unnamed_parameters(vec![self.codegen_ty(trait_ty)], Type::unit()) + .to_pointer(); + + Expr::symbol_expression(drop_sym_name, drop_sym.typ).address_of().cast_to(trait_fn_ty) } fn codegen_vtable_methods( @@ -825,7 +822,7 @@ impl<'tcx> GotocCtx<'tcx> { |ctx, var| { // Build the vtable // See compiler/rustc_codegen_llvm/src/gotoc/typ.rs `trait_vtable_field_types` for field order - let drop_irep = ctx.codegen_vtable_drop_in_place(); + let drop_irep = ctx.codegen_vtable_drop_in_place(&src_mir_type, trait_type); let (vt_size, vt_align) = ctx.codegen_vtable_size_and_align(&src_mir_type); let size_assert = ctx.check_vtable_size(&src_mir_type, vt_size.clone()); let mut vtable_fields = vec![drop_irep, vt_size, vt_align]; diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index 43f52886f2cb..57e5698c4ed9 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -96,6 +96,7 @@ impl<'tcx> GotocCtx<'tcx> { } // TODO: this function doesn't handle unwinding which begins if the destructor panics + // https://github.com/model-checking/rmc/issues/221 fn codegen_drop(&mut self, location: &Place<'tcx>, target: &BasicBlock) -> Stmt { // instance for drop function let loc_ty = self.place_ty(location); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index ca1634134450..5aab106d6120 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -175,13 +175,14 @@ impl<'tcx> GotocCtx<'tcx> { /// 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`. - /// - /// Currently, we also add a well-formed flag field to the end of the struct. fn trait_vtable_field_types(&mut self, t: &'tcx ty::TyS<'tcx>) -> Vec { + // `drop_in_place` is a function with type t -> (), the vtable needs a + // pointer to it + let drop_ty = + Type::code_with_unnamed_parameters(vec![self.codegen_ty(t)], Type::unit()).to_pointer(); + let mut vtable_base = vec![ - // TODO: get the correct type for the drop in place. For now, just use void* - // https://github.com/model-checking/rmc/issues/11 - Type::datatype_component("drop", Type::void_pointer()), + Type::datatype_component("drop", drop_ty), Type::datatype_component("size", Type::size_t()), Type::datatype_component("align", Type::size_t()), ]; diff --git a/src/test/cbmc/DynTrait/vtable_size_align.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs similarity index 87% rename from src/test/cbmc/DynTrait/vtable_size_align.rs rename to src/test/cbmc/DynTrait/vtable_size_align_drop.rs index 58a5db683c19..48d576fd0be5 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks the `size` and `align` fields of vtables, for a +// This test checks the `size` and `align` fields of vtables, for a // dynamic trait where two implementing structs have different sizes. // The strategy is to cast the dyn trait object to a raw::TraitObject // then do some unsafe pointer math. @@ -12,6 +12,7 @@ use std::intrinsics::size_of; use std::mem::transmute; +use std::ptr::drop_in_place; use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); @@ -45,18 +46,16 @@ impl Animal for Cow { // Returns some struct that implements Animal, but we don't know which one at compile time. fn random_animal(random_number: i64) -> Box { - if random_number < 5 { - Box::new(Sheep { sheep_num : 7 }) - } else { - Box::new(Cow { cow_num : 9 }) + if random_number < 5 { + Box::new(Sheep { sheep_num: 7 }) + } else { + Box::new(Cow { cow_num: 9 }) } } fn main() { - let ptr_size = size_of::<&usize>() as isize; - // The vtable is laid out as the right hand side here: - // + // // +-------+------------------+ // | size | value | // +-------+------------------+ @@ -65,8 +64,8 @@ fn main() { // | usize | align in bytes | // | ? | function ptrs... | // +-------+------------------+ - // - // This layout taken from miri's handling: + // + // This layout taken from miri's handling: // https://github.com/rust-lang/rust/blob/ec487bf3cfc9ce386da25169509fae8f2b4d4eec/compiler/rustc_mir/src/interpret/traits.rs#L155 // Check layout/values for Sheep @@ -81,17 +80,17 @@ fn main() { // Note: i32 ptr cast assert!(*(data_ptr as *mut i32) == 7); // From Sheep - + let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(!vtable_ptr.is_null()); + assert!(drop_from_vtrable(vtable_ptr) == drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); assert!(align_from_vtable(vtable_ptr) == size_of::()); } - // Check layout/values for Cow + // Check layout/values for Cow unsafe { let animal_cow = random_animal(6); @@ -103,15 +102,14 @@ fn main() { // Note: i8 ptr cast assert!(*(data_ptr as *mut i8) == 9); // From Cow - + let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(!vtable_ptr.is_null()); + assert!(drop_from_vtrable(vtable_ptr) == drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); assert!(align_from_vtable(vtable_ptr) == size_of::()); } } - \ No newline at end of file diff --git a/src/test/cbmc/DynTrait/vtable_size_align_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs similarity index 70% rename from src/test/cbmc/DynTrait/vtable_size_align_fail.rs rename to src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs index 267ed54e304d..126e5e0a135d 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_fail.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks the `size` and `align` fields of vtables, for a +// This test checks the `size` and `align` fields of vtables, for a // dynamic trait where two implementing structs have different sizes. // The strategy is to cast the dyn trait object to a raw::TraitObject // then do some unsafe pointer math. @@ -14,9 +14,11 @@ use std::intrinsics::size_of; use std::mem::transmute; +use std::ptr::drop_in_place; use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); +include!("../../rmc-prelude.rs"); // Different sized data fields on each struct struct Sheep { @@ -47,10 +49,10 @@ impl Animal for Cow { // Returns some struct that implements Animal, but we don't know which one at compile time. fn random_animal(random_number: i64) -> Box { - if random_number < 5 { - Box::new(Sheep { sheep_num : 7 }) - } else { - Box::new(Cow { cow_num : 9 }) + if random_number < 5 { + Box::new(Sheep { sheep_num: 7 }) + } else { + Box::new(Cow { cow_num: 9 }) } } @@ -58,7 +60,7 @@ fn main() { let ptr_size = size_of::<&usize>() as isize; // The vtable is laid out as the right hand side here: - // + // // +-------+------------------+ // | size | value | // +-------+------------------+ @@ -67,8 +69,8 @@ fn main() { // | usize | align in bytes | // | ? | function ptrs... | // +-------+------------------+ - // - // This layout taken from miri's handling: + // + // This layout taken from miri's handling: // https://github.com/rust-lang/rust/blob/ec487bf3cfc9ce386da25169509fae8f2b4d4eec/compiler/rustc_mir/src/interpret/traits.rs#L155 // Check layout/values for Sheep @@ -82,18 +84,21 @@ fn main() { let data_ptr = trait_object.data; // Note: i32 ptr cast - assert!(*(data_ptr as *mut i32) != 7); // From Sheep - + __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 7, "Wrong data"); // From Sheep + let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(vtable_ptr.is_null()); - + __VERIFIER_expect_fail( + drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut (), + "Wrong drop", + ); + // Size and align as usizes - assert!(size_from_vtable(vtable_ptr) != size_of::()); - assert!(align_from_vtable(vtable_ptr) != size_of::()); + __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); + __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); } - // Check layout/values for Cow + // Check layout/values for Cow unsafe { let animal_cow = random_animal(6); @@ -104,16 +109,18 @@ fn main() { let data_ptr = trait_object.data; // Note: i8 ptr cast - assert!(*(data_ptr as *mut i8) != 9); // From Cow - + __VERIFIER_expect_fail(*(data_ptr as *mut i8) != 9, "Wrong data"); // From Cow + let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(vtable_ptr.is_null()); + __VERIFIER_expect_fail( + drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut (), + "Wrong drop", + ); // Size and align as usizes - assert!(size_from_vtable(vtable_ptr) != size_of::()); - assert!(align_from_vtable(vtable_ptr) != size_of::()); + __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); + __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); } } - \ No newline at end of file diff --git a/src/test/cbmc/Helpers/vtable_utils_ignore.rs b/src/test/cbmc/Helpers/vtable_utils_ignore.rs index b7d843947a9e..74c60d5305c2 100644 --- a/src/test/cbmc/Helpers/vtable_utils_ignore.rs +++ b/src/test/cbmc/Helpers/vtable_utils_ignore.rs @@ -3,6 +3,13 @@ // Because each regression test does not share a crate, we just use // an import! to share this code across test directories. +fn drop_from_vtrable(vtable_ptr : *mut usize) -> *mut () { + // 1st pointer-sized position + unsafe { + *vtable_ptr as *mut () + } +} + fn size_from_vtable(vtable_ptr : *mut usize) -> usize { // 2nd usize-sized position unsafe { diff --git a/src/test/rmc-prelude.rs b/src/test/rmc-prelude.rs index 05ce76d90d1a..32949166a1f9 100644 --- a/src/test/rmc-prelude.rs +++ b/src/test/rmc-prelude.rs @@ -5,7 +5,7 @@ fn __VERIFIER_assume(cond: bool) { unimplemented!() } -fn __VERIFIER_expect_fail(cond: bool) { +fn __VERIFIER_expect_fail(cond: bool, message: &str) { unimplemented!() }