Implement Arbitrary for Range*

model-checking · Oct 31, 2024 · e93e86d · e93e86d
1 parent 1fe80f9
commit e93e86d
Showing 1 changed file with 79 additions and 0 deletions.
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
@@ -193,6 +193,85 @@ macro_rules! generate_arbitrary {
         pub mod slice {
             kani_core::slice_generator!();
         }
+
+        mod range_structures {
+            use super::Arbitrary;
+            use core::{
+                mem,
+                ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive},
+            };
+
+            impl<T> Arbitrary for Bound<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    match u8::any() % 3 {
+                        0 => Bound::Included(T::any()),
+                        1 => Bound::Excluded(T::any()),
+                        _ => Bound::Unbounded,
+                    }
+                }
+            }
+
+            impl<T> Arbitrary for Range<T>
+            where
+                T: Arbitrary + PartialOrd,
+            {
+                fn any() -> Self {
+                    let (mut first, mut second) = (T::any(), T::any());
+                    adjust(&mut first, &mut second);
+                    first..second
+                }
+            }
+
+            impl<T> Arbitrary for RangeFrom<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    T::any()..
+                }
+            }
+
+            impl<T> Arbitrary for RangeInclusive<T>
+            where
+                T: Arbitrary + PartialOrd,
+            {
+                fn any() -> Self {
+                    let (mut first, mut second) = (T::any(), T::any());
+                    adjust(&mut first, &mut second);
+                    first..=second
+                }
+            }
+
+            impl<T> Arbitrary for RangeTo<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    ..T::any()
+                }
+            }
+
+            impl<T> Arbitrary for RangeToInclusive<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    ..=T::any()
+                }
+            }
+
+            fn adjust<T>(first: &mut T, second: &mut T)
+            where
+                T: PartialOrd,
+            {
+                if first > second {
+                    mem::swap(first, second);
+                }
+            }
+        }
     };
 }