Merged
Conversation
N1ark
commented
Feb 22, 2026
N1ark
force-pushed
the
bump-rustc
branch
3 times, most recently
from
b097f0b to
fc0282b
Compare
N1ark
force-pushed
the
bump-rustc
branch
2 times, most recently
from
cc0694d to
8669dde
Compare
Nadrieril
reviewed
Feb 23, 2026
Nadrieril
reviewed
Feb 23, 2026
Nadrieril
reviewed
Feb 23, 2026
N1ark
force-pushed
the
bump-rustc
branch
5 times, most recently
from
85f201f to
5ef2cea
Compare
Nadrieril
reviewed
Feb 23, 2026
Comment on lines
143
to
148
| ((((*_4)).1).0).0 = [move _5] | ||
| storage_dead(_5) | ||
| _3 = move _4 | ||
| conditional_drop[{impl Destruct for alloc::boxed::Box<T>[@TraitClause0, @TraitClause1]}<MaybeUninit<[u8; 1 : usize]>[{built_in impl Sized for [u8; 1 : usize]}], Global>[{built_in impl MetaSized for MaybeUninit<[u8; 1 : usize]>[{built_in impl Sized for [u8; 1 : usize]}]}, {built_in impl Sized for Global}]] _4 | ||
| storage_dead(_4) | ||
| vec_2 = box_assume_init_into_vec_unsafe<u8, 1 : usize>[{built_in impl Sized for u8}](move _3) |
Member
There was a problem hiding this comment.
It's important that vec![] expands to safe code that aeneas can translate. So we'll still need a reconstruction pass, hopefully much simpler now. The only difference is that we should use Box::<MaybeUninit<_>>::write instead of writing by hand then calling box_assume_init_into_vec_unsafe.
Contributor
Author
There was a problem hiding this comment.
this will be left for a separate PR; to have it written down somewhere:
the goal is to have a reconstruction of the following form (assuming the shape above):
_T = [move _5]
_3 = Box::write(move _4, move _T)
_B = unsize<Box<[T; N]>, Box<[T]>> _3
vec_2 = (((((*_B)).1).0).0).into_vec()
Nadrieril
reviewed
Feb 23, 2026
Nadrieril
reviewed
Feb 23, 2026
N1ark
force-pushed
the
bump-rustc
branch
2 times, most recently
from
dad517e to
40bff4f
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In smaller bits, ordered chronologically
Slight change to filename parsing
Overhaul filename handling for cross-compiler consistency rust-lang/rust#149709
Slightly change due to a change to
TyCtx::destructure_constrefactor
destructure_construst-lang/rust#150411Remove the runtime check
NullOps, addOperand::RuntimeCheckReplace Rvalue::NullaryOp by a variant in mir::Operand. rust-lang/rust#148766
Manually ignore
Destructparent traits fordyn TraitReplace
#[rustc_do_not_implement_via_object]with#[rustc_dyn_incompatible_trait]rust-lang/rust#148637Tweaked
get_mir, now thatis_ctfe_mir_availableis gone; amusingly i think this change means more functions are now translated (e.g. see the diff forslice-index-range.out, wherecore::slice::index::slice_index_fail::do_panic#3::runtime's body is not missing anymore)Couple of cleanups and optimizations around MIR encoding rust-lang/rust#152096
Removetransform/resugar/reconstruct_boxes.rs, thanks to theBox::newandvec!rework (see below)replace box_new with lower-level intrinsics rust-lang/rust#148190
After discussion this last bump is kept for a separate PR as it also involves changes to the transformation pass to reconstruct the
vec!into something safeThe main thing i need some attention for in the review is the change in
translate-traits, to ignoreDestruct: if you have a better fix for it let me knowci: use AeneasVerif/aeneas#796
ci: use AeneasVerif/eurydice#381