Fix codegen crashes on SVE tuples and non-power-of-two Simd on aarch64

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

@@ -661,6 +661,19 @@ impl GotocCtx<'_, '_> {
             AggregateKind::Adt(_, variant_index, ..) if res_ty.kind().is_enum() => {
                 self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc)
             }
+            AggregateKind::Adt(..)
+                if rustc_internal::internal(self.tcx, res_ty).is_scalable_vector() =>
+            {
+                // The layout of a tuple of scalable vectors has a single offset, so the operands
+                // cannot be ordered by it. `codegen_scalable_vector_tuple_fields` lays the fields
+                // out in declaration order, which is the order of the operands.
+                let typ = self.codegen_ty_stable(res_ty);
+                Expr::struct_expr_from_values(
+                    typ,
+                    operands.iter().map(|op| self.codegen_operand_stable(op)).collect(),
+                    &self.symbol_table,
+                )
+            }
             AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => {
                 let typ = self.codegen_ty_stable(res_ty);
                 let layout = self.layout_of_stable(res_ty);

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

@@ -6,8 +6,8 @@ use cbmc::utils::aggr_tag;
 use cbmc::{InternString, InternedString};
 use kani_metadata::UnstableFeature;
 use rustc_abi::{
-    BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
-    TagEncoding, TyAndLayout, VariantIdx, VariantLayout, Variants,
+    BackendRepr, BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData,
+    Primitive, Size, TagEncoding, TyAndLayout, VariantIdx, VariantLayout, Variants,
 };
 use rustc_ast::ast::Mutability;
 use rustc_index::IndexVec;
@@ -1184,16 +1184,46 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
         self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| {
             let variant = &def.variants().raw[0];
             let layout = ctx.layout_of(ty);
+            let align = Size::from_bits(layout.layout.align.abi.bits());
+            if def.repr().scalable() && variant.fields.len() > 1 {
+                return ctx.codegen_scalable_vector_tuple_fields(variant, subst, align);
+            }
             ctx.codegen_variant_struct_fields(
                 variant,
                 subst,
                 &layout.layout.fields,
-                Size::from_bits(layout.layout.align.abi.bits()),
+                align,
                 Size::ZERO,
             )
         })
     }
 
+    /// The fields of a tuple of scalable vectors, such as `svint32x4_t(svint32_t, svint32_t,
+    /// svint32_t, svint32_t)` in `core::arch::aarch64`.
+    ///
+    /// rustc lays such a tuple out as a single `SimdScalableVector` whose `FieldsShape` holds one
+    /// offset however many vectors the tuple has, so `codegen_struct_fields` cannot place its
+    /// fields, c.f. <https://github.com/model-checking/kani/issues/4963>. A scalable vector has no
+    /// size fixed at compile time; rustc sizes it at its minimum (a 128-bit vector) and so does
+    /// Kani. The members are all the same vector type, so they are placed back to back, which
+    /// adds up to the size rustc reports for the tuple.
+    fn codegen_scalable_vector_tuple_fields(
+        &mut self,
+        variant: &VariantDef,
+        subst: &'tcx GenericArgsRef<'tcx>,
+        align: Size,
+    ) -> Vec<DatatypeComponent> {
+        let mut fields = Vec::with_capacity(variant.fields.len());
+        let mut offset = Size::ZERO;
+        for field in &variant.fields {
+            let fld_ty = field.ty(self.tcx, subst).skip_normalization();
+            fields.push(DatatypeComponent::field(field.name.to_string(), self.codegen_ty(fld_ty)));
+            offset += self.layout_of(fld_ty).size;
+        }
+        fields.extend(self.codegen_alignment_padding(offset, align, fields.len()));
+        fields
+    }
+
     /// generate a struct representing the layout of the variant
     /// Generate a struct representing the layout of the variant.
     ///
