Skip to content

Commit 171b81a

Browse files
Copilotssyram
andauthored
VTable Metadata pass: size, align & drop
Drop shims are correctly implemented with recursion to handle both Array & Tuple cases. * Initial plan * Initial analysis and planning for vtable metadata computation Co-authored-by: ssyram <[email protected]> * Initial analysis and plan for vtable metadata computation Co-authored-by: ssyram <[email protected]> * Implement basic drop case analysis in vtable metadata computation Co-authored-by: ssyram <[email protected]> * Improve drop case analysis with proper Drop trait detection Co-authored-by: ssyram <[email protected]> * Successfully implement null drop operands for types that don't need drop Co-authored-by: ssyram <[email protected]> * Refactor vtable metadata computation to use struct-based approach Co-authored-by: ssyram <[email protected]> * Changes before error encountered Co-authored-by: ssyram <[email protected]> * Changes before error encountered Co-authored-by: ssyram <[email protected]> * Improve drop shim generation with better structured naming and case distinction Co-authored-by: ssyram <[email protected]> * Implement actual drop shim function generation for vtable metadata Co-authored-by: ssyram <[email protected]> * Fix drop shim function generation with proper lifetime handling Co-authored-by: ssyram <[email protected]> * Implement proper dyn trait types and Concretize cast for drop shims Co-authored-by: ssyram <[email protected]> * Set drop shim functions as transparent for better naming display Co-authored-by: ssyram <[email protected]> * Implement generics handling for drop shim functions - first iteration Co-authored-by: ssyram <[email protected]> * Fix drop shim parameter types and implement proper dyn trait handling Co-authored-by: ssyram <[email protected]> * Implement generics handling for drop shim function references Co-authored-by: ssyram <[email protected]> * Refactor code organization and fix drop shim parameter types from pointers to references Co-authored-by: ssyram <[email protected]> * Fix generics handling with proper region variables and minimal generic parameters Co-authored-by: ssyram <[email protected]> * Complete vtable drop shim implementation with proper reference types and simplified generics Co-authored-by: ssyram <[email protected]> * re-implemented layout info * Delete vtables * minor adjust * Implement create_dyn_trait_param_type by extracting from drop field type and handle Unknown case Co-authored-by: ssyram <[email protected]> * fixd drop receiver * Add drop_glue field to TypeDecl for tracking drop implementations (#14) * Initial plan * Add drop_glue field to TypeDecl and implement translation logic Co-authored-by: ssyram <[email protected]> * Fix test case ordering after adding drop_glue field Co-authored-by: ssyram <[email protected]> * Fix panic in combine_span_iter when handling empty iterators Co-authored-by: ssyram <[email protected]> * new ml & no-enqueue --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: ssyram <[email protected]> Co-authored-by: ssyram <[email protected]> * types fixed * Implement proper generics handling for drop shim functions Co-authored-by: ssyram <[email protected]> * revised drop case * Implement comprehensive drop case analysis with array, tuple, and Box support Co-authored-by: ssyram <[email protected]> * minor * minor * Implement concretize casting for array, tuple, and Box drop shims Co-authored-by: ssyram <[email protected]> * Enhance drop shim generation with structured drop case analysis Co-authored-by: ssyram <[email protected]> * Implement tuple field access with projections for drop shims Co-authored-by: ssyram <[email protected]> * Complete comprehensive drop shim logic implementation with detailed case analysis Co-authored-by: ssyram <[email protected]> * Simplify and combine DropShimKind and DropCase enums, simplify Box handling Co-authored-by: ssyram <[email protected]> * fixed drop field * Implement complete tuple and array drop shim logic with CFG blocks and function calls Co-authored-by: ssyram <[email protected]> * Fix unused block_id assignment and add tuple/array drop test cases Co-authored-by: ssyram <[email protected]> * new example added * Complete Box drop shim generics fix with proper trait clauses Fix Box drop shim generics - provide T and A type parameters correctly Co-Authored-By: ssyram <[email protected]> * Revert "Complete Box drop shim generics fix with proper trait clauses" This reverts commit b889ebb. * Initial analysis and understanding of Box drop generics issue Co-authored-by: ssyram <[email protected]> * fixed the case * Initial analysis and planning for Box drop generics and region binder fixes Co-authored-by: ssyram <[email protected]> * Fix region binders and partial Box generics handling Co-authored-by: ssyram <[email protected]> * Changes before error encountered Co-authored-by: ssyram <[email protected]> * Fix compilation errors and add missing Box detection methods Co-authored-by: ssyram <[email protected]> * Major progress on Box generics extraction and region variable fixes Co-authored-by: ssyram <[email protected]> * Initial analysis and planning for Box drop generics and region binder fixes Fix compilation errors and add missing Box detection methods Changes before error encountered Fix region binders and partial Box generics handling Co-Authored-By: ssyram <[email protected]> * Revert "Initial analysis and planning for Box drop generics and region binder fixes" This reverts commit 2802a90. * Revert "Merge branch 'copilot/fix-95d3f204-c7e2-4956-8a71-c4a3988443ca' of https://github.com/ssyram/charon into copilot/fix-95d3f204-c7e2-4956-8a71-c4a3988443ca" This reverts commit 048ec8f, reversing changes made to eb84c07. * name & generic some fix * Implement region binder fix and Box built-in detection for drop shim generation Co-authored-by: ssyram <[email protected]> * Fix generics mismatch and improve Box built-in detection for drop shims Co-authored-by: ssyram <[email protected]> * fixed test region mismatch * Fix tuple drop shim generation to create proper field-by-field drop logic Co-authored-by: ssyram <[email protected]> * Complete array and tuple drop shim implementation with proper traversal logic Co-authored-by: ssyram <[email protected]> * init-reform * Refactor drop shim generation with proper constant expressions and utility methods - Use `new_var()` and `place_for_var()` utilities instead of manual local creation - Use `ConstantExpr` directly instead of casting to primitive types - Fix scoping issues with concrete place by using `clone()` in loops - Clean up code organization and use `return_place()` utility - Remove unused variables to eliminate warnings - All vtables tests now pass Co-authored-by: ssyram <[email protected]> * Fix array drop shim counter types to match array length expression type Co-authored-by: ssyram <[email protected]> * example changed * Implement comprehensive drop shim generation with proper array/tuple traversal and drop calls Co-authored-by: ssyram <[email protected]> * Fix Vec<T> drop detection by bypassing needs_drop for ADT types Co-authored-by: ssyram <[email protected]> * Fix recursive drop case analysis to handle primitive types correctly Co-authored-by: ssyram <[email protected]> * Simplify analyze_drop_case and fix projection issues in drop shim generation Co-authored-by: ssyram <[email protected]> * fixed box issue & new box example * Extract helper structures and simplify constant creation Co-authored-by: ssyram <[email protected]> * Refactor analyze_drop_case into smaller focused functions and organize code sections Co-authored-by: ssyram <[email protected]> * Clean up verbose comments, remove unused code, and simplify function structure Co-authored-by: ssyram <[email protected]> * new example * more cleanup * new framework * debug done with new complex example --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: ssyram <[email protected]> Co-authored-by: ssyram <[email protected]>
1 parent 4d92302 commit 171b81a

