Enforce unsafe blocks to have comments explaining why the required invariants hold

[WalterSmuts]

What it does

This is the users side of the missing_safety_doc lint. Enforce each block of unsafe to have a corresponding comment explaining why all the calls to unsafe meet the invariants required by the Safety section of the unsafe fn.

Motivation

unsafe rust relaxes some of the invariant that safe rust enforces. This is to allow the programmer to express some operations that the compiler cannot prove will be memory safe. The point being highlighted is that unsafe rust is not a mechanism the programmer can use to do unsafe things, but rather a promise to the compiler that the code is safe even though the compiler cannot prove it. The burden of proof then lies on the programmer [and reviewers] to ensure that all the invariants that the function requires to hold, does hold. This does not mean the programmer cannot provide an incorrect proof, but it does make the following less likely:

• The programmer ignores the requirements of an unsafe function.
• Incorrect logic in a proof used by the programmer slips past the reviewer because the logic is now explicit and part of the code.
• These invariants are also less likely to be overlooked when modifying the program because they are part of the source code.

Stricter variant

A possible future improvement would update the missing_safety_doc lint to require the documentation to provide a list of the invariants required by the unsafe fn, each with an identifier - e.g. dangling_pointer and an explanation of what it entails. The missing_safety_proof lint would then provide the same list of identifiers, but instead of explaining the required invariant would contain a proof of why that invariant holds at that point in the code. The documentation can then easily provide links from the proof to the explanation via the identifier.

Some Safety documentation is already in list form, e.g. pointer as_ref method:

    /// # Safety
    ///
    /// When calling this method, you have to ensure that *either* the pointer is null *or*
    /// all of the following is true:
    ///
    /// * The pointer must be properly aligned.
    ///
    /// * It must be "dereferenceable" in the sense defined in [the module documentation].
    ///
    /// * The pointer must point to an initialized instance of `T`.
    ///
    /// * You must enforce Rust's aliasing rules, since the returned lifetime `'a` is
    ///   arbitrarily chosen and does not necessarily reflect the actual lifetime of the data.
    ///   In particular, while this reference exists, the memory the pointer points to must
    ///   not get mutated (except inside `UnsafeCell`).
    ///
    /// This applies even if the result of this method is unused!
    /// (The part about being initialized is not yet fully decided, but until
    /// it is, the only safe approach is to ensure that they are indeed initialized.)
    ///

Lint Name

missing_safety_proof

Category

style - Same as missing_safety_check although I can see both moving to correctness.

Advantage

• More likely to have users of unsafe fn's read the Safety documentation of the function they're using.
• Explaining the reason invariants hold forces the programmer to think critically about whether they really do hold in their case.
• The logic used by the programmer to prove that the unsafe block is safe is part of the code and directly observable by a reviewer. The reviewer then has a much easier time verifying that the proof actually holds.
• Subsequent changes to the code will be less likely to break the invariants required by the functions if the assumptions are written explicitly in the vicinity of the code being changed.

Drawbacks

• Only useful if folks use the missing_safety_check lint. Currently this is one of the most commonly ignored lints, so this is legitimately a concern.
• Extra effort required by user of unsafe functions to explain why the invariants hold.
• Unclear how a single unsafe block containing multiple unsafe fn's should be handled. This could result in one of the unsafe operations being overlooked while another is being explained.
• Unclear how this lint would evolve into the stricter variant where each invariant is addressed separately.

Example

use std::ptr::null;

struct MyType {}

fn main() {
    let my_type = MyType {};
    let reference: &MyType = &my_type;
    #[allow(unused_assignments)]
    let mut pointer = reference as *const MyType;
    #[allow(clippy::drop_non_drop)]
    drop(my_type);
    pointer = null();
    let _valid_reference = unsafe { pointer.as_ref() };
}

Could be written as:

use std::ptr::null;

struct MyType {}

fn main() {
    let my_type = MyType {};
    let reference: &MyType = &my_type;
    #[allow(unused_assignments)]
    let mut pointer = reference as *const MyType;
    #[allow(clippy::drop_non_drop)]
    drop(my_type);
    pointer = null();

    // # Safety proof
    // Three lines above I set the pointer to null.
    let _valid_reference = unsafe { pointer.as_ref() };
}

[Jarcho]

This is covered by undocumented_unsafe_blocks.

[WalterSmuts]

Wow, this is almost exactly what I had in mind. And kudos to @Serial-ATA for implementing it!

I do have a couple of questions regarding some of the choices made:

1. Why the discrepancy between the style of missing_safety_doc and undocumented_unsafe_blocks?

    // SAFETY:
    vs
    /// # Safety

I understand one is meant for documentations /// and one is meant for comments // so the # in missing_safety_doc represents a heading in markdown and is not appropriate for a comment. The required colon : and required lack of colon in the other seems unnecessary to have different along with the capitalisation mattering in the one and not the other.

2. Why is the missing_safety_doc lint at the allow level? Not enough consensus that this is useful to warn on per default?

3. Any thoughts on the suggestion of a stricter and more structured variant of both of these lints? Let me know if more motivation is required.

[Jarcho]

missing_safety_doc matches the formatting for markdown headers. undocumented_unsafe_blocks matches other comment markers like TODO, FIXME and such.

undocumented_unsafe_blocks was conservatively placed as a restriction lint. I don't think there's been any discussion about using a different category.

A structured version could be interesting, but also far from trivial. The Safety section on functions is just prose describing the preconditions, not something machine parsable. It would be possible to have a pair of lints require a formatted doc section and a formatted comment section, but I'm not sure if it would end up widely used enough to be generally useful.

[Alexendoo]

Closing since this is implemented as undocumented_unsafe_blocks