UB checks should fail verification for harnesses annotated with #[should_panic] #3571
Description
I believe we need to create a new UB check property category, and audit the compiler to use the new category for UB instrumentation. The #[should_panic] implementation should take this new category into consideration. Note that this is already the case for some UB's checks.
The motivation is to allow users to write safety harness that succeed as long as no UB is detected.
Here is a small example of how Kani inconsistencyt:
#[kani::proof]
#[kani::should_panic]
pub fn rust_ub_fails() {
let ptr = 0 as *const u32;
let _invalid_ref = unsafe { &*ptr };
}
#[kani::proof]
#[kani::should_panic]
pub fn rust_ub_should_fail() {
let ptr = 10 as *const u32;
let _invalid_read = unsafe { *ptr };
}Running this with kani:
$ kani --output-format terse ub_checks.rs
Kani Rust Verifier 0.55.0 (standalone)
Checking harness rust_ub_should_fail...
VERIFICATION RESULT:
** 1 of 2 failed
Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment
File: "ub_checks.rs", line 12, in rust_ub_should_fail
VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
Verification Time: 0.020638932s
Checking harness rust_ub_fails...
VERIFICATION RESULT:
** 1 of 2 failed
Failed Checks: dereference failure: pointer invalid
File: "ub_checks.rs", line 5, in rust_ub_fails
VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
Verification Time: 0.018083837s
Summary:
Verification failed for - rust_ub_fails
Complete - 1 successfully verified harnesses, 1 failures, 2 total.