Skip to content

Commit 29f7a35

Browse files
Implement kani::Arbitrary for Wrapping, Saturating, and Simd types (#328)
Implement `kani::Arbitrary` for the `Wrapping`, `Saturating`, and `Simd` types. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <[email protected]>
1 parent ad096af commit 29f7a35

File tree

3 files changed

+24
-0
lines changed

3 files changed

+24
-0
lines changed

library/core/src/num/saturating.rs

+10
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
//! Definitions of `Saturating<T>`.
22
33
use crate::fmt;
4+
#[cfg(kani)]
5+
use crate::kani;
46
use crate::ops::{
57
Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign,
68
Mul, MulAssign, Neg, Not, Rem, RemAssign, Sub, SubAssign,
@@ -37,6 +39,14 @@ use crate::ops::{
3739
#[rustc_diagnostic_item = "Saturating"]
3840
pub struct Saturating<T>(#[stable(feature = "saturating_int_impl", since = "1.74.0")] pub T);
3941

42+
#[cfg(kani)]
43+
#[stable(feature = "saturating_int_impl", since = "1.74.0")]
44+
impl<T: kani::Arbitrary> kani::Arbitrary for Saturating<T> {
45+
fn any() -> Self {
46+
Self { 0: kani::any() }
47+
}
48+
}
49+
4050
#[stable(feature = "saturating_int_impl", since = "1.74.0")]
4151
impl<T: fmt::Debug> fmt::Debug for Saturating<T> {
4252
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

library/core/src/num/wrapping.rs

+10
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
//! Definitions of `Wrapping<T>`.
22
33
use crate::fmt;
4+
#[cfg(kani)]
5+
use crate::kani;
46
use crate::ops::{
57
Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign,
68
Mul, MulAssign, Neg, Not, Rem, RemAssign, Shl, ShlAssign, Shr, ShrAssign, Sub, SubAssign,
@@ -42,6 +44,14 @@ use crate::ops::{
4244
#[rustc_diagnostic_item = "Wrapping"]
4345
pub struct Wrapping<T>(#[stable(feature = "rust1", since = "1.0.0")] pub T);
4446

47+
#[cfg(kani)]
48+
#[stable(feature = "rust1", since = "1.0.0")]
49+
impl<T: kani::Arbitrary> kani::Arbitrary for Wrapping<T> {
50+
fn any() -> Self {
51+
Self { 0: kani::any() }
52+
}
53+
}
54+
4555
#[stable(feature = "rust1", since = "1.0.0")]
4656
impl<T: fmt::Debug> fmt::Debug for Wrapping<T> {
4757
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

library/portable-simd/crates/core_simd/src/vector.rs

+4
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@ use crate::simd::{
55
ptr::{SimdConstPtr, SimdMutPtr},
66
};
77

8+
#[cfg(kani)]
9+
use crate::kani;
10+
811
/// A SIMD vector with the shape of `[T; N]` but the operations of `T`.
912
///
1013
/// `Simd<T, N>` supports the operators (+, *, etc.) that `T` does in "elementwise" fashion.
@@ -100,6 +103,7 @@ use crate::simd::{
100103
// avoided, as it will likely become illegal on `#[repr(simd)]` structs in the future. It also
101104
// causes rustc to emit illegal LLVM IR in some cases.
102105
#[repr(simd, packed)]
106+
#[cfg_attr(kani, derive(kani::Arbitrary))]
103107
pub struct Simd<T, const N: usize>([T; N])
104108
where
105109
LaneCount<N>: SupportedLaneCount,

0 commit comments

Comments
 (0)