From 325c9e4c6ec7022be9ac6c7a5d99cf67db8cd715 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 23 Oct 2024 14:44:15 -0400
Subject: [PATCH] Fix ICE due to mishandling of Aggregate rvalue for raw
 pointers to trait objects (#3636)

Add a match arm for the
`AggregateKind::RawPtr(TyKind::RigidTy(RigidTy::Dynamic(..)))` case.
Pointers to trait objects [are
fat](https://github.com/rust-lang/rust/blob/master/library/core/src/ptr/metadata.rs#L20-#L27),
so generate a fat pointer for the rvalue.

Resolves #3631

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 11 +++++
 .../CodegenAggregateRawPtrTraitObject/main.rs | 46 +++++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 tests/kani/CodegenAggregateRawPtrTraitObject/main.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/kani/CodegenAggregateRawPtrTraitObject/main.rs b/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs
new file mode 100644
index 000000000000..92ffb413ae70
--- /dev/null
+++ b/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",
+        );
+    }
+}