Pre-RFC: Unsafe reasons

[scottmcm]

@chrefr

For example, you can call the above function like the following:

unsafe {
    my_unsafe_fn().unsafe(reason1, reason2);
}

TBH, I think needing them in the middle of the call like that will defacto result in people being unwilling to actually list out the reasons in nice separable ways, because it'll just be so ugly to see them all through the middle of the logic.

I do like the direction of having to meet all the requirements -- not just the ones you remembered -- but think it should work differently so while you still need to cover them, you don't need to repeat them endlessly.

For example, I think of code like this:

let a = ptr::read(x);
let b = ptr::read(y);
ptr::write(x, b);
ptr::write(y, a);

And, looking at the good safety comments on those functions, I'm really not convinced that I want to have to see it as

unsafe {
    let a = ptr::read(x).unsafe(valid_for_read, properly_aligned, initialized_for_type);
    let b = ptr::read(y).unsafe(valid_for_read, properly_aligned, initialized_for_type);
    ptr::write(x, b).unsafe(valid_for_write, properly_aligned);
    ptr::write(y, a).unsafe(valid_for_write, properly_aligned);
}

when that still didn't cover the "oh yeah and you better not extra-drop those return values from read".

My current thinking instead is I'd prefer something like sketched here:

Detect and Fix Overscope unsafe Block

TBH, I think we need tooling to better help computers help double-check that humans at least considered everything, even if it can't check the proof itself. (Though stuff like kani being able to check the proof would also be nice!) And my hope is that in doing that, we do it in a way that does allow big-scoped unsafe blocks again, because it would allow "proving" the thing once, but in a smart way. Like if you have a local let p: *mut SomethingCopy = ...;, then there shouldn't be a need for t…

Where rather than needing to repeat things, maybe I can instead have

unsafe
    [properly_aligned(x), "this came from a reference so it must be"]    
    [properly_aligned(y), "this came from a reference so it must be"]    
    [...]
{
    let a = ptr::read(x);
    let b = ptr::read(y);
    ptr::write(x, b);
    ptr::write(y, a);
}

where the function was defined with something like

unsafe
    [properly_aligned(ptr), "it must be normally ABI aligned for its pointee type"]
    [readable(ptr, 1), "must be able to read one element of its pointee type"]
    [...]
fn read<T>(ptr: *const T) -> T;

and the compiler makes sure I "proved" the necessary things to be able to call it, doing proper handling for the variable names involved.

(Maybe readable(in_ptr, count) and writeable(out_ptr, count) would exist on copy_nonoverlapping, for example, as well, to cover cross-parameter requirements.)