Potentially missing overflow check in bitshift operators for vector expressions

[adpaco-aws]

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.

[tautschnig]

I'm afraid that check "attempt to shift left with overflow" is one that Kani generates (it's already part of the generated symtab JSON file), it's not one generated by CBMC. So Kani will need to duplicate this for the SIMD case.