diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index e63e819ead9d..26a1c4563c54 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -69,13 +69,11 @@ mod intrinsics { } #[cfg(target_endian = "little")] - unsafe fn simd_bitmask_impl( - input: &[T; LANES], - ) -> [u8; MASK_LEN] + unsafe fn simd_bitmask_impl(input: &[T; LANES]) -> [u8; mask_len(LANES)] where T: MaskElement, { - let mut mask_array = [0; MASK_LEN]; + let mut mask_array = [0; mask_len(LANES)]; for lane in (0..input.len()).rev() { let byte = lane / 8; let mask = &mut mask_array[byte]; @@ -101,13 +99,14 @@ mod intrinsics { #[rustc_diagnostic_item = "KaniModelSimdBitmask"] pub(super) unsafe fn simd_bitmask(input: T) -> U where - [u8; size_of::()]: Sized, + [u8; mask_len(LANES)]: Sized, E: MaskElement, { // These checks are compiler sanity checks to ensure we are not doing anything invalid. - assert!( - size_of::() >= mask_len(LANES), - "Expected size of return type to be greater or equal to the mask lanes", + assert_eq!( + size_of::(), + size_of::<[u8; mask_len(LANES)]>(), + "Expected size of return type and mask lanes to match", ); assert_eq!( size_of::(), @@ -116,8 +115,8 @@ mod intrinsics { ); let data = &*(&input as *const T as *const [E; LANES]); - let mask = simd_bitmask_impl::() }>(data); - (&mask as *const [u8; size_of::()] as *const U).read() + let mask = simd_bitmask_impl(data); + (&mask as *const [u8; mask_len(LANES)] as *const U).read() } /// Structure used for sanity check our parameters. @@ -128,7 +127,7 @@ mod intrinsics { #[cfg(test)] mod test { use super::intrinsics as kani_intrinsic; - use std::{fmt::Debug, mem::size_of, simd::*}; + use std::{fmt::Debug, simd::*}; extern "platform-intrinsic" { fn simd_bitmask(x: T) -> U; @@ -138,8 +137,8 @@ mod test { /// masks with lanes represented using i16. #[test] fn test_bitmask_i16() { - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false)); - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true)); } /// Tests that the model correctly fails if an invalid value is given. @@ -156,23 +155,21 @@ mod test { /// Tests that the model correctly fails if the size parameter of the mask doesn't match the /// expected number of bytes in the representation. #[test] - #[should_panic( - expected = "Expected size of return type to be greater or equal to the mask lanes" - )] + #[should_panic(expected = "Expected size of return type and mask lanes to match")] fn test_invalid_generics() { - let mask = mask32x32::splat(false); - assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u8, i32, 32>(mask) }, u8::MAX); + let mask = mask32x16::splat(false); + assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 2>(mask) }, u16::MAX); } /// Test that the `simd_bitmask` model is equivalent to the intrinsic for a few random values. /// These values shouldn't be symmetric and ensure that we also handle endianness correctly. #[test] fn test_bitmask_i32() { - check_portable_bitmask::<_, i32, 8>(mask32x8::from([ + check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([ true, true, false, true, false, false, false, true, ])); - check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true])); + check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true])); } #[repr(simd)] @@ -188,14 +185,16 @@ mod test { } /// Compare the value returned by our model and the portable simd representation. - fn check_portable_bitmask(mask: Mask) + fn check_portable_bitmask(mask: Mask) where T: std::simd::MaskElement, LaneCount: SupportedLaneCount, E: kani_intrinsic::MaskElement, + [u8; kani_intrinsic::mask_len(LANES)]: Sized, + u64: From, { assert_eq!( - unsafe { kani_intrinsic::simd_bitmask::<_, u64, E, LANES>(mask.clone()) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, mask.to_bitmask() ); } @@ -206,11 +205,26 @@ mod test { T: Clone, U: PartialEq + Debug, E: kani_intrinsic::MaskElement, - [u8; size_of::()]: Sized, + [u8; kani_intrinsic::mask_len(LANES)]: Sized, { assert_eq!( unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) }, unsafe { simd_bitmask::(mask) } ); } + + /// Similar to portable simd_harness. + #[test] + fn check_mask_harness() { + // From array doesn't work either. Manually build [false, true, false, true] + let mut mask = mask32x4::splat(false); + mask.set(1, true); + mask.set(3, true); + let bitmask = mask.to_bitmask(); + assert_eq!(bitmask, 0b1010); + + let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + assert_eq!(kani_mask, bitmask); + } + } diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index a368c7060e4e..0a0b6d435d46 100644 --- a/tests/kani/SIMD/portable_simd.rs +++ b/tests/kani/SIMD/portable_simd.rs @@ -4,7 +4,7 @@ //! Ensure we have basic support of portable SIMD. #![feature(portable_simd)] -use std::simd::{mask32x4, u64x16}; +use std::simd::{mask32x4, u32x4, u64x16}; #[kani::proof] fn check_sum_any() { @@ -23,3 +23,11 @@ fn check_mask() { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); } + +#[kani::proof] +fn check_resize() { + let x = u32x4::from_array([0, 1, 2, 3]); + assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]); + assert_eq!(x.resize::<2>(9).to_array(), [0, 1]); + +}