Drop for dynamic objects (model-checking#402)

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs

@@ -67,10 +67,19 @@ impl<'tcx> ProjectedPlace<'tcx> {
 
 /// Constructor
 impl<'tcx> ProjectedPlace<'tcx> {
-    fn check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool {
+    fn check_expr_typ_mismatch(
+        expr: &Expr,
+        typ: &TypeOrVariant<'tcx>,
+        ctx: &mut GotocCtx<'tcx>,
+    ) -> Option<(Type, Type)> {
         match typ {
-            TypeOrVariant::Type(t) => &ctx.codegen_ty(t) == expr.typ(),
-            TypeOrVariant::Variant(_) => true, //TODO, what to do here?
+            TypeOrVariant::Type(t) => {
+                let expr_ty = expr.typ().clone();
+                let type_from_mir = ctx.codegen_ty(t);
+                if expr_ty != type_from_mir { Some((expr_ty, type_from_mir)) } else { None }
+            }
+            // TODO: handle Variant https://github.com/model-checking/rmc/issues/448
+            TypeOrVariant::Variant(_) => None,
         }
     }
 
@@ -107,12 +116,14 @@ impl<'tcx> ProjectedPlace<'tcx> {
         // TODO: these assertions fail on a few regressions. Figure out why.
         // I think it may have to do with boxed fat pointers.
         // https://github.com/model-checking/rmc/issues/277
-        if !Self::check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx) {
+        if let Some((expr_ty, ty_from_mir)) =
+            Self::check_expr_typ_mismatch(&goto_expr, &mir_typ_or_variant, ctx)
+        {
             warn!(
-                "Unexpected type mismatch in projection: \n{:?}\n{:?}",
-                &goto_expr, &mir_typ_or_variant
+                "Unexpected type mismatch in projection:\n{:?}\nExpr type\n{:?}\nType from MIR\n{:?}",
+                goto_expr, expr_ty, ty_from_mir
             );
-        };
+        }
 
         assert!(
             Self::check_fat_ptr_typ(&fat_ptr_goto_expr, &fat_ptr_mir_typ, ctx),

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/rvalue.rs

@@ -721,26 +721,26 @@ impl<'tcx> GotocCtx<'tcx> {
         ty: Ty<'tcx>,
         trait_ty: &'tcx ty::TyS<'tcx>,
     ) -> Expr {
-        let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty);
+        let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty).polymorphize(self.tcx);
         let drop_sym_name = self.symbol_name(drop_instance);
-        let param_types = vec![self.codegen_ty(trait_ty)];
 
         // 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(param_types, Type::unit()).to_pointer();
+        let trait_fn_ty = self.trait_vtable_drop_type(trait_ty);
 
         if let Some(drop_sym) = self.symbol_table.lookup(&drop_sym_name) {
             Expr::symbol_expression(drop_sym_name, drop_sym.clone().typ)
                 .address_of()
                 .cast_to(trait_fn_ty)
         } else {
-            // TODO: check why in https://github.com/model-checking/rmc/issues/66
-            debug!(
-                "WARNING: drop_in_place not found for {:?}",
-                self.readable_instance_name(drop_instance),
-            );
-            Type::void_pointer().null().cast_to(trait_fn_ty)
+            // We skip an entire submodule of the standard library, so drop is missing
+            // for it.
+            self.codegen_unimplemented(
+                format!("drop_in_place for {}", drop_sym_name).as_str(),
+                trait_fn_ty,
+                Location::none(),
+                "https://github.com/model-checking/rmc/issues/281",
+            )
         }
     }
 

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs

@@ -99,27 +99,74 @@ 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);
-        let instance = Instance::resolve_drop_in_place(self.tcx, loc_ty);
-        if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) {
+        let drop_instance = Instance::resolve_drop_in_place(self.tcx, loc_ty);
+        if let Some(hk) = self.hooks.hook_applies(self.tcx, drop_instance) {
             let le = self.codegen_place(location).goto_expr;
-            hk.handle(self, instance, vec![le], None, Some(*target), None)
+            hk.handle(self, drop_instance, vec![le], None, Some(*target), None)
         } else {
-            let drop_implementation = match instance.def {
-                InstanceDef::Virtual(..) => self
-                    .codegen_unimplemented(
-                        "drop_in_place for dynamic argument",
-                        Type::Empty,
-                        Location::none(),
-                        "https://github.com/model-checking/rmc/issues/11",
-                    )
-                    .as_stmt(Location::none()),
-                InstanceDef::DropGlue(..) => Stmt::skip(Location::none()),
+            let drop_implementation = match drop_instance.def {
+                InstanceDef::DropGlue(_, None) => {
+                    // We can skip empty DropGlue functions
+                    Stmt::skip(Location::none())
+                }
                 _ => {
-                    let func = self.codegen_func_expr(instance, None);
-                    func.call(vec![self.codegen_place(location).goto_expr.address_of()])
-                        .as_stmt(Location::none())
+                    match loc_ty.kind() {
+                        ty::Dynamic(..) => {
+                            // Virtual drop via a vtable lookup
+                            let trait_fat_ptr =
+                                self.codegen_place(location).fat_ptr_goto_expr.unwrap();
+
+                            // Pull the function off of the fat pointer's vtable pointer
+                            let vtable_ref =
+                                trait_fat_ptr.to_owned().member("vtable", &self.symbol_table);
+                            let vtable = vtable_ref.dereference();
+                            let fn_ptr = vtable.member("drop", &self.symbol_table);
+
+                            // Pull the self argument off of the fat pointer's data pointer
+                            let self_ref =
+                                trait_fat_ptr.to_owned().member("data", &self.symbol_table);
+                            let self_ref =
+                                self_ref.cast_to(trait_fat_ptr.typ().clone().to_pointer());
+
+                            let func_exp: Expr = fn_ptr.dereference();
+                            func_exp.call(vec![self_ref]).as_stmt(Location::none())
+                        }
+                        _ => {
+                            // Non-virtual, direct drop call
+                            assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _)));
+
+                            let func = self.codegen_func_expr(drop_instance, None);
+                            let place = self.codegen_place(location);
+                            let arg = if let Some(fat_ptr) = place.fat_ptr_goto_expr {
+                                // Drop takes the fat pointer if it exists
+                                fat_ptr
+                            } else {
+                                place.goto_expr.address_of()
+                            };
+                            // The only argument should be a self reference
+                            let args = vec![arg];
+
+                            // We have a known issue where nested Arc and Mutex objects result in
+                            // drop_in_place call implementations that fail to typecheck. Skipping
+                            // drop entirely causes unsound verification results in common cases
+                            // like vector extend, so for now, add a sound special case workaround
+                            // for calls that fail the typecheck.
+                            // https://github.com/model-checking/rmc/issues/426
+                            // Unblocks: https://github.com/model-checking/rmc/issues/435
+                            if Expr::typecheck_call(&func, &args) {
+                                func.call(args)
+                            } else {
+                                self.codegen_unimplemented(
+                                    format!("drop_in_place call for {:?}", func).as_str(),
+                                    func.typ().return_type().unwrap().clone(),
+                                    Location::none(),
+                                    "https://github.com/model-checking/rmc/issues/426",
+                                )
+                            }
+                            .as_stmt(Location::none())
+                        }
+                    }
                 }
             };
             let goto_target = Stmt::goto(self.current_fn().find_label(target), Location::none());
@@ -310,7 +357,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         // should be a fat pointer for the trait
                         let trait_fat_ptr = fargs[0].to_owned();
 
-                        //Check the Gotoc-level fat pointer type
+                        // Check the Gotoc-level fat pointer type
                         assert!(trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table));
 
                         self.codegen_virtual_funcall(

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs

@@ -293,19 +293,21 @@ impl<'tcx> GotocCtx<'tcx> {
         })
     }
 
