Fix unsized coercion of a struct element (rust-lang#1880)

Fix issues with how we are generating code for casting (rust-lang#566, and rust-lang#1528).

Restructure the unsize casting to be done in one pass instead with deep recursion (rust-lang#1531). This also reuses the code from the reachability analysis, so we don't have to keep two ways of traversing the same structure.

Author: celinval

cprover_bindings/src/goto_program/expr.rs

@@ -732,7 +732,7 @@ impl Expr {
         for field in non_padding_fields {
             let field_typ = field.field_typ().unwrap();
             let value = components.get(&field.name()).unwrap();
-            assert_eq!(value.typ(), field_typ);
+            assert_eq!(value.typ(), field_typ, "Unexpected type for {:?}", field.name());
         }
 
         let values = fields

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

@@ -24,9 +24,7 @@ use rustc_target::abi::{
     VariantIdx, Variants,
 };
 use rustc_target::spec::abi::Abi;
-use std::collections::BTreeMap;
 use std::iter;
-use std::iter::FromIterator;
 use tracing::{debug, trace, warn};
 use ty::layout::HasParamEnv;
 
@@ -1166,7 +1164,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// 3. references to structs whose last field is a unsized object (slice / trait)
     ///    - `matches!(pointee_type.kind(), ty::Adt(..) if self.is_unsized(t))
     ///
-    pub fn codegen_fat_ptr(&mut self, pointee_type: Ty<'tcx>) -> Type {
+    fn codegen_fat_ptr(&mut self, pointee_type: Ty<'tcx>) -> Type {
         assert!(
             !self.use_thin_pointer(pointee_type),
             "Generating a fat pointer for a type requiring a thin pointer: {:?}",
@@ -1781,24 +1779,6 @@ impl<'tcx> GotocCtx<'tcx> {
 
 /// Use maps instead of lists to manage mir struct components.
 impl<'tcx> GotocCtx<'tcx> {
-    /// A mapping from mir field names to mir field types for a mir struct (for a single-variant adt)
-    pub fn mir_struct_field_types(
-        &self,
-        struct_type: Ty<'tcx>,
-    ) -> BTreeMap<InternedString, Ty<'tcx>> {
-        match struct_type.kind() {
-            ty::Adt(adt_def, adt_substs) if adt_def.variants().len() == 1 => {
-                let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
-                BTreeMap::from_iter(
-                    fields.iter().map(|field| {
-                        (field.name.to_string().into(), field.ty(self.tcx, adt_substs))
-                    }),
-                )
-            }
-            _ => unreachable!("Expected a single-variant ADT. Found {:?}", struct_type),
-        }
-    }
-
     /// Extract a trait type from a `Struct<dyn T>`.
     /// Note that `T` must be the last element of the struct.
     /// This also handles nested cases: `Struct<Struct<dyn T>>` returns `dyn T`

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

@@ -108,7 +108,7 @@ impl<'tcx> GotocCtx<'tcx> {
             })
             .collect::<Vec<_>>();
 
-        type_members.iter().rev().fold(boxed_value, |value, (name, typ)| {
+        type_members.iter().rfold(boxed_value, |value, (name, typ)| {
             Expr::struct_expr_with_nondet_fields(
                 typ.clone(),
                 btree_string_map![(*name, value),],

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --mir-linker --enable-unstable
+//! Check the basic coercion when using box of box.
+//! Tests are broken down into different crates to ensure that the reachability works for each case.
+
+mod defs;
+use defs::*;
+use std::boxed::Box;
+
+#[kani::proof]
+fn check_double_coercion() {
+    let id = kani::any();
+    let inner: Box<Box<dyn Identity>> = Box::new(Box::new(Inner { id }));
+    assert_eq!(inner.id(), id.into());
+    assert_eq!(id_from_coerce(*inner), id.into());
+}

tests/kani/DynTrait/unsized_rc_cast_fixme.rs renamed to tests/kani/DynTrait/unsized_rc_cast.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --mir-linker --enable-unstable
+//! Check the basic coercion from using built-in references and pointers.
+//! Tests are broken down into different crates to ensure that the reachability works for each case.
+
+mod defs;
+use defs::*;
+
+#[kani::proof]
+fn check_base_coercion() {
+    let inner_id = kani::any();
+    let outer_id = kani::any();
+    // Generate a fat pointer with a pointer to the vtable for `impl Identity for Inner`.
+    let outer: &Outer<(dyn Identity + Send)> = &Outer { inner: Inner { id: inner_id }, outer_id };
+    let identity: &Outer<(dyn Identity)> = outer;
+    // Create a new fat pointer to inner using the metadata from outer fat pointer.
+    assert_eq!(id_from_dyn(&identity.inner), inner_id.into());
+}