-
Notifications
You must be signed in to change notification settings - Fork 347
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Initial work on Miri permissive-exposed-provenance #2059
Conversation
It is definitely not allowed by LLVM, but also for now I don't think I want any "udi stuff" in Miri. That's just too many extra complications. I view this as something we add solely to remain compatible with legacy (non-strict-provenance) code; there's only so much maintenance burden in Miri that that code is worth having, IMO. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks a lot!
I think I have one major structural suggestion: we should avoid runtime checks in memory_read
and the other hooks, and instead use the type system to ensure that we have concrete provenance there.
What if the Machine
trait contained two types, Tag
and ConcreteTag
? And the "reify" function returns a ConcreteTag
, while these hooks here take a ConcreteTag
. Then we can never forget to use the right kind of tag. (And we also will never accidentally mix up a Pointer<Tag>
with ConcreteTag
data.)
Or maybe we instead add an associated type TagExtra
or so, and define ConcreteTag = (AllocId, TagExtra)
. Then we don't need a function to get the alloc ID out of a ConcreteTag
. Also see rust-lang/rust#96165.
(I should also note I have not looked at the Stacked Borrows part yet. I am first focusing on getting the other parts to work.) |
☔ The latest upstream changes (presumably #2071) made this pull request unmergeable. Please resolve the merge conflicts. |
☔ The latest upstream changes (presumably #2084) made this pull request unmergeable. Please resolve the merge conflicts. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks great overall, thanks a ton!
That means I can start nitpicking, so lots of small comments. :)
d9234b7
to
b12f96b
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, I think we are getting there. :) However I unresolved some comments that you had marked as resolved but that are still open.
This is nearing the phase where there's lots of small tweaking going on to improve code structure, function names, comments and such. If you want I can also take over and finish the PR from here.
The one high-level question that is still open is that test you added about the NULL pointer -- that does not seem right; I think we want to allow that code and might even have it in the run-pass test.
Awesome, I think this is basically ready. :) The only thing that is missing is updating the README. Would you like help with that? Also, please squash all these commits together into one. |
Yes please, I'd appreciate the help. I'll squash everything after that. |
I think it might be easier if we land your PR, and I do the README change as a follow-up PR. So could you squash? Then I'll approve. :) |
@bors r+ |
📌 Commit e1a62b9 has been approved by |
🔒 Merge conflict This pull request and the master branch diverged in a way that cannot be automatically merged. Please rebase on top of the latest master branch, and let the reviewer approve again. How do I rebase?Assuming
You may also read Git Rebasing to Resolve Conflicts by Drew Blessing for a short tutorial. Please avoid the "Resolve conflicts" button on GitHub. It uses Sometimes step 4 will complete without asking for resolution. This is usually due to difference between how Error message
|
☔ The latest upstream changes (presumably #2139) made this pull request unmergeable. Please resolve the merge conflicts. |
Resolved conflicts |
📌 Commit f8f2255 has been approved by |
☀️ Test successful - checks-actions |
clean up int2ptr code a bit Follow-up to #2059
Miri portions of the changes for portions of a permissive ptr-to-int model for Miri. This is more restrictive than what we currently have so it will probably need a flag once I figure out how to hook that up.
There's a few TODOs here, namely related to
fn memory_read
and friends. We pass it the maybe/unreified provenance beforeptr_get_alloc
reifies it into a concrete one, so it doesn't have theAllocId
(or the SB tag, but that's getting ahead of ourselves). One way this could be fixed is changingptr_get_alloc
and (ptr_try_get_alloc_id
on the rustc side) to return a pointer with the tag fixed up. We could also take in different arguments, but I'm not sure what works best.The other TODOs here are how permissive this model could be. This currently does not enforce that a ptr-to-int cast happens before the corresponding int-to-ptr (colloquial meaning of happens before, not atomic meaning). Example:
We also allow the resulting pointer to dereference different non-contiguous allocations (the "not any udi stuff" mentioned above), which I'm not sure if is allowed by LLVM.
This is the Miri side of rust-lang/rust#95826.