Skip to content

Better Unsized Type support #797

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
Nadrieril merged 10 commits into from
Oct 1, 2025
Merged

Better Unsized Type support #797

Nadrieril merged 10 commits into from
Oct 1, 2025

Conversation

@ssyram
Copy link
Contributor

@ssyram ssyram commented Aug 4, 2025 •
edited by Nadrieril
Loading

Following #608 , this PR aims to provide the metadata explicitly when a reference / raw pointer is created. Specifically, a new field Operand is added to both Rvalue::Ref & Rvalue::RawPtr. It is () to correspond to the explicit None case of the PtrMetadata.

This also involves a rework on the data structure of PtrMetadata. Now, PtrMetadata::VTable refers directly to the virtual table struct generated. Also, a variant PtrMetadata::InheritFrom is added to handle the generic case.

A new type kind TyKind::PtrMetadata is added to serve as generic case placeholder. I.e., for types T<U : ?Sized> with U parametrized, use TyKind::PtrMetadata(U) to refer to the potential metadata type.

Besides, during translate_rvalue when translating the function bodies, as types are not yet fully translated, it is hard to get the metadata in place. So a placeholder () is inserted there and a new pass insert_ptr_metadata for Cleanup phase is added to compute the correct value.

Now the feature should work quite well except the potential bug of taking the metadata from the index / subslice projections.

ci: use AeneasVerif/aeneas#609
ci: use AeneasVerif/eurydice#288

@ssyram ssyram force-pushed the better-unsized-type branch 2 times, most recently from 5374cf5 to 4f619fc Compare August 4, 2025 10:11
@ssyram ssyram mentioned this pull request Aug 7, 2025
Closed
@ssyram ssyram force-pushed the better-unsized-type branch from bc8f83c to d7659ad Compare August 7, 2025 09:12
@ssyram ssyram marked this pull request as ready for review August 7, 2025 09:15
@ssyram ssyram force-pushed the better-unsized-type branch 2 times, most recently from e87cafe to 4a97f82 Compare August 8, 2025 10:25
@ssyram ssyram mentioned this pull request Aug 9, 2025
Merged
@ssyram ssyram force-pushed the better-unsized-type branch from cf228f8 to c52dbbc Compare August 25, 2025 05:51
@ssyram
Copy link
Contributor Author

ssyram commented Aug 25, 2025 •
edited
Loading

Previously, the metadata was wrongly fetched even when the access is not to the DST field (the last field). I.e., previously, in cases like accessing struct Dst<U : ?Sized> { foo : i32, dst : U } with &dst.foo, will still wrongly trigger fetching metadata from dst as that for foo. This is now fixed. But more errors come that: now, accessing the fields of opaque types will cause an error -- because we cannot tell whether we are taking the last field or not.

I newly added a pass for resolving the InheritFrom case. When the type var requires Sized, the ptr-metadata is resolve to PtrMetadata::None.

@ssyram ssyram force-pushed the better-unsized-type branch 2 times, most recently from 36a6776 to 5950145 Compare August 25, 2025 07:57
@Nadrieril
Copy link
Member

Nadrieril commented Sep 9, 2025

CI is failing, could you fix it before I have a look?

Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 9, 2025
View reviewed changes
@ssyram
Copy link
Contributor Author

ssyram commented Sep 14, 2025 •
edited
Loading

CI is failing, could you fix it before I have a look?

Yes, it is a known problem with the assoc-types.

@ssyram
Copy link
Contributor Author

ssyram commented Sep 14, 2025

OK, latest changes merged, but the results are the same: the support for assoc-types are required to let the overall process of fetching metadata go smoothly.

Nadrieril
Nadrieril reviewed Sep 15, 2025
View reviewed changes
@Nadrieril
Copy link
Member

Nadrieril commented Sep 15, 2025 •
edited
Loading

OK, latest changes merged, but the results are the same: the support for assoc-types are required to let the overall process of fetching metadata go smoothly.

What support do you need exactly? I haven't noticed anything related to associated types.

@ssyram
Copy link
Contributor Author

ssyram commented Sep 15, 2025

OK, with the newly merged support for assoc-types, now the remaining is some generic inconsistency. Will try to fix tomorrow.

@ssyram
Copy link
Contributor Author

ssyram commented Sep 16, 2025

CI should pass now. Originally, the vtable_ref was taken out with generics not properly substituted by the info in the existential type. Now, by the process taken from the vtable_dispatch_transform pass from #762 , the whole should pass the test. Now there is one missing part: the slice / index operation.

@Nadrieril Nadrieril marked this pull request as draft September 16, 2025 13:27
@Nadrieril
Copy link
Member

Nadrieril commented Sep 16, 2025

Marking the PR as draft for now, please mark it as ready once you've fixed the subslice things and CI passes.

@ssyram
Copy link
Contributor Author

