diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index eba48f539759..631259be31cc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -535,16 +535,8 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty) } "simd_or" => codegen_intrinsic_binop!(bitor), - // TODO: `simd_shl` and `simd_shr` don't check overflow cases. - // - "simd_shl" => codegen_intrinsic_binop!(shl), - "simd_shr" => { - if fargs[0].typ().base_type().unwrap().is_signed(self.symbol_table.machine_model()) - { - codegen_intrinsic_binop!(ashr) - } else { - codegen_intrinsic_binop!(lshr) - } + "simd_shl" | "simd_shr" => { + self.codegen_simd_shift_with_distance_check(fargs, intrinsic, p, loc) } // "simd_shuffle#" => handled in an `if` preceding this match "simd_sub" => self.codegen_simd_op_with_overflow( @@ -1588,6 +1580,75 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(vec![check_stmt, expr_place], loc) } + /// Intrinsics which encode a SIMD bitshift. + /// Also checks for valid shift distance. Shifts on an integer of type T are UB if shift + /// distance < 0 or >= T::BITS. + fn codegen_simd_shift_with_distance_check( + &mut self, + mut fargs: Vec, + intrinsic: &str, + p: &Place<'tcx>, + loc: Location, + ) -> Stmt { + let values = fargs.remove(0); + let distances = fargs.remove(0); + + let values_len = values.typ().len().unwrap(); + let distances_len = distances.typ().len().unwrap(); + assert_eq!(values_len, distances_len, "expected same length vectors"); + + let value_type = values.typ().base_type().unwrap(); + let distance_type = distances.typ().base_type().unwrap(); + let value_width = value_type.sizeof_in_bits(&self.symbol_table); + let value_width_expr = Expr::int_constant(value_width, distance_type.clone()); + let distance_is_signed = distance_type.is_signed(self.symbol_table.machine_model()); + + let mut excessive_check = Expr::bool_false(); + let mut negative_check = Expr::bool_false(); + for i in 0..distances_len { + let index = Expr::int_constant(i, Type::ssize_t()); + let distance = distances.clone().index_array(index); + let excessive_distance_cond = distance.clone().ge(value_width_expr.clone()); + excessive_check = excessive_check.or(excessive_distance_cond); + if distance_is_signed { + let negative_distance_cond = distance.is_negative(); + negative_check = negative_check.or(negative_distance_cond); + } + } + let excessive_check_stmt = self.codegen_assert_assume( + excessive_check.not(), + PropertyClass::ArithmeticOverflow, + format!("attempt {intrinsic} with excessive shift distance").as_str(), + loc, + ); + + let op_fun = match intrinsic { + "simd_shl" => Expr::shl, + "simd_shr" => { + if distance_is_signed { + Expr::ashr + } else { + Expr::lshr + } + } + _ => unreachable!("expected a simd shift intrinsic"), + }; + let res = op_fun(values, distances); + let expr_place = self.codegen_expr_to_place(p, res); + + if distance_is_signed { + let negative_check_stmt = self.codegen_assert_assume( + negative_check.not(), + PropertyClass::ArithmeticOverflow, + format!("attempt {intrinsic} with negative shift distance").as_str(), + loc, + ); + Stmt::block(vec![excessive_check_stmt, negative_check_stmt, expr_place], loc) + } else { + Stmt::block(vec![excessive_check_stmt, expr_place], loc) + } + } + /// `simd_shuffle` constructs a new vector from the elements of two input /// vectors, choosing values according to an input array of indexes. /// 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..bfb3313a5ae9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -116,6 +116,14 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::BitXor => ce1.bitxor(ce2), BinOp::Div => ce1.div(ce2), BinOp::Rem => ce1.rem(ce2), + BinOp::ShlUnchecked => ce1.shl(ce2), + BinOp::ShrUnchecked => { + if self.operand_ty(e1).is_signed() { + ce1.ashr(ce2) + } else { + ce1.lshr(ce2) + } + } _ => unreachable!("Unexpected {:?}", op), } } @@ -343,11 +351,14 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => { self.codegen_scalar_binop(op, e1, e2) } - // We currently rely on CBMC's UB checks for shift which isn't always accurate. - // We should implement the checks ourselves. - // See https://github.com/model-checking/kani/issues/2374 - BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2), - BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2), + BinOp::ShlUnchecked | BinOp::ShrUnchecked => { + let result = self.codegen_unchecked_scalar_binop(op, e1, e2); + let check = self.check_unchecked_shift_distance(e1, e2, loc); + Expr::statement_expression( + vec![check, result.clone().as_stmt(loc)], + result.typ().clone(), + ) + } BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => { self.codegen_binop_with_overflow_check(op, e1, e2, loc) } @@ -455,6 +466,39 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Check for valid unchecked shift distance. + /// Shifts on an integer of type T are UB if shift distance < 0 or >= T::BITS. + fn check_unchecked_shift_distance( + &mut self, + value: &Operand<'tcx>, + distance: &Operand<'tcx>, + loc: Location, + ) -> Stmt { + let value_expr = self.codegen_operand(value); + let distance_expr = self.codegen_operand(distance); + let value_width = value_expr.typ().sizeof_in_bits(&self.symbol_table); + let value_width_expr = Expr::int_constant(value_width, distance_expr.typ().clone()); + + let excessive_distance_check = self.codegen_assert_assume( + distance_expr.clone().lt(value_width_expr), + PropertyClass::ArithmeticOverflow, + "attempt to shift by excessive shift distance", + loc, + ); + + if distance_expr.typ().is_signed(self.symbol_table.machine_model()) { + let negative_distance_check = self.codegen_assert_assume( + distance_expr.is_non_negative(), + PropertyClass::ArithmeticOverflow, + "attempt to shift by negative distance", + loc, + ); + Stmt::block(vec![negative_distance_check, excessive_distance_check], loc) + } else { + excessive_distance_check + } + } + /// Create an initializer for a generator struct. fn codegen_rvalue_generator( &mut self, @@ -582,24 +626,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/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 96770d562e79..cd87e13782e9 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -167,7 +167,6 @@ impl KaniSession { args.push("--div-by-zero-check".into()); args.push("--float-overflow-check".into()); args.push("--nan-check".into()); - args.push("--undefined-shift-check".into()); // With PR #647 we use Rust's `-C overflow-checks=on` instead of: // --unsigned-overflow-check // --signed-overflow-check diff --git a/tests/.gitignore b/tests/.gitignore index e5e7c802005a..55cf0ad46a3b 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1,2 +1,12 @@ *.goto -*.json \ No newline at end of file +*.json + +# Temporary folders +rmet*/ +kani_concrete_playback + +# Binary artifacts +*out +smoke +check_tests +function diff --git a/tests/expected/intrinsics/simd-shl-operand-negative/expected b/tests/expected/intrinsics/simd-shl-operand-negative/expected deleted file mode 100644 index b437e2374575..000000000000 --- a/tests/expected/intrinsics/simd-shl-operand-negative/expected +++ /dev/null @@ -1,2 +0,0 @@ -FAILURE\ -shift operand is negative \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shl-operand-negative/main.rs b/tests/expected/intrinsics/simd-shl-operand-negative/main.rs deleted file mode 100644 index 3d7969d8d4b6..000000000000 --- a/tests/expected/intrinsics/simd-shl-operand-negative/main.rs +++ /dev/null @@ -1,27 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Checks that `simd_shl` returns a failure if the operand is negative. -//! Note: The "operand is negative" property isn't checked for `simd_shr`, only -//! for `simd_shl`. -#![feature(repr_simd, platform_intrinsics)] - -#[repr(simd)] -#[allow(non_camel_case_types)] -#[derive(Clone, Copy, PartialEq, Eq)] -pub struct i32x2(i32, i32); - -extern "platform-intrinsic" { - fn simd_shl(x: T, y: T) -> T; -} - -#[kani::proof] -fn test_simd_shl() { - let value = kani::any(); - let values = i32x2(value, value); - let shift = kani::any(); - kani::assume(shift >= 0); - kani::assume(shift < 32); - let shifts = i32x2(shift, shift); - let _result = unsafe { simd_shl(values, shifts) }; -} diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/expected b/tests/expected/intrinsics/simd-shl-shift-negative/expected index 0e4e9fadb811..c3b2e1184e06 100644 --- a/tests/expected/intrinsics/simd-shl-shift-negative/expected +++ b/tests/expected/intrinsics/simd-shl-shift-negative/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance is negative \ No newline at end of file +attempt simd_shl with negative shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs index ebde0284a497..0c7116b30567 100644 --- a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs +++ b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shl() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift < 32); diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/expected b/tests/expected/intrinsics/simd-shl-shift-too-large/expected index 65d41d1518fc..2c50f584f06c 100644 --- a/tests/expected/intrinsics/simd-shl-shift-too-large/expected +++ b/tests/expected/intrinsics/simd-shl-shift-too-large/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance too large \ No newline at end of file +attempt simd_shl with excessive shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs index e7cffe4ebb92..fff9aadf1900 100644 --- a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs +++ b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shl() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift >= 0); diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/expected b/tests/expected/intrinsics/simd-shr-shift-negative/expected index 0e4e9fadb811..49a75a18308e 100644 --- a/tests/expected/intrinsics/simd-shr-shift-negative/expected +++ b/tests/expected/intrinsics/simd-shr-shift-negative/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance is negative \ No newline at end of file +attempt simd_shr with negative shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs index ca8cbbc3e0d7..580f0337db25 100644 --- a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs +++ b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shr() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift < 32); diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/expected b/tests/expected/intrinsics/simd-shr-shift-too-large/expected index 65d41d1518fc..adc26e269699 100644 --- a/tests/expected/intrinsics/simd-shr-shift-too-large/expected +++ b/tests/expected/intrinsics/simd-shr-shift-too-large/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance too large \ No newline at end of file +attempt simd_shr with excessive shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs index 87718ec48553..3d9cd5e0c919 100644 --- a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs +++ b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shr() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift >= 0); diff --git a/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs b/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs new file mode 100644 index 000000000000..288698a0fbee --- /dev/null +++ b/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that shifting negative values yields the expected results. + +#[kani::proof] +#[kani::unwind(5)] +fn sheck_shl() { + let val: i32 = kani::any(); + let dist: u8 = kani::any(); + kani::assume(dist < 32); + assert_eq!(val << dist, val.wrapping_mul(2_i32.wrapping_pow(dist.into()))); +} + +#[kani::proof] +#[kani::unwind(5)] +fn check_shr() { + let val: i32 = kani::any(); + let dist: u8 = kani::any(); + kani::assume(dist < 32); + let result = (val as i64).div_euclid(2_i64.pow(dist.into())); + assert_eq!(val >> dist, result as i32); +} diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs index cd2c7ceb756a..1041f918123f 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs @@ -23,7 +23,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shl() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift >= 0); 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()); +} diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index 143dd683f76f..70669b325e9e 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -8,4 +8,3 @@ Failed Checks: attempt to calculate the remainder with overflow Failed Checks: attempt to shift left with overflow Failed Checks: attempt to shift right with overflow Failed Checks: arithmetic overflow on signed shl -Failed Checks: shift operand is negative diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected index 6cd10b4bafd5..b3a4cb77c6ae 100644 --- a/tests/ui/should-panic-attribute/unexpected-failures/expected +++ b/tests/ui/should-panic-attribute/unexpected-failures/expected @@ -1,9 +1,9 @@ -undefined-shift\ +arithmetic_overflow\ Status: FAILURE\ -Description: "shift distance too large" +Description: "attempt to shift by excessive shift distance" Failed Checks: panicked on the `1` arm! Failed Checks: panicked on the `0` arm! -Failed Checks: shift distance too large +Failed Checks: attempt to shift by excessive shift distance VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)