Codegen drop_in_place type and vtable pointer (rust-lang#222)

* Add vtable drop_in_place

* Fix __VERIFIER_expect_fail

Author: avanhatt

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];

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);

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<DatatypeComponent> {
+        // `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()),
         ];

src/test/cbmc/DynTrait/vtable_size_align.rs renamed to 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<dyn Animal> {
-    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::<Sheep> as *mut ());
 
         // Size and align as usizes
         assert!(size_from_vtable(vtable_ptr) == size_of::<i32>());
         assert!(align_from_vtable(vtable_ptr) == size_of::<i32>());
     }
-     // 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::<Cow> as *mut ());
 
         // Size and align as usizes
         assert!(size_from_vtable(vtable_ptr) == size_of::<i8>());
         assert!(align_from_vtable(vtable_ptr) == size_of::<i8>());
     }
 }
- 

src/test/cbmc/DynTrait/vtable_size_align_fail.rs renamed to 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,18 +49,18 @@ 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<dyn Animal> {
-    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       |
     // +-------+------------------+
@@ -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::<Sheep> as *mut (),
+            "Wrong drop",
+        );
+
         // Size and align as usizes
-        assert!(size_from_vtable(vtable_ptr) != size_of::<i32>());
-        assert!(align_from_vtable(vtable_ptr) != size_of::<i32>());
+        __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::<i32>(), "Wrong size");
+        __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::<i32>(), "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::<Cow> as *mut (),
+            "Wrong drop",
+        );
 
         // Size and align as usizes
-        assert!(size_from_vtable(vtable_ptr) != size_of::<i8>());
-        assert!(align_from_vtable(vtable_ptr) != size_of::<i8>());
+        __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::<i8>(), "Wrong size");
+        __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::<i8>(), "Wrong align");
     }
 }
- 

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 {

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!()
 }