File tree

105 files changed

+7241
-476
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

105 files changed

+7241
-476
lines changed

charon-ml/src/PrintTypes.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -335,8 +335,8 @@ and trait_ref_to_string (env : 'a fmt_env) (tr : trait_ref) : string =
335335
"dyn(" ^ trait ^ ")"
336336
| UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
337337

338-
and trait_instance_id_to_string (env : 'a fmt_env)
339-
(id : trait_instance_id) : string =
338+
and trait_instance_id_to_string (env : 'a fmt_env) (id : trait_instance_id) :
339+
string =
340340
match id with
341341
| Self -> "Self"
342342
| TraitImpl impl_ref -> trait_impl_ref_to_string env impl_ref

charon-ml/src/generated/Generated_GAstOfJson.ml

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1840,6 +1840,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
18401840
("kind", kind);
18411841
("layout", layout);
18421842
("ptr_metadata", ptr_metadata);
1843+
("drop_glue", drop_glue);
18431844
] ->
18441845
let* def_id = type_decl_id_of_json ctx def_id in
18451846
let* item_meta = item_meta_of_json ctx item_meta in
@@ -1850,8 +1851,18 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
18501851
let* ptr_metadata =
18511852
option_of_json ptr_metadata_of_json ctx ptr_metadata
18521853
in
1854+
let* drop_glue = option_of_json trait_impl_ref_of_json ctx drop_glue in
18531855
Ok
1854-
({ def_id; item_meta; generics; src; kind; layout; ptr_metadata }
1856+
({
1857+
def_id;
1858+
item_meta;
1859+
generics;
1860+
src;
1861+
kind;
1862+
layout;
1863+
ptr_metadata;
1864+
drop_glue;
1865+
}
18551866
: type_decl)
18561867
| _ -> Error "")
18571868

charon-ml/src/generated/Generated_Types.ml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -866,6 +866,9 @@ and type_decl = {
866866
are unable to obtain the info. See
867867
[translate_types::{impl ItemTransCtx}::translate_ptr_metadata] for
868868
more details. *)
869+
drop_glue : trait_impl_ref option;
870+
(** The drop implementation for this type, if any. This is [Some] if and
871+
only if the given type has a drop implementation. *)
869872
}
870873

871874
and type_decl_kind =

charon/src/ast/expressions_utils.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,4 +240,11 @@ impl Operand {
240240
Operand::Const(c) => &c.ty,
241241
}
242242
}
243+
244+
pub fn opaque(msg: String, ty: Ty) -> Self {
245+
Operand::Const(Box::new(ConstantExpr {
246+
value: RawConstantExpr::Opaque(msg),
247+
ty,
248+
}))
249+
}
243250
}

