Skip to content

Is "validity on typed copy" enough? #189

Closed
@RalfJung

Description

@RalfJung

With #175, I am basically proposing to make the "validity invariant" arise from the bytelist -> value -> bytelist conversion that (in my view) happens any time a "typed cooy" is performed (in particular every time the assignment operator is executed). This also exactly matches when Miri currently checks validity.

It is conceivable, however, to be even more aggressive about this. Consider:

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

Is this code UB? On the one hand, the last line stores a 0 into what could be thought of as a pointer to a NonZeroU32. On the other hand, if we look at this locally / operationally, all we are doing is writing a 0 to a *mut u32. We never "look" at that 0 at type NonZeroU32. Miri sees no UB here.
(NonZeroU32 is just an example; this can happen with basically any type that has a niche.)

This code certainly makes some layout assumptions, like Option<NonZeroU32> being basically the same as u32, but that is something we already or almost guarantee. And certainly the following code is 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);
}

So, is there anything wrong with the first code? Do we want that (or some variant thereof) to be UB? Is there an optimization that could gain us?

(I thought we already had an issue about this somewhere, and I recall discussing this with @rkruppe, but I cannot find an issue so maybe it was just in chat.)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions