Supporting dyn Trait

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1952,6 +1952,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
           ("layout", layout);
           ("ptr_metadata", ptr_metadata);
           ("repr", repr);
+          ("drop_glue", drop_glue);
         ] ->
         let* def_id = type_decl_id_of_json ctx def_id in
         let* item_meta = item_meta_of_json ctx item_meta in
@@ -1961,6 +1962,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
         let* layout = option_of_json layout_of_json ctx layout in
         let* ptr_metadata = ptr_metadata_of_json ctx ptr_metadata in
         let* repr = option_of_json repr_options_of_json ctx repr in
+        let* drop_glue = option_of_json trait_impl_ref_of_json ctx drop_glue in
         Ok
           ({
              def_id;
@@ -1971,6 +1973,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
              layout;
              ptr_metadata;
              repr;
+             drop_glue;
            }
             : type_decl)
     | _ -> Error "")

charon-ml/src/generated/Generated_Types.ml

@@ -929,6 +929,9 @@ and type_decl = {
   repr : repr_options option;
       (** The representation options of this type declaration as annotated by
           the user. Is [None] for foreign type declarations. *)
+  drop_glue : trait_impl_ref option;
+      (** The drop implementation for this type, if any. This is [Some] if and
+          only if the given type has a drop implementation. *)
 }
 
 and type_decl_kind =

charon/src/ast/expressions_utils.rs

@@ -105,6 +105,13 @@ impl Operand {
             Operand::Const(constant_expr) => &constant_expr.ty,
         }
     }
+
+    pub fn opaque(msg: String, ty: Ty) -> Self {
+        Operand::Const(Box::new(ConstantExpr {
+            kind: ConstantExprKind::Opaque(msg),
+            ty,
+        }))
+    }
 }
 
 impl Rvalue {

charon/src/ast/krate.rs

@@ -83,6 +83,11 @@ impl TryFrom<ItemId> for FunId {
         Ok(FunId::Regular(x.try_into()?))
     }
 }
+impl From<TypeDeclId> for TypeId {
+    fn from(x: TypeDeclId) -> Self {
+        TypeId::Adt(x)
+    }
+}
 
 /// A reference to a translated item.
 #[derive(

charon/src/ast/meta_utils.rs