charon/src/ast/krate.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,11 @@ impl TryFrom<AnyTransId> for FunId {
8585
Ok(FunId::Regular(x.try_into()?))
8686
}
8787
}
88+
impl From<TypeDeclId> for TypeId {
89+
fn from(x: TypeDeclId) -> Self {
90+
TypeId::Adt(x)
91+
}
92+
}
8893

8994
/// A reference to a translated item.
9095
#[derive(

charon/src/ast/meta_utils.rs

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,8 +120,14 @@ pub fn combine_span(m0: &Span, m1: &Span) -> Span {
120120

121121
/// Combine all the span information in a slice.
122122
pub fn combine_span_iter<'a, T: Iterator<Item = &'a Span>>(mut ms: T) -> Span {
123-
// The iterator should have a next element
124-
let mut mc: Span = *ms.next().unwrap();
123+
// Handle the case where the iterator might be empty
124+
let mut mc: Span = match ms.next() {
125+
Some(span) => *span,
126+
None => {
127+
// Return a dummy span if the iterator is empty
128+
return Span::dummy();
129+
}
130+
};
125131
for m in ms {
126132
mc = combine_span(&mc, m);
127133
}

charon/src/ast/types.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -457,6 +457,9 @@ pub struct TypeDecl {
457457
/// but due to some limitation to be fixed, we are unable to obtain the info.
458458
/// See `translate_types::{impl ItemTransCtx}::translate_ptr_metadata` for more details.
459459
pub ptr_metadata: Option<PtrMetadata>,
460+
/// The drop implementation for this type, if any.
461+
/// This is `Some` if and only if the given type has a drop implementation.
462+
pub drop_glue: Option<TraitImplRef>,
460463
}
461464

462465
generate_index_type!(VariantId, "Variant");
@@ -763,6 +766,11 @@ impl Ty {
763766
pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
764767
self.0.with_inner_mut(f)
765768
}
769+
770+
/// Returns `usize` type.
771+
pub fn mk_usize() -> Ty {
772+
Ty::new(TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)))
773+
}
766774
}
767775

768776
impl<'s, V: Visit<'s, TyKind>> Drive<'s, V> for Ty {

charon/src/ast/types_utils.rs

Lines changed: 213 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
//! This file groups everything which is linked to implementations about [crate::types]
22
use crate::ast::*;
3+
use crate::formatter::IntoFormatter;
34
use crate::ids::Vector;
5+
use crate::pretty::FmtWithCtx;
46
use derive_generic_visitor::*;
57
use std::collections::HashSet;
68
use std::convert::Infallible;
@@ -597,6 +599,211 @@ impl Ty {
597599
}
598600
}
599601

