Fix handling of dyn T (rust-lang#1073)

During codegen we were handling `dyn T` the same way as `&dyn T` which
was causing a bunch of type mismatch warnings.

To fix that, I first changed how we encode trait fat pointers. We
used to encode them as:

```
struct RefToTrait {
    void* data;
    Tag* vtable;
}
```

But now we encode them as:

```
struct RefToTrait {
    T* data;     // This is a typedef to void*.
    Tag* vtable;
}
```

Then I modified encoding `dyn T` to codegen a thin pointer `T*`. I had
also to modify places where we were forcing `void*` to be the type of
the `data` field.

* Fix vtable restriction after `dyn T` refactoring.

The vtable restriction code was relying on the fact that `dyn T` and
`&dyn T` were generating the same gotoc expression. Instead, we now
ensure that we pass the fat pointer type to the function that creates
the vtable call site.

* Fix Rc<dyn> and add a bunch of debug stuff.

I'm still seeing tons of type mismatch on std crate and unable to find
vtable warnings.

* Add testcase for issue-990

* Clean up code for PR

* Codegen unimplemented for dropping unsized struct

We were incorrectly handling them. I'm mitigation this issue for now and
I created a testcase.

Note: Without this mitigation but with the fix to fat
pointers not using void*, this was failing codegen of firecracker.

* Replace bool by Unit

* PR comments + better tests

* Add assertion and improve comments

Author: celinval

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -15,7 +15,7 @@ use rustc_middle::ty::{self, Instance};
 use std::collections::BTreeMap;
 use std::convert::TryInto;
 use std::iter::FromIterator;
-use tracing::{debug, info_span, warn};
+use tracing::{debug, info_span};
 
 /// Utility to skip functions that can't currently be successfully codgenned.
 impl<'tcx> GotocCtx<'tcx> {
@@ -73,7 +73,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let _trace_span =
             info_span!("CodegenFunction", name = self.current_fn().readable_name()).entered();
         if old_sym.is_function_definition() {
-            warn!("Double codegen of {:?}", old_sym);
+            tracing::info!("Double codegen of {:?}", old_sym);
         } else if self.should_skip_current_fn() {
             debug!("Skipping function {}", self.current_fn().readable_name());
             let body = self.codegen_fatal_error(

kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs

@@ -14,7 +14,9 @@ mod rvalue;
 mod span;
 mod statement;
 mod static_var;
-mod typ;
+
+// Visible for all codegen module.
+pub(super) mod typ;
 
 pub use assert::PropertyClass;
 pub use typ::TypeExt;

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -16,7 +16,7 @@ use rustc_middle::{
     ty::{self, Ty, TypeAndMut, VariantDef},
 };
 use rustc_target::abi::{TagEncoding, Variants};
-use tracing::{debug, warn};
+use tracing::{debug, trace, warn};
 
 /// A projection in Kani can either be to a type (the normal case),
 /// or a variant in the case of a downcast.
@@ -114,6 +114,14 @@ impl<'tcx> ProjectedPlace<'tcx> {
                         {
                             None
                         }
+                        // TODO: Do we really need this?
+                        // https://github.com/model-checking/kani/issues/1092
+                        ty::Dynamic(..)
+                            if expr_ty.is_pointer()
+                                && *expr_ty.base_type().unwrap() == type_from_mir =>
+                        {
+                            None
+                        }
                         _ => Some((expr_ty, type_from_mir)),
                     }
                 } else {
@@ -325,6 +333,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let before = before?;
         match proj {
             ProjectionElem::Deref => {
+                trace!(?before, ?proj, "codegen_projection");
                 let base_type = before.mir_typ();
                 let inner_goto_expr = if base_type.is_box() {
                     self.deref_box(before.goto_expr)
@@ -341,7 +350,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 } else {
                     before.fat_ptr_mir_typ
                 };
-
                 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())

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -140,7 +140,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // The thin pointer in the resulting fat pointer is a pointer to the value
         let thin_pointer = if place_goto_expr.typ().is_pointer() {
-            // The value is itself a pointer (eg, a void pointer), just use this pointer
+            // The value is itself a pointer, just use this pointer
             place_goto_expr
         } else if place_goto_expr.typ().is_array_like() {
             // The value is an array (eg, a flexible struct member), point to the first array element
@@ -162,12 +162,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if self.use_slice_fat_pointer(place_mir_type) {
             slice_fat_ptr(result_goto_type, thin_pointer, metadata, &self.symbol_table)
         } else if self.use_vtable_fat_pointer(place_mir_type) {
-            dynamic_fat_ptr(
-                result_goto_type,
-                thin_pointer.cast_to(Type::void_pointer()),
-                metadata,
-                &self.symbol_table,
-            )
+            dynamic_fat_ptr(result_goto_type, thin_pointer, metadata, &self.symbol_table)
         } else {
             unreachable!();
         }
@@ -720,10 +715,12 @@ impl<'tcx> GotocCtx<'tcx> {
         t: Ty<'tcx>,
         idx: usize,
     ) -> Expr {
+        debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field");
         let vtable_field_name = self.vtable_field_name(instance.def_id(), idx);
         let vtable_type = Type::struct_tag(self.vtable_name(t));
         let field_type =
             vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap();
+        debug!(?vtable_field_name, ?vtable_type, "codegen_vtable_method_field");
 
         // Lookup in the symbol table using the full symbol table name/key
         let fn_name = self.symbol_name(instance);
@@ -741,6 +738,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // Create a pointer to the method
             // Note that the method takes a self* as the first argument, but the vtable field type has a void* as the first arg.
             // So we need to cast it at the end.
+            debug!(?fn_symbol, fn_typ=?fn_symbol.typ, ?field_type, "codegen_vtable_method_field");
             Expr::symbol_expression(fn_symbol.name, fn_symbol.typ.clone())
                 .address_of()
                 .cast_to(field_type)
@@ -773,6 +771,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 );
             }
 
+            debug!(?ty, ?trait_ty, "codegen_drop_in_place");
+            debug!(?drop_instance, ?trait_fn_ty, "codegen_drop_in_place");
+            debug!(drop_sym=?drop_sym.clone().typ, "codegen_drop_in_place");
+
             Expr::symbol_expression(drop_sym_name, drop_sym.clone().typ)
                 .address_of()
                 .cast_to(trait_fn_ty)
@@ -959,20 +961,23 @@ impl<'tcx> GotocCtx<'tcx> {
         if src_mir_type.kind() == dst_mir_type.kind() {
             return None; // no cast required, nothing to do
         }
+        debug!(?src_goto_expr, ?src_mir_type, ?dst_mir_type, "cast_unsized_dyn_trait");
 
         // The source destination must be a fat pointers to a dyn trait object
         assert!(self.is_vtable_fat_pointer(src_mir_type));
         assert!(self.is_vtable_fat_pointer(dst_mir_type));
 
+        let dst_goto_type = self.codegen_ty(dst_mir_type);
+
+        // Cast the data type.
         let dst_mir_dyn_ty = pointee_type(dst_mir_type).unwrap();
+        let dst_data_type = self.codegen_trait_data_pointer(dst_mir_dyn_ty);
+        let data =
+            src_goto_expr.to_owned().member("data", &self.symbol_table).cast_to(dst_data_type);
 
-        // Get the fat pointer data and vtable fields, and cast the type of
-        // the vtable.
-        let dst_goto_type = self.codegen_ty(dst_mir_type);
-        let data = src_goto_expr.to_owned().member("data", &self.symbol_table);
+        // Retrieve the vtable and cast the vtable type.
         let vtable_name = self.vtable_name(dst_mir_dyn_ty);
         let vtable_ty = Type::struct_tag(vtable_name).to_pointer();
-
         let vtable = src_goto_expr.member("vtable", &self.symbol_table).cast_to(vtable_ty);
 
         // Construct a fat pointer with the same (casted) fields and new type
@@ -1108,15 +1113,19 @@ impl<'tcx> GotocCtx<'tcx> {
     fn cast_sized_pointer_to_trait_fat_pointer(
         &mut self,
         src_goto_expr: Expr,
-        _src_mir_type: Ty<'tcx>,
+        src_mir_type: Ty<'tcx>,
         dst_mir_type: Ty<'tcx>,
         src_pointee_type: Ty<'tcx>,
         dst_pointee_type: Ty<'tcx>,
     ) -> Option<Expr> {
+        tracing::trace!(?src_pointee_type, ?dst_pointee_type, "cast_thin_2_fat_ptr");
+        tracing::trace!(?src_mir_type, ?dst_mir_type, "cast_thin_2_fat_ptr");
         if let Some((concrete_type, trait_type)) =
             self.nested_pair_of_concrete_and_trait_types(src_pointee_type, dst_pointee_type)
         {
-            let dst_goto_expr = src_goto_expr.cast_to(Type::void_pointer());
+            tracing::trace!(?concrete_type, ?trait_type, "cast_thin_2_fat_ptr");
+            let dst_goto_expr =
+                src_goto_expr.cast_to(self.codegen_ty(dst_pointee_type).to_pointer());
             let dst_goto_type = self.codegen_ty(dst_mir_type);
             let vtable = self.codegen_vtable(concrete_type, trait_type);
             let vtable_expr = vtable.address_of();

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -3,6 +3,7 @@
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::PropertyClass;
+use crate::codegen_cprover_gotoc::codegen::typ::pointee_type;
 use crate::codegen_cprover_gotoc::utils;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
@@ -20,7 +21,7 @@ use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{Instance, InstanceDef, Ty};
 use rustc_span::Span;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
-use tracing::{debug, info_span};
+use tracing::{debug, info_span, warn};
 
 impl<'tcx> GotocCtx<'tcx> {
     fn codegen_ret_unit(&mut self) -> Stmt {
@@ -152,6 +153,7 @@ impl<'tcx> GotocCtx<'tcx> {
     // https://github.com/model-checking/kani/issues/221
     fn codegen_drop(&mut self, location: &Place<'tcx>, target: &BasicBlock) -> Stmt {
         let loc_ty = self.place_ty(location);
+        debug!(?loc_ty, "codegen_drop");
         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 =
@@ -174,18 +176,34 @@ impl<'tcx> GotocCtx<'tcx> {
                             )
                             .fat_ptr_goto_expr
                             .unwrap();
+                            debug!(?trait_fat_ptr, "codegen_drop: ");
 
                             // 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 =
+                            if let Some(typ) = pointee_type(self.local_ty(location.local)) {
+                                if !(typ.is_trait() || typ.is_box()) {
+                                    warn!(self_type=?typ, "Unsupported drop of unsized");
+                                    return self
+                                        .codegen_unimplemented(
+                                            format!("Unsupported drop unsized struct: {:?}", typ)
+                                                .as_str(),
+                                            Type::Empty,
+                                            Location::None,
+                                            "https://github.com/model-checking/kani/issues/1072",
+                                        )
+                                        .as_stmt(Location::None);
+                                }
+                            }
+                            let self_data =
                                 trait_fat_ptr.to_owned().member("data", &self.symbol_table);
                             let self_ref =
-                                self_ref.cast_to(trait_fat_ptr.typ().clone().to_pointer());
+                                self_data.clone().cast_to(trait_fat_ptr.typ().clone().to_pointer());
 
                             let call =
                                 fn_ptr.dereference().call(vec![self_ref]).as_stmt(Location::none());