Skip to content

Bump rustc to remove ShallowInitBox#1033

Closed
N1ark wants to merge 4 commits into
AeneasVerif:mainfrom
soteria-tools:bump-rustc-boxes
Closed

Bump rustc to remove ShallowInitBox#1033
N1ark wants to merge 4 commits into
AeneasVerif:mainfrom
soteria-tools:bump-rustc-boxes

Conversation

@N1ark

@N1ark N1ark commented Feb 24, 2026

Copy link
Copy Markdown
Collaborator

Continuation of #1030
Fixes #973
Related to rust-lang/rust#148190

Added a transformation pass to make vec! safe. For the following original MIR:

((((*_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)

we want something akin to

_T = [move _5]
_3 = Box::write(move _4, move _T)
_B = unsize<Box<[T; N]>, Box<[T]>>(move _3)
vec_2 = std::slice::{impl}::into_vec(move _B)

ci: use AeneasVerif/aeneas#1033

@N1ark
N1ark force-pushed the bump-rustc-boxes branch from 23c1721 to f1141c7 Compare April 10, 2026 00:28
@N1ark
N1ark marked this pull request as ready for review April 10, 2026 12:24
@N1ark

N1ark commented Apr 10, 2026

Copy link
Copy Markdown
Collaborator Author

@Nadrieril ready for review :D
fyi i added builtin functions rather than actual function calls for Box::write and Box::into_vec, because by the time the pass runs the TyCtx is lost so we can't retrieve them. Either way I think it makes sense given the other builtin functions (cough cough BoxNew)

@N1ark
N1ark force-pushed the bump-rustc-boxes branch from 8b64f36 to af64464 Compare April 10, 2026 12:29
Comment thread charon/src/ast/expressions.rs
Comment thread charon/tests/ui/regressions/issue-1075-primty-def-id.out Outdated
@Nadrieril

Copy link
Copy Markdown
Member

(I really want to get rid of BoxNew, it's an artefact of a time long past ^^)

@N1ark
N1ark force-pushed the bump-rustc-boxes branch from cc5ca80 to a315830 Compare April 10, 2026 12:35
@N1ark

N1ark commented Apr 16, 2026

Copy link
Copy Markdown
Collaborator Author

@Nadrieril is it ok to leave this as is for now so we can keep bumping the toolchain, and we eventually get rid of all the builtin functions later? ill go through the issues for this PR dw; this is partly because @joshlf is opening a PR to have some sort of automatic toolchain bumper in CI (since often the toolchain bump doesn't cause any breakage)

@Nadrieril

Nadrieril commented Apr 17, 2026

Copy link
Copy Markdown
Member

yes do leave the builtins like this we can make it better later

@N1ark
N1ark force-pushed the bump-rustc-boxes branch 3 times, most recently from fc4adb2 to ea025e0 Compare May 13, 2026 08:21
@N1ark

N1ark commented May 13, 2026

Copy link
Copy Markdown
Collaborator Author

@Nadrieril rebased this on main; lmk if you want me to change anything

@Nadrieril

Copy link
Copy Markdown
Member

PR looks good! I was only waiting on the corresponding aeneas and eurydice changes :3

@N1ark
N1ark force-pushed the bump-rustc-boxes branch from ea025e0 to 49e78ea Compare May 13, 2026 11:00
@Nadrieril

Copy link
Copy Markdown
Member

Closing in favor of #1193

@Nadrieril Nadrieril closed this May 28, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Bug: Incorrect reconstruction of vec!

2 participants