602+
pub fn needs_drop(&self, translated: &TranslatedCrate) -> Result<bool, String> {
603+
match self.kind() {
604+
TyKind::Adt(type_decl_ref) => match type_decl_ref.id {
605+
TypeId::Adt(type_decl_id) => {
606+
let type_decl = translated.type_decls.get(type_decl_id).ok_or_else(|| {
607+
format!(
608+
"Type declaration for {} not found",
609+
type_decl_id.with_ctx(&translated.into_fmt())
610+
)
611+
})?;
612+
Ok(type_decl.drop_glue.is_some())
613+
}
614+
TypeId::Tuple => {
615+
let tuple_generics = &type_decl_ref.generics.types;
616+
// A tuple needs drop if any of its elements need drop
617+
for element_ty in tuple_generics.iter() {
618+
if element_ty.needs_drop(translated)? {
619+
return Ok(true);
620+
}
621+
}
622+
Ok(false)
623+
}
624+
TypeId::Builtin(builtin_ty) => match builtin_ty {
625+
BuiltinTy::Box => Ok(true), // Box always needs drop
626+
BuiltinTy::Array => {
627+
let element_ty = &type_decl_ref.generics.types[0];
628+
element_ty.needs_drop(translated)
629+
}
630+
BuiltinTy::Str | BuiltinTy::Slice => Ok(false), // str & [T] does not need drop
631+
},
632+
},
633+
TyKind::DynTrait(..) => Ok(false),
634+
TyKind::Literal(..) => Ok(false), // Literal types do not need drop
635+
TyKind::Ref(..) | TyKind::RawPtr(..) => Ok(false), // References and raw pointers do not need drop
636+
TyKind::FnPtr(..) => Ok(false), // Function pointers do not need drop
637+
TyKind::FnDef(..) => Ok(false), // Function definitions do not need drop
638+
TyKind::TraitType(..) | TyKind::TypeVar(..) | TyKind::Never | TyKind::Error(_) => {
639+
Err(format!(
640+
"Cannot determine if type {} needs drop",
641+
self.with_ctx(&translated.into_fmt())
642+
))
643+
}
644+
}
645+
}
646+
647+
/// Returns either the layout of this type, or a string with the reason why we couldn't compute it.
648+
pub fn layout(&self, translated: &TranslatedCrate) -> Result<Layout, String> {
649+
match self.kind() {
650+
TyKind::Adt(type_decl_ref) => {
651+
match &type_decl_ref.id {
652+
TypeId::Adt(type_decl_id) => {
653+
let type_decl =
654+
translated.type_decls.get(*type_decl_id).ok_or_else(|| {
655+
format!(
656+
"Type declaration for {} not found",
657+
type_decl_id.with_ctx(&translated.into_fmt())
658+
)
659+
})?;
660+
let layout = type_decl
661+
.layout
662+
.as_ref()
663+
.ok_or("Layout not available for ADT")?;
664+
Ok(layout.clone())
665+
}
666+
TypeId::Tuple => {
667+
// Get the tuple element types from generics
668+
let element_types = &type_decl_ref.generics.types;
669+
// Compute layout for tuple elements
670+
let mut total_size: Option<u64> = Some(0);
671+
let mut max_align: Option<u64> = Some(1);
672+
let mut is_uninhabited = false;
673+
674+
for element_ty in element_types.iter() {
675+
let element_layout = element_ty.layout(translated)?;
676+
if element_layout.uninhabited {
677+
is_uninhabited = true;
678+
}
679+
680+
match (
681+
total_size,
682+
element_layout.size,
683+
element_layout.align,
684+
max_align,
685+
) {
686+
(
687+
Some(current_size),
688+
Some(elem_size),
689+
Some(elem_align),
690+
Some(current_max_align),
691+
) => {
692+
// Apply alignment padding
693+
let aligned_size =
694+
(current_size + elem_align - 1) / elem_align * elem_align;
695+
total_size = Some(aligned_size + elem_size);
696+
max_align = Some(current_max_align.max(elem_align));
697+
}
698+
_ => {
699+
// If any size or alignment is None, the final result is None
700+
total_size = None;
701+
max_align = None;
702+
}
703+
}
704+
}
705+
706+
if is_uninhabited {
707+
// If any element is uninhabited, the whole tuple is uninhabited
708+
return Ok(Layout {
709+
size: Some(0),
710+
align: max_align.or(Some(1)), // Ensure at least 1-byte alignment
711+
uninhabited: true,
712+
variant_layouts: Vector::new(),
713+
discriminant_layout: None,
714+
});
715+
}
716+
717+
// Final padding to struct alignment
718+
let final_size = match (total_size, max_align) {
719+
(Some(size), Some(align)) => Some((size + align - 1) / align * align),
720+
_ => None,
721+
};
722+
723+
Ok(Layout {
724+
size: final_size,
725+
align: max_align,
726+
uninhabited: is_uninhabited,
727+
variant_layouts: Vector::new(),
728+
discriminant_layout: None,
729+
})
730+
}
731+
TypeId::Builtin(builtin_ty) => {
732+
match builtin_ty {
733+
BuiltinTy::Box => Err("TODO: handle Box with ptr-metadata".to_string()),
734+
BuiltinTy::Array => {
735+
// Array layout: element_type repeated const_generics[0] times
736+
let element_ty = &type_decl_ref.generics.types[0];
737+
let element_layout = element_ty.layout(translated)?;
738+
739+
if element_layout.uninhabited {
740+
return Ok(Layout {
741+
size: Some(0),
742+
align: element_layout.align,
743+
uninhabited: true,
744+
variant_layouts: Vector::new(),
745+
discriminant_layout: None,
746+
});
747+
}
748+
749+
let cg = type_decl_ref
750+
.generics
751+
.const_generics
752+
.get(ConstGenericVarId::ZERO)
753+
.unwrap();
754+
let ConstGeneric::Value(Literal::Scalar(scalar)) = cg else {
755+
return Err(format!(
756+
"No instant available const generic value or wrong format value: {}",
757+
cg.with_ctx(&translated.into_fmt())
758+
));
759+
};
760+
let len = scalar.as_uint().or_else(|e| {
761+
Err(format!("Failed to get array length: {:?}", e))
762+
})?;
763+
764+
let element_size = element_layout.size;
765+
let align = element_layout.align;
766+
767+
let size = element_size.map(|s| s * (len as u64));
768+
769+
Ok(Layout {
770+
size,
771+
align,
772+
uninhabited: false,
773+
variant_layouts: Vector::new(),
774+
discriminant_layout: None,
775+
})
776+
}
777+
BuiltinTy::Slice | BuiltinTy::Str => {
778+
Err("DST does not have layout".to_string())
779+
}
780+
}
781+
}
782+
}
783+
}
784+
TyKind::Literal(lit_ty) => {
785+
// For literal types, create a simple scalar layout
786+
let size =
787+
lit_ty.target_size(translated.target_information.target_pointer_size) as u64;
788+
Ok(Layout {
789+
size: Some(size),
790+
align: Some(size), // Scalar types are self-aligned
791+
uninhabited: false,
792+
variant_layouts: Vector::new(),
793+
discriminant_layout: None,
794+
})
795+
}
796+
TyKind::RawPtr(_, _) | TyKind::Ref(_, _, _) => {
797+
Err("TODO: handle pointer/reference with ptr-metadata".to_string())
798+
}
799+
TyKind::TypeVar(_) => Err("No layout due to generic".to_string()),
800+
_ => Err(format!(
801+
"Don't know how to compute layout for type {}",
802+
self.with_ctx(&translated.into_fmt())
803+
)),
804+
}
805+
}
806+
600807
/// Substitue the given `target_ty` with the `replacement` type recursively in this type.
601808
/// E.g., if `self` is `Vec<i32>`, `target_ty` is `i32` and `replacement` is `Vec<i32>`, then
602809
/// `self` will become `Vec<Vec<i32>>`.
@@ -711,6 +918,12 @@ impl TypeDeclRef {
711918
}
712919
}
713920

