Tracking Issue: Automatically ensure validity invariants of unsafe operations

[celinval]

Requested feature: Kani should automatically check if unsafe operations can break validity invariants which can trigger UB. According to the Rust reference, producing an invalid value, even in private fields and locals is undefined behavior. "Producing" a value happens any time a value is assigned to or read from a place, passed to a function/primitive operation or returned from a function/primitive operation.
Use case: Checking that unsafe code doesn't trigger UB.
Link to relevant documentation (Rust reference, Nomicon, RFC): Rust UB reference and definition of validity invariant.

Test case:

#[kani::requires(!ptr.is_null())]
#[kani::ensures(!result.as_ptr().is_null())] // Compiler warns that this should always be nonnull().
pub unsafe fn new_unchecked<T>(ptr: *mut T) -> NonNull<T> {
    NonNull::<T>::new_unchecked(ptr)
}

Since it is not possible to programmatically verify undefined behavior, Kani compiler must insert checks before the UB actually happens.

Tasks

• RFC for UB checks
• Implement basic checks
• Mitigate checks that aren't implemented yet
• Add tests

[celinval]

Note for self: We should use implement rust-lang/project-stable-mir#58 and use the valid range from Scalar type. We would need to traverse structures to add proper checks. Maybe experiment with transforming StableMIR instead of regular MIR. This would play well since we want the monomorphic version to add validity checks. Here are a few good places to see how rustc / MIRI handle these things:

• ValidityVisitor: https://github.com/rust-lang/rust/blob/master/compiler/rustc_const_eval/src/interpret/validity.rs#L655
• List of errors: https://github.com/rust-lang/rust/blob/d8b00690ec3aa2d2fb0d3eb00e862195501186f9/compiler/rustc_const_eval/messages.ftl#L416-L474 (Some are not relevant for this issue)