From 1f20a2ba9a3ddf60c4a0b9eebd6fedba1a577532 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 17 Apr 2025 16:34:37 -0400 Subject: [PATCH 1/4] derive kani::Arbitrary for Wrapping and Saturating types --- library/core/src/num/saturating.rs | 1 + library/core/src/num/wrapping.rs | 1 + 2 files changed, 2 insertions(+) diff --git a/library/core/src/num/saturating.rs b/library/core/src/num/saturating.rs index 3f4791e163e69..b54d1305d3e28 100644 --- a/library/core/src/num/saturating.rs +++ b/library/core/src/num/saturating.rs @@ -35,6 +35,7 @@ use crate::ops::{ #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default, Hash)] #[repr(transparent)] #[rustc_diagnostic_item = "Saturating"] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Saturating(#[stable(feature = "saturating_int_impl", since = "1.74.0")] pub T); #[stable(feature = "saturating_int_impl", since = "1.74.0")] diff --git a/library/core/src/num/wrapping.rs b/library/core/src/num/wrapping.rs index 55fa91d0b9f49..6a0049df77aad 100644 --- a/library/core/src/num/wrapping.rs +++ b/library/core/src/num/wrapping.rs @@ -40,6 +40,7 @@ use crate::ops::{ #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default, Hash)] #[repr(transparent)] #[rustc_diagnostic_item = "Wrapping"] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Wrapping(#[stable(feature = "rust1", since = "1.0.0")] pub T); #[stable(feature = "rust1", since = "1.0.0")] From 88e434d9ef855f99f9aab87df983477f71754930 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 18 Apr 2025 11:27:08 -0400 Subject: [PATCH 2/4] Implement Arbitrary manually The implementations need a stability attribute. Co-authored-by: Michael Tautschnig --- library/core/src/num/saturating.rs | 9 ++++++++- library/core/src/num/wrapping.rs | 9 ++++++++- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/saturating.rs b/library/core/src/num/saturating.rs index b54d1305d3e28..59164e703eb47 100644 --- a/library/core/src/num/saturating.rs +++ b/library/core/src/num/saturating.rs @@ -35,9 +35,16 @@ use crate::ops::{ #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default, Hash)] #[repr(transparent)] #[rustc_diagnostic_item = "Saturating"] -#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Saturating(#[stable(feature = "saturating_int_impl", since = "1.74.0")] pub T); +#[cfg(kani)] +#[stable(feature = "saturating_int_impl", since = "1.74.0")] +impl kani::Arbitrary for Saturating { + fn any() -> Self { + Self { 0: kani::any() } + } +} + #[stable(feature = "saturating_int_impl", since = "1.74.0")] impl fmt::Debug for Saturating { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { diff --git a/library/core/src/num/wrapping.rs b/library/core/src/num/wrapping.rs index 6a0049df77aad..33e982d9b6208 100644 --- a/library/core/src/num/wrapping.rs +++ b/library/core/src/num/wrapping.rs @@ -40,9 +40,16 @@ use crate::ops::{ #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default, Hash)] #[repr(transparent)] #[rustc_diagnostic_item = "Wrapping"] -#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Wrapping(#[stable(feature = "rust1", since = "1.0.0")] pub T); +#[cfg(kani)] +#[stable(feature = "rust1", since = "1.0.0")] +impl kani::Arbitrary for Wrapping { + fn any() -> Self { + Self { 0: kani::any() } + } +} + #[stable(feature = "rust1", since = "1.0.0")] impl fmt::Debug for Wrapping { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { From a14018a9af64536c1c7643662acb0064cf80b6f6 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 18 Apr 2025 11:28:33 -0400 Subject: [PATCH 3/4] add use crate::kani to top of files --- library/core/src/num/saturating.rs | 2 ++ library/core/src/num/wrapping.rs | 2 ++ 2 files changed, 4 insertions(+) diff --git a/library/core/src/num/saturating.rs b/library/core/src/num/saturating.rs index 59164e703eb47..6426d6460fea2 100644 --- a/library/core/src/num/saturating.rs +++ b/library/core/src/num/saturating.rs @@ -1,6 +1,8 @@ //! Definitions of `Saturating`. use crate::fmt; +#[cfg(kani)] +use crate::kani; use crate::ops::{ Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign, Mul, MulAssign, Neg, Not, Rem, RemAssign, Sub, SubAssign, diff --git a/library/core/src/num/wrapping.rs b/library/core/src/num/wrapping.rs index 33e982d9b6208..491845f6ef8f4 100644 --- a/library/core/src/num/wrapping.rs +++ b/library/core/src/num/wrapping.rs @@ -1,6 +1,8 @@ //! Definitions of `Wrapping`. use crate::fmt; +#[cfg(kani)] +use crate::kani; use crate::ops::{ Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign, Mul, MulAssign, Neg, Not, Rem, RemAssign, Shl, ShlAssign, Shr, ShrAssign, Sub, SubAssign, From d508266f0af45c8735b0eb50a23a3721d4f8139a Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 18 Apr 2025 11:30:59 -0400 Subject: [PATCH 4/4] derive Arbitrary on Simd --- library/portable-simd/crates/core_simd/src/vector.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/portable-simd/crates/core_simd/src/vector.rs b/library/portable-simd/crates/core_simd/src/vector.rs index d76a6cd52bfc5..4bbc4f59732bb 100644 --- a/library/portable-simd/crates/core_simd/src/vector.rs +++ b/library/portable-simd/crates/core_simd/src/vector.rs @@ -5,6 +5,9 @@ use crate::simd::{ ptr::{SimdConstPtr, SimdMutPtr}, }; +#[cfg(kani)] +use crate::kani; + /// A SIMD vector with the shape of `[T; N]` but the operations of `T`. /// /// `Simd` supports the operators (+, *, etc.) that `T` does in "elementwise" fashion. @@ -100,6 +103,7 @@ use crate::simd::{ // avoided, as it will likely become illegal on `#[repr(simd)]` structs in the future. It also // causes rustc to emit illegal LLVM IR in some cases. #[repr(simd, packed)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Simd([T; N]) where LaneCount: SupportedLaneCount,