From 28d1288af4e0ad18b51e522bc6e32a7a4eb80d1b Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 23 Oct 2024 11:29:53 -0400
Subject: [PATCH] fix issue 3631

---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 11 +++++
 tests/expected/issue-3631/issue-3631.expected |  1 +
 tests/expected/issue-3631/issue-3631.rs       | 44 +++++++++++++++++++
 3 files changed, 56 insertions(+)
 create mode 100644 tests/expected/issue-3631/issue-3631.expected
 create mode 100644 tests/expected/issue-3631/issue-3631.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 779874f2ff77..7f578940d98e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/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) })
diff --git a/tests/expected/issue-3631/issue-3631.expected b/tests/expected/issue-3631/issue-3631.expected
new file mode 100644
index 000000000000..f9a64dc8af9a
--- /dev/null
+++ b/tests/expected/issue-3631/issue-3631.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESS
\ No newline at end of file
diff --git a/tests/expected/issue-3631/issue-3631.rs b/tests/expected/issue-3631/issue-3631.rs
new file mode 100644
index 000000000000..6f1d2d2c6aa0
--- /dev/null
+++ b/tests/expected/issue-3631/issue-3631.rs
@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![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 main() {
+    // 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",
+        );
+    }
+}