alexcrichton opened PR #6338 from alexcrichton:miri-stacked-borrows
to bytecodealliance:main
:
This is a series of commits hot on the tail of https://github.com/bytecodealliance/wasmtime/pull/6332. Previously Wasmtime was only valid under the Tree Borrows model in MIRI which is a much newer but less restrictive model for Rust's borrowing. After some discussion on Zulip though I concluded that there's no reason for us to rely purely on Tree Borrows and it's probably best to work under Stacked Borrows as well. This commit does that.
This commit also goes a bit further and gets everything working under strict provenance as well to fix any warnings coming out of MIRI. This means that we should be in a pretty strong position with respect to the verification running on CI, where the main remaining hole is lack of coverage.
alexcrichton requested wasmtime-core-reviewers for a review on PR #6338.
alexcrichton requested jameysharp for a review on PR #6338.
alexcrichton requested wasmtime-default-reviewers for a review on PR #6338.
sunfishcode submitted PR review.
sunfishcode submitted PR review.
sunfishcode created PR review comment:
This could be simplified slightly to
.sub(...)
.
sunfishcode created PR review comment:
Could you add a comment about why this is a casted
1
instead ofnull_mut()
?
sunfishcode created PR review comment:
Since this takes an immutable
&self
, should it return a*const VMContext
, with a separatevmctx_mut(&mut self)
or so if a*mut VMContext
is needed?
sunfishcode created PR review comment:
I'm not sure how to parse "the pointer's valid is trivially derivable from any
&Instance
pointer.
alexcrichton created PR review comment:
Oh the reason for this is the
NonNull
wrapper makes it incompatible withnull_mut
. Is there something you think is worth explicitly calling out here though?
alexcrichton created PR review comment:
I won't pretend to be an expert on Stacked or Tree Borrows unfortunately, so all I can really say for sure is that this passes everything successfully there, so it's at least not a fundamental requirement. While I think it's best to model as carrying mutability it's not actually required due to the way the
vmctx
pointer is derived now (as it's derived from a pointer stored inself
rather than purely fromself
). This means that the new*_mut
methods from https://github.com/bytecodealliance/wasmtime/commit/0977952dcd9d482bff7c288868ccb52769b3a92e aren't actually required and we can technically go back tovmctx_plus_offset(&self, u32) -> *mut T
, but I figured it's best to leave as-is for at least documentation purposes.
sunfishcode created PR review comment:
Ah, makes sense. Yeah, when I see a
1
being casted to a pointer, my first thought is "is this a magic value that something somewhere else knows about?". A comment stating that the intent is that, no, this is just intended as a placeholder would help.
alexcrichton created PR review comment:
Oops I typo'd and it's supposed to be
s/valid/value/
alexcrichton updated PR #6338.
alexcrichton updated PR #6338.
alexcrichton updated PR #6338.
CraftSpider submitted PR review.
CraftSpider submitted PR review.
CraftSpider created PR review comment:
Is
NonNull::dangling
not sufficient here? Internally, it's justinvalid_mut(align_of::<T>())
CraftSpider created PR review comment:
Drive by comment:
*mut
and*const
are, as far as I'm aware, treated as functionally the same in SB/TB, with their mutability determined by how they're derived, not their type. So,&T -> *mut T -> &T
and&mut T -> *const T -> &mut T
roundtrips are fine, but&T -> *mut T -> &mut T
isn't.This works here for the reasons alex mentioned - since it's derived from the original selfref pointer, it keeps its permissions as long as it isn't invalidated.
alexcrichton updated PR #6338.
alexcrichton created PR review comment:
Ah yes that works perfectly!
sunfishcode submitted PR review:
Yes, I can do that.
alexcrichton merged PR #6338.
Last updated: Nov 22 2024 at 17:03 UTC