Restore simd_shl and simd_shr intrinsics (rust-lang#1964)

Author: adpaco-aws

docs/src/rust-feature-support/intrinsics.md

@@ -268,8 +268,8 @@ Name | Support | Notes |
 `simd_ne`  | Yes | |
 `simd_or`  | Yes | |
 `simd_rem`  | No | |
-`simd_shl`  | No | |
-`simd_shr`  | No | |
+`simd_shl`  | Yes | Doesn't check for overflow cases (#1963)[https://github.com/model-checking/kani/issues/1963] |
+`simd_shr`  | Yes | Doesn't check for overflow cases (#1963)[https://github.com/model-checking/kani/issues/1963] |
 `simd_shuffle*`  | No | |
 `simd_sub`  | Yes | |
 `simd_xor`  | Yes | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -606,15 +606,15 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "simd_or" => codegen_intrinsic_binop!(bitor),
             "simd_rem" => unstable_codegen!(codegen_intrinsic_binop!(rem)),
-            "simd_shl" => unstable_codegen!(codegen_intrinsic_binop!(shl)),
+            // TODO: `simd_shl` and `simd_shr` don't check overflow cases.
+            // <https://github.com/model-checking/kani/issues/1963>
+            "simd_shl" => codegen_intrinsic_binop!(shl),
             "simd_shr" => {
-                // Remove this attribute once unstable_codegen! is removed.
-                #[allow(clippy::if_same_then_else)]
                 if fargs[0].typ().base_type().unwrap().is_signed(self.symbol_table.machine_model())
                 {
-                    unstable_codegen!(codegen_intrinsic_binop!(ashr))
+                    codegen_intrinsic_binop!(ashr)
                 } else {
-                    unstable_codegen!(codegen_intrinsic_binop!(lshr))
+                    codegen_intrinsic_binop!(lshr)
                 }
             }
             // "simd_shuffle#" => handled in an `if` preceding this match

tests/expected/intrinsics/simd-shl-operand-negative/expected

@@ -0,0 +1,2 @@
+FAILURE\
+shift operand is negative

tests/expected/intrinsics/simd-shl-operand-negative/main.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `simd_shl` returns a failure if the operand is negative.
+//! Note: The "operand is negative" property isn't checked for `simd_shr`, only
+//! for `simd_shl`.
+#![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;
+}
+
+#[kani::proof]
+fn test_simd_shl() {
+    let value = kani::any();
+    let values = i32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift >= 0);
+    kani::assume(shift < 32);
+    let shifts = i32x2(shift, shift);
+    let _result = unsafe { simd_shl(values, shifts) };
+}

tests/expected/intrinsics/simd-shl-shift-negative/expected

@@ -0,0 +1,2 @@
+FAILURE\
+shift distance is negative

tests/expected/intrinsics/simd-shl-shift-negative/main.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `simd_shl` returns a failure if the shift distance is negative.
+#![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;
+}
+
+#[kani::proof]
+fn test_simd_shl() {
+    let value = kani::any();
+    kani::assume(value >= 0);
+    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) };
+}

tests/expected/intrinsics/simd-shl-shift-too-large/expected

@@ -0,0 +1,2 @@
+FAILURE\
+shift distance too large

tests/expected/intrinsics/simd-shl-shift-too-large/main.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `simd_shl` returns a failure if the shift distance is too large.
+#![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;
+}
+
+#[kani::proof]
+fn test_simd_shl() {
+    let value = kani::any();
+    kani::assume(value >= 0);
+    let values = i32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift >= 0);
+    let shifts = i32x2(shift, shift);
+    let _result = unsafe { simd_shl(values, shifts) };
+}

tests/expected/intrinsics/simd-shr-shift-negative/expected

@@ -0,0 +1,2 @@
+FAILURE\
+shift distance is negative

tests/expected/intrinsics/simd-shr-shift-negative/main.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `simd_shr` returns a failure if the shift distance is negative.
+#![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_shr<T>(x: T, y: T) -> T;
+}
+
+#[kani::proof]
+fn test_simd_shr() {
+    let value = kani::any();
+    kani::assume(value >= 0);
+    let values = i32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift < 32);
+    let shifts = i32x2(shift, shift);
+    let _result = unsafe { simd_shr(values, shifts) };
+}

tests/expected/intrinsics/simd-shr-shift-too-large/expected

@@ -0,0 +1,2 @@
+FAILURE\
+shift distance too large

tests/expected/intrinsics/simd-shr-shift-too-large/main.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `simd_shr` returns a failure if the shift distance is too large.
+#![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_shr<T>(x: T, y: T) -> T;
+}
+
+#[kani::proof]
+fn test_simd_shr() {
+    let value = kani::any();
+    kani::assume(value >= 0);
+    let values = i32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift >= 0);
+    let shifts = i32x2(shift, shift);
+    let _result = unsafe { simd_shr(values, shifts) };
+}

tests/kani/Intrinsics/SIMD/Operators/bitshift.rs

@@ -0,0 +1,60 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that the `simd_shl` and `simd_shr` intrinsics are supported and they
+//! return the expected results.
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i32x2(i32, i32);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct u32x2(u32, u32);
+
+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_simd_shl() {
+    let value = kani::any();
+    kani::assume(value >= 0);
+    let values = i32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift >= 0);
+    kani::assume(shift < 32);
+    let shifts = i32x2(shift, shift);
+    let normal_result = value << shift;
+    let simd_result = unsafe { simd_shl(values, shifts) };
+    assert_eq!(normal_result, simd_result.0);
+}
+
+#[kani::proof]
+fn test_simd_shr_signed() {
+    let value = kani::any();
+    let values = i32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift >= 0);
+    kani::assume(shift < 32);
+    let shifts = i32x2(shift, shift);
+    let normal_result = value >> shift;
+    let simd_result = unsafe { simd_shr(values, shifts) };
+    assert_eq!(normal_result, simd_result.0);
+}
+
+#[kani::proof]
+fn test_simd_shr_unsigned() {
+    let value = kani::any();
+    let values = u32x2(value, value);
+    let shift = kani::any();
+    kani::assume(shift < 32);
+    let shifts = u32x2(shift, shift);
+    let normal_result = value >> shift;
+    let simd_result = unsafe { simd_shr(values, shifts) };
+    assert_eq!(normal_result, simd_result.0);
+}