Support trait_upcasting

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

@@ -26,7 +26,10 @@ use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
 };
-use stable_mir::ty::{ClosureKind, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy, VariantIdx};
+use stable_mir::ty::{
+    Binder, ClosureKind, ExistentialPredicate, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy,
+    VariantIdx,
+};
 use std::collections::BTreeMap;
 use tracing::{debug, trace, warn};
 
@@ -1528,9 +1531,26 @@ impl GotocCtx<'_> {
                         VtblEntry::MetadataSize => Some(vt_size.clone()),
                         VtblEntry::MetadataAlign => Some(vt_align.clone()),
                         VtblEntry::Vacant => None,
-                        // TODO: trait upcasting
-                        // https://github.com/model-checking/kani/issues/358
-                        VtblEntry::TraitVPtr(_trait_ref) => None,
+                        VtblEntry::TraitVPtr(trait_ref) => {
+                            let projections = match dst_mir_type.kind() {
+                                TyKind::RigidTy(RigidTy::Dynamic(predicates, ..)) => predicates
+                                    .iter()
+                                    .filter_map(|pred| match &pred.value {
+                                        ExistentialPredicate::Projection(proj) => {
+                                            Some(Binder::bind_with_vars(
+                                                proj.clone(),
+                                                pred.bound_vars.clone(),
+                                            ))
+                                        }
+                                        _ => None,
+                                    })
+                                    .collect(),
+                                _ => vec![],
+                            };
+
+                            let dyn_ref = ctx.trait_ref_to_dyn_trait(*trait_ref, projections);
+                            Some(ctx.codegen_vtable(src_mir_type, dyn_ref, loc).address_of())
+                        }
                         VtblEntry::Method(instance) => Some(ctx.codegen_vtable_method_field(
                             rustc_internal::stable(instance),
                             trait_type,
@@ -1593,18 +1613,44 @@ impl GotocCtx<'_> {
                 };
                 slice_fat_ptr(fat_ptr_type, dst_data_expr, dst_goto_len, &self.symbol_table)
             }
