diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 4482ee1d1f84..e24af9d9ecb1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -340,6 +340,7 @@ impl<'tcx> GotocCtx<'tcx> { field: FieldIdx, field_ty: Ty<'tcx>, ) -> Expr { + let field_ty = self.monomorphize(field_ty); if matches!(field_ty.kind(), ty::Array { .. }) { // Array based assert_eq!(field.index(), 0); diff --git a/tests/kani/SIMD/generic_access.rs b/tests/kani/SIMD/generic_access.rs new file mode 100644 index 000000000000..280175a781c6 --- /dev/null +++ b/tests/kani/SIMD/generic_access.rs @@ -0,0 +1,50 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we can use a generic function to access field of `repr_simd`. +#![feature(portable_simd, repr_simd)] + +use std::simd::SimdElement; + +mod array_based { + use super::*; + + #[repr(simd)] + struct CustomSimd([T; LANES]); + + fn check_fields( + simd: CustomSimd, + expected: [T; LANES], + ) { + assert_eq!(simd.0, expected); + } + + #[kani::proof] + fn check_field_access() { + let data: [u8; 16] = kani::any(); + let vec = CustomSimd(data.clone()); + check_fields(vec, data); + } +} + +mod fields_based { + use super::*; + + #[repr(simd)] + struct CustomSimd(T, T); + + fn check_fields( + simd: CustomSimd, + expected: [T; LANES], + ) { + assert_eq!(simd.0, expected[0]); + assert_eq!(simd.1, expected[1]) + } + + #[kani::proof] + fn check_field_access() { + let data: [u8; 16] = kani::any(); + let vec = CustomSimd(data[0], data[1]); + check_fields(vec, data); + } +}