diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 49cb15a18def..f6941391e4c3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/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 { diff --git a/tests/expected/intrinsics/simd-as-array-based/expected b/tests/expected/intrinsics/simd-as-array-based/expected new file mode 100644 index 000000000000..52152e7c2e1e --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-as-array-based/main.rs b/tests/expected/intrinsics/simd-as-array-based/main.rs new file mode 100644 index 000000000000..e4a329f6831b --- /dev/null +++ b/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); + } +} diff --git a/tests/kani/SIMD/array_based_simd_projection_fixed.rs b/tests/kani/SIMD/array_based_simd_projection_fixed.rs new file mode 100644 index 000000000000..107c471fb30b --- /dev/null +++ b/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; 4]); + +impl Clone for ArraySimd { + fn clone(&self) -> Self { + *self + } +} + +#[kani::proof] +fn test_array_simd_transmute() { + let v = ArraySimd::([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 = std::mem::transmute(v); + let _same_size_different_scalar: ArraySimd = std::mem::transmute(v); + } +} + +#[kani::proof] +fn test_different_array_sizes() { + let v2 = ArraySimd::([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::([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); + } +} diff --git a/tests/kani/SIMD/simd_array_projection_fix.rs b/tests/kani/SIMD/simd_array_projection_fix.rs new file mode 100644 index 000000000000..14f68e1757f8 --- /dev/null +++ b/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; 2]); + +impl Clone for V { + 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::(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::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::([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]); + } +}