ssyram commented Sep 17, 2025

OK, will try now.

@ssyram ssyram force-pushed the better-unsized-type branch from ce1fa9b to 1056c27 Compare September 17, 2025 13:49
@ssyram
Copy link
Contributor Author

ssyram commented Sep 17, 2025 •
edited
Loading

OK, done. Sorry for being late, it's the first time I do this.

@Nadrieril
Copy link
Member

Nadrieril commented Sep 17, 2025

Thanks! Could you do the eurydice update? It should be a tiny PR that just ignores the new field probably. I'll do aeneas.

@Nadrieril Nadrieril force-pushed the better-unsized-type branch 2 times, most recently from 62c638d to f3d2530 Compare September 17, 2025 14:25
@Nadrieril Nadrieril mentioned this pull request Sep 17, 2025
Merged
@ssyram
Copy link
Contributor Author

ssyram commented Sep 18, 2025 •
edited
Loading

OK, a very good news is that AeneasVerif/eurydice#259 is a perfect deploy of this PR in Eurydice, which, using the info of metadata, has restructured the whole support of DST in Eurydice. The latest change in that PR merged the latest version of the main official branch of Eurydice and has been tested to be fully compatible with this PR. Hopefully, @protz we can polish AeneasVerif/eurydice#259 to get fully ready next week and when @Nadrieril is back the week after next, we can merge both PR altogether!

@Nadrieril
Copy link
Member

Nadrieril commented Sep 29, 2025

This is proving tricky on the aeneas side, we're working on it.

@ssyram
Copy link
Contributor Author

ssyram commented Sep 29, 2025

OK, it seems that @protz is also working on the array PR, before the DST PR can get ready.

@Nadrieril Nadrieril force-pushed the better-unsized-type branch 2 times, most recently from 5e1851a to f3695c0 Compare September 30, 2025 09:45
@Nadrieril Nadrieril mentioned this pull request Sep 30, 2025
Closed
@Nadrieril Nadrieril force-pushed the better-unsized-type branch from f3695c0 to 7cf6388 Compare October 1, 2025 09:34
ssyram and others added 8 commits October 1, 2025 11:45
@ssyram @Nadrieril
Better unsized type
f9a646f 
* fixed ptr metadata

fixed PtrMetadata & its obtainment

* metadata type & fixation in index to function call

* fixed transform_constant_expr

* two todo for bug fix

* new pass to fix metadata obtainment

* fixed syntactic error in test

* fixed `translate_ptr_metadata` & doc test bug fixed

* fixed build for the merge

for `insert_ptr_metadata` & `simplify_constants`

* update Hax & ML gen & ML print fix

* version updated

* fixed `()` as ptr metadata

Now the ptr metadata will not introduce new `RawConstantExpr::Adt`

Also fixed for `simplify_constants`

* tests

* fixed get-metadata

* debug: no ptr-metadata for non-final field access

* pass for resolving sized ptr-metadata inheritance

Update insert_ptr_metadata.rs

* Update charon/src/bin/charon-driver/translate/translate_trait_objects.rs

Co-authored-by: Nadrieril <[email protected]>

* Update charon/src/bin/charon-driver/translate/translate_types.rs

Co-authored-by: Nadrieril <[email protected]>

* as advised

* some change

* more on merge

* changes as per advice

* per advice: from panic to TyErr

* bug fix: vtable reference generic error

* half fix of subslice operation

* fixed subslice ptr-metadata

* formatting

* version

* resolving PtrMetadata<T> for Sized<T>

including code revision as advised

---------

Co-authored-by: Nadrieril <[email protected]>
@Nadrieril
Use a global instead of a local for unit metadata
3a762d8
@Nadrieril
Hide unit metadata
3f9850e
@Nadrieril
Add test
6fc0d52
@Nadrieril
Consider every param to be sized when hiding marker traits
634cce3
@Nadrieril
Cleanup insert_ptr_metadata
8dca512
@Nadrieril
Make ptr metadata work like a field projection
609ded1 
This is important to give llbc clear semantics wrt references: we
previously had to copy a mutable reference in order to read its
metadata, but mutable references are importantly not copyable.
@Nadrieril
No longer need to introduce extra statements to compute metadata
eaa116a
@Nadrieril Nadrieril force-pushed the better-unsized-type branch from 7cf6388 to eaa116a Compare October 1, 2025 09:45
@Nadrieril Nadrieril enabled auto-merge October 1, 2025 10:02
@Nadrieril Nadrieril added this pull request to the merge queue Oct 1, 2025
Merged via the queue into AeneasVerif:main with commit 39bb864 Oct 1, 2025
13 of 14 checks passed
@Nadrieril Nadrieril mentioned this pull request Oct 17, 2025
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Nadrieril Nadrieril Nadrieril left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ssyram @Nadrieril