+    /// `drop_in_place` is a function with type &self -> (), the vtable for
+    /// dynamic trait objects needs a pointer to it
+    pub fn trait_vtable_drop_type(&mut self, t: &'tcx ty::TyS<'tcx>) -> Type {
+        Type::code_with_unnamed_parameters(vec![self.codegen_ty(t).to_pointer()], Type::unit())
+            .to_pointer()
+    }
+
     /// 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`.
     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![
-            Type::datatype_component("drop", drop_ty),
+            Type::datatype_component("drop", self.trait_vtable_drop_type(t)),
             Type::datatype_component("size", Type::size_t()),
             Type::datatype_component("align", Type::size_t()),
         ];
@@ -365,6 +367,12 @@ impl<'tcx> GotocCtx<'tcx> {
         use rustc_middle::ty::print::Printer;
         let mut name = String::new();
         let printer = FmtPrinter::new(self.tcx, &mut name, Namespace::TypeNS);
+
+        // Monomorphizing the type ensures we get a cannonical form for dynamic trait
+        // objects with auto traits, such as:
+        //   StructTag("tag-std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync)>") }
+        //   StructTag("tag-std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>") }
+        let t = self.monomorphize(t);
         with_no_trimmed_paths(|| printer.print_type(t).unwrap());
         // TODO: The following line is a temporary measure to remove the static lifetime
         // appearing as \'static in mangled type names.  This should be done using regular

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/compiler_interface.rs

@@ -95,7 +95,11 @@ impl CodegenBackend for GotocCodegenBackend {
                     MonoItem::Fn(instance) => {
                         c.call_with_panic_debug_info(
                             |ctx| ctx.codegen_function(instance),
-                            format!("codegen_function: {}", c.readable_instance_name(instance)),
+                            format!(
+                                "codegen_function: {}\n{}",
+                                c.readable_instance_name(instance),
+                                c.symbol_name(instance)
+                            ),
                         );
                     }
                     MonoItem::Static(def_id) => {

scripts/std-lib-regression.sh

@@ -14,29 +14,35 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 RMC_DIR=$SCRIPT_DIR/..
 
 # Log output
-STD_LIB_LOG="/tmp/SizeAndAlignOfDstTest/log.txt"
-
-# Use a unit test that requires mutex and cell
+STD_LIB_LOG="/tmp/StdLibTest/log.txt"
 echo "Starting RMC codegen for the Rust standard library"
 cd /tmp
-if [ -d SizeAndAlignOfDstTest ]; then rm -rf SizeAndAlignOfDstTest; fi
-cargo new SizeAndAlignOfDstTest
-cd SizeAndAlignOfDstTest
-cp $RMC_DIR/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs src/main.rs 
-rustup component add rust-src --toolchain nightly > /dev/null 2>&1
-RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo +nightly build -Z build-std --target x86_64-unknown-linux-gnu 2> $STD_LIB_LOG
+if [ -d StdLibTest ]; then rm -rf StdLibTest; fi
+cargo new StdLibTest
+cd StdLibTest
+
+# Check that we have the nighly toolchain, which is required for -Z build-std
+if ! rustup toolchain list | grep -q nightly; then
+  echo "Installing nightly toolchain"
+  rustup toolchain install nightly
+fi
+
+echo "Starting cargo build with RMC"
+RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo +nightly build -Z build-std --target x86_64-unknown-linux-gnu &> $STD_LIB_LOG
 
 # For now, we expect a linker error, but no modules should fail with a compiler
 # panic. 
 #
 # With https://github.com/model-checking/rmc/issues/109, this check can be
 # removed to just allow the success of the previous line to determine the 
 # success of this script (with no $STD_LIB_LOG needed)
-RESULT=$?
+
+# TODO: this check is insufficient if the failure is before codegen
+# https://github.com/model-checking/rmc/issues/375
 if grep -q "error: internal compiler error: unexpected panic" $STD_LIB_LOG; then
   echo "Panic on building standard library"
   cat $STD_LIB_LOG
   exit 1
 else 
 echo "Successful RMC codegen for the Rust standard library"
-fi
+fi

src/test/cbmc/DynTrait/drop_boxed_dyn.rs

@@ -0,0 +1,50 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check drop implementation for a boxed dynamic trait object.
+
+include!("../../rmc-prelude.rs");
+
+static mut CELL: i32 = 0;
+
+trait T {
+    fn t(&self) {}
+}
+
+struct Concrete1;
+
+impl T for Concrete1 {}
+
+impl Drop for Concrete1 {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = 1;
+        }
+    }
+}
+
+struct Concrete2;
+
+impl T for Concrete2 {}
+
+impl Drop for Concrete2 {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = 2;
+        }
+    }
+}
+
+fn main() {
+    {
+        let x: Box<dyn T>;
+        if __nondet() {
+            x = Box::new(Concrete1 {});
+        } else {
+            x = Box::new(Concrete2 {});
+        }
+    }
+    unsafe {
+        assert!(CELL == 1 || CELL == 2);
+    }
+}

src/test/cbmc/DynTrait/drop_concrete.rs

@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check drop implementation for a concrete, non-trait object.
+
+static mut CELL: i32 = 0;
+
+struct Concrete1;
+
+impl Drop for Concrete1 {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = 1;
+        }
+    }
+}
+
+fn main() {
+    {
+        let _x1 = Concrete1 {};
+    }
+    unsafe {
+        assert!(CELL == 1);
+    }
+}