search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
306 stars 40 forks source link

Unsound transmute between `&Predecessors` #127

Closed shinmao closed 1 year ago

shinmao commented 1 year ago

https://github.com/digama0/mm0/blob/98496badaf6464e56ed7b4204e7d54b85667cb01/mm0-rs/components/mmcc/src/types/mir.rs#L966-L974 The unsound transmute lies in the compute_predecessors which provides reference type conversion. I found that the definition of Predecessors is struct of repr(Rust) in the behind. https://github.com/digama0/mm0/blob/98496badaf6464e56ed7b4204e7d54b85667cb01/mm0-rs/components/mmcc/src/types/mod.rs#L39-L41 repr(Rust) is unspecified representation that we can't guarantee the layout of the struct. Here, suggest to add repr(C) to the struct to make the layout stable.

digama0 commented 1 year ago

References to Sized types are guaranteed to have the ABI of a pointer, so this is a guaranteed layout. Even if it was a transmute from Predecessors to Predecessors it would still be sound because it is the same type, the layout of any type is the same as itself. (In this case it's not quite the same type because of the lifetimes, but rust also guarantees that the layout of a type does not depend on lifetimes, or else lifetime erasure would not be sound.)

shinmao commented 1 year ago

You are right. Thanks for correcting me.