Initial work on Miri permissive-exposed-provenance

[carbotaniuman]

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.

This implements a form of permissive exposed-address provenance, wherein the only way to expose the address is with a cast to usize (ideally expose_addr). This is more restrictive than C in that stuff like reading the representation bytes (via unions, type-punning, transmute) does not expose the address, only expose_addr. This is less restrictive than C in that a pointer casted from an integer has union provenance of all exposed pointers, not any udi stuff.

There's a few TODOs here, namely related to fn memory_read and friends. We pass it the maybe/unreified provenance before ptr_get_alloc reifies it into a concrete one, so it doesn't have the AllocId (or the SB tag, but that's getting ahead of ourselves). One way this could be fixed is changing ptr_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:

let ptr = 0x2000 as *const i32;
let a: i32 = 5;
let a_ptr = &a as *const i32;

// value is 0x2000;
a_ptr as usize;

println!("{}", unsafe { *ptr }); // this is valid

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.

[RalfJung]

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.

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.

[RalfJung]

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.

[RalfJung]

(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.)

[bors]

☔ The latest upstream changes (presumably #2071) made this pull request unmergeable. Please resolve the merge conflicts.

[bors]

☔ The latest upstream changes (presumably #2084) made this pull request unmergeable. Please resolve the merge conflicts.

[RalfJung]

This looks great overall, thanks a ton!
That means I can start nitpicking, so lots of small comments. :)

[RalfJung]

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.

[RalfJung]

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.

[carbotaniuman]

The only thing that is missing is updating the README. Would you like help with that?

Yes please, I'd appreciate the help. I'll squash everything after that.

[RalfJung]

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. :)

[RalfJung]

@bors r+
Hooray 🎉 thanks @carbotaniuman :-)

[bors]

📌 Commit e1a62b9 has been approved by RalfJung

[bors]

🔒 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 self is your fork and upstream is this repository, you can resolve the conflict following these steps:

1. git checkout master (switch to your branch)
2. git fetch upstream master (retrieve the latest master)
3. git rebase upstream/master -p (rebase on top of it)
4. Follow the on-screen instruction to resolve conflicts (check git status if you got lost).
5. git push self master --force-with-lease (update this PR)

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 git merge instead of git rebase which makes the PR commit history more difficult to read.

Sometimes step 4 will complete without asking for resolution. This is usually due to difference between how Cargo.lock conflict is handled during merge and rebase. This is normal, and you should still perform step 5 to update this PR.

Error message

Auto-merging src/stacked_borrows.rs
Auto-merging src/machine.rs
Auto-merging src/lib.rs
CONFLICT (content): Merge conflict in src/lib.rs
Auto-merging src/helpers.rs
Auto-merging src/eval.rs
Automatic merge failed; fix conflicts and then commit the result.

[bors]

☔ The latest upstream changes (presumably #2139) made this pull request unmergeable. Please resolve the merge conflicts.

[RalfJung]

Resolved conflicts
@bors r+

[bors]

📌 Commit f8f2255 has been approved by RalfJung

[bors]

⌛ Testing commit f8f2255 with merge ab03d32...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing ab03d32 to master...