-            (TyKind::RigidTy(RigidTy::Dynamic(..)), TyKind::RigidTy(RigidTy::Dynamic(..))) => {
-                // Cast between fat pointers. Cast the data and the source
+            (
+                ref src_ty @ TyKind::RigidTy(RigidTy::Dynamic(.., ref src_dyn_kind)),
+                ref dst_ty @ TyKind::RigidTy(RigidTy::Dynamic(.., ref dst_dyn_kind)),
+            ) => {
+                assert_eq!(
+                    src_dyn_kind, dst_dyn_kind,
+                    "casting from `{src_dyn_kind:?}` to `{dst_dyn_kind:?}` is not supported"
+                );
+                // Cast between dyn pointers. Cast the data and the source
                 let src_data = src_goto_expr.to_owned().member("data", &self.symbol_table);
                 let dst_data = src_data.cast_to(dst_data_type);
 
                 // Retrieve the vtable and cast the vtable type.
                 let src_vtable = src_goto_expr.member("vtable", &self.symbol_table);
                 let vtable_name = self.vtable_name_stable(metadata_dst_type);
                 let vtable_ty = Type::struct_tag(vtable_name).to_pointer();
-                let dst_vtable = src_vtable.cast_to(vtable_ty);
 
-                // Construct a fat pointer with the same (casted) fields and new type
+                // Note: Logic based on upstream rustc_codegen_ssa:
+                // https://github.com/rust-lang/rust/blob/8bf5a8d/compiler/rustc_codegen_ssa/src/base.rs#L171
+                let dst_vtable = if src_ty.trait_principal() == dst_ty.trait_principal()
+                    || dst_ty.trait_principal().is_none()
+                {
+                    // If we're casting to the same dyn trait, we can reuse the old vtable
+                    src_vtable.cast_to(vtable_ty)
+                } else if let Some(vptr_entry_idx) = self.tcx.supertrait_vtable_slot((
+                    rustc_internal::internal(self.tcx, metadata_src_type),
+                    rustc_internal::internal(self.tcx, metadata_dst_type),
+                )) {
+                    // Otherwise, if the principals differ and our vtable contains a pointer to the supertrait vtable,
+                    // we can load that
+                    src_vtable
+                        .dereference()
+                        .member(vptr_entry_idx.to_string(), &self.symbol_table)
+                        .cast_to(vtable_ty)
+                } else {
+                    // Fallback to original vtable
+                    src_vtable.cast_to(vtable_ty)
+                };
                 dynamic_fat_ptr(fat_ptr_type, dst_data, dst_vtable, &self.symbol_table)
             }
             (_, TyKind::RigidTy(RigidTy::Dynamic(..))) => {

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

@@ -10,20 +10,24 @@ use rustc_abi::{
 };
 use rustc_ast::ast::Mutability;
 use rustc_index::IndexVec;
-use rustc_middle::ty::GenericArgsRef;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::print::FmtPrinter;
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{
-    self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig, Ty,
-    TyCtxt, TyKind, UintTy, VariantDef, VtblEntry,
+    self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig,
+    TraitRef, Ty, TyCtxt, TyKind, UintTy, VariantDef, VtblEntry,
 };
+use rustc_middle::ty::{ExistentialTraitRef, GenericArgsRef};
 use rustc_middle::ty::{List, TypeFoldable};
 use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::Body;
 use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::ty::{
+    Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
+    Ty as StableTy,
+};
 use tracing::{debug, trace, warn};
 
 /// Map the unit type to an empty struct
@@ -254,8 +258,7 @@ impl<'tcx> GotocCtx<'tcx> {
             .is_sized(*self.tcx.at(rustc_span::DUMMY_SP), ty::TypingEnv::fully_monomorphized())
     }
 
-    /// Generates the type for a single field for a dynamic vtable.
-    /// In particular, these fields are function pointers.
+    /// Generates the type for a supertrait vtable pointer field for a vtable.
     fn trait_method_vtable_field_type(
         &mut self,
         instance: Instance<'tcx>,
@@ -274,6 +277,44 @@ impl<'tcx> GotocCtx<'tcx> {
         DatatypeComponent::field(vtable_field_name, fn_ptr)
     }
 
+    pub fn trait_ref_to_dyn_trait(
+        &self,
+        trait_ref: TraitRef<'tcx>,
+        projections: Vec<Binder<ExistentialProjection>>,
+    ) -> StableTy {
+        let existential_trait_ref =
+            rustc_internal::stable(ExistentialTraitRef::erase_self_ty(self.tcx, trait_ref));
+        let binder = Binder::dummy(ExistentialPredicate::Trait(existential_trait_ref));
+
+        let mut predictates = vec![binder];
+        predictates.extend(
+            projections.into_iter().map(|proj| proj.map_bound(ExistentialPredicate::Projection)),
+        );
+        let rigid =
+            RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn);
+
+        stable_mir::ty::Ty::from_rigid_kind(rigid)
+    }
+
+    /// Generates the type for a single field for a dynamic vtable.
+    /// In particular, these fields are function pointers.
+    fn trait_vptr_vtable_field_type(
+        &mut self,
+        idx: usize,
+        trait_ref: TraitRef<'tcx>,
+        projections: Vec<Binder<ExistentialProjection>>,
+    ) -> DatatypeComponent {
+        let dyn_trait = self.trait_ref_to_dyn_trait(trait_ref, projections);
+        let vtable_ty =
+            self.codegen_trait_vtable_type(rustc_internal::internal(self.tcx, dyn_trait));
+        let vtable_ptr = vtable_ty.to_pointer();
+
+        // vtable field name, i.e., 3_vol (idx_method)
+        let vtable_field_name = self.vtable_field_name(idx);
+
+        DatatypeComponent::field(vtable_field_name, vtable_ptr)
+    }
+
     /// Generates a vtable that looks like this:
     ///   struct io::error::vtable {
     ///      void *drop_in_place;
@@ -383,9 +424,11 @@ impl<'tcx> GotocCtx<'tcx> {
                         VtblEntry::Method(instance) => {
                             Some(self.trait_method_vtable_field_type(instance, idx))
                         }
-                        // TODO: trait upcasting
-                        // https://github.com/model-checking/kani/issues/358
-                        VtblEntry::TraitVPtr(..) => None,
+                        VtblEntry::TraitVPtr(trait_ref) => Some(self.trait_vptr_vtable_field_type(
+                            idx,
+                            trait_ref,
+                            binder.projection_bounds().map(rustc_internal::stable).collect(),
+                        )),
                         VtblEntry::MetadataDropInPlace
                         | VtblEntry::MetadataSize
                         | VtblEntry::MetadataAlign

tests/kani/DynTrait/upcast.rs

@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that upcasting to a supertrait works correctly.
+
+trait SubTrait: SuperTrait2 + SuperTrait1 {}
+
+impl<T: SuperTrait1 + SuperTrait2> SubTrait for T {}
+
+trait SuperTrait1 {
+    fn trigger(&self, _old: &()) {}
+}
+
+trait SuperTrait2 {
+    #[allow(unused)]
+    fn func(&self) {}
+}
+
+#[derive(Clone, Copy, Default)]
+struct Struct;
+
+impl SuperTrait1 for Struct {}
+impl SuperTrait2 for Struct {}
+
+#[kani::proof]
+fn main() {
+    let val: &dyn SubTrait = &Struct;
+    (val as &dyn SuperTrait1).trigger(&());
+}