diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 9122667c3c37..454b1150f0cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/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); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 7ddb47730fef..cc89e085c0ec 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/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. . 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 { + 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`) + // 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`, 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`) - // rather than a bare `u64`. - Type::vector(cbmc_type, size.as_u64()) + Type::vector(cbmc_type, size) } /// the function type of the current instance diff --git a/tests/kani/SIMD/non_power_of_two_lanes.rs b/tests/kani/SIMD/non_power_of_two_lanes.rs new file mode 100644 index 000000000000..31f291aba87e --- /dev/null +++ b/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 for Simd`. +#![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 = 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, + tail: u8, +} + +#[kani::proof] +fn check_size_and_offsets() { + assert_eq!(size_of::>(), 24); + assert_eq!(size_of::>(), 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]); +} diff --git a/tests/script-based-pre/autoharness_sve_tuple/check.sh b/tests/script-based-pre/autoharness_sve_tuple/check.sh new file mode 100755 index 000000000000..1c8462118629 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/autoharness_sve_tuple/config.yml b/tests/script-based-pre/autoharness_sve_tuple/config.yml new file mode 100644 index 000000000000..c342fc7f498b --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/autoharness_sve_tuple/expected b/tests/script-based-pre/autoharness_sve_tuple/expected new file mode 100644 index 000000000000..5eafc989ab5a --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/autoharness_sve_tuple/sve_tuple.rs b/tests/script-based-pre/autoharness_sve_tuple/sve_tuple.rs new file mode 100644 index 000000000000..f7eabcf556c4 --- /dev/null +++ b/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. +//! . +#![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()) } +}