simd_div and simd_rem don't check for overflow cases

[adpaco-aws]

Both simd_div and simd_rem are missing an overflow check that is done for the regular division operators (i.e., / and %). Consider this example:

#![feature(repr_simd, platform_intrinsics)]

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);

extern "platform-intrinsic" {
    fn simd_div<T>(x: T, y: T) -> T;
    fn simd_rem<T>(x: T, y: T) -> T;
}

#[kani::proof]
fn test_normal() {
    let val_1: i32 = kani::any();
    let val_2: i32 = kani::any();
    kani::assume(val_1 == i32::MIN);
    kani::assume(val_2 == -1);
    let result: i32 = val_1 / val_2;
}

#[kani::proof]
fn test_simd() {
    let val_1 = kani::any();
    kani::assume(val_1 == i32::MIN);
    let values_1 = i32x2(val_1, val_1);
    let val_2 = kani::any();
    kani::assume(val_2 == -1);
    let values_2 = i32x2(val_2, val_2);
    let result = unsafe { simd_div(values_1, values_2) };
}

This is verification output for test_normal:

RESULTS:
Check 1: test_normal.assertion.1
         - Status: SUCCESS
         - Description: "attempt to divide by zero"
         - Location: tests/kani/Intrinsics/SIMD/Operators/div_rem.rs:19:23 in function test_normal

Check 2: test_normal.assertion.2
         - Status: FAILURE
         - Description: "attempt to divide with overflow"
         - Location: tests/kani/Intrinsics/SIMD/Operators/div_rem.rs:19:23 in function test_normal

Check 3: test_normal.division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"
         - Location: tests/kani/Intrinsics/SIMD/Operators/div_rem.rs:19:23 in function test_normal

This is the verification output for test_simd:

Check 1: division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"

Check 2: division-by-zero.2
         - Status: SUCCESS
         - Description: "division by zero"

There are several concerns here:

• The overflow check is missing when using the vector operator.
• The "attempt to divide by zero" check is missing when using the vector operator.

Note that Kani tweaks the output a little bit in this example. In particular, for properties with class division-by-zero it omits the variables, the original outputs are:

Check 3: test_normal.division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero in var_10 / var_11"
         - Location: tests/kani/Intrinsics/SIMD/Operators/div_rem.rs:19:23 in function test_normal

Check 1: division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero in var_16[0] / var_17[0]"

Check 2: division-by-zero.2
         - Status: SUCCESS
         - Description: "division by zero in var_16[1] / var_17[1]"

In diffblue/cbmc#7367 I asked the CBMC folks about this missing check, but it turns out these checks are being generated by MIR! I don't think that the "attempt to divide by zero" property is needed here (as it's basically a duplicate of "division by zero"), but it's unclear how to insert the "attempt to divide with overflow" property for SIMD intrinsics.

[reisnera]

While fixing this for integers, and thanks to @celinval's review, I've realized that CBMC does checks for overflow/NaN/division by zero on floating point division but apparently not for remainder. This seems to be corroborated by the CBMC manual on page 41 here. So for example:

#![feature(repr_simd, platform_intrinsics)]

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct f32x2(f32, f32);

extern "platform-intrinsic" {
    fn simd_div<T>(x: T, y: T) -> T;
    fn simd_rem<T>(x: T, y: T) -> T;
}

#[kani::proof]
fn test_simd_div() {
    let dividend: f32 = kani::any::<i16>().into();
    let dividends = f32x2(dividend, dividend);
    let divisor: f32 = kani::any::<i16>().into();
    kani::assume(divisor > 0.0 && divisor < 5.0);
    let divisors = f32x2(divisor, divisor);
    let _simd_result = unsafe { simd_div(dividends, divisors) };
}

#[kani::proof]
fn test_simd_rem() {
    let dividend: f32 = kani::any::<i16>().into();
    let dividends = f32x2(dividend, dividend);
    let divisor: f32 = kani::any::<i16>().into();
    kani::assume(divisor > 0.0 && divisor < 5.0);
    let divisors = f32x2(divisor, divisor);
    let _simd_result = unsafe { simd_rem(dividends, divisors) };
}

The verification for test_simd_div gives, in part:

Check 1: division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"

Check 2: NaN.1
         - Status: SUCCESS
         - Description: "NaN on division"

Check 3: overflow.1
         - Status: SUCCESS
         - Description: "arithmetic overflow on floating-point division"

[...]

However, test_simd_rem gives only:

RESULTS:
Check 1: division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"

[...]

I was able to fix the original issue and implement an integer overflow check, however it looks like I'll have to implement floating point overflow/NaN checks specifically for simd_rem. Definitely going to have to do some reading on this one...

[reisnera]

Upon further reflection/reading, I think simd_rem really doesn't overflow since the magnitude of its result should be less than the divisor. I don't think it needs a separate NaN check either since I think it can only produce NaN if the divisor is 0 which CBMC is already checking.

Edit: Upon further further reflection, I have no idea what to do with simd_rem :)