Fix issue with value_of / align_of traits

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

@@ -84,10 +84,10 @@ impl<'tcx> GotocCtx<'tcx> {
         let intrinsic = self.symbol_name(instance);
         let intrinsic = intrinsic.as_str();
         let loc = self.codegen_span_option(span);
-        debug!(
-            "codegen_intrinsic:\n\tinstance {:?}\n\tfargs {:?}\n\tp {:?}\n\tspan {:?}",
-            instance, fargs, p, span
-        );
+        debug!(?instance, "codegen_intrinsic");
+        debug!(?fargs, "codegen_intrinsic");
+        debug!(?p, "codegen_intrinsic");
+        debug!(?span, "codegen_intrinsic");
         let sig = instance.ty(self.tcx, ty::ParamEnv::reveal_all()).fn_sig(self.tcx);
         let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
         let ret_ty = self.monomorphize(sig.output());
@@ -956,15 +956,12 @@ impl<'tcx> GotocCtx<'tcx> {
         }
         match t.kind() {
             ty::Dynamic(..) => {
-                //TODO figure out if this needs to be done, or if the result we want here is for the fat pointer.
-                //We need to get the actual value from the vtable like in codegen_ssa/glue.rs
-                // let vs = self.layout_of(self.tcx.vtable_methods(binder.principal().unwrap().with_self_ty(self.tcx, t)));
-                // https://rust-lang.github.io/unsafe-code-guidelines/layout/pointers.html
-                // The size of &dyn Trait is two words.
-                let size = Expr::int_constant((layout.size.bytes_usize()) * 2, Type::size_t());
-                // The alignment of &dyn Trait is the word size.
-                let align = Expr::int_constant(layout.align.abi.bytes(), usizet);
-                SizeAlign { size, align }
+                // For traits, we need to retrieve the size and alignment from the vtable.
+                let vtable = arg.member("vtable", &self.symbol_table).dereference();
+                SizeAlign {
+                    size: vtable.clone().member("size", &self.symbol_table),
+                    align: vtable.member("align", &self.symbol_table),
+                }
             }
             ty::Slice(_) | ty::Str => {
                 let unit_t = match t.kind() {

tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs

@@ -0,0 +1,57 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --unwind 3
+
+//! This test case checks the behavior of align_of_val for traits.
+#![allow(dead_code)]
+
+use std::mem::align_of_val;
+
+trait T {}
+
+struct A {
+    id: u128,
+}
+
+impl T for A {}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_align_simple() {
+    let a = A { id: 0 };
+    let t: &dyn T = &a;
+    assert_eq!(align_of_val(t), 8);
+    assert_eq!(align_of_val(&t), 8);
+}
+
+trait Wrapper<T: ?Sized> {
+    fn inner(&self) -> &T;
+}
+
+struct Concrete<T: ?Sized> {
+    id: i16,
+    inner: T,
+}
+
+impl<T: ?Sized> Wrapper<T> for Concrete<T> {
+    fn inner(&self) -> &T {
+        &self.inner
+    }
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_align_inner() {
+    let val = 10u8;
+    let conc_wrapper: Concrete<u8> = Concrete { id: 0, inner: val };
+    let trait_wrapper = &conc_wrapper as &dyn Wrapper<u8>;
+
+    assert_eq!(align_of_val(conc_wrapper.inner()), 1); // This is the alignment of val.
+    assert_eq!(align_of_val(&conc_wrapper), 2); // This is the alignment of Concrete.
+    assert_eq!(align_of_val(trait_wrapper), 2); // This is also the alignment of Concrete.
+    assert_eq!(align_of_val(&trait_wrapper), 8); // This is the alignment of the fat pointer.
+}
+
+// This can be run with rustc for comparison.
+fn main() {
+    check_align_simple();
+    check_align_inner();
+}

tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs → tests/kani/Intrinsics/SizeOfVal/size_of_fat_ptr.rs

@@ -3,19 +3,23 @@
 // kani-flags: --unwind 3
 
 //! This test case checks the behavior of size_of_val for traits.
+#![allow(dead_code)]
+
 use std::mem::size_of_val;
 
 trait T {}
 
-struct A {}
+struct A {
+    id: u128,
+}
 
 impl T for A {}
 
 #[cfg_attr(kani, kani::proof)]
 fn check_size_simple() {
-    let a = A {};
+    let a = A { id: 0 };
     let t: &dyn T = &a;
-    assert_eq!(size_of_val(t), 0);
+    assert_eq!(size_of_val(t), 16);
     assert_eq!(size_of_val(&t), 16);
 }