@@ -1633,8 +1663,22 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
         debug! {"handling simd with layout {:?}", layout};
 
         let (element, size) = match layout {
-            SimdVector { element, count } => (element, count),
-            _ => unreachable!(),
+            // As of nightly-2026-08-21 the lane count is a `BackendLaneCount` (a `NonZero<u16>`)
+            // rather than a bare `u64`.
+            SimdVector { element, count } => (*element, count.as_u64()),
+            // `core::simd::Simd` is `#[repr(simd, packed)]`, and rustc lays out a packed vector
+            // whose lane count is not a power of two, such as `Simd<i16, 12>`, as memory with no
+            // padding instead of as a vector. The lanes are taken from the type instead. CBMC
+            // aligns a vector to 1 and Kani pads structs itself, so a vector of that many lanes has
+            // the size and field offsets rustc gives the packed type.
+            BackendRepr::Memory { sized: true } => {
+                let (count, lane_ty) = ty.simd_size_and_type(self.tcx);
+                let BackendRepr::Scalar(element) = self.layout_of(lane_ty).backend_repr else {
+                    unreachable!("SIMD lane `{lane_ty}` is not a scalar")
+                };
+                (element, count)
+            }
+            _ => unreachable!("unexpected layout for SIMD type `{ty}`: {layout:?}"),
         };
 
         // CBMC requires a numeric vector element type, so a pointer lane is modeled as an unsigned
@@ -1657,9 +1701,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
             self.codegen_ty(rust_type)
         };
 
-        // As of nightly-2026-08-21 the lane count is a `BackendLaneCount` (a `NonZero<u16>`)
-        // rather than a bare `u64`.
-        Type::vector(cbmc_type, size.as_u64())
+        Type::vector(cbmc_type, size)
     }
 
     /// the function type of the current instance

tests/kani/SIMD/non_power_of_two_lanes.rs

@@ -0,0 +1,67 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! `core::simd::Simd` is `#[repr(simd, packed)]`, so rustc lays out one whose lane count is not a
+//! power of two as memory with no padding rather than as a vector. Kani's vector lowering only
+//! expected the latter and crashed on every such `Simd`, including the NEON conversions in `core`
+//! such as `From<int16x4x3_t> for Simd<i16, 12>`.
+#![feature(portable_simd)]
+
+use std::mem::{offset_of, size_of};
+use std::simd::Simd;
+use std::simd::cmp::SimdPartialEq;
+
+#[kani::proof]
+fn check_arithmetic_and_lanes() {
+    let a: [i16; 12] = kani::any();
+    let b: [i16; 12] = kani::any();
+    kani::assume(a.iter().all(|x| *x > -1000 && *x < 1000));
+    kani::assume(b.iter().all(|x| *x > -1000 && *x < 1000));
+    let sum = Simd::from_array(a) + Simd::from_array(b);
+    let i: usize = kani::any_where(|i| *i < 12);
+    assert_eq!(sum[i], a[i] + b[i]);
+    assert_eq!(Simd::from_array(a).to_array(), a);
+}
+
+#[kani::proof]
+fn check_mask() {
+    let a: [u8; 3] = kani::any();
+    let b: [u8; 3] = kani::any();
+    let eq = Simd::from_array(a).simd_eq(Simd::from_array(b));
+    assert_eq!(eq.all(), a == b);
+}
+
+#[kani::proof]
+fn check_transmute() {
+    let x: [u8; 3] = kani::any();
+    let v: Simd<u8, 3> = unsafe { std::mem::transmute(x) };
+    assert_eq!(v, Simd::from_array(x));
+    let back: [u8; 3] = unsafe { std::mem::transmute(v) };
+    assert_eq!(back, x);
+}
+
+#[repr(C)]
+struct Packed {
+    v: Simd<i16, 12>,
+    tail: u8,
+}
+
+#[kani::proof]
+fn check_size_and_offsets() {
+    assert_eq!(size_of::<Simd<i16, 12>>(), 24);
+    assert_eq!(size_of::<Simd<u8, 3>>(), 3);
+    assert_eq!(offset_of!(Packed, tail), 24);
+    let p = Packed { v: Simd::splat(kani::any()), tail: kani::any() };
+    let tail = p.tail;
+    let copy = Packed { v: p.v, tail: p.tail };
+    assert_eq!(copy.tail, tail);
+    assert_eq!(copy.v, p.v);
+}
+
+#[kani::proof]
+fn check_pointer_lanes() {
+    let x = [1u8, 2, 3];
+    let ptrs: Simd<*const u8, 3> = Simd::from_array([&x[0], &x[1], &x[2]]);
+    let i: usize = kani::any_where(|i| *i < 3);
+    assert_eq!(unsafe { *ptrs[i] }, x[i]);
+}

