Potentially missing overflow check in bitshift operators for vector expressions #7362
Description
CBMC version: 5.69.1 (+ this Kani branch)
Operating system: ubuntu-20.04
Exact command line resulting in the issue: Default kani command 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) };
}What behaviour did you expect: Expected the properties to be checked to be the same for both << and simd_shl.
What happened instead: The properties checked aren't the same for both << and simd_shl. In particular, when I run the program above in Kani, I see the following 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
And the following 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"
The SIMD vector expression successfully duplicates all checks except for "attempt to shift left with overflow". The comments in goto_check_c.cpp make me think this check is still necessary (even if it overlaps with "shift distance too large" in some cases), but I couldn't find the origin of that check.
So I was expecting this check to also be generated for the SIMD vector expression. Same thing goes for the >> and simd_shr duo.