From ff40897f12214837e4bad05f6e7160347791e8fb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Dec 2023 12:53:34 -0800 Subject: [PATCH] Revert model change and add new test The change was only needed in the test case, since the way portable simd invokes the intrinsic is still the same My current hypothesis is that the current failure could be an issue with simd_shuffle --- library/kani/src/models/mod.rs | 60 ++++++++++++++++++++------------ tests/kani/SIMD/portable_simd.rs | 10 +++++- 2 files changed, 46 insertions(+), 24 deletions(-) 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]); + +}