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

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

@@ -709,13 +709,23 @@ 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
+                        // Case 1: Last field is a slice
+                        } else if !generic_args.0.is_empty()
+                            && generic_args.0.first().unwrap().expect_ty().kind().is_slice()
+                        {
+                            slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
+                        // Case 2: Last field is a trait object
                         } else {
                             let vtable_expr = meta
                                 .member("_vtable_ptr", &self.symbol_table)

tests/kani/CodegenRawPtrADTSliceTail/main.rs

@@ -0,0 +1,49 @@
+// 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 check_size_of_overflows() {
+        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);
+    }
+}
+
+// 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);
+    }
+}