Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects

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

@@ -726,6 +726,17 @@ impl GotocCtx<'_> {
                             dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
                         }
                     }
+                    TyKind::RigidTy(RigidTy::Dynamic(..)) => {
+                        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]);
+                        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 pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) })

tests/kani/CodegenAggregateRawPtrTraitObject/main.rs

@@ -0,0 +1,46 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// Test that Kani can verify code that produces a aggregate raw pointer to trait objects
+// c.f. https://github.com/model-checking/kani/issues/3631
+
+#![feature(ptr_metadata)]
+
+use std::ptr::NonNull;
+
+trait SampleTrait {
+    fn get_value(&self) -> i32;
+}
+
+struct SampleStruct {
+    value: i32,
+}
+
+impl SampleTrait for SampleStruct {
+    fn get_value(&self) -> i32 {
+        self.value
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+fn check_nonnull_dyn_from_raw_parts() {
+    // Create a SampleTrait object from SampleStruct
+    let sample_struct = SampleStruct { value: kani::any() };
+    let trait_object: &dyn SampleTrait = &sample_struct;
+
+    // Get the raw data pointer and metadata for the trait object
+    let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap();
+    let metadata = std::ptr::metadata(trait_object);
+
+    // Create NonNull<dyn SampleTrait> from the data pointer and metadata
+    let nonnull_trait_object: NonNull<dyn SampleTrait> =
+        NonNull::from_raw_parts(trait_ptr, metadata);
+
+    unsafe {
+        // Ensure trait method and member is preserved
+        kani::assert(
+            trait_object.get_value() == nonnull_trait_object.as_ref().get_value(),
+            "trait method and member must correctly preserve",
+        );
+    }
+}