The custom sysroot build for the MIR Linker introduced by #1717 builds the standard library in debug mode. This enables a bunch of safety checks and debug assertions from the standard library. Some of these checks are for intrinsics safety checks. The issues here are:
- A lot of these checks make our intrinsics checks redundant.
- The
std checks are added before actually calling the intrinsic and they are not super user friendly.
For example, the following testcase from the expected suite:
|
#[kani::proof] |
|
fn test_copy_nonoverlapping_unaligned() { |
|
let arr: [i32; 3] = [0, 1, 0]; |
|
let src: *const i32 = arr.as_ptr(); |
|
// Passing `max_count` is guaranteed to overflow |
|
// the count in bytes for `i32` pointers |
|
let max_count = usize::MAX / 4 + 1; |
|
|
|
unsafe { |
|
let dst = src.add(1) as *mut i32; |
|
core::intrinsics::copy_nonoverlapping(src, dst, max_count); |
|
} |
|
} |
Without the MIR Linker, it fails with the following error:
Failed Checks: copy_nonoverlapping: attempt to compute number in bytes which would overflow
With the MIR Linker, the error is:
Failed Checks: called `Option::unwrap()` on a `None` value
This happens because of the std check is_nonoverlapping which has a call to checked_mul().unwrap(). The checked_mul() is None in the overflow scenario.
The custom sysroot build for the MIR Linker introduced by #1717 builds the standard library in debug mode. This enables a bunch of safety checks and debug assertions from the standard library. Some of these checks are for intrinsics safety checks. The issues here are:
stdchecks are added before actually calling the intrinsic and they are not super user friendly.For example, the following testcase from the
expectedsuite:kani/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs
Lines 6 to 18 in 78761bd
Without the MIR Linker, it fails with the following error:
With the MIR Linker, the error is:
This happens because of the std check
is_nonoverlappingwhich has a call tochecked_mul().unwrap(). Thechecked_mul()is None in the overflow scenario.