@@ -120,8 +120,14 @@ pub fn combine_span(m0: &Span, m1: &Span) -> Span {
 
 /// Combine all the span information in a slice.
 pub fn combine_span_iter<'a, T: Iterator<Item = &'a Span>>(mut ms: T) -> Span {
-    // The iterator should have a next element
-    let mut mc: Span = *ms.next().unwrap();
+    // Handle the case where the iterator might be empty
+    let mut mc: Span = match ms.next() {
+        Some(span) => *span,
+        None => {
+            // Return a dummy span if the iterator is empty
+            return Span::dummy();
+        }
+    };
     for m in ms {
         mc = combine_span(&mc, m);
     }

charon/src/ast/types.rs

@@ -467,6 +467,9 @@ pub struct TypeDecl {
     /// Is `None` for foreign type declarations.
     #[drive(skip)]
     pub repr: Option<ReprOptions>,
+    /// The drop implementation for this type, if any.
+    /// This is `Some` if and only if the given type has a drop implementation.
+    pub drop_glue: Option<TraitImplRef>,
 }
 
 generate_index_type!(VariantId, "Variant");

charon/src/ast/types_utils.rs

@@ -669,6 +669,238 @@ impl Ty {
         }
     }
 
+    pub fn needs_drop(&self, translated: &TranslatedCrate) -> Result<bool, String> {
+        match self.kind() {
+            TyKind::Adt(type_decl_ref) => match type_decl_ref.id {
+                TypeId::Adt(type_decl_id) => {
+                    let type_decl = translated.type_decls.get(type_decl_id).ok_or_else(|| {
+                        format!(
+                            "Type declaration for {} not found",
+                            type_decl_id.with_ctx(&translated.into_fmt())
+                        )
+                    })?;
+                    Ok(type_decl.drop_glue.is_some())
+                }
+                TypeId::Tuple => {
+                    let tuple_generics = &type_decl_ref.generics.types;
+                    // A tuple needs drop if any of its elements need drop
+                    for element_ty in tuple_generics.iter() {
+                        if element_ty.needs_drop(translated)? {
+                            return Ok(true);
+                        }
+                    }
+                    Ok(false)
+                }
+                TypeId::Builtin(builtin_ty) => match builtin_ty {
+                    BuiltinTy::Box => Ok(true), // Box always needs drop
+                    BuiltinTy::Array => {
+                        let element_ty = &type_decl_ref.generics.types[0];
+                        element_ty.needs_drop(translated)
+                    }
+                    BuiltinTy::Str | BuiltinTy::Slice => Ok(false), // str & [T] does not need drop
+                },
+            },
+            TyKind::DynTrait(..) => Ok(false),
+            TyKind::Literal(..) => Ok(false), // Literal types do not need drop
+            TyKind::PtrMetadata(..) => Ok(false), // Pointer metadata does not need drop, as it is either usize or a vtable pointer
+            TyKind::Ref(..) | TyKind::RawPtr(..) => Ok(false), // References and raw pointers do not need drop
+            TyKind::FnPtr(..) => Ok(false),                    // Function pointers do not need drop
+            TyKind::FnDef(..) => Ok(false), // Function definitions do not need drop
+            TyKind::TraitType(..) | TyKind::TypeVar(..) | TyKind::Never | TyKind::Error(_) => {
+                Err(format!(
+                    "Cannot determine if type {} needs drop",
+                    self.with_ctx(&translated.into_fmt())
+                ))
+            }
+        }
+    }
+
+    /// Returns either the layout of this type, or a string with the reason why we couldn't compute it.
+    pub fn layout(&self, translated: &TranslatedCrate) -> Result<Layout, String> {
+        match self.kind() {
+            TyKind::Adt(type_decl_ref) => {
+                match &type_decl_ref.id {
+                    TypeId::Adt(type_decl_id) => {
+                        let type_decl =
+                            translated.type_decls.get(*type_decl_id).ok_or_else(|| {
+                                format!(
+                                    "Type declaration for {} not found",
+                                    type_decl_id.with_ctx(&translated.into_fmt())
+                                )
+                            })?;
+                        let layout = type_decl
+                            .layout
+                            .as_ref()
+                            .ok_or("Layout not available for ADT")?;
+                        Ok(layout.clone())
+                    }
+                    TypeId::Tuple => {
+                        // Get the tuple element types from generics
+                        let element_types = &type_decl_ref.generics.types;
+                        // Compute layout for tuple elements
+                        let mut total_size: Option<u64> = Some(0);
+                        let mut max_align: Option<u64> = Some(1);
+                        let mut is_uninhabited = false;
+
+                        for element_ty in element_types.iter() {
+                            let element_layout = element_ty.layout(translated)?;
+                            if element_layout.uninhabited {
+                                is_uninhabited = true;
+                            }
+
+                            match (
+                                total_size,
+                                element_layout.size,
+                                element_layout.align,
+                                max_align,
+                            ) {
+                                (
+                                    Some(current_size),
+                                    Some(elem_size),
+                                    Some(elem_align),
+                                    Some(current_max_align),
+                                ) => {
+                                    // Apply alignment padding
+                                    let aligned_size =
+                                        (current_size + elem_align - 1) / elem_align * elem_align;
+                                    total_size = Some(aligned_size + elem_size);
+                                    max_align = Some(current_max_align.max(elem_align));
+                                }
+                                _ => {
+                                    // If any size or alignment is None, the final result is None
+                                    total_size = None;
+                                    max_align = None;
+                                }
+                            }
+                        }
+
+                        if is_uninhabited {
+                            // If any element is uninhabited, the whole tuple is uninhabited
+                            return Ok(Layout {
+                                size: Some(0),
+                                align: max_align.or(Some(1)), // Ensure at least 1-byte alignment
+                                uninhabited: true,
+                                variant_layouts: Vector::new(),
+                                discriminant_layout: None,
+                            });
+                        }
+
+                        // Final padding to struct alignment
+                        let final_size = match (total_size, max_align) {
+                            (Some(size), Some(align)) => Some((size + align - 1) / align * align),
+                            _ => None,
+                        };
+
+                        Ok(Layout {
+                            size: final_size,
+                            align: max_align,
+                            uninhabited: is_uninhabited,
+                            variant_layouts: Vector::new(),
+                            discriminant_layout: None,
+                        })
+                    }
+                    TypeId::Builtin(builtin_ty) => {
+                        match builtin_ty {
+                            BuiltinTy::Box => Err("TODO: handle Box with ptr-metadata".to_string()),
+                            BuiltinTy::Array => {
+                                // Array layout: element_type repeated const_generics[0] times
+                                let element_ty = &type_decl_ref.generics.types[0];
+                                let element_layout = element_ty.layout(translated)?;
+
+                                if element_layout.uninhabited {
+                                    return Ok(Layout {
+                                        size: Some(0),
+                                        align: element_layout.align,
+                                        uninhabited: true,
+                                        variant_layouts: Vector::new(),
+                                        discriminant_layout: None,
+                                    });
+                                }
+
+                                let cg = type_decl_ref
+                                    .generics
+                                    .const_generics
+                                    .get(ConstGenericVarId::ZERO)
+                                    .unwrap();
+                                let ConstGeneric::Value(Literal::Scalar(scalar)) = cg else {
+                                    return Err(format!(
+                                        "No instant available const generic value or wrong format value: {}",
+                                        cg.with_ctx(&translated.into_fmt())
+                                    ));
+                                };
+                                let len = scalar.as_uint().or_else(|e| {
+                                    Err(format!("Failed to get array length: {:?}", e))
+                                })?;
+
+                                let element_size = element_layout.size;
+                                let align = element_layout.align;
+
+                                let size = element_size.map(|s| s * (len as u64));
+
+                                Ok(Layout {
+                                    size,
+                                    align,
+                                    uninhabited: false,
+                                    variant_layouts: Vector::new(),
+                                    discriminant_layout: None,
+                                })
+                            }
+                            BuiltinTy::Slice | BuiltinTy::Str => {
+                                Err("DST does not have layout".to_string())
+                            }
+                        }
+                    }
+                }
+            }
+            TyKind::Literal(lit_ty) => {
+                // For literal types, create a simple scalar layout
+                let size =
+                    lit_ty.target_size(translated.target_information.target_pointer_size) as u64;
+                Ok(Layout {
+                    size: Some(size),
+                    align: Some(size), // Scalar types are self-aligned
+                    uninhabited: false,
+                    variant_layouts: Vector::new(),
+                    discriminant_layout: None,
+                })
+            }
+            TyKind::RawPtr(_, _) | TyKind::Ref(_, _, _) => {
+                Err("TODO: handle pointer/reference with ptr-metadata".to_string())
+            }
+            TyKind::TypeVar(_) => Err("No layout due to generic".to_string()),
+            _ => Err(format!(
+                "Don't know how to compute layout for type {}",
+                self.with_ctx(&translated.into_fmt())
+            )),
+        }
+    }
+
+    /// Substitue the given `target_ty` with the `replacement` type recursively in this type.
+    /// E.g., if `self` is `Vec<i32>`, `target_ty` is `i32` and `replacement` is `Vec<i32>`, then
+    /// `self` will become `Vec<Vec<i32>>`.
+    /// No recursion is performed for `target_ty` and `replacement`.
+    pub fn substitute_ty(&mut self, target_ty: &Ty, replacement: &Ty) {
+        #[derive(Visitor)]
+        struct SubstituteVisitor<'a, 'b> {
+            target_ty: &'a Ty,
+            replacement: &'b Ty,
+        }
+        impl VisitAstMut for SubstituteVisitor<'_, '_> {
+            fn visit_ty(&mut self, x: &mut Ty) -> ::std::ops::ControlFlow<Self::Break> {
+                if *x == *self.target_ty {
+                    *x = self.replacement.clone();
+                    ControlFlow::Continue(())
+                } else {
+                    self.visit_inner(x)
+                }
+            }
+        }
+        let _ = self.drive_mut(&mut SubstituteVisitor {
+            target_ty,
+            replacement,
+        });
+    }
+
     /// Return true if this is a scalar type
     pub fn is_scalar(&self) -> bool {
         match self.kind() {
@@ -822,6 +1054,12 @@ impl TypeDeclRef {
     }
 }
 
+impl From<LiteralTy> for Ty {
+    fn from(lit: LiteralTy) -> Ty {
+        TyKind::Literal(lit).into_ty()
+    }
+}
+
 impl TraitDeclRef {
     pub fn self_ty<'a>(&'a self, krate: &'a TranslatedCrate) -> Option<&'a Ty> {
         match self.generics.types.iter().next() {

charon/src/ast/values_utils.rs

@@ -1,4 +1,6 @@
 //! Implementations for [crate::values]
+use core::panic;
+
 use crate::ast::*;
 
 #[derive(Debug, Clone)]
@@ -229,6 +231,32 @@ impl ScalarValue {
     }
 }
 
+impl From<Literal> for ConstantExpr {
+    fn from(lit: Literal) -> Self {
+        let ty = match &lit {
+            Literal::Scalar(scalar) => match scalar {
+                ScalarValue::Signed(int_ty, _) => {
+                    TyKind::Literal(LiteralTy::Int(*int_ty)).into_ty()
+                }
+                ScalarValue::Unsigned(uint_ty, _) => {
+                    TyKind::Literal(LiteralTy::UInt(*uint_ty)).into_ty()
+                }
+            },
+            Literal::Float(float) => TyKind::Literal(LiteralTy::Float(float.ty)).into_ty(),
+            Literal::Bool(_) => TyKind::Literal(LiteralTy::Bool).into_ty(),
+            Literal::Char(_) => TyKind::Literal(LiteralTy::Char).into_ty(),
+            _ => panic!(
+                "Only scalar literals can be converted to ConstantExpr, got {:?}",
+                lit
+            ),
+        };
+        ConstantExpr {
+            kind: ConstantExprKind::Literal(lit),
+            ty,
+        }
+    }
+}
+
 /// Custom serializer that stores 128 bit integers as strings to avoid overflow.
 pub(crate) mod scalar_value_ser_de {
     use std::{marker::PhantomData, str::FromStr};