Skip to content
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

Stacked Borrows: Incompatibilities with LLVM noalias #86

Closed
RalfJung opened this issue Feb 6, 2019 · 12 comments
Closed

Stacked Borrows: Incompatibilities with LLVM noalias #86

RalfJung opened this issue Feb 6, 2019 · 12 comments
Labels
A-aliasing-model Topic: Related to the aliasing model (e.g. Stacked/Tree Borrows) A-optimization Category: Discussing optimizations we might (not) want to support A-provenance Topic: Related to when which values have which provenance (but not which alias restrictions follow) C-open-question Category: An open question that we should revisit

Comments

@RalfJung
Copy link
Member

RalfJung commented Feb 6, 2019

There are programs that are accepted by Stacked Borrows and conflict with LLVM noalias. @arielb1 had the following example in this long discussion on Zulip:

let x: &mut u32 = a;
let raw_ptr: *const u32 = x;
foo(x, raw_ptr);

fn foo(x: &mut u32, raw_ptr: *const u32) -> u32 {
    let x = &mut *x; // stack is now [..., Uniq(N)]
    *x = 5;
    let y = &*x; // stack is now [..., Uniq(N), Shr]

    // this is OK according to stacked borrows because of the Shr tag, but is UB
    // according to LLVM noalias and would be hard to make non-UB.
    unsafe { *raw_ptr }
}

On a high level, the problem is that create a raw reference is like a "broadcast" that lets every raw pointer now access this location, whereas LLVM only lets newly created raw pointers be used for that.

@RalfJung RalfJung added the A-aliasing-model Topic: Related to the aliasing model (e.g. Stacked/Tree Borrows) label Feb 6, 2019
@arielb1
Copy link

arielb1 commented Feb 6, 2019

That example is straight #87 - we do want to do be able to delay the write to x in real life. The real problem with noalias is that it brings along with it LLVM provenance tracking:

unsafe fn foo(x: &mut u32, raw_ptr: *const u32) -> u32 {
    let x: *mut u32 = &mut *x; // stack is now [..., Uniq(N), Shr]

    *x = 5; // access a raw pointer, OK because of the Shr.

    // this is OK according to stacked borrows because of the Shr tag, but is UB
    // according to LLVM noalias and would be hard to make non-UB.
    unsafe { *raw_ptr }
}

LLVM provenance tracking is unsound around int->ptr casts and the like and not well-defined in any case, so bringing it along is harmful.

@RalfJung
Copy link
Member Author

RalfJung commented Apr 17, 2019

@arielb1 the example in my first post here is basically a duplicate of #87. That issue is resolved by rust-lang/miri#695: the following is now UB.

fn main() { unsafe {
    let x = &mut 0;
    let raw = x as *mut _;
    let x = &mut *x; // kill `raw`
    let _y = &*x; // this should not activate `raw` again
    let _val = *raw; //~ ERROR
} }

However, I assume other incompatibilities with LLVM remain, so I'll keep this open. There'll be a blog post on this new Stacked Borrows soon; it'd be great if you could then try to help find new incompatibilities with LLVM @arielb1.

@RalfJung
Copy link
Member Author

@comex came up with an example of UB that Miri does not catch, based on Stacked Borrows not tracking raw pointers currently.

See here for why we currently cannot do this more precise tracking: We'd have to fix Rc, but the fix is not expressible without something like &raw.

@RalfJung RalfJung added C-open-question Category: An open question that we should revisit A-optimization Category: Discussing optimizations we might (not) want to support A-provenance Topic: Related to when which values have which provenance (but not which alias restrictions follow) and removed A-optimization Category: Discussing optimizations we might (not) want to support labels Aug 14, 2019
@RalfJung
Copy link
Member Author

Since rust-lang/miri#872, retagging is "shallow" in the sense that only "bare" references are retagged and can be used for reasoning. So, things like Pin<&mut T> would actually not be treated like a reference.

This is in contrast to how we compile (with -Zmutable-noalias), where we do add noalias for newtypes around references.

@comex
Copy link

comex commented Aug 21, 2019

Hmm... that might be a good idea for now, but it doesn't seem like a good long-term approach to me, as it implies that single-field structs would no longer be zero-overhead abstractions.

@RalfJung
Copy link
Member Author

Yeah. We probably want this for some but not all newtypes.

@eddyb
Copy link
Member

eddyb commented Aug 22, 2019

Pin is a lang item and definitely subject to special-casing.
In a sense, Box<T> is currently just a *mut T newtype special-cased to noalias.
It would be trivial to do something similar for Pin, but in the opposite direction.

@RalfJung
Copy link
Member Author

We also need the "opt-out of noalias" for Ref, RefMut and vec_deque::Drain though -- and maybe more.

@gnzlbg
Copy link
Contributor

gnzlbg commented Aug 22, 2019

We also need the "opt-out of noalias" for Ref, RefMut and vec_deque::Drain though -- and maybe more.

These types aren't really special, and fixing these is a PR from libstd away. I'd be more comfortable with such PRs if miri were actually able to detect these issues if we were to commit test cases that trigger them. Is this possible?

@RalfJung
Copy link
Member Author

RalfJung commented Aug 22, 2019

Miri used to be able to detect them and I removed that for several reasons -- the main one being that I thought surely Stacked Borrows is too strict here, and we should fix the model instead of complaining about legitimate code. I could certainly bring that back (would require reverting a rustc PR and a Miri PR).

Would be interesting to get a lang team opinion on that -- rust-lang/rust#63787 is probably the better place for that discussion, though.

@RalfJung
Copy link
Member Author

Miri now tags raw references by default, and the new -Zmiri-retag-fields flag re-enables recursive retagging. I think this means that with that flag Stacked Borrows is actually sound wrt our LLVM attributes, finally! (The main caveat is around int2ptr casts, where Miri has to start approximating things, and LLVM doesn't give us a sufficiently precise spec.)

@JakobDegen
Copy link
Contributor

Closing as having been fixed by more recent versions of SB and by TB

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-aliasing-model Topic: Related to the aliasing model (e.g. Stacked/Tree Borrows) A-optimization Category: Discussing optimizations we might (not) want to support A-provenance Topic: Related to when which values have which provenance (but not which alias restrictions follow) C-open-question Category: An open question that we should revisit
Projects
None yet
Development

No branches or pull requests

6 participants