Fix codegen for rvalue aggregate raw pointer to an adt with slice tail

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

@@ -709,21 +709,37 @@ impl GotocCtx<'_> {
                         let meta = self.codegen_operand_stable(&operands[1]);
                         slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
                     }
-                    TyKind::RigidTy(RigidTy::Adt(..)) => {
+                    TyKind::RigidTy(RigidTy::Adt(_, generic_args)) => {
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         let data_cast =
                             data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
                         let meta = self.codegen_operand_stable(&operands[1]);
+                        // This is a thin raw pointer; `pointee_ty` is a statically sized ADT and has zero-sized metadata.
                         if meta.typ().sizeof(&self.symbol_table) == 0 {
                             data_cast
+                        // This is a wide raw pointer; `pointee_ty` is a DST and has non-zero-sized metadata.
+                        // An ADT can be a DST if it is a struct and its last field is a DST.
+                        // c.f. https://doc.rust-lang.org/nomicon/exotic-sizes.html#dynamically-sized-types-dsts
                         } else {
-                            let vtable_expr = meta
-                                .member("_vtable_ptr", &self.symbol_table)
-                                .member("pointer", &self.symbol_table)
-                                .cast_to(
-                                    typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
-                                );
-                            dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
+                            let mut dst_field = *generic_args.0.first().expect("To construct an ADT that is a DST, there must be a generic argument").expect_ty();
+                            while let TyKind::RigidTy(RigidTy::Adt(_, generic_args)) =
+                                dst_field.kind()
+                            {
+                                dst_field = *generic_args.0.first().unwrap().expect_ty();
+                            }
+
+                            if dst_field.kind().is_slice() {
+                                slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
+                            } else {
+                                let vtable_expr = meta
+                                    .member("_vtable_ptr", &self.symbol_table)
+                                    .member("pointer", &self.symbol_table)
+                                    .cast_to(
+                                        typ.lookup_field_type("vtable", &self.symbol_table)
+                                            .unwrap(),
+                                    );
+                                dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
+                            }
                         }
                     }
                     TyKind::RigidTy(RigidTy::Dynamic(..)) => {

tests/kani/CodegenRawPtrADTSliceTail/main.rs

@@ -0,0 +1,58 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// Test codegen for a raw pointer to a struct whose last field is a slice
+
+#![feature(layout_for_ptr)]
+#![feature(ptr_metadata)]
+
+// https://github.com/model-checking/kani/issues/3615
+mod issue_3615 {
+    use std::ptr;
+
+    #[derive(Clone, Copy, kani::Arbitrary)]
+    struct Wrapper<T: ?Sized> {
+        _size: usize,
+        _value: T,
+    }
+
+    #[kani::proof]
+    pub fn from_raw_parts_for_slices() {
+        let var: Wrapper<[u64; 4]> = kani::any();
+        let fat_ptr: *const Wrapper<[u64]> = &var as *const _;
+        let (thin_ptr, _) = fat_ptr.to_raw_parts();
+        let new_size: usize = kani::any();
+        let _new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size);
+    }
+
+    #[kani::proof]
+    pub fn from_raw_parts_for_slices_nested() {
+        let var: Wrapper<Wrapper<[u8; 4]>> = kani::any();
+        let fat_ptr: *const Wrapper<Wrapper<[u8]>> = &var as *const _;
+        let (thin_ptr, _) = fat_ptr.to_raw_parts();
+        let new_size: usize = kani::any();
+        let _new_ptr: *const Wrapper<Wrapper<[u8]>> = ptr::from_raw_parts(thin_ptr, new_size);
+    }
+}
+
+// https://github.com/model-checking/kani/issues/3638
+mod issue_3638 {
+    use std::ptr::NonNull;
+
+    #[derive(kani::Arbitrary)]
+    struct Wrapper<T: ?Sized>(usize, T);
+
+    #[cfg(kani)]
+    #[kani::proof]
+    fn main() {
+        // Create a SampleTrait object from SampleStruct
+        let original: Wrapper<[u8; 10]> = kani::any();
+        let slice: &Wrapper<[u8]> = &original;
+
+        // Get the raw data pointer and metadata for the trait object
+        let slice_ptr = NonNull::new(slice as *const _ as *mut ()).unwrap();
+        let metadata = std::ptr::metadata(slice);
+
+        // Create NonNull<dyn SampleTrait> from the data pointer and metadata
+        let _: NonNull<Wrapper<[u8]>> = NonNull::from_raw_parts(slice_ptr, metadata);
+    }
+}