Fix SIMD projection mismatch for array-based SIMD types

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

@@ -122,6 +122,37 @@ impl ProjectedPlace {
                         {
                             None
                         }
+                        // SIMD types with array representation can have type mismatches during projection
+                        // because the GOTO representation is a vector type while the field access yields an array type.
+                        // This is expected for array-based SIMD types - see issue #2264.
+                        TyKind::RigidTy(RigidTy::Adt(def, _))
+                            if rustc_internal::internal(ctx.tcx, def).repr().simd() =>
+                        {
+                            // Check if the MIR type is an array (array-based SIMD representation)
+                            if matches!(t.kind(), TyKind::RigidTy(RigidTy::Array(..))) {
+                                // For array-based SIMD, expr_ty should be a vector and type_from_mir should be an array
+                                // Both represent the same data, just with different type representations
+                                if expr_ty.is_vector() || type_from_mir.is_vector() {
+                                    None
+                                } else {
+                                    Some((expr_ty, type_from_mir))
+                                }
+                            } else {
+                                Some((expr_ty, type_from_mir))
+                            }
+                        }
+                        TyKind::RigidTy(RigidTy::Array(..)) => {
+                            // Also handle when the type is an array that might be part of a SIMD structure
+                            // If both types are compatible in size and one is a vector, allow it
+                            if (expr_ty.is_vector() || type_from_mir.is_vector())
+                                && expr_ty.sizeof(&ctx.symbol_table)
+                                    == type_from_mir.sizeof(&ctx.symbol_table)
+                            {
+                                None
+                            } else {
+                                Some((expr_ty, type_from_mir))
+                            }
+                        }
                         _ => Some((expr_ty, type_from_mir)),
                     }
                 } else {

tests/expected/intrinsics/simd-as-array-based/expected

@@ -0,0 +1,22 @@
+Kani Rust Verifier
+CBMC version
+Reading GOTO program from file
+Generating GOTO Program
+Adding CPROVER library
+Removal of function pointers and virtual functions
+Generic Property Instrumentation
+Running with \d+ object bits
+Starting Bounded Model Checking
+Runtime Symex: \d+\.\d+s
+size of program expression: \d+ steps
+slicing removed \d+ assignments
+Generated \d+ VCC\(s\), \d+ remaining after simplification
+Runtime Postprocess Equation: \d+\.\d+(e-\d+)?s
+
+RESULTS:
+VERIFICATION:- SUCCESSFUL
+
+Verification Time: \d+\.\d+s
+
+Manual Harness Summary:
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/intrinsics/simd-as-array-based/main.rs

@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --no-assertion-reach-checks
+//
+//! Test for the `simd_as` intrinsic with array-based SIMD types.
+//! This test verifies that the intrinsic correctly handles type conversions
+//! between SIMD vectors with array-based representations, fixing issue #2264.
+
+#![feature(repr_simd, core_intrinsics)]
+
+use std::intrinsics::simd::simd_as;
+
+#[derive(Copy)]
+#[repr(simd)]
+struct Vu32([u32; 2]);
+
+impl Clone for Vu32 {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+#[derive(Copy)]
+#[repr(simd)]
+struct Vi32([i32; 2]);
+
+impl Clone for Vi32 {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+#[kani::proof]
+fn test_simd_as_same_size() {
+    unsafe {
+        let u = Vu32([u32::MIN, u32::MAX]);
+        let _i: Vi32 = simd_as(u);
+    }
+}

tests/kani/SIMD/array_based_simd_projection_fixed.rs

@@ -0,0 +1,59 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Fix for array-based SIMD projection mismatch issue #2264
+//!
+//! This test verifies that projection mismatches with array-based SIMD types
+//! no longer occur after the fix in the check_expr_typ_mismatch function.
+
+#![feature(repr_simd)]
+
+#[derive(Copy)]
+#[repr(simd)]
+struct ArraySimd<T>([T; 4]);
+
+impl<T: Copy> Clone for ArraySimd<T> {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+#[kani::proof]
+fn test_array_simd_transmute() {
+    let v = ArraySimd::<u32>([1, 2, 3, 4]);
+
+    // These operations previously caused projection mismatch errors
+    // but should now work correctly
+    unsafe {
+        let _array: [u32; 4] = std::mem::transmute(v);
+        let _same_size_different_type: ArraySimd<i32> = std::mem::transmute(v);
+        let _same_size_different_scalar: ArraySimd<f32> = std::mem::transmute(v);
+    }
+}
+
+#[kani::proof]
+fn test_different_array_sizes() {
+    let v2 = ArraySimd::<u16>([1, 2, 3, 4]);
+
+    // Test conversions to array types
+    unsafe {
+        let _arr2: [u16; 4] = std::mem::transmute(v2);
+
+        // Test same total bit size conversion (u16[4] = 64 bits = u32[2] = 64 bits)
+        let v2_as_u32: [u32; 2] = std::mem::transmute(v2);
+        assert_eq!(v2_as_u32.len(), 2);
+    }
+}
+
+#[kani::proof]
+fn test_field_access_equivalent() {
+    let v = ArraySimd::<i32>([10, 20, 30, 40]);
+
+    // Test that we can access the underlying data
+    unsafe {
+        let arr: [i32; 4] = std::mem::transmute(v);
+        assert_eq!(arr[0], 10);
+        assert_eq!(arr[1], 20);
+        assert_eq!(arr[2], 30);
+        assert_eq!(arr[3], 40);
+    }
+}

tests/kani/SIMD/simd_array_projection_fix.rs

@@ -0,0 +1,84 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Test for projection mismatch fix with array-based SIMD types.
+//! This addresses the issue described in https://github.com/model-checking/kani/issues/2264
+//! where array-based SIMD types would cause projection mismatches during type conversions.
+
+#![feature(repr_simd)]
+
+#[derive(Copy)]
+#[repr(simd)]
+struct V<T>([T; 2]);
+
+impl<T: Copy> Clone for V<T> {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+#[derive(Copy)]
+#[repr(simd)]
+struct VF32([f32; 2]);
+
+impl Clone for VF32 {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+#[derive(Copy)]
+#[repr(simd)]
+struct VU32([u32; 2]);
+
+impl Clone for VU32 {
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+// Test transmute between SIMD types with same representation size
+// This should work with the projection fix for array-based SIMD types
+fn test_simd_transmute_same_size() {
+    let v_f32 = VF32([1.0f32, 2.0f32]);
+    let v_u32: VU32 = unsafe { std::mem::transmute(v_f32) };
+
+    // Verify the transmute worked by checking bit patterns
+    let f32_bits = 1.0f32.to_bits();
+    let u32_val = unsafe { std::mem::transmute::<VU32, [u32; 2]>(v_u32) };
+    assert_eq!(u32_val[0], f32_bits);
+}
+
+// Test field access on array-based SIMD (this was part of the original issue)
+fn test_simd_field_access() {
+    let v = V::<u32>([u32::MIN, u32::MAX]);
+
+    // This should work without projection mismatch errors
+    unsafe {
+        let arr: [u32; 2] = std::mem::transmute(v);
+        assert_eq!(arr[0], u32::MIN);
+        assert_eq!(arr[1], u32::MAX);
+    }
+}
+
+#[kani::proof]
+fn verify_simd_transmute_same_size() {
+    test_simd_transmute_same_size();
+}
+
+#[kani::proof]
+fn verify_simd_field_access() {
+    test_simd_field_access();
+}
+
+#[kani::proof]
+fn verify_simd_clone() {
+    let v = V::<i32>([42, -42]);
+    let v2 = v.clone();
+
+    unsafe {
+        let arr1: [i32; 2] = std::mem::transmute(v);
+        let arr2: [i32; 2] = std::mem::transmute(v2);
+        assert_eq!(arr1[0], arr2[0]);
+        assert_eq!(arr1[1], arr2[1]);
+    }
+}