simd_shl and simd_shr don't check overflow cases #1963
Description
Both simd_shl and simd_shr are missing an overflow check that is done for the regular bit-shift 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_shl<T>(x: T, y: T) -> T;
fn simd_shr<T>(x: T, y: T) -> T;
}
#[kani::proof]
fn test_normal() {
let value: i32 = kani::any();
let shift: i32 = kani::any();
kani::assume(value == 1);
kani::assume(shift == 32);
let result: i32 = value << shift;
}
#[kani::proof]
fn test_simd() {
let value = kani::any();
kani::assume(value == 1);
let values = i32x2(value, value);
let shift = kani::any();
kani::assume(shift == 32);
let shifts = i32x2(shift, shift);
let result = unsafe { simd_shl(values, shifts) };
}This is the verification output for test_normal:
RESULTS:
Check 1: test_normal.assertion.1
- Status: FAILURE
- Description: "attempt to shift left with overflow"
- Location: tests/kani/Intrinsics/SIMD/Operators/bitshift.rs:29:23 in function test_normal
Check 2: test_normal.undefined-shift.1
- Status: SUCCESS
- Description: "shift distance is negative"
- Location: tests/kani/Intrinsics/SIMD/Operators/bitshift.rs:29:23 in function test_normal
Check 3: test_normal.undefined-shift.2
- Status: FAILURE
- Description: "shift distance too large"
- Location: tests/kani/Intrinsics/SIMD/Operators/bitshift.rs:29:23 in function test_normal
Check 4: test_normal.undefined-shift.3
- Status: SUCCESS
- Description: "shift operand is negative"
- Location: tests/kani/Intrinsics/SIMD/Operators/bitshift.rs:29:23 in function test_normal
This is the verification output for test_simd:
RESULTS:
Check 1: undefined-shift.1
- Status: SUCCESS
- Description: "shift distance is negative"
Check 2: undefined-shift.2
- Status: FAILURE
- Description: "shift distance too large"
Check 3: undefined-shift.3
- Status: SUCCESS
- Description: "shift operand is negative"
Check 4: undefined-shift.4
- Status: SUCCESS
- Description: "shift distance is negative"
Check 5: undefined-shift.5
- Status: FAILURE
- Description: "shift distance too large"
Check 6: undefined-shift.6
- Status: SUCCESS
- Description: "shift operand is negative"
In diffblue/cbmc#7362 I asked the CBMC about this missing check, but it turns out these checks are being generated by MIR! It's not clear to me if they're necessary, as some overflow cases overlap with the "shift is too large" cases, for example. It's also unclear how to include them for SIMD intrinsics.