What about: invalid not-used-again values? Is "validity on typed copy" enough?

[RalfJung]

(Taken from https://github.com/rust-rfcs/unsafe-code-guidelines/issues/69#issuecomment-459445822.)

How do we feel about this code -- UB or not?

fn main() { unsafe {
    let mut x = Some(&0); 
    match x {
        Some(ref mut b) => {
            let u = b as *mut &i32 as *mut usize;
            // Just writing into a *mut u8
            *u = 0;
        }
        None => panic!(),
    }
    assert!(x.is_some());
} }

This "magically" changes the discriminant. OTOH, it is very similar to

fn main() { unsafe {
    let mut x = Some(&0); 
    (&mut x as *mut _ as *mut usize) = 0;
    assert!(x.is_some());
} }

which is definitely allowed (it makes assumptions about layout, but we do guarantee layout of Option<&T>.

Other examples:

fn main() { unsafe {
  let mut x = true;
  let xptr = &mut x as *mut bool as *mut u8;
  *xptr = 2;
} }

fn main() { unsafe {
    let mut x = Some(true); 
    match x {
        Some(ref mut b) => {
            let u = b as *mut bool as *mut u8;
            // Just writing into a *mut u8
            *u = 2;
        }
        None => panic!(),
    }
    assert!(x.is_some());
} }

#![feature(rustc_attrs)]

#[rustc_layout_scalar_valid_range_start(1)]
#[repr(transparent)]
pub(crate) struct NonZero(u32);

fn main() { unsafe {
    let mut x = Some(NonZero(1)); 
    match x {
        Some(NonZero(ref mut c)) => {
            // Just writing 0 into an &mut u32
            *c = 0;
        }
        None => panic!(),
    }
    assert!(x.is_some());
} }

[hanna-kruppe]

To clarify, the last example doesn't need the unsafe {}, right? It's not "safe code" (you can modify it to be unquestionably UB by omitting the Option and reading x after the end) but that's due to the use of #[rustc_layout_scalar_valid_range_start], not due to any individual operation in main.

[RalfJung]

@rkruppe It needs the unsafe, we have fixed unsafety checks in rustc to require an unsafe block to create a reference into a rustc_layout_scalar_valid_range_start struct.

[RalfJung]

See https://github.com/rust-lang/unsafe-code-guidelines/issues/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, xref would need to have some kind of "provenance" remembering that it was created from a pointer to NonZeroU32, not a pointer to u32.

[CAD97]

Just some musings I came up with:

When moving a !Copy type, invalidating the old name is obviously correct.

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 copy of a Copy value could be a move as well?

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 c binding only "owns" the right to write to the NonZeroU32.

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. <*const Option<NonZeroU32>>::cast::<u32> is valid because of the guaranteed niche optimization, but <*const NonZeroU32>::cast::<Option<NonZeroU32>> is not valid, even if said pointer lives in that type (unless it was derived from a wider pointer).)

[RalfJung]

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.

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. On the other hand, physical overlap is the thing that matters for aliasing, which is what Stacked Borrows is all about. And note that there is nothing in the validity machinery that has any problem with deriving "outer" pointers from "inner" pointers". Only Stacked Borrows cares.

[RalfJung]

(Moved to new issue)

[thomcc]

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 [u8; size_of::<String>()] where the last byte is used for length and tags.

It's very important to me* that I not increase the size relative to std::string::String, and that includes for representing things like Option<String> or Result<String, E>.

This means I need the NonNull byte pointer, and can't use this as a union, even though conceptually it's used as one. This all means it just looks like a pretty normal string:

#[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 &mut self as a &mut [u8; N] when writing as a small string, and &self as a &[u8; N] when reading as one. The only true parts about it when we're small are that NonNull stays zeroed, and that CapFlags

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 push for the small string case ended up needing too many checks to avoid writing to NonNull<u8> -- essentially you want to ask a subset of (on 64 bit) 'are our first 7 bytes nul' && 'is the incoming c == '\0'' && 'will it get written to the 8th byte'. this is hot code, so more checks, even if they're correctly predicted, are bad.***

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 #[cold] function).

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 push much of the time), and should be rare enough. Unfortunately, the only place this is convenient to punt it to is the non-ascii push case (which is less hot, but very far from cold), and doing so isn't exactly ideal...

**** 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)

[RalfJung]

@digama0 raised concerns about this current "feature" of the semantics proposed so far. They also say

I won't elaborate on it more in this thread, but my proposal could enforce this property without requiring a typed memory.

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

The property we would like to establish is that when the lifetime of the &mut b ends, b is again valid at type bool, but in an operational model we can't just say that, so instead, when &mut b as *mut bool is executed, we push on the borrow stack of b a record that, when popped, reasserts the bool invariant at this byte.

So this sounds to me like bool is stored in the borrow stack, which is part of memory. So I would call this "typed memory".

[digama0]

The memory doesn't contain bool on the borrow stack, it contains one of a small set of predicates on bytes representing byte sized slices of a validity property. One of those predicates is "this byte is 0 or 1", so in that sense yes it's put bool on the stack, but that doesn't mean that you have some recursive type going into the memory or a chicken and egg problem defining what types and memory are.

[RalfJung]

predicates on bytes

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. :-) But I am worried that it still adds a lot of complexity without enough benefit.

recursive type going into the memory or a chicken and egg problem defining what types and memory are.

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.

[digama0]

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.

[chorman0773]

any access to that memory at another type is UB

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 Option<T> should not be able affect the entire Option. This means that when T is niche-optimizing, it should be impossible to correctly (where correct shall mean the absense of undefined behaviour) write an invalid value to the inner field.

[RalfJung]

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.

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.

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;

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 UnsafeCell), which is very convenient when doing low-level stuff by casting pointers back and forth.

I think the shadow state should be the absolute minimum that we need for good optimizations.

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)

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.

@chorman0773

I don't think asserting that memory written through a mutable reference (and derivatives of that reference) as being valid at drop is fair.

Do you mean "I do think"?

Ideally, a write to the inner field of an Option should not be able affect the entire Option. This means that when T is niche-optimizing, it should be impossible to correctly (where correct shall mean the absense of undefined behaviour) write an invalid value to the inner field.

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.

[RalfJung]

it should be impossible to correctly (where correct shall mean the absense of undefined behaviour) write an invalid value to the inner field.

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.

[chorman0773]

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 Option<T> is fundamentally equivalent to the C

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)

