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