921+
impl From<LiteralTy> for Ty {
922+
fn from(lit: LiteralTy) -> Ty {
923+
TyKind::Literal(lit).into_ty()
924+
}
925+
}
926+
714927
impl TraitDeclRef {
715928
pub fn self_ty<'a>(&'a self, krate: &'a TranslatedCrate) -> Option<&'a Ty> {
716929
match self.generics.types.iter().next() {

charon/src/ast/values_utils.rs

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
//! Implementations for [crate::values]
2+
use core::panic;
3+
24
use crate::ast::*;
35

46
#[derive(Debug, Clone)]
@@ -207,6 +209,32 @@ impl ScalarValue {
207209
}
208210
}
209211

212+
impl From<Literal> for ConstantExpr {
213+
fn from(lit: Literal) -> Self {
214+
let ty = match &lit {
215+
Literal::Scalar(scalar) => match scalar {
216+
ScalarValue::Signed(int_ty, _) => {
217+
TyKind::Literal(LiteralTy::Int(*int_ty)).into_ty()
218+
}
219+
ScalarValue::Unsigned(uint_ty, _) => {
220+
TyKind::Literal(LiteralTy::UInt(*uint_ty)).into_ty()
221+
}
222+
},
223+
Literal::Float(float) => TyKind::Literal(LiteralTy::Float(float.ty)).into_ty(),
224+
Literal::Bool(_) => TyKind::Literal(LiteralTy::Bool).into_ty(),
225+
Literal::Char(_) => TyKind::Literal(LiteralTy::Char).into_ty(),
226+
_ => panic!(
227+
"Only scalar literals can be converted to ConstantExpr, got {:?}",
228+
lit
229+
),
230+
};
231+
ConstantExpr {
232+
value: RawConstantExpr::Literal(lit),
233+
ty,
234+
}
235+
}
236+
}
237+
210238
/// Custom serializer that stores 128 bit integers as strings to avoid overflow.
211239
pub(crate) mod scalar_value_ser_de {
212240
use std::{marker::PhantomData, str::FromStr};

0 commit comments

Comments
 (0)