diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 95fadc7bbaf2..4482ee1d1f84 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -23,7 +23,7 @@ use tracing::{debug, trace, warn}; /// A projection in Kani can either be to a type (the normal case), /// or a variant in the case of a downcast. -#[derive(Debug)] +#[derive(Copy, Clone, Debug)] pub enum TypeOrVariant<'tcx> { Type(Ty<'tcx>), Variant(&'tcx VariantDef), @@ -235,15 +235,21 @@ impl<'tcx> TypeOrVariant<'tcx> { } impl<'tcx> GotocCtx<'tcx> { + /// Codegen field access for types that allow direct field projection. + /// + /// I.e.: Algebraic data types, closures, and generators. + /// + /// Other composite types such as array only support index projection. fn codegen_field( &mut self, - res: Expr, - t: TypeOrVariant<'tcx>, - f: &FieldIdx, + parent_expr: Expr, + parent_ty_or_var: TypeOrVariant<'tcx>, + field: &FieldIdx, + field_ty_or_var: TypeOrVariant<'tcx>, ) -> Result { - match t { - TypeOrVariant::Type(t) => { - match t.kind() { + match parent_ty_or_var { + TypeOrVariant::Type(parent_ty) => { + match parent_ty.kind() { ty::Alias(..) | ty::Bool | ty::Char @@ -254,56 +260,98 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Never | ty::FnDef(..) | ty::GeneratorWitness(..) + | ty::GeneratorWitnessMIR(..) | ty::Foreign(..) | ty::Dynamic(..) | ty::Bound(..) | ty::Placeholder(..) | ty::Param(_) | ty::Infer(_) - | ty::Error(_) => unreachable!("type {:?} does not have a field", t), - ty::Tuple(_) => { - Ok(res.member(&Self::tuple_fld_name(f.index()), &self.symbol_table)) - } - ty::Adt(def, _) if def.repr().simd() => { - // this is a SIMD vector - the index represents one - // of the elements, so we want to index as an array - // Example: - // pub struct i64x2(i64, i64); - // fn main() { - // let v = i64x2(1, 2); - // assert!(v.0 == 1); // refers to the first i64 - // assert!(v.1 == 2); - // } - let size_index = Expr::int_constant(f.index(), Type::size_t()); - Ok(res.index_array(size_index)) - } + | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"), + ty::Tuple(_) => Ok(parent_expr + .member(&Self::tuple_fld_name(field.index()), &self.symbol_table)), + ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field( + parent_expr, + *field, + field_ty_or_var.expect_type(), + )), // if we fall here, then we are handling either a struct or a union ty::Adt(def, _) => { - let field = &def.variants().raw[0].fields[*f]; - Ok(res.member(&field.name.to_string(), &self.symbol_table)) + let field = &def.variants().raw[0].fields[*field]; + Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table)) + } + ty::Closure(..) => { + Ok(parent_expr.member(&field.index().to_string(), &self.symbol_table)) } - ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)), ty::Generator(..) => { - let field_name = self.generator_field_name(f.as_usize()); - Ok(res + let field_name = self.generator_field_name(field.as_usize()); + Ok(parent_expr .member("direct_fields", &self.symbol_table) .member(field_name, &self.symbol_table)) } - _ => unimplemented!(), + ty::Str | ty::Array(_, _) | ty::Slice(_) | ty::RawPtr(_) | ty::Ref(_, _, _) => { + unreachable!( + "element of {parent_ty:?} is not accessed via field projection" + ) + } } } // if we fall here, then we are handling an enum - TypeOrVariant::Variant(v) => { - let field = &v.fields[*f]; - Ok(res.member(&field.name.to_string(), &self.symbol_table)) + TypeOrVariant::Variant(parent_var) => { + let field = &parent_var.fields[*field]; + Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table)) } TypeOrVariant::GeneratorVariant(_var_idx) => { - let field_name = self.generator_field_name(f.index()); - Ok(res.member(field_name, &self.symbol_table)) + let field_name = self.generator_field_name(field.index()); + Ok(parent_expr.member(field_name, &self.symbol_table)) } } } + /// This is a SIMD vector, which has 2 possible internal representations: + /// 1- Multi-field representation (original and currently deprecated) + /// In this case, a field is one lane (i.e.: one element) + /// Example: + /// ```ignore + /// pub struct i64x2(i64, i64); + /// fn main() { + /// let v = i64x2(1, 2); + /// assert!(v.0 == 1); // refers to the first i64 + /// assert!(v.1 == 2); + /// } + /// ``` + /// 2- Array-based representation + /// In this case, the projection refers to the entire array. + /// ```ignore + /// pub struct i64x2([i64; 2]); + /// fn main() { + /// let v = i64x2([1, 2]); + /// assert!(v.0 == [1, 2]); // refers to the entire array + /// } + /// ``` + /// * Note that projection inside SIMD structs may eventually become illegal. + /// See thread. + /// + /// Since the goto representation for both is the same, we use the expected type to decide + /// what to return. + fn codegen_simd_field( + &mut self, + parent_expr: Expr, + field: FieldIdx, + field_ty: Ty<'tcx>, + ) -> Expr { + if matches!(field_ty.kind(), ty::Array { .. }) { + // Array based + assert_eq!(field.index(), 0); + let field_typ = self.codegen_ty(field_ty); + parent_expr.reinterpret_cast(field_typ) + } else { + // Return the given field. + let index_expr = Expr::int_constant(field.index(), Type::size_t()); + parent_expr.index_array(index_expr) + } + } + /// If a local is a function definition, ignore the local variable name and /// generate a function call based on the def id. /// @@ -424,7 +472,8 @@ impl<'tcx> GotocCtx<'tcx> { } ProjectionElem::Field(f, t) => { let typ = TypeOrVariant::Type(t); - let expr = self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f)?; + let expr = + self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f, typ)?; ProjectedPlace::try_new( expr, typ, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 22b26a3489b4..88a2f3cd4a2c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -582,24 +582,28 @@ impl<'tcx> GotocCtx<'tcx> { AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => { let typ = self.codegen_ty(res_ty); let layout = self.layout_of(res_ty); - let vector_element_type = typ.base_type().unwrap().clone(); - Expr::vector_expr( - typ, - layout - .fields - .index_by_increasing_offset() - .map(|idx| { - let cgo = self.codegen_operand(&operands[idx.into()]); - // The input operand might actually be a one-element array, as seen - // when running assess on firecracker. - if *cgo.typ() == vector_element_type { - cgo - } else { - cgo.transmute_to(vector_element_type.clone(), &self.symbol_table) - } - }) - .collect(), - ) + trace!(shape=?layout.fields, "codegen_rvalue_aggregate"); + assert!(operands.len() > 0, "SIMD vector cannot be empty"); + if operands.len() == 1 { + let data = self.codegen_operand(&operands[0u32.into()]); + if data.typ().is_array() { + // Array-based SIMD representation. + data.transmute_to(typ, &self.symbol_table) + } else { + // Multi field-based representation with one field. + Expr::vector_expr(typ, vec![data]) + } + } else { + // Multi field SIMD representation. + Expr::vector_expr( + typ, + layout + .fields + .index_by_increasing_offset() + .map(|idx| self.codegen_operand(&operands[idx.into()])) + .collect(), + ) + } } AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => { self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc) diff --git a/tests/kani/SIMD/array_simd_repr.rs b/tests/kani/SIMD/array_simd_repr.rs new file mode 100644 index 000000000000..076427415091 --- /dev/null +++ b/tests/kani/SIMD/array_simd_repr.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify that Kani can properly handle SIMD declaration and field access using array syntax. + +#![allow(non_camel_case_types)] +#![feature(repr_simd)] + +#[repr(simd)] +#[derive(Clone, PartialEq, Eq, PartialOrd, kani::Arbitrary)] +pub struct i64x2([i64; 2]); + +#[kani::proof] +fn check_diff() { + let x = i64x2([1, 2]); + let y = i64x2([3, 4]); + assert!(x != y); +} + +#[kani::proof] +fn check_ge() { + let x: i64x2 = kani::any(); + kani::assume(x.0[0] > 0); + kani::assume(x.0[1] > 0); + assert!(x > i64x2([0, 0])); +} + +#[derive(Clone, Debug)] +#[repr(simd)] +struct CustomSimd([T; LANES]); + +#[kani::proof] +fn simd_vec() { + let simd = CustomSimd([0u8; 10]); + let idx: usize = kani::any_where(|x: &usize| *x < 10); + assert_eq!(simd.0[idx], 0); +} diff --git a/tests/kani/SIMD/multi_field_simd.rs b/tests/kani/SIMD/multi_field_simd.rs new file mode 100644 index 000000000000..d54cf1a07bdb --- /dev/null +++ b/tests/kani/SIMD/multi_field_simd.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify that Kani can properly handle SIMD declaration and field access using multi-field syntax. +//! Note: Multi-field SIMD is actually being deprecated, but until it's removed, we might +//! as well keep supporting it. +//! See for more details. + +#![allow(non_camel_case_types)] +#![feature(repr_simd)] + +#[repr(simd)] +#[derive(PartialEq, Eq, PartialOrd, kani::Arbitrary)] +pub struct i64x2(i64, i64); + +#[kani::proof] +fn check_diff() { + let x = i64x2(1, 2); + let y = i64x2(3, 4); + assert!(x != y); +} + +#[kani::proof] +fn check_ge() { + let x: i64x2 = kani::any(); + kani::assume(x.0 > 0); + kani::assume(x.1 > 0); + assert!(x > i64x2(0, 0)); +} diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs new file mode 100644 index 000000000000..9f7d0f536dcc --- /dev/null +++ b/tests/kani/SIMD/portable_simd.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we have basic support of portable SIMD. +#![feature(portable_simd)] + +use std::simd::u64x16; + +#[kani::proof] +fn check_sum_any() { + let a = u64x16::splat(0); + let b = u64x16::from_array(kani::any()); + // Cannot compare them directly: https://github.com/model-checking/kani/issues/2632 + assert_eq!((a + b).as_array(), b.as_array()); +} diff --git a/tests/kani/SIMD/simd_float_ops_fixme.rs b/tests/kani/SIMD/simd_float_ops_fixme.rs new file mode 100644 index 000000000000..d258a2119eca --- /dev/null +++ b/tests/kani/SIMD/simd_float_ops_fixme.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we can handle SIMD defined in the standard library +//! FIXME: +#![allow(non_camel_case_types)] +#![feature(repr_simd, platform_intrinsics, portable_simd)] +use std::simd::f32x4; + +extern "platform-intrinsic" { + fn simd_add(x: T, y: T) -> T; + fn simd_eq(x: T, y: T) -> U; +} + +#[repr(simd)] +#[derive(Clone, PartialEq, kani::Arbitrary)] +pub struct f32x2(f32, f32); + +impl f32x2 { + fn as_array(&self) -> &[f32; 2] { + unsafe { &*(self as *const f32x2 as *const [f32; 2]) } + } +} + +#[kani::proof] +fn check_sum() { + let a = f32x2(0.0, 0.0); + let b = kani::any::(); + let sum = unsafe { simd_add(a.clone(), b) }; + assert_eq!(sum.as_array(), a.as_array()); +} + +#[kani::proof] +fn check_sum_portable() { + let a = f32x4::splat(0.0); + let b = f32x4::from_array(kani::any()); + // Cannot compare them directly: https://github.com/model-checking/kani/issues/2632 + assert_eq!((a + b).as_array(), b.as_array()); +}