From bf4a207b4058095b551264b90882f97287138cb9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 5 Jun 2024 13:10:10 +0000
Subject: [PATCH] PtrMetadata

---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 47 +++++++++++++++++--
 .../src/codegen_cprover_gotoc/utils/utils.rs  |  2 +-
 2 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 42d3ef31f4c1..395bf0892da2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -800,10 +800,49 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
                 UnOp::Neg => self.codegen_operand_stable(e).neg(),
                 UnOp::PtrMetadata => {
-                    // 1. create a test that uses std::ptr::metadata
-                    // 2. figure out what the operand is (should be a raw ptr)
-                    // 3. figure out what res_ty is
-                    todo!()
+                    let src_goto_expr = self.codegen_operand_stable(e);
+                    let dst_goto_typ = self.codegen_ty_stable(res_ty);
+                    debug!(
+                        "PtrMetadata |{:?}| with result type |{:?}|",
+                        src_goto_expr, dst_goto_typ
+                    );
+                    if let Some(_vtable_typ) =
+                        src_goto_expr.typ().lookup_field_type("vtable", &self.symbol_table)
+                    {
+                        let vtable_expr = src_goto_expr.member("vtable", &self.symbol_table);
+                        let dst_components =
+                            dst_goto_typ.lookup_components(&self.symbol_table).unwrap();
+                        assert_eq!(dst_components.len(), 2);
+                        assert_eq!(dst_components[0].name(), "_vtable_ptr");
+                        assert!(dst_components[0].typ().is_pointer());
+                        assert_eq!(dst_components[1].name(), "_phantom");
+                        self.assert_is_rust_phantom_data_like(&dst_components[1].typ());
+                        Expr::struct_expr(
+                            dst_goto_typ,
+                            btree_string_map![
+                                ("_vtable_ptr", vtable_expr.cast_to(dst_components[0].typ())),
+                                (
+                                    "_phantom",
+                                    Expr::struct_expr(
+                                        dst_components[1].typ(),
+                                        [].into(),
+                                        &self.symbol_table
+                                    )
+                                )
+                            ],
+                            &self.symbol_table,
+                        )
+                    } else if let Some(len_typ) =
+                        src_goto_expr.typ().lookup_field_type("len", &self.symbol_table)
+                    {
+                        assert_eq!(len_typ, dst_goto_typ);
+                        src_goto_expr.member("len", &self.symbol_table)
+                    } else {
+                        unreachable!(
+                            "fat pointer with neither vtable nor len: {:?}",
+                            src_goto_expr
+                        );
+                    }
                 }
             },
             Rvalue::Discriminant(p) => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index e369f64beda9..16edca2a826c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -125,7 +125,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Best effort check if the struct represents a rust `std::marker::PhantomData`
-    fn assert_is_rust_phantom_data_like(&self, t: &Type) {
+    pub fn assert_is_rust_phantom_data_like(&self, t: &Type) {
         // TODO: A `std::marker::PhantomData` appears to be an empty struct, in the cases we've seen.
         // Is there something smarter we can do here?
         assert!(t.is_struct_like());