tests/script-based-pre/autoharness_sve_tuple/check.sh

@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+echo "--- functions over SVE tuples get harnesses and compile"
+echo "--- passing a tuple through verifies"
+echo "--- an unsupported SVE operation fails its harness, not the run"
+
+# SVE is only available on aarch64.
+case "$(uname -m)" in
+    aarch64 | arm64) ;;
+    *) exit 0 ;;
+esac
+
+kani autoharness -Z autoharness sve_tuple.rs --output-format=terse > out.log 2>&1 || true
+
+grep -qE '^\| sve_tuple +\| pass_x2 +\| #\[kani::proof\] +\| Success' out.log
+grep -qE '^\| sve_tuple +\| pass_x4 +\| #\[kani::proof\] +\| Success' out.log
+grep -q 'sve_tuple_get is not currently supported by Kani' out.log
+grep -qE '^\| sve_tuple +\| first +\| #\[kani::proof\] +\| Failure' out.log
+# The load reaches no further than its predicate, the first LLVM intrinsic it calls.
+grep -q 'call to LLVM intrinsic `llvm.aarch64.sve.ld4.sret.nxv4i32` (1)' out.log
+grep -q 'call to LLVM intrinsic `llvm.aarch64.sve.ptrue.nxv4i1` is not currently supported' out.log
+grep -qE '^\| sve_tuple +\| load +\| #\[kani::proof\] +\| Failure' out.log
+if grep -qE 'panicked|internal compiler error' out.log; then
+    echo "unexpected compiler crash"
+    exit 1
+fi
+
+rm -f out.log

tests/script-based-pre/autoharness_sve_tuple/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: check.sh
+expected: expected

tests/script-based-pre/autoharness_sve_tuple/expected

@@ -0,0 +1,3 @@
+--- functions over SVE tuples get harnesses and compile
+--- passing a tuple through verifies
+--- an unsupported SVE operation fails its harness, not the run

tests/script-based-pre/autoharness_sve_tuple/sve_tuple.rs

@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Tuples of SVE scalable vectors, such as `svint32x4_t`, are laid out by rustc with a single
+//! field offset however many vectors they hold. Kani's struct lowering asserted that each field
+//! has an offset, so `core` failed to compile on aarch64, c.f.
+//! <https://github.com/model-checking/kani/issues/4963>.
+#![feature(stdarch_aarch64_sve)]
+
+use std::arch::aarch64::*;
+
+/// The harness builds the tuple field by field with `kani::any`.
+#[target_feature(enable = "sve")]
+pub fn pass_x2(t: svint32x2_t) -> svint32x2_t {
+    t
+}
+
+#[target_feature(enable = "sve")]
+pub fn pass_x4(t: svint32x4_t) -> svint32x4_t {
+    t
+}
+
+/// Reading a member goes through the `sve_tuple_get` intrinsic, which Kani does not support.
+#[target_feature(enable = "sve")]
+pub fn first(t: svint32x4_t) -> svint32_t {
+    svget4_s32::<0>(t)
+}
+
+/// The load is an LLVM intrinsic, which Kani does not support.
+#[target_feature(enable = "sve")]
+pub fn load(x: [i32; 16]) -> svint32x4_t {
+    unsafe { svld4_s32(svptrue_b32(), x.as_ptr()) }
+}