search

rust-lang / miri

An interpreter for Rust's mid-level intermediate representation
Apache License 2.0
4.31k stars 327 forks source link

Tree Borrows: Make tree root always be initialized #3415

Closed JoJoDeveloping closed 5 months ago

JoJoDeveloping commented 5 months ago

This PR fixes a slight annoyance we discovered while formally proving that certain optimizations are sound with Tree Borrows. In particular... (copied from the commit message):

There should never be an Active but not initialized node in the borrow tree. If such a node exists, and if it has a protector, then on a foreign read, it could become disabled. This leads to some problems when formally proving that read moving optimizations are sound.

The root node is the only node for which this can happen, since all other nodes can only become Active when actually used. But special-casing the root node here is annoying to reason about, everything becomes much nicer if we can simply say that all Active nodes must be initialized. This requires making the root node default-initialized.

This is also more intuitive, since the root arguably becomes initialized during the allocation, which can be considered a write.

JoJoDeveloping commented 5 months ago

After some further thought, we decided to make the root note default Disabled and to manually set it to Active initialized on all in-bounds positions. This way, out-of-bounds accesses are also UB in TB.

RalfJung commented 5 months ago

LGTM, just one comment nit. :)

RalfJung commented 5 months ago

Thanks! @bors r+

bors commented 5 months ago

:pushpin: Commit 5b208c4cf95f083e49fa3fe45f11406ca425075a has been approved by RalfJung

It is now in the queue for this repository.

bors commented 5 months ago

:hourglass: Testing commit 5b208c4cf95f083e49fa3fe45f11406ca425075a with merge 7cf91ad8cbabb003bd6fb1646274e5bd68ea7d57...

bors commented 5 months ago

:sunny: Test successful - checks-actions Approved by: RalfJung Pushing 7cf91ad8cbabb003bd6fb1646274e5bd68ea7d57 to master...