[RalfJung]

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.

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 item bigger, which is a problem as we have a lot of those, and it adds the 'tcx lifetime everywhere, but I think it should work. And similarly, in a formal mathematical semantics I'd probably add a syntactic type rather than a "predicate on values", that will be easier to handle -- it maintains countability and decidable equality and all these things you want to have for your machine state.

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

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

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 UnsafeCell has to disable niches or else Option<UnsafeCell<bool>> would go horribly wrong. Your proposal does not change this.

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 (Statement::SetDiscriminant and Rvalue::Discriminant). Any optimization that wants to work on niches would need special treatment for that case anyway. IOW, it's not like Stacked Borrows the way it works right now requires special care around niches -- it is that something like your proposal would allow a more "stacked-borrows-like" treatment of SetDiscriminant and Discriminant. As mentioned before, the question is if such things come up often enough, i.e. if such optimizations can be applied often enough, to justify the extra complexity.

[RalfJung]

Another note: if we end up deciding for https://github.com/rust-lang/unsafe-code-guidelines/issues/77 that validity of a reference is just about its bits, then your proposal would have the strange consequence that a &mut bool pointing to a non-bool byte is itself valid, but when you reborrow that reference and then pop the reborrow off the stack, now you have UB. Basically you end up with "depth 1 validity on mutable reference invalidation", which is somewhat odd.

[RalfJung]

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 &mut tag off the stack, that doesn't mean this reference is entirely invalid, just that it is invalid for this location. There is no place where Stacked Borrows "knows that a reference has been dropped".

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.

[digama0]

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.

Writes have to be correct for the type of the reference being used for the write, not the memory location. If you want to write whatever you like, you cast the reference and write at a different type. This part is no different from the current model.

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 UnsafeCell), which is very convenient when doing low-level stuff by casting pointers back and forth.

I think the shadow state should be the absolute minimum that we need for good optimizations.

I think there is quite a lot of type-like information contained in those "unique timestamps". It's not types, but it is lifetimes, and there are a half dozen ways to slightly tweak the available information to store the relevant information needed to reassert mut borrows without necessarily "storing types" (also why is that so scary? you haven't elaborated other than to point out that some folks moved away from typed memory in CompCert, which seems like a rhetorical technique rather than an argument).

Note that this whole mut borrow write thing only works on &mut T references, not pointers of any kind. Those are just as they always have been, free rein to write whatever wherever, but all the references have to still be good when their borrows end.

An alternative approach uses code insertion in the model, i.e. drop impls for mut borrows. You are already doing this with retag so it shouldn't be too much different, and then the drop impl can carry the appropriate type to write at. This approach has its own problems though (where does the code go?) but it seems like this is work that is already done for real drop impls so perhaps it's a solved problem.

And similarly, in a formal mathematical semantics I'd probably add a syntactic type rather than a "predicate on values", that will be easier to handle -- it maintains countability and decidable equality and all these things you want to have for your machine state.

A "predicate on values" is just u8 -> bool, which is plenty decidable and countable, being isomorphic to [bool; 256]. Probably you wouldn't want that in miri though, as it's pretty big; an enumeration of validity properties that have been defined (aka types) is probably much smaller.

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 UnsafeCell has to disable niches or else Option<UnsafeCell> would go horribly wrong. Your proposal does not change this.

That sounds like the compiler performing as we would expect: an optimization is not sound under certain conditions, so it doesn't do them. That is what I would call "upholding the fiction". What is not upholding the fiction is performing the optimization even in cases where it changes observable (non-UB) behavior, allowing the option-nulling code.

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 &mut bool pointing to a non-bool byte is itself valid, but when you reborrow that reference and then pop the reborrow off the stack, now you have UB. Basically you end up with "depth 1 validity on mutable reference invalidation", which is somewhat odd.

I agree; if references aren't necessarily valid in the first place then there is no point reasserting validity. It might be possible to get some approximation of it where you try not to perform the write-back if the location was never written to while the borrow in question was active, but it looks dicey. I think you will lose the ability to reason about the option-nulling code in any case.

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 &mut tag off the stack, that doesn't mean this reference is entirely invalid, just that it is invalid for this location. There is no place where Stacked Borrows "knows that a reference has been dropped".

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.

This is a good point. How do multiple unique borrows with the same tag arise? From transmute? Perhaps this data should not be stored in memory at all, but rather in the "code part" where the locals are, because those have proper types. If you store the list of "open borrows" attached to tags, then every time a tag representing a mutable borrow is invalidated you look up the tag to find the mapping of borrows (the &mut's in the code) associated to that tag and simulate writes to each of them. (I guess a mutable borrow ends when the borrow tokens on any of its bytes is invalidated; I can't think of any example where the remaining borrow tokens are still usable.)

I should learn more precisely how miri is laid out besides just the SB model on memory, since it seems important how stack variables and the instruction pointer / code are tracked here.

[chorman0773]

Also I think what you call "dependent" is what is usually called "generic" in Rust; dependent types are something else

Somewhat. IIRC Generic types simply refers to generic parameter type. A Dependent type, in this context, refers to a type for which the properties depend on a Generic type. Some properties can be known, some can't (for example, *mut T is Sized, has no niches, and is a pointer, whereas T may not have any of those properties known or disputed (by default Sized is known), therefore I must assume the worst case for optimization (until after generic instantiation), which generally is a contradiction as two opposed properties could need to be assumed for a purely unbound T.

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 UnsafeCell has to disable niches or else Option<UnsafeCell> would go horribly wrong. Your proposal does not change this.

As you mentioned, UnsafeCell hides niches (though I would elect not to disable them, I simply tag UnsafeCell in a way that precludes it from being treated as a niche-optimization candidate, the invariants would still be applied), and yes, it would cause the model to break down if it was not (though its moot, as it is treated as such), since you can mutate through an interior exclusive reference, and still observe the Option through its own shared reference. However, because UnsafeCell blanket hides niches, I believe the argument is without merit.

Niche optimization of enums depends on the validity invariant in more ways than one. Absent this UB, certain types of Niche Optimizations would, as mentioned by @digma0, alter the behaviour of certain code. So in effect, not having this UB could make the non-mandatory optimizations violate the as-if rule, assuming rust has the as-if rule. According to a strict interpretation of rust's rules (ignoring UCG for this exposition), Some(b), where b is a bool cannot possibly produce None. That is, Some(b).is_some() is a tautology in rust. Using the same reasoning, a reasonable conclusion is that a write to a &mut bool cannot alter the variant. From that conclusion, if it was possible to write in a niche, then niche optimizing Option<bool> is an invalid transformation, because it doesn't satisfy the as-if rule. The only way that it could then be possible to perform the niche optimization is if the as-if rule did not apply, which requires that the program in question have undefined behaviour (This is dependant on rust actually prohibiting this, but I can see nothing in any of the limited documentation rust has that would make the transformation sound, IE. semantically mapping to the untransformed). Note that this is not an authorative interpretation, it's simply my reasonable interpretation, based on the little "normative" information rust has.

[RalfJung]

Writes have to be correct for the type of the reference being used for the write, not the memory location. If you want to write whatever you like, you cast the reference and write at a different type. This part is no different from the current model.

Ah I see, so writes are "allowed to change the type of memory", so to speak.

