Skip to content

Commit 3a2b368

Browse files
N1arkN1ark
committed
Distinguish unsizes: VTableDirect/VTableNested 
1 parent d5860e4 commit 3a2b368

22 files changed

+385
-868
lines changed

‎charon-ml/src/generated/Generated_Expressions.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -377,7 +377,8 @@ and unop =
377377

378378
and unsizing_metadata =
379379
| MetaLength of const_generic
380-
| MetaVTablePtr of trait_ref
380+
| MetaVTableDirect of trait_ref * global_decl_ref option
381+
| MetaVTableNested of trait_ref * field_id option
381382
| MetaUnknown
382383
[@@deriving
383384
show,

‎charon-ml/src/generated/Generated_GAstOfJson.ml‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2158,9 +2158,14 @@ and unsizing_metadata_of_json (ctx : of_json_ctx) (js : json) :
21582158
| `Assoc [ ("Length", length) ] ->
21592159
let* length = const_generic_of_json ctx length in
21602160
Ok (MetaLength length)
2161-
| `Assoc [ ("VTablePtr", v_table_ptr) ] ->
2162-
let* v_table_ptr = trait_ref_of_json ctx v_table_ptr in
2163-
Ok (MetaVTablePtr v_table_ptr)
2161+
| `Assoc [ ("VTableDirect", `List [ x_0; x_1 ]) ] ->
2162+
let* x_0 = trait_ref_of_json ctx x_0 in
2163+
let* x_1 = option_of_json global_decl_ref_of_json ctx x_1 in
2164+
Ok (MetaVTableDirect (x_0, x_1))
2165+
| `Assoc [ ("VTableNested", `List [ x_0; x_1 ]) ] ->
2166+
let* x_0 = trait_ref_of_json ctx x_0 in
2167+
let* x_1 = option_of_json field_id_of_json ctx x_1 in
2168+
Ok (MetaVTableNested (x_0, x_1))
21642169
| `String "Unknown" -> Ok MetaUnknown
21652170
| _ -> Error "")
21662171

‎charon/Cargo.lock‎

Lines changed: 3 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎charon/Cargo.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ ustr = { version = "1.1.0", features = ["serde"] }
8787
wait-timeout = { version = "0.2.0", optional = true }
8888
which = "7.0"
8989

90-
hax = { package = "hax-frontend-exporter", git = "https://github.com/AeneasVerif/hax", branch = "main", optional = true }
90+
hax = { package = "hax-frontend-exporter", git = "https://github.com/N1ark/hax", branch = "vtables", optional = true }
9191
# hax = { package = "hax-frontend-exporter", path = "../../hax/frontend/exporter", optional = true }
9292
macros = { path = "./macros" }
9393

‎charon/src/ast/expressions.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,8 @@ pub enum CastKind {
222222
#[charon::variants_prefix("Meta")]
223223
pub enum UnsizingMetadata {
224224
Length(ConstGeneric),
225-
VTablePtr(TraitRef),
225+
VTableDirect(TraitRef, Option<GlobalDeclRef>),
226+
VTableNested(Binder<TraitRef>, Vec<FieldId>),
226227
Unknown,
227228
}
228229

‎charon/src/bin/charon-driver/translate/translate_bodies.rs‎

Lines changed: 99 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ use std::ops::Deref;
1010
use std::ops::DerefMut;
1111
use std::panic;
1212

13+
use crate::translate::translate_generics::BindingLevel;
14+
1315
use super::translate_crate::*;
1416
use super::translate_ctx::*;
1517
use charon_lib::ast::ullbc_ast::StatementKind;
@@ -508,6 +510,7 @@ impl BodyTransCtx<'_, '_, '_> {
508510
let tgt_ty = self.translate_ty(span, tgt_ty)?;
509511

510512
// Translate the operand
513+
let src_hax_ty = hax_operand.ty();
511514
let mut operand = self.translate_operand(span, hax_operand)?;
512515
let src_ty = operand.ty().clone();
513516

@@ -566,28 +569,118 @@ impl BodyTransCtx<'_, '_, '_> {
566569
self.translate_constant_expr_to_const_generic(span, len)?;
567570
UnsizingMetadata::Length(len)
568571
}
569-
hax::UnsizingMetadata::VTablePtr(impl_expr) => {
572+
hax::UnsizingMetadata::DirectVTable(impl_expr) => {
570573
let tref = self.translate_trait_impl_expr(span, impl_expr)?;
571-
match &impl_expr.r#impl {
574+
let vtable = match &impl_expr.r#impl {
572575
hax::ImplExprAtom::Concrete(tref) => {
573576
// Ensure the vtable type is translated.
574-
let _: GlobalDeclId = self.register_item(
577+
Some(self.translate_item(
575578
span,
576579
tref,
577580
TransItemSourceKind::VTableInstance(
578581
TraitImplSource::Normal,
579582
),
580-
);
583+
)?)
581584
}
582585
// TODO(dyn): more ways of registering vtable instance?
583586
_ => {
584587
trace!(
585588
"impl_expr not triggering registering vtable: {:?}",
586589
impl_expr
587-
)
590+
);
591+
None
592+
}
593+
};
594+
UnsizingMetadata::VTableDirect(tref, vtable)
595+
}
596+
hax::UnsizingMetadata::NestedVTable(impl_expr) => {
597+
let (hax::TyKind::Ref(_, src_hax_ty, _)
598+
| hax::TyKind::RawPtr(src_hax_ty, _)) = src_hax_ty.kind()
599+
else {
600+
raise_error!(
601+
self,
602+
span,
603+
"Nested vtable unsizing only supported for ref types, got {:?}",
604+
src_hax_ty
605+
);
606+
};
607+
let hax::TyKind::Dynamic(self_ty, preds, region) =
608+
src_hax_ty.kind()
609+
else {
610+
raise_error!(
611+
self,
612+
span,
613+
"Nested vtable unsizing only supported for dyn traits, got {:?}",
614+
src_hax_ty
615+
);
616+
};
617+
618+
// Add a binder that contains the existentially quantified type.
619+
self.binding_levels.push(BindingLevel::new(true));
620+
621+
// Add the existentially quantified type.
622+
let ty_id = self
623+
.innermost_binder_mut()
624+
.push_type_var(self_ty.index, self_ty.name.clone());
625+
let ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(ty_id)).into_ty();
626+
627+
let region = self.translate_region(span, region)?;
628+
self.innermost_binder_mut().params.types_outlive.push(
629+
RegionBinder::empty(OutlivesPred(ty.clone(), region.clone())),
630+
);
631+
self.register_predicates(preds, PredicateOrigin::Dyn)?;
632+
633+
let tref = self.translate_trait_impl_expr(span, impl_expr)?;
634+
let params = self.binding_levels.pop().unwrap().params;
635+
let binder = Binder {
636+
params: params,
637+
skip_binder: tref,
638+
kind: BinderKind::Dyn,
639+
};
640+
641+
let hax::ImplExprAtom::LocalBound { index, path, .. } =
642+
&impl_expr.r#impl
643+
else {
644+
raise_error!(
645+
self,
646+
span,
647+
"Unexpected impl expr in NestedVTable unsizing metadata"
648+
);
649+
};
650+
651+
let fields = if *index != 0 {
652+
let mut fields = Vec::new();
653+
for segment in path {
654+
let hax::ImplExprPathChunk::Parent {
655+
predicate, index, ..
656+
} = segment
657+
else {
658+
raise_error!(
659+
self,
660+
span,
661+
"Unexpected path segment in NestedVTable unsizing metadata"
662+
);
663+
};
664+
let vtable =
665+
self.vtable_for_itemref(&predicate.value.trait_ref)?;
666+
let index = TraitClauseId::new(*index);
667+
let Some(Some(field)) = vtable.clauses.get(index) else {
668+
raise_error!(
669+
self,
670+
span,
671+
"VTable missing field {} for predicate {:?}",
672+
index,
673+
predicate.value.trait_ref
674+
);
675+
};
676+
fields.push(*field);
588677
}
678+
fields
679+
} else {
680+
vec![]
589681
};
590-
UnsizingMetadata::VTablePtr(tref)
682+
683+
UnsizingMetadata::VTableNested(binder, fields)
591684
}
592685
hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown,
593686
};

‎charon/src/bin/charon-driver/translate/translate_trait_objects.rs‎

Lines changed: 36 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -148,14 +148,19 @@ impl ItemTransCtx<'_, '_> {
148148
}
149149
}
150150

151-
enum VTableField {
151+
pub enum VTableField {
152152
Size,
153153
Align,
154154
Drop,
155155
Method(hax::DefId, hax::Binder<hax::TyFnSig>),
156156
SuperTrait(hax::Clause),
157157
}
158158

159+
pub struct VTableData {
160+
pub fields: Vec<VTableField>,
161+
pub clauses: Vector<TraitClauseId, Option<FieldId>>,
162+
}
163+
159164
//// Generate the vtable struct.
160165
impl ItemTransCtx<'_, '_> {
161166
/// Query whether a trait is dyn compatible.
@@ -239,11 +244,11 @@ impl ItemTransCtx<'_, '_> {
239244
Ok(Some(vtable_ref))
240245
}
241246

242-
fn vtable_fields(
247+
fn vtable_data(
243248
&mut self,
244249
trait_def: &hax::FullDef,
245250
implied_predicates: &hax::GenericPredicates,
246-
) -> Result<Vec<VTableField>, Error> {
251+
) -> Result<VTableData, Error> {
247252
let mut fields = vec![];
248253
// Basic fields.
249254
fields.push(VTableField::Size);
@@ -271,17 +276,21 @@ impl ItemTransCtx<'_, '_> {
271276
}
272277

273278
// Supertrait fields.
274-
for (clause, _span) in &implied_predicates.predicates {
275-
if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() {
276-
// If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
277-
if !self.pred_is_for_self(&pred.trait_ref) {
278-
continue;
279-
}
279+
let mut clauses = Vector::new();
280+
for (i, (clause, _span)) in implied_predicates.predicates.iter().enumerate() {
281+
let trait_clause_id = TraitClauseId::new(i);
282+
// If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
283+
if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref()
284+
&& self.pred_is_for_self(&pred.trait_ref)
285+
{
286+
clauses.set_slot(trait_clause_id, Some(FieldId::new(fields.len())));
280287
fields.push(VTableField::SuperTrait(clause.clone()));
288+
} else {
289+
clauses.set_slot(trait_clause_id, None);
281290
}
282291
}
283292

284-
Ok(fields)
293+
Ok(VTableData { fields, clauses })
285294
}
286295

287296
fn gen_vtable_struct_fields(
@@ -293,9 +302,9 @@ impl ItemTransCtx<'_, '_> {
293302
let mut fields = Vector::new();
294303
let mut supertrait_counter = (0..).into_iter();
295304

296-
let fields_list = self.vtable_fields(trait_def, implied_predicates)?;
305+
let vtable = self.vtable_data(trait_def, implied_predicates)?;
297306

298-
for field in fields_list.into_iter() {
307+
for field in vtable.fields.into_iter() {
299308
let (name, ty) = match field {
300309
VTableField::Size => ("size".into(), usize_ty()),
301310
VTableField::Align => ("align".into(), usize_ty()),
@@ -347,6 +356,21 @@ impl ItemTransCtx<'_, '_> {
347356
Ok(fields)
348357
}
349358

359+
pub fn vtable_for_itemref(&mut self, tref: &hax::ItemRef) -> Result<VTableData, Error> {
360+
let trait_def = self.hax_def(tref)?;
361+
362+
let (hax::FullDefKind::Trait {
363+
implied_predicates, ..
364+
}
365+
| hax::FullDefKind::TraitAlias {
366+
implied_predicates, ..
367+
}) = trait_def.kind()
368+
else {
369+
unreachable!("Non-trait passed to `field_for_vtable_supertrait`")
370+
};
371+
self.vtable_data(&*trait_def, implied_predicates)
372+
}
373+
350374
/// This is a temporary check until we support `dyn Trait` with `--monomorphize`.
351375
pub(crate) fn check_no_monomorphize(&self, span: Span) -> Result<(), Error> {
352376
if self.monomorphize() {

‎charon/src/pretty/fmt_with_ctx.rs‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -292,7 +292,19 @@ impl<C: AstFormatter> FmtWithCtx<C> for CastKind {
292292
)?;
293293
match meta {
294294
UnsizingMetadata::Length(len) => write!(f, ", {}", len.with_ctx(ctx))?,
295-
UnsizingMetadata::VTablePtr(tref) => write!(f, ", {}", tref.with_ctx(ctx))?,
295+
UnsizingMetadata::VTableDirect(tref, vt) => {
296+
write!(f, ", {} with ", tref.with_ctx(ctx))?;
297+
match vt {
298+
Some(vt) => write!(f, "{}", vt.with_ctx(ctx))?,
299+
None => write!(f, "?")?,
300+
}
301+
}
302+
UnsizingMetadata::VTableNested(tref, fields) => {
303+
write!(f, ", ")?;
304+
tref.fmt_split_with(ctx, |ctx, tref| format!("{}", tref.with_ctx(ctx)));
305+
let fields = fields.iter().map(|x| format!("{}", x.index())).format(", ");
306+
write!(f, " at [{}]", fields)?
307+
}
296308
UnsizingMetadata::Unknown => {}
297309
}
298310
write!(f, ">")

‎charon/tests/ptr-metadata.json‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,6 @@
3030
"test_crate::GenericBehindIndirection": "None",
3131
"test_crate::GenericBehindIndirectionUnsized": "None",
3232
"test_crate::ThinGeneric": "None",
33-
"test_crate::Showable::{vtable}": "None",
34-
"core::marker::MetaSized::{vtable}": "None",
3533
"alloc::alloc::Global": "None",
3634
"core::cmp::Ordering": "None",
3735
"core::option::Option": "None",

0 commit comments

Comments
 (0)