Fix SIMD field access (#2660)

Change #2633 was incomplete and it doesn't work in the context of generic functions. This PR fixes that.

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);

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: SimdElement, const LANES: usize>([T; LANES]);
+
+    fn check_fields<T: SimdElement + PartialEq, const LANES: usize>(
+        simd: CustomSimd<T, LANES>,
+        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: SimdElement>(T, T);
+
+    fn check_fields<T: SimdElement + PartialEq, const LANES: usize>(
+        simd: CustomSimd<T>,
+        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);
+    }
+}