(also why is that so scary? you haven't elaborated other than to point out that some folks moved away from typed memory in CompCert, which seems like a rhetorical technique rather than an argument)

Not sure if I'd call it "scary", but my dislike for typed memory stems mostly from experience with strict aliasing in C++: it is a huge pain for programmers (see all the projects using -fno-strict-aliasing and the many more projects that should set this flag) and gives very weak optimizations compared to Stacked Borrows. So I think we just don't need it. Also I think there yet has to be a proposal that integrates this well with a language that allows byte-wise memory access and mutation. (The C object memory model is a huge mess and AFAIK still has not been described precisely. The best approximation I know is in this thesis.)

Your proposal attempts this, but I think it does not work because Stacked Borrows is per-location, which validity invariants are not (see the discussion about multiple stacks with the same tag).

A "predicate on values" is just u8 -> bool, which is plenty decidable and countable, being isomorphic to [bool; 256]. Probably you wouldn't want that in miri though, as it's pretty big; an enumeration of validity properties that have been defined (aka types) is probably much smaller.

Ah, I thought by "value" you meant something more like this enum. Also "predicate" usually means X -> Prop, not X -> bool, and Prop certainly does not have decidable equality. But indeed if you interpret predicates like that, they remain countable, finite even.

I agree; if references aren't necessarily valid in the first place then there is no point reasserting validity.

Ah, but I think there is -- note that in my example in the OP, the x that is "invalidated in a sneaky way" is not a reference but a local variable!

An alternative approach uses code insertion in the model, i.e. drop impls for mut borrows. You are already doing this with retag so it shouldn't be too much different, and then the drop impl can carry the appropriate type to write at. This approach has its own problems though (where does the code go?) but it seems like this is work that is already done for real drop impls so perhaps it's a solved problem.

The problem is that references do not have drop glue, and this is exploited by the borrow checker. There is no good way to find out, in code, where a lifetime ends -- and with Polonius, that question might not even be well-defined any more.

So I am pretty wary of any proposal that relies on performing some action in the semantics when a lifetime ends. Stacked Borrows was specifically designed to not do that, to avoid these problems.

This is a good point. How do multiple unique borrows with the same tag arise?

When you create an &mut i32, each of the 4 location separately tracks the tag of that reference. Now there are 4 stacks with that tag in them, and removing the tag from these stacks can happen independently and in any order. Only if the last of them is removed would we want to check the invariant again. That seems very non-local compared to the rest of Stacked Borrows.

@chorman0773

As you mentioned, UnsafeCell hides niches (though I would elect not to disable them, I simply tag UnsafeCell in a way that precludes it from being treated as a niche-optimization candidate, the invariants would still be applied),

The invariants certainly still apply. Hiding the niches affects optimizations, it does not affect UB.

Niche optimization of enums depends on the validity invariant in more ways than one. Absent this UB, certain types of Niche Optimizations would, as mentioned by @digma0, alter the behaviour of certain code. So in effect, not having this UB could make the non-mandatory optimizations violate the as-if rule, assuming rust has the as-if rule. According to a strict interpretation of rust's rules (ignoring UCG for this exposition), Some(b), where b is a bool cannot possibly produce None. That is, Some(b).is_some() is a tautology in rust. Using the same reasoning, a reasonable conclusion is that a write to a &mut bool cannot alter the variant. From that conclusion, if it was possible to write in a niche, then niche optimizing Option is an invalid transformation, because it doesn't satisfy the as-if rule. The only way that it could then be possible to perform the niche optimization is if the as-if rule did not apply, which requires that the program in question have undefined behaviour (This is dependant on rust actually prohibiting this, but I can see nothing in any of the limited documentation rust has that would make the transformation sound, IE. semantically mapping to the untransformed). Note that this is not an authorative interpretation, it's simply my reasonable interpretation, based on the little "normative" information rust has.

This is a good point. I also used to motivate niche optimizations based on these invariants. But I am not sure any more that this is the right approach. Nowadays I see this to be more like struct layout: if you write unsafe code that assumes struct fields are laid out in a particular order, your code is wrong as that order might change in future compiler versions. But your code is not UB, as there is no UB clause that your code violates. We justify struct field reordering not by saying "code that relies on this is UB", we justify it by saying "struct field order is explicitly documented as unspecified, and this may change any time".

So, likewise, we can justify enum layout optimizations by saying "enum layout is explicitly documented as unspecified, and if you assume that the bool in an Option<bool> is in a separate memroy location, you are relying on unspecified details that may change any time, and hence your code is wrong".

[chorman0773]

We can justify by saying "enum layout is explicitly unspecified"

I come from a C++ background, where in some cases unspecified behaviour gives the compiler considerable latitude (in fact, like Rust with repr(Rust), the layout of a type which isn't a standard-layout type is unspecified, though it requires that fields with the same access specifier not be relatively reordered). However, it isn't all powerful, it simply grants a choice to the implementation, where it's not required to document how the choice is made. Some semantics cannot be altered, even when the program relies on unspecified behaviour (for example, writing to a pointer to a field of a struct that isn't pointer-interconvertible with the struct isn't capable of actually writing to a different field), and require UB to be lifted (where the standard says anything can happen in the entire program if some part of it does cause UB). Even in rust, we have the same thing. A &mut T to the first field of a struct Foo(T,U,V) cannot possibly alter the second or third fields, even though the relative order is not specified. My reasoning depends on this similarly extending to enums, where the fact that an Option<T> is Some(t), isn't changeable from the inner t. We have established that it is intuitively wrong, but I'm making the argument this may also be entirely incorrect, because rust doesn't have anything that allows it to occur, at least, interpreting the reference provenance rules from my C++ background. &mut t is capable of altering t, and nothing beyond that, even that happens to physical exist at the same memory address.

[RalfJung]

Even in rust, we have the same thing. A &mut T to the first field of a struct Foo(T,U,V) cannot possibly alter the second or third fields, even though the relative order is not specified. My reasoning depends on this similarly extending to enums

Exactly. And I am saying that is not correct reasoning. The enum discriminant is not a field, it can be arbitrarily encoded in the invalid values of all the fields of the enum, in ways that need not be specified by the compiler.

[chorman0773]

Then, would a valid interpretation be that it is logically a separate field (and therefore unreachable) from the inner &mut t, but it can physically overlap? As I say, I treat enum as a specially tagged union of structures (with a common initial sequence, in this case, an i1 which is effectively equivalent to bool, though with disimilar guarantees), and would like to maintain the reachability optimization. including when T is dependant (and may thus be a niche-optimization candidate). If its not valid for the user to rely on the fact the optimization does not occur, then it shouldn't also be valid to rely on the fact the optimization does occur, or that performing some operation would have the result of changing the variant, even if it does occur. However, where would that be left? Unspecified behaviour? Interesting behaviour as the result of a particular choice for unspecified behaviour? This is exactly what undefined behaviour is, becuse it is definately not defined. The only question comes with where the undefined behaviour occurs. As you mentioned, rust needs to justify undefined behaviour. It would arguably be better to specify something as undefined, then have it be undefined because of some wierd language lawyering like this. Code that would be broken by this is either already causes undefined behaviour, or relies on completely unspecified behaviour, that might even permit an interpretation that its undefined anyways. I would argue that this UB is completely justified, especially since both compiler devs and users are arguing for it, and it makes the above situtation a lot easier to reason about, because its not "It's maybe undefined behaviour possibly, or maybe it's not technically, but maybe it is actually" and that's a headache and a half, but "it is definately undefined behaviour". There definately is code that relies on a reference to the inner field not being able to affect the outer option. I presume that my Option<T>s never become None from out from under me, and when I'm already in unsafe code, I will do manual optimizations that rely on that being the case (doubly so if the consensus on the thread is that its not valid for the compiler to perform such optimizations themselves). Generally speaking, right now if you pass a &mut T to a (potentially arbitrary) unsafe function, you got the &mut T from out of an option, and T either has a niche, or is a dependant type that may have a non-hidden niche, you can't assume the reference is still safe to use. Both the compiler and users have to be incredibly defensive. I think this definately justifies having some level of this as UB.

[RalfJung]

If its not valid for the user to rely on the fact the optimization does not occur, then it shouldn't also be valid to rely on the fact the optimization does occur, or that performing some operation would have the result of changing the variant, even if it does occur.

Agreed.

However, where would that be left? Unspecified behaviour? Interesting behaviour as the result of a particular choice for unspecified behaviour?

I like "interesting behavior", standards should have that. :rofl: More seriously, I think this is just like code that relies on struct field layout -- i.e., unspecified behavior, or more precisely, code relying on unspecified parts of the semantics.

This is exactly what undefined behaviour is, becuse it is definately not defined.

No, not really. With unspecified behavior, if your assumption happens to be right, you actually get guaranteed correct compilation. This is probably an inconsequential difference for programmers, but when thinking about the fine details of these semantics in a formal way, it makes a big difference.

It would arguably be better to specify something as undefined, then have it be undefined because of some wierd language lawyering like this.

I respectfully disagree. We have good formal ways to define Undefined Behavior (as paradoxical as that may sound), and we have good formal ways to define "unspecified aspects of the semantics", and they are formally quite distinct. Once you care about mathematical precision, you thus need to tease these things apart.

The way to define unspecified aspects of the semantics is to parameterize the spec by these aspects. IOW, to actually execute a Rust program, you must make concrete choices for the layout of all structs, enums and unions (and more). These choices are somewhat constrained (e.g. for repr(C) the layout is fully defined, but for repr(Rust) there are very few constraints). For your program to be "well-behaved" Rust code, it must run correctly (without UB) for all possible choices of parameters.

This is very unlike UB, which is typically formalized by some error condition in the abstract machine that is used to specify the possible behaviors of a Rust program.

There definately is code that relies on a reference to the inner field not being able to affect the outer option. I presume that my Options never become None from out from under me, and when I'm already in unsafe code, I will do manual optimizations that rely on that being the case

This thread is not about assumptions that unsafe code authors can make about unknown safe code. This thread is about assumptions that the compiler can make about arbitrary (safe or unsafe) code.

Generally speaking, right now if you pass a &mut T to a (potentially arbitrary) unsafe function, you got the &mut T from out of an option, and T either has a niche, or is a dependant type that may have a non-hidden niche, you can't assume the reference is still safe to use.

(Again, these are not "dependent types", which means "types that depend on values". We call functions where we do not know the concrete T generic functions in Rust.)

You are conflating "reasoning the unsafe programmer can make about its environment" with "reasoning the compiler can make about unknown code". Unsafe code that calls unknown safe code can certainly rely on that code not "messing" with the niche. This is part of soundness. But achieving the same for the compiler is a lot harder, and much less necessary.

[chorman0773]

This thread is about assumptions that the compiler can make about arbitrary (safe or unsafe) code.

The specification is a bi-directional contract, by your own admission. The reasoning I can make about surrounding code which can perform an arbitrary action and the reasoning compilers can make are inherently connected (only extended by what I document as undefined behaviour, which is still undefined, not "can lead to undefined behaviour in safe code"). For example, I can reason that no surrounding code has undefined behaviour, because I don't need to reason about when it does. The original arguement was additionally brought for argumentative purposes, showing a user's perspective, the perspective which originally prompted the continued discussion, aruging that it has dual justitification.

No, not really. With unspecified behavior, if your assumption happens to be right, you actually get guaranteed correct compilation. This is probably an inconsequential difference for programmers, but when thinking about the fine details of these semantics in a formal way, it makes a big difference.

Also, the reason I argue it would still result in undefined behaviour is this, if a valid interpreation allows the physical memory to overlap, but remain logically distinct fields, then we can consider a write to a &mut t in Some(t) to only alter that t. This means that, for the Option<bool> case, unsafe{*(&mut b as *mut bool as *mut u8) = 2} would result in leaving 2 in b, so at the very least it would then be UB to read the original Option. Therefore, we have a valid interpretation under which the optimization is applied, but the result is undefined behaviour. If this is arguably invalid, then we could argue that not applying the optimization is similarily invalid, because it similarily results in undefined behaviour. This is what I mean by having undefined behaviour because of some wierd language lawyering, because there exists a valid choice for the unspecified behaviour of the language which results in that code having undefined behaviour, even if it is not explicitly designated as such. This is, in fact, is primarily not present in C or C++ (it is significantly harder to construct a situtation where this occurs, and is not always undefined), which makes it considerably harder to reason about what code does, because you can't be sure if there is actual undefined behaviour or the program is correct.

I would also add that you can make assumptions about the result of undefined behaviour, because a valid result of undefined behaviour is to assign some meaning to it (C++ compilers do it all the time, for example, they allow type-punning through unions, even though the strict rules of C++ make that undefined). If I know what my environment is, I can manipulate my code to cause undefined behaviour in a way that an extension actually gives meaning to, and this is done all the time in low-level software code, including compiler support libraries (I'm pretty sure libcore has some formal UB that rustc has assigned meaning to for that specific reason).

[RalfJung]

The specification is a bi-directional contract, by your own admission. The reasoning I can make about surrounding code which can perform an arbitrary action and the reasoning compilers can make are inherently connected (only extended by what I document as undefined behaviour, which is still undefined, not "can lead to undefined behaviour in safe code").

The contract between unsafe code and the compiler, and between unsafe code and the surrounding safe code, is not the same contract though, as I have spelled out a while ago and pointed out many times in this thread.

I would also add that you can make assumptions about the result of undefined behaviour, because a valid result of undefined behaviour is to assign some meaning to it (C++ compilers do it all the time, for example, they allow type-punning through unions, even though the strict rules of C++ make that undefined). If I know what my environment is, I can manipulate my code to cause undefined behaviour in a way that an extension actually gives meaning to, and this is done all the time in low-level software code, including compiler support libraries (I'm pretty sure libcore has some formal UB that rustc has assigned meaning to for that specific reason).

No, no you cannot. That is exactly what UB is about. It does not matter what the hardware does and there is no amount of assumptions that can salvage code with UB, short of auditing the generated assembly code (at which point you might just write assembly yourself).

Unless you are talking about language dialects here, like "Rust without that UB clause". But then you are opening yet another discussion that is even further from the topic at hand... this is derailing quickly, as you keep bringing more and more into this discussion. The thread is about normative Rust, not about language dialects. There is no way to have a structured discussion here if we cannot even have a coherent topic. If you want to question the foundations on which UB in Rust rests, please do not do it in the middle of a thread discussing a very specific technical question for one proposed aliasing model. That will just make it impossible to figure out later what anyone thought about the aliasing model.

I get the feeling this is leading nowhere, as we cannot even agree on the most basic principles of how to make the Rust type system and language precise, or on well-established principles such as Undefined Behavior. Without that shared ground, there is little point in discussing specifics I think.

I will only respond further here for things that have to do with the OP (scroll all the way up in case you forgot what this thread is about), for example:

• concrete examples for why we might want that code to be UB (in the form of optimizations this enables)
• concrete proposals for how to specify it as UB

If you take trouble with the justification for enum optimizations, please do so in a separate thread.

[digama0]

Question: It is not clear to me from this discussion whether it is part of the safety invariant that code cannot change a Some(t) to a None through the &mut T reference. I'm pretty sure that this is impossible with safe Rust code, but for unsafe rust code that is safe and certified good in the strongest way, in a safe fn in another crate, can this happen?

If the answer is "yes", then it seems we've broken ADTs being "algebraic data types" in the type theory sense. Once you are at the safe rust level, I would hope you can forget about all this unsafe hackery, and treat your mutation like it would be in a pure functional language. If you are familiar with Haskell's lens library, I think it gives a pretty good notion of what a reference is at the logical level: it is a way of getting and setting values inside a larger structure, with functions essentially of type A -> T and T -> A -> A where A is the structure we are borrowing from and T is the reference type. (Haskell lenses are generalized quite a bit beyond this but this isn't meant to be a detailed comparison, only a point of reference.)

Specifically as regards the OP example, it is possible to define a lens (well, a traversal) over the content of an option (or Maybe in Haskell's case), and this has the effect of replacing Just a with Just (f a) where f is the function that operates on the content of the reference. In particular, you never get a Nothing out of this.

Now I know that there are lots of ways that Rust is not Haskell, and in particular it does less to shield you from the "raw bits" as it were. But I do think that in safe code, at least, when we have all the invariants, you should be able to deal with the code in a more abstract way and still be correct. In short, I consider it very important that this behavior not be considered acceptable, even if we think it is an open question how to fix the model to make it UB.

[CAD97]

Question: It is not clear to me from this discussion whether it is part of the safety invariant that code cannot change a Some(t) to a None through the &mut T reference.

While it's not formally a safety invariant, it is definitely impossible to break this property in safe code.

This relies on something like writing a 0 into a &mut NonZeroU8. That's obviously not possible in safe code.

Additionally, any code receiving an &mut NonZeroU8, if it wishes to be sound, can break this property without extra preconditions. You can't leave an invalid value of T in the refered location, because you have no context where that location is, and if it happens to be one where that invalid T is a valid representation for some containing context.

It is only the capability of unsafe with full, complete knowledge of context that is in question here.

(My position is that it's definitely a desirable property, but one very difficult to specify beyond throwing up your hands, giving up defining it operationally, and saying "pointer provenance.")

[RalfJung]

Question: It is not clear to me from this discussion whether it is part of the safety invariant that code cannot change a Some(t) to a None through the &mut T reference.

Good question, thanks for asking! In my terminology, what you are asking about is the safety invariant of a type like fn(&mut T). What exactly is that function (not) allowed to do when we call it? What exactly is the safety contract that all safe code will uphold, and that unsafe code can both rely on and must make sure to uphold to its clients? This is really hard to make precise; to my knowledge there has been exactly one attempt of this so far, and you can read all about it in my PhD thesis. Unfortunately I do not model enum layout optimizations so I did not answer your question... but it would be reasonable to demand that this contract disallows a fn(&mut T) from messing with niches that are logically, but not physically, "outside" the T. You gave good reasons for why we would want this to be true.

However, there is no reason to make that contract identical with UB (and I think it would be rather ill-advised, as I argued before). And while making the contract precise will likely require very fancy logical machinery of the kind I use in my thesis, UB can and should be defined much simpler.

That's why I am so keen on not mixing up discussions about the safety contract and UB ("validity"). For the safety contract we are limited to informal, vague discussions if we do not want to require people to take PhD-level courses on program logics. For UB I think we can have precise technical discussions without requiring quite so much background.

[chorman0773]

I will only respond further here for things that have to do with the OP (scroll all the way up in case you forgot what this thread is about), for example

I have given that example, that maintaining a logical separation between the discriminant of an Option and it's field even where it is not or may not be physically located at different address allows a number of optimizations in a generic context that rely on reachability rules to be maintained. The example code shown previously could reasonably delete the assert as it otherwise lacks side effects. For exposition, in lccc, Option<T>s definition is exactly translated to (absent name choices)

generic<type %0> type union #niche_optimize Option{
    type struct{ #discriminant __esel: i1; #niche_payload __0: %0;} _Some;
    type struct {#discriminant __esel: i1;} _None;
};

As this shows, even though rust doesn't consider the discriminant a separate field, in the particular implementation, it is. The niche optimization would be one of the last transformations I perform on the code (it would be part of the reentrant cycle performing generic instantiation and reification). My goal is to assert that, regardless of %0 (which replaces T here) and its properties, a pointer to _Some.__0cannot modify __esel, which is what would result in a change of the variant from Some to None. Right now, this is a valid optimization for a type that isn't a niche-optimization candidate (either is a concrete or reified type that doesn't have a niche, or a generic type that is known to have a niche, such as *mut T (does generic even entirely cover every type that depends on a generic parameter)). In the previous example by digama0, assuming f(&mut t) is an optimization black-box, optimizing the read of the discriminant field from either side of f should be fine, and has the advantage of removing a conditional branch in the assert case.

Also, the specification for how to make it UB proposed is reasonable in my opinion, and I affirm it. When the lifetime of a mutable reference ends, or the scope of it ends, whichever is longer, the last value written through the reference, or any derivative pointer, must be valid for the type T, or the behaviour is undefined. This preserves the above optimization, as well as making sure it's basically impossible to observe an invalid value in a correct program, except maybe through that &mut.

[RalfJung]

When the lifetime of a mutable reference ends,

As I have laid out above, this is not a very well-defined notion -- and to my knowledge, with Polonious, there is not even such a thing as "the point where a lifetime ends". With Polonious, a lifetime is not some region of code, but some set of memory locations a reference could point to, and such sets do not have an "end".

[digama0]

As I have laid out above, this is not a very well-defined notion -- and to my knowledge, with Polonious, there is not even such a thing as "the point where a lifetime ends". With Polonious, a lifetime is not some region of code, but some set of memory locations a reference could point to, and such sets do not have an "end".

That's at the code level, but AFAIK it still remains the case that lifetimes still correspond to a contiguous temporal region in the execution trace of the program. In particular, a lifetime can be said to "end" in SB when some/all of the relevant borrow stack items are popped due to an access further up the stack. Hence my earlier attempt to use this to trigger a write-back effect, as this is the point at which up stack references become able to access the memory again.

[chorman0773]

On Sun, 18 Oct 2020 at 12:30, Mario Carneiro notifications@github.com wrote:

As I have laid out above, this is not a very well-defined notion -- and to my knowledge, with Polonious, there is not even such a thing as "the point where a lifetime ends". With Polonious, a lifetime is not some region of code, but some set of memory locations a reference could point to, and such sets do not have an "end".

That's at the code level, but AFAIK it still remains the case that lifetimes still correspond to a contiguous temporal region in the execution trace of the program. In particular, a lifetime can be said to "end" in SB when some/all of the relevant borrow stack items are popped due to an access further up the stack. Hence my earlier attempt to use this to trigger a write-back effect, as this is the point at which up stack references become able to access the memory again.

Yeah, this is what I referred to, the lifetime at execution time. The SB interpretation could be that. I have a similar mechanism for tracking the runtime lifetime of references/pointers, which would have the same effect.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/rust-lang/unsafe-code-guidelines/issues/84#issuecomment-711276673, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABGLD242547CRUQ5THFQM4DSLMJZBANCNFSM4GUT5QKA .

[RalfJung]

That's at the code level, but AFAIK it still remains the case that lifetimes still correspond to a contiguous temporal region in the execution trace of the program. In particular, a lifetime can be said to "end" in SB when some/all of the relevant borrow stack items are popped due to an access further up the stack. Hence my earlier attempt to use this to trigger a write-back effect, as this is the point at which up stack references become able to access the memory again.

The problem is that there is this weird time when some of the relevant items have been removed but others still exist.

I guess what I am saying is, there's a lot of unknowns here and things that would need exploring. I personally think this is too complex compared to the optimizations it justifies, so I am unlikely to be doing that exploring. But if someone else figures out all the details, we'd certainly learn something from that. :)

[digama0]

Well, that sounds promising, compared to your usual strategy of immediately shooting down my poorly thought out ideas. :grin:

Regarding that weird in between time (which I hedged with the "some/all" bit), based on borrow-checker-sourced intuitions, I would say that it is the first invalidation of a byte that is really the critical point, because that is when you would see the region end.

let mut x = [0; 30];
let y = &mut x;
let z = &mut *y;
y[0] = 0; // invalidates z[0] but not other bytes
z[1] = 1; // still an error

I had to run a test just now, but it turns out that the borrow checker still has the same error with a tuple instead of an array:

let mut x = (0, 1);
let y = &mut x;
let z = &mut *y;
y.0 = 0; // invalidates z.0 but not other bytes
z.1 = 1; // still an error

I thought at first that rust would split the borrow, but I guess that doesn't apply here where we directly reborrow the tuple reference.

But as a result of this, I think it is impossible from safe code to tell if SB had a rule along the lines "when a Uniq is popped from the stack, all other copies of it in other bytes are removed from their respective stacks", so that mutable borrows are never removed in stages.

We can of course write unsafe code that can see the difference:

let mut x = (0, 1);
let y = &mut x;
let y2: *mut _ = y;
let z = &mut *y;
unsafe { (*y2).0 = 0 };
z.1 = 1; // UB? Only if the line above invalidates all the bytes of z

More to the point, if this is not UB then we can make a write-back at the first invalidation insufficient to ensure that the referent is well typed at the end of the block:

let mut x = (false, false);
let y = &mut x;
let y2: *mut _ = y;
let z = &mut *y;
unsafe { (*y2).0 = true }; // z.0 is invalidated here
unsafe { *(&mut z.1 as *mut _ as *mut u8) = 2 };
drop(x); // x contains (true, 2)

Assuming we want to keep the piecemeal invalidation, a simple option would be to perform the full write-back on every invalidation of a byte of z. That means two write-backs in this example, one with (true, false) and one with (true, 2) (where the second would cause UB by being ill-typed for the access). But this doesn't really work, because then we are accessing the first byte of z after it has been invalidated, which is UB right there, even without any type mismatch. (We have no guarantee that the memory hasn't already been repurposed for another type by that point.)

I'll come back to this later, to explore the other options: write-back on last invalidation, invalidating all the bytes at once, performing a partial write-back(?) per byte. For the piecemeal invalidations, it is worth thinking about what properties are supposed to hold of the bytes reclaimed from the borrow.

[chorman0773]

Based on request and suggestion of @RalfJung in #253, I have a concrete example of the transformation applied (and the rationale). This is based on the initial code snipet posted at the top of the thread, and shows the xir (xlang ir, used by lccc) before and after the optimization is applied (and only a few other, similar optimizations, but note that it is not fully optimized), using the definition I showed above for Option<T> in the IR. For completness, the code sample being translated is

fn main() { unsafe {
    let mut x = Some(&0); 
    match x {
        Some(ref mut b) => {
            let u = b as *mut &i32 as *mut usize;
            // Just writing into a *mut u8
            *u = 0;
        }
        None => panic!(),
    }
    assert!(x.is_some());
} }

Note: the ir is a stack-based load-store architecture with objects and lvalues as the primitive unit. types on the stack (read Left to Right for head to tail) are shown each line

declare function main() -> (){
    let _0: Option<*readonly dereferenceable(4)  bound(#0) i32>;
    begin tag #0
    begin storage _0
    local _0 // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    dup // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>,lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    member struct _Some  // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0, lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    member struct __esel  // Stack [lvalue i1, lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    const i1 0 // Stack [i1,lvalue i1,lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    assign  // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    member struct _Some //  [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0]
    member struct __0 // [lvalue *readonly dereferenceable(4)  bound(#0) i32]
    const i32 0 // [i32, lvalue *readonly dereferenceable(4)  bound(#0) i32]
    temporary #0 // [lvalue i32, lvalue *readonly dereferenceable(4)  bound(#0) i32]
    lock shared #0 derive *readonly dereferenceable(4)  bound(#0) i32  address_of [*readonly dereferenceable(4)  bound(#0) i32, lvalue *readonly dereferenceable(4)  bound(#0) i32]
    assign // [] 
    local _0 // [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
     member struct _Some  //  [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0] 
    dup // [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0, lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0] 
    member sturct __esel // [lvalue i1, lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0] 
    as_rvalue // [i1, lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0] 
    begin block $1 
    switch [i1 0: @0, i1 -1: @1]
    target @0 [lvalue Option<*readonly dereferenceable(4) bound(#0) i32>::0 ] // [lvalue Option<*readonly dereferenceable(4) bound(#0) i32>::0 ]
    member struct __0 //  [lvalue *readonly dereferenceable(4) bound(#0) i32]
    begin tag #1 
    lock exclusive #1 derive *noalias dereference_write(8) bound(#1) *readonly dereferenceable(4) bound(#0) i32 address_of // [*noalias dereference_write(8) bound(#1) *readonly dereferenceable(4) bound(#0) i32]
    derive **readonly dereferenceable(4) bound(#0) i32 // [**readonly dereferenceable(4) bound(#0)]
    derive *u64 // [*u64]
    indirect // [lvalue u64]
    const uint(64) 0 // [lvalue u64,u64]
    assign // [] 
    end tag #1 // []
    exit block $1 0 // []
    target @1 [] // []
    const global_address ::core::panicking::panic::#signature(&str)->!  // [*fn noreturn (*readonly u8,u64)->!]
    const uint(64) 18 [u64,*fn noreturn (*readonly u8,uint(64))->!]
    const address_of  string_literal "Panicked at main.rs:9" // [ *readonly u8,u64,*fn noreturn (*readonly u8,u64)->!]
    call fn noreturn (*readonly u8,u64)->! // []
    exit block $1 0
    end block $1 []
    local _0 // [lvalue Option<*readonly dereferenceable(4) i32>]
    member struct _Some // [lvalue Option<*readonly dereferenceable(4) i32>::0]
    member struct __esel // [lvalue i1]
    as_rvalue // [i1]
    bnz @2 
    exit block $0 0
    target @2 [] // []
    const global_address ::core::panicking::panic::#signature(&str)->!  // [*fn noreturn (*readonly u8,u64)->!]
    const uint(64) 42 [u64,*fn noreturn (*readonly u8,uint(64))->!]
    const address_of  string_literal "Assertion failed: x.is_some() at main.rs:11" // [ *readonly u8,u64,*fn noreturn (*readonly u8,u64)->!]
    call fn noreturn (*readonly u8,u64)->! // []
    end storage _0
    end tag #0
}

After the dead branch elimination, the first panic is removed. In the proposed optimization, both panics would be removed by the same optimization (because if it wasn't None beforehand, and the pointer to the __0 field can't access __esel, then it must still be some after the transformation). This also allows a dead store elimination pass to remove the initial store to __esel (since it's never read, though this has marginal effects, as the __esel field would be merged into the __0 field, so the store would be elimitated anyways), and eventually, during type lowering, the outer option can be deleted because it's always Some.

declare function main() -> (){
    let _0: Option<*readonly dereferenceable(4)  bound(#0) i32>;
    begin tag #0
    begin storage _0
    local _0 // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    dup // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>,lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    member struct _Some  // Stack [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0, lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    member struct _Some //  [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0]
    member struct __0 // [lvalue *readonly dereferenceable(4)  bound(#0) i32]
    const i32 0 // [i32, lvalue *readonly dereferenceable(4)  bound(#0) i32]
    temporary #0 // [lvalue i32, lvalue *readonly dereferenceable(4)  bound(#0) i32]
    lock shared #0 derive *readonly dereferenceable(4)  bound(#0) i32  address_of [*readonly dereferenceable(4)  bound(#0) i32, lvalue *readonly dereferenceable(4)  bound(#0) i32]
    assign // [] 
    local _0 // [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>]
    member struct _Some  //  [lvalue Option<*readonly dereferenceable(4)  bound(#0) i32>::0] 
    member struct __0 //  [lvalue *readonly dereferenceable(4) bound(#0) i32]
    begin tag #1 
    lock exclusive #1 derive *noalias dereference_write(8) bound(#1) *readonly dereferenceable(4) bound(#0) i32 address_of // [*noalias dereference_write(8) bound(#1) *readonly dereferenceable(4) bound(#0) i32]
    derive **readonly dereferenceable(4) bound(#0) i32 convert reinterpret // [**readonly dereferenceable(4) bound(#0)]
    derive *u64 // [*u64] convert reinterpret
    indirect // [lvalue u64]
    const uint(64) 0 // [lvalue u64,u64]
    assign // [] 
    end tag #1 // []
    local _0
    member struct _Some
    as_rvalue
    pop
    exit block $0 0 // []
    end storage _0
    end tag #0   
}

In this transparent case, this UB would actually allow the entire function to be removed as unreachable code. The 4 lines before the exit block $0 loads the _Some member, which has an invalid value because _Some.__0 has an invalid value. Through value store tracking, it can prove that null is stored (0 is transmuted to *readonly deferenceable(4) bound(#0) i32, which yields a null pointer), which is invalid, so it can replace that segment with const undef invalid Option<...>::0 which is xir for "unreachable code" (specifically, it produces the invalid value of whatever type you want, it's mere existance is UB).

[RalfJung]

@digama0 thanks for spelling that out!

Assuming we want to keep the piecemeal invalidation

So the alternative you have in mind here is that references always get entirely invalidated all at once? That would be strictly more UB than we have currently... so we'd have to figure out if this is not incompatible with too much unsafe code. On the other hand, this could provide the chance to significantly reduce the amount of state we need to track, if we do not need to track everything per-location any more! That would be great for Miri. I will definitely consider this for the next version of Stacked Borrows.

More to the point, if this is not UB then we can make a write-back at the first invalidation insufficient to ensure that the referent is well typed at the end of the block:

I am not entirely sure what you mean by "write-back" here, do you mean the act of checking that some memory still conforms to its validity invariant? I did not think anything would be "written" there.

unsafe { (*y2).0 = true }; // z.0 is invalidated here

In fact this line is UB because creating z invalidated y2... or did you mean z to reborrow from y2 instead?

That means two write-backs in this example, one with (true, false) and one with (true, 2) (where the second would cause UB by being ill-typed for the access). But this doesn't really work, because then we are accessing the first byte of z after it has been invalidated, which is UB right there, even without any type mismatch. (We have no guarantee that the memory hasn't already been repurposed for another type by that point.)

We probably do have to check this on each partial invalidation, because even when just a part of the parent pointer is being used again, we will want to be sure that it is valid. OTOH, we might be in a situation where even parts of the parent pointer are already invalid while parts of the child pointer are still valid... that seems problematic? Is that what you are referring to here?

[RalfJung]

So the alternative you have in mind here is that references always get entirely invalidated all at once? That would be strictly more UB than we have currently... so we'd have to figure out if this is not incompatible with too much unsafe code.

Specifically, here is the kind of code this would rule out:

fn foo(x: &mut (i32, i32)) {
  let raw = x as *mut _;
  x.0 = 2;
  (*raw).1 = 3; // UB because the above line entire invalidates `raw`.
}

[RalfJung]

@chorman0773 Without fully grasping your IR, is it fair to say that you want to optimize that code to remove the assertion at the end? I.e., you end up with

fn main() { unsafe {
    let mut x = Some(&0); 
    match x {
        Some(ref mut b) => {
            let u = b as *mut &i32 as *mut usize;
            // Just writing into a *mut u8
            *u = 0;
        }
        None => unreachable_unchecked(), // the other unreachable branch you mentioned?
    }
    // assert!(x.is_some()); <- assert cannot fail, and thus can be removed.
} }

For this particular program of course this is rather silly, but the more interesting case is replacing the Some arm by calling some unknown function and giving it b.

[chorman0773]

is it fair to say that you want to optimize that code to remove the assertion at the end?

Yes, that would be the goal. x.is_some() has no side effects, and with the optimization, is known to be a tautology, so the assert is dead code. The None branch is elimitated because at the original match, x is known to be Some(t). Technically, the assert is replaced with something effectively the same as core::hint::assume(x.is_some()) which is what the steps at the bottom were doing, so as to preserve the use of x in optimizations.

the more interesting case is replacing the Some arm by calling some unknown function and giving it b.

Yeah, ideally, I'd be able to make the same optimization replacing the arm with, say, a call to core::hint::black_box() (which is respected on lccc, though remains a best effort when the code generator also does its own optimizations).

[digama0]

More to the point, if this is not UB then we can make a write-back at the first invalidation insufficient to ensure that the referent is well typed at the end of the block:

I am not entirely sure what you mean by "write-back" here, do you mean the act of checking that some memory still conforms to its validity invariant? I did not think anything would be "written" there.

That is what I mean. Concretely I don't know if it needs to be a write access or a read access or some other category entirely, but what it is doing is ensuring that the memory is valid at the same type as the original type of the borrow. No memory is changed by this operation, and even the borrow stacks don't have to change (beyond what they already do, in this case when a write access token is popped).

unsafe { (*y2).0 = true }; // z.0 is invalidated here

In fact this line is UB because creating z invalidated y2... or did you mean z to reborrow from y2 instead?

Ah, you are right. My intention was to have y2 be "the same" as y with only the effects of pointer casting, not reborrows. Having z borrow from y2 instead of y should be sufficient to fix the example.

We probably do have to check this on each partial invalidation, because even when just a part of the parent pointer is being used again, we will want to be sure that it is valid. OTOH, we might be in a situation where even parts of the parent pointer are already invalid while parts of the child pointer are still valid... that seems problematic? Is that what you are referring to here?

Yes, that is my worry. It means that this "write-back" operation (or better, "re-validation") needs to be able to validate a memory segment which has holes punched in it by invalidated bytes, to ensure at least that the bytes that are visible are valid at any subfield type that corresponds to a contiguous and valid subpart of the bytes. For example, if T = (u32, bool) and bytes 0,3,4 are visible with values [0, -, -, 42, true] then we need to at least validate that true is valid for bool, and we might also validate that there exist bytes completing [0, -, -, 42] such that the result is a valid u32, although that sounds like a bit of headache to define.

[RalfJung]

and we might also validate that there exist bytes completing [0, -, -, 42] such that the result is a valid u32, although that sounds like a bit of headache to define.

That is indeed the case I am most worried about... in particular if you think of cases like [0, -, -, -] and whether this is a valid NonZeroU32.

[jessa0]

This code (see this issue) in the zeroize crate almost matches one of your examples, setting the memory behind a generic T in an Option<T> to a possibly invalid bit pattern and setting it back to a valid one afterward, but uses ptr::write_volatile to perform the writes of the invalid bit pattern. I'm not personally clear on the guarantees of volatile writes in Rust, but does this change the consideration of whether the code is UB or not?

[thomcc]

Hmm, I think volatile does not change the consideration of this sort of thing. At least in C, it just makes the read/write visible operations to the abstract machine. I think Rust intends to adopt similar semantics here, but could be wrong.

Assuming I'm not wrong, it wouldn't change whether or not the read/write is UB, just whether or not the compiler is free to remove them if they aren't UB (of course, it becomes free to remove them if they're UB, although in practice compilers probably would err on the side of not touching them).

That said, it's still an open question as to if this is UB. You should probably tend towards not doing stuff like this, but I'm unsure about the options available to zeroize given its guarantees (I've spent 0 time thinking about them).

[RalfJung]

Interesting. That code is very careful to re-establish any possible invariants before returning control to other code... but some of the proposals above for making "invalid not-used-again values" UB would probably also make this UB.

I view this as an argument that we should only assert validity on typed copies.

Hmm, I think volatile does not change the consideration of this sort of thing.

Correct.

[elichai]

Interesting. That code is very careful to re-establish any possible invariants before returning control to other code... but some of the proposals above for making "invalid not-used-again values" UB would probably also make this UB.

Does it change anything if the problematic code is separated into it's own function that doesn't contain live references?

ie

fn zeroize_raw<T: Zeroize>(ptr: *mut Option<T>) {
    intrinsics::volatile_set_memory(ptr.cast::<u8>(), 0, mem::size_of::<Option<T>>());
    ptr.write_volatile(None);
}

(this one on its own seem correct/safe)

but then the caller will be:

fn zeroize<T: Zeroize>(opt: &mut Option<T>) {
    unsafe {zeroize_option(opt)};
}

[RalfJung]

I don't think function calls would make a difference. But this depends a lot on the details and details are severely lacking from the proposals that would make anything UB here.

[sollyucko]

Not sure if this has been mentioned yet, but what about only requiring values to be valid when either it is read (including by implicit drop), or when the lifetime of a mutable reference pointing to it ends? (This would check the invariants of the type of the read/reference, not the write.)

This would make the first example UB, at the end of the match body, when the reference from the ref mut ends, but make the zeroize example valid, since there are no reads or reference endings while the value is invalid.

[CAD97]

The main problem with that is defining "lifetime of a borrow ends" operationally. In stacked borrows as currently implemented, the borrow stack of a location is only updated when a borrow of that location is used. The e.g. Uniq tag isn't popped until an e.g. Shr tag beneath it is used to access the value, independent of when the scope of the borrow checker ends.

I suppose you could just delay the validity check until the tag is actually popped (which would always happen before the location is freed), but that feels like spooky action at a distance to me, to fail that late. But maybe that's also the best operational definition of "fix it before you leave?"