-
Notifications
You must be signed in to change notification settings - Fork 58
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
What about: invalid not-used-again values? Is "validity on typed copy" enough? #84
Comments
To clarify, the last example doesn't need the |
@rkruppe It needs the |
See #189 for me describing this problem again. ;) An interesting observation: the following code is certainly fine; FFI code does something like this all the time when using Option<&T> on the interface: fn main() {
let mut x = Some(NonZeroU32::new(1).unwrap());
let xref = &mut x as *mut _ as *mut u32;
unsafe { *xref = 0 };
println!("{:?}", x);
} Operationally, this is basically the same as the problematic use std::num::NonZeroU32;
fn main() {
let mut x = Some(NonZeroU32::new(1).unwrap());
let xref = match x {
Some(ref mut c) => c as *mut NonZeroU32 as *mut u32,
None => panic!(),
};
unsafe { *xref = 0 }; // writing 0 into a `*mut u32`
println!("{:?}", x);
} To distinguish the two, |
Just some musings I came up with: When moving a Example: let a: Thing1 = default();
let aref = &a as *const _;
let b: Thing2 = transmute(a);
// `aref` is invalid _even if_ we guaranteed `b` were in the same physical location
// as a logical move has occurred So maybe the last Example: let mut x = Some(&0);
match x {
Some(ref mut b) => {
let u = b as *mut bool as *mut u8;
// `b` is no longer required to be valid, as it has been "moved"
// Just writing into a *mut u8
*u = 2;
}
None => panic!(),
}
dbg!(x); On the other hand, the origin provenance makes sense as well. Using this example for clarity: let mut x = Some(NonZeroU32::new(1).unwrap());
let xref = match x {
Some(ref mut c) => c as *mut NonZeroU32 as *mut u32,
None => panic!(),
};
unsafe { *xref = 0 }; // writing 0 into a `*mut u32`
dbg!(x); It "makes sense" that the Naively, it feels like this should behave the same as let mut x = (1u32, 0u32);
let x1ref = &mut x.1 as *mut u32;
let xref = xref.sub(1) as *mut (u32, u32);
*xref = (0, 0);
dbg!(x); Specifically, it's taking a reference into the "interior" of an allocated object and "upgrading" it to a pointer to the full object to write the full object. It just so happens that the physical pointers are the same. My intuition here is suggesting something like guaranteed niche optimizations shouldn't matter for what operations you are allowed do with a pointer, just how you're able to accomplish said operations, as well as what memory reinterpretation is allowed. I don't know how practical that is, but it seems somewhat logical. (e.g. |
Yes, that is a way to look at it. Your "upgrading" example would be rejected by Stacked Borrows because that pointer is not allowed to write to the "outer" memory. |
(Moved to new issue) |
I asked about this on zulip, and was told to write my use case for why I'm doing it here. Here's more words about it than you asked for: I'm trying to write a highly tuned string type, using as many performance tricks as I can manage without hurting the average case. This includes (among other tricks) zero-cost conversion from &'static str, using atomic refcounts + clone-on-write for large strings, and of course, why I'm here, the classic small-string-optimization/inline-string-optimization well known from its use in C++ stdlibs. While I have a bunch of representations, all of them except SSO are more-or-less representationally equivalent (keeps most branches out of the non-small path). When in the SSO case though, it is essentially It's very important to me* that I not increase the size relative to This means I need the #[repr(C)]
pub struct String {
data: NonNull<u8>,
len: usize,
cap_flags: CapFlags, // just a usize**
} But it's a bit of a lie -- I just interpret Anyway, The issue is this: naively, the push_byte code (e.g. the part of the code handling when an ascii character is the arg to I tried a bit, and am probably going to try harder****, but ultimately ended up just performing the write unconditionally, and testing if afterwards our first field when read as a usize is zero (if it is quickly writing a non-zero to that byte and calling a This is a branch in a relatively hot path that I'm annoyed with (it's easily predictable but oh my god it seems like such a ridiculous edge case), but it ended up with better codegen than the alternatives I've tried so far. That said I haven't really finished tuning things so it's very possible that sort of write/read pattern is ultimately problematic in other ways... Anyway that was extremely rambling, but probably at least explained enough to get a good idea of the picture. * Mostly because I suspect it matters a lot in practice, even though llvm makes the cost of memcpys often hard to measure. I doubt increasing memcpy traffic would be favorable for very much rust code... ** CapFlags is a transparent wrapper for a usize that just holds both the capacity and two flag bits, while managing endian-specific stuff to keep them in the right place so that reading flags from it and from the final byte of the string both work. *** The most promising is probably the c == '\0' test, which the compiler should be able to do away with when c is constant (which appears to be the common case for arguments to **** since this makes me uncomfortable -- and rightfully so, wasn't properly accounting for the case where a macro that can expand to contain profiling data could possibly panic if the right --cfg was passed... (alright thats it i'm leaving before i think to give one of my footnotes a footnote) |
@digama0 raised concerns about this current "feature" of the semantics proposed so far. They also say
I assume this is using the same notion of "typed memory" as I do, i.e., a memory that contains types in its state. I am curious how you want to do that -- the proposal so far says
So this sounds to me like |
The memory doesn't contain |
That's what a type is, though... so even if you managed to "hack" around my particular definition of "typed memory", this still shares all the same problems of having a ton of shadow state that programmers (and tools like Miri) need to keep track of. You just have semantic types (i.e., predicates on values) in your memory instead of the usual syntactic types. I do agree that something like this could work, and indeed it is the most elegant working proposal I have seen so far. :-)
What makes typed memory hard to use in C/C++ is not the "chicken and egg" problem of formally defining it; indeed there is no problem at all there, e.g. the original CompCert memory model was typed -- but they moved away from typed memory since then. |
I think the term "typed memory" is not doing us favors here. To me, that implies that a value has a type in memory from now until it is deallocated, and any access to that memory at another type is UB. In my proposal, the type is only asserted on reads, on writes, and when a mut borrow ends (also thought of as a write). In the intervening period unsafe code can write whatever it likes. We are already carrying quite a bit of shadow state in memory, including in particular the tags of unique references that have been converted to raw pointers. So the necessary information is already present; it might be possible to just look up the type of the reference with that tag and simulate a write to it (using the type it was declared as), so that would avoid any type state altogether. The point is really that the mutable borrow should not be able to be dropped while bad memory is in it, and a simulated write has exactly the right effect. The only tricky thing is the timing of the write but stacked borrows handles that well enough using the borrow stack. |
This is actually not the case, typed memory does not imply strict aliasing (C and C++ have both, but they are constructed through different parts of the standards). Other than that, I do agreee. Rust shouldn't adopt a model that imposes typed memory, but I don't think asserting that memory written through a mutable reference (and derivatives of that reference) as being valid at drop is fair. In the absense of #77 requiring it (which bring the UB to wherever the mutable reference becomes active again, through SB or another mechanism), this is a fair substitute. Ideally, a write to the inner field of an |
If it is asserted on writes, then how can it write whatever it likes? All writes need to be of the right type. If that's not "typed memory", I do not know what is.
Indeed the aliasing model requires all these tags as shadow state. But you are proposing to add even more shadow state. So far the shadow state is completely type-agnostic (except for I think the shadow state should be the absolute minimum that we need for good optimizations.
Ah, what a hack. ;) This makes a couple of assumptions though about only one such reference existing or all such references having the same type, which is not necessarily true.
Do you mean "I do think"?
But why? I don't agree, and you just stated a preference without giving arguments. There need to be good arguments for every extra bit of UB, usually in the form of optimizations that outweigh the cost of the extra proof obligation and mental burden for programmers. |
That is not even the case with the proposal on the table, is it? Validity is checked when the borrow item is removed from the stack; in the mean time other code could break and then restore the invariant and that would be allowed. |
To the point where it can affect surrounding code, I don't believe this can apply. If we assert validity whenever a &mut is dropped from the borrow stack, you can't possibly observe the field itself, except through the &mut in a broken-invariant state, and therefore you can't observe the effects on the Option. As for why, an union Option{
struct{bool engaged; T value;} Some;
struct{bool engaged;} None;
}; not-withstanding layout rules. C says you can't reach the engaged field or the Outer Struct from the value field, and SB says the same AFAIK (I believe it also says you can't reach the outer struct from the inner engaged, but C would permit that). I think this should be a valid assertion even when T has a niche, or is a dependant type that may have a niche. By protecting validity at &mut drop, we can maintain the assertion for these types. This increases the potential optimizations for dependant (not-yet monomorphized) types, which reduces the number of times optimizations need to be performed (I know rustc can perform MIR optimizations, though idk if it performs optimizations in dependant contexts) |
Okay, so you would be fine with temporarily violating the invariant. That would also still permit @thomcc's usecase. FWIW, I think the easiest way to implement this in Miri would be to add type information somewhere here. That makes
Essentially, yes, though the details differ greatly between Stacked Borrows and C. Also note that in Stacked Borrows all of this is only true for references; with raw pointers, there are no such restrictions. (Mixing references and raw ptrs is more complicated, no need to get into this now.)
I would be curious for a concrete example of such an optimization. (Also I think what you call "dependent" is what is usually called "generic" in Rust; dependent types are something else. Just trying to make sure I correctly understand the words you are using.) It seems like you want to provide the fiction that the embedded niche is a separate field in a disjoint location. First of all let me note that this fiction cannot be entirely held up -- when concurrency is involved, whether or not two things overlap in memory matters a lot, so So the question is one of how close niches can be to behave like "normal fields"; they will always have to be treated separately. Also note that in MIR, the niche is not just a normal field -- it can only be interacted with through special MIR operations ( |
Another note: if we end up deciding for #77 that validity of a reference is just about its bits, then your proposal would have the strange consequence that a |
I just realized there is a larger problem with your proposal: everything in SB is per-location, but validity invariants are not! When we are popping an So to implement your proposal we'd actually have to keep track of how many locations a tag is active for, or something like that, and even then I am not convinced it would work out... maybe that is checking some things too late then. |
(FYI I noticed this after writing the original comment and rewrote this section, see the edit.)
Indeed it is, and I would expect Miri to notice such things assuming it appears as language UB. In the particular case of
That's not how provenance works (at least in the current implementation). There is no pointer provenance that says you can't write 0 to a location. If you have let p: &mut NonZeroU8 = &mut NonZeroU8::new(1);
// *p = NonZeroU8::new_unchecked(0); // UB
// *(p as *mut NonZeroU8) = NonZeroU8::new_unchecked(0); // still UB
*(p as *mut NonZeroU8 as *mut u8) = 0; // DB
// println!("{}", *p); // UB, because we are reading 0 at type NonZeroU8 The validity invariant depends only on the type you are writing at, as determined by the static type of the things on each side of the |
And my example shows that pointer provenance remembering what type it's "really" writing to isn't tractable, either. The problem with it is that raw pointer operations necessarily don't change provenance. If you have Essentially, this is the example where you have I also strongly expect that bytewise memcpy should be implementable inside the abstract machine (given a There are two "solutions" to this I know of so far, neither of which are particularly nice.
So, TL;DR of that: there isn't even a known way to say the OP example is UB without a major restructuring of how SB's model of the AM semantics works. (And if you want to go earn your PhD making a formally sound competing model to SB, then I say glhf!) |
So, I would actually disagree with this being typed memory "basically in name only". I think it more resembles a "capability" model. #316 I think in part comes down to how permissions get restricted and unrestricted as passed through various phases of the memory lifecycle. The memory is untyped and very general in providence, but the allocator may impose restrictions when the memory leaves, which the allocator itself doesn't have to obey once it is passed back, as long as it was the allocator that imposed those restrictions. The memory remaining untyped for the entire program while the pointers carry further restrictions plays a valuable role. However, I think the memcopy problem is a pretty big one here. If we have a However, this code having radically different meaning based on fn func1<T, F: FnOnce(&mut T)>(mut v: Option<T>, f: F) -> bool {
match &mut v {
Some(ref mut b) => f(b),
None => (),
}
return true;
}
fn func2<T, F: FnOnce(&mut T)>(mut v: Option<T>, f: F) -> bool {
match v {
Some(ref mut b) => f(b),
None => return true,
};
return v.is_some();
} When We can also imagine a 'hard mode' memcopy, where it spreads the writes across multiple threads for some reason. I do feel even this should be legal. But when I think about the actual reasoning I think justifies it, it comes out as something between the two options given. Something like "this write is allowed through this pointer, when this pointer promised to obey certain rules, because by the time it will be observed (see: popping tags) I promise that someone will have fixed this up". When I try to imagine formalizing this, it seems like the most general way would be something like... when you hand out a pointer, you get to set the rules that then get triggered when tags are popped and such, and even if it is transmuted or such that can only narrow the rules further. This... also seems like it helps with the nested allocator case in some ways, but... the level of generality of this sort of reasoning makes me worry about actually implementing it into a checker. It seems like the general pattern here would be saying that pointers/references get to encode generators for predicates that get written every time they are used to write, and then get checked on read. Having functions generating functions as a basic building block for providence checking at least sounds bad. But the actually relevant ones there seem... at lot easier to handle. Owning an allocation seems the most complicated in a lot of ways, but is the primary thing stacked borrows was made to solve.. Leaving the selected constructor in the same state that it was when the inner reference was made seems downright trivial in comparison. |
I view this as a consequence of doing layout optimizations. It's not surprising that for code doing byte-wise accesses, this has consequences. Reordering fields also changes some otherwise 'generic' properties in code working on
It doesn't seem trivial to me. 🤷 Stacked Borrows doesn't really do anything with 'ownership', it 'just' checks that the sequence of pointer accesses made to a byte of memory makes sense (and it does that independently for each byte). The 'selected constructor' is a very subtle concept -- it basically doesn't exist on the Abstract Machine, it is an emergent property that comes up after interpreting a bunch of bytes using a given type, and with types like |
(Ignoring the opsem,) I would like to argue that asserting validity at expiry typically matches developer reasoning better, and better behaves like safety invariant does. I argue that semantically, the OP example1 is similar to e.g. the practice of Obviously the safe interface still requires restoring the type-valid (and type-safe) bytes. This is about the validity requirement. For that, I still hold my previously stated position that we have and should keep untyped memory, and that means only doing type-dependent assertions when doing a typed operation (copy, maybe retag; pop is untyped). The observation is that restoring the invariants before exiting through the invariant-holder matches the usual patterns, and diverging from this for unsafe opsem is a difference that will need to be learned. Footnotes
|
I have a proposal for an opsem which could disallow the OP example (at least as written): use a protected tag for
There is an important caveat to inserting protectors on fn main() { unsafe {
let mut z = Some(&0);
match z {
Some(ref mut b) => {
(x as *mut &i32 as *mut usize).write(0);
assert!(z.is_none());
}
None => unreachable!(),
}
} } Issuing protectors here thus requires removing the protector when the borrow is invalidated non-lexically. This information may not be available in the current structure of MIR, and would need to be added during MIR borrowck. This limits the viability of the approach somewhat. (Protectors could additionally be used on any introduced reference with this semantic of scheduling the removal of the protector.) Also to note: this is not to advocate for this approach, just to note it as an approach. noted later: there's a significant flaw with this approach: using a parent raw pointer does not cause the child reference to be known to be invalidated. |
@CAD97 so you are arguing that we should not have UB for "invalid values on tag invalidation", but you are also proposing an opsem for achieving exactly that thing you don't want? That's a bit confusing so I am trying to make sure I understand you correctly here. :) |
My position is roughly summarized as
Footnotes
|
An interesting variant of invalid-not-used-again values came up on Zulip w.r.t. MIR drop elaboration: // only ever instantiated at <T=bool>
unsafe fn drop_uninit<T>() {
let mut x = std::mem::zeroed::<T>();
let p = addr_of_mut!(x) as *mut MaybeUninit<u8>;
p.write(MaybeUninit::uninit());
// Drop(x) <- current MIR
// drop_in_place(&mut x); // <- proposal
}
fn main() {
unsafe { drop_uninit::<bool>(); }
} This is very similar to an example in the OP let mut x = true;
let xptr = &mut x as *mut bool as *mut u8;
*xptr = 2; but perhaps slightly more interesting due to writing |
FWIW the |
FWIW https://github.com/rust-lang/rfcs/blob/master/text/2195-really-tagged-unions.md contains an example that expects at least temporary violation of the validity invariant of an |
…oli-obk Handle discriminant in DataflowConstProp cc `@jachris` r? `@JakobDegen` This PR attempts to extend the DataflowConstProp pass to handle propagation of discriminants. We handle this by adding 2 new variants to `TrackElem`: `TrackElem::Variant` for enum variants and `TrackElem::Discriminant` for the enum discriminant pseudo-place. The difficulty is that the enum discriminant and enum variants may alias each another. This is the issue of the `Option<NonZeroUsize>` test, which is the equivalent of rust-lang/unsafe-code-guidelines#84 with a direct write. To handle that, we generalize the flood process to flood all the potentially aliasing places. In particular: - any write to `(PLACE as Variant)`, either direct or through a projection, floods `(PLACE as OtherVariant)` for all other variants and `discriminant(PLACE)`; - `SetDiscriminant(PLACE)` floods `(PLACE as Variant)` for each variant. This implies that flooding is not hierarchical any more, and that an assignment to a non-tracked place may need to flood a tracked place. This is handled by `for_each_aliasing_place` which generalizes `preorder_invoke`. As we deaggregate enums by putting `SetDiscriminant` last, this allows to propagate the value of the discriminant. This refactor will allow to make rust-lang#107009 able to handle discriminants too.
…oli-obk Handle discriminant in DataflowConstProp cc ``@jachris`` r? ``@JakobDegen`` This PR attempts to extend the DataflowConstProp pass to handle propagation of discriminants. We handle this by adding 2 new variants to `TrackElem`: `TrackElem::Variant` for enum variants and `TrackElem::Discriminant` for the enum discriminant pseudo-place. The difficulty is that the enum discriminant and enum variants may alias each another. This is the issue of the `Option<NonZeroUsize>` test, which is the equivalent of rust-lang/unsafe-code-guidelines#84 with a direct write. To handle that, we generalize the flood process to flood all the potentially aliasing places. In particular: - any write to `(PLACE as Variant)`, either direct or through a projection, floods `(PLACE as OtherVariant)` for all other variants and `discriminant(PLACE)`; - `SetDiscriminant(PLACE)` floods `(PLACE as Variant)` for each variant. This implies that flooding is not hierarchical any more, and that an assignment to a non-tracked place may need to flood a tracked place. This is handled by `for_each_aliasing_place` which generalizes `preorder_invoke`. As we deaggregate enums by putting `SetDiscriminant` last, this allows to propagate the value of the discriminant. This refactor will allow to make rust-lang#107009 able to handle discriminants too.
(Taken from #69 (comment).)
How do we feel about this code -- UB or not?
This "magically" changes the discriminant. OTOH, it is very similar to
which is definitely allowed (it makes assumptions about layout, but we do guarantee layout of
Option<&T>
.Other examples:
The text was updated successfully, but these errors were encountered: