From bf6bf695f56b165b765795bbcadc60604aabb93b Mon Sep 17 00:00:00 2001
From: Caio <c410.f3r@gmail.com>
Date: Sat, 2 Nov 2024 14:59:42 -0300
Subject: [PATCH] Address comments

---
 library/kani_core/src/arbitrary.rs |  23 ++----
 tests/kani/Arbitrary/ops.rs        | 113 +++++++++++++++++++++++++++++
 2 files changed, 118 insertions(+), 18 deletions(-)
 create mode 100644 tests/kani/Arbitrary/ops.rs

diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index b73c33aafa68..3ef474b65364 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -208,7 +208,7 @@ macro_rules! generate_arbitrary {
                 T: Arbitrary,
             {
                 fn any() -> Self {
-                    match u8::any() % 3 {
+                    match u8::any() {
                         0 => Bound::Included(T::any()),
                         1 => Bound::Excluded(T::any()),
                         _ => Bound::Unbounded,
@@ -218,12 +218,10 @@ macro_rules! generate_arbitrary {
 
             impl<T> Arbitrary for Range<T>
             where
-                T: Arbitrary + PartialOrd,
+                T: Arbitrary,
             {
                 fn any() -> Self {
-                    let (mut first, mut second) = (T::any(), T::any());
-                    adjust(&mut first, &mut second);
-                    first..second
+                    T::any()..T::any()
                 }
             }
 
@@ -238,12 +236,10 @@ macro_rules! generate_arbitrary {
 
             impl<T> Arbitrary for RangeInclusive<T>
             where
-                T: Arbitrary + PartialOrd,
+                T: Arbitrary,
             {
                 fn any() -> Self {
-                    let (mut first, mut second) = (T::any(), T::any());
-                    adjust(&mut first, &mut second);
-                    first..=second
+                    T::any()..=T::any()
                 }
             }
 
@@ -264,15 +260,6 @@ macro_rules! generate_arbitrary {
                     ..=T::any()
                 }
             }
-
-            fn adjust<T>(first: &mut T, second: &mut T)
-            where
-                T: PartialOrd,
-            {
-                if first > second {
-                    mem::swap(first, second);
-                }
-            }
         }
     };
 }
diff --git a/tests/kani/Arbitrary/ops.rs b/tests/kani/Arbitrary/ops.rs
new file mode 100644
index 000000000000..c0de47c41749
--- /dev/null
+++ b/tests/kani/Arbitrary/ops.rs
@@ -0,0 +1,113 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that users can generate range structures
+
+extern crate kani;
+
+use std::ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive};
+
+#[kani::proof]
+fn bound() {
+    let elem: Wrapper<Bound<u8>> = kani::any();
+    assert!(elem < 100);
+}
+
+#[kani::proof]
+fn range() {
+    let elem: Wrapper<Range<u8>> = kani::any();
+    match elem.0 {
+        Bound::Included(elem) => {
+            assert!(elem < 100);
+        }
+        Bound::Excluded(elem) => {
+            assert!(elem < 100);
+        }
+        Bound::Unbounded => {}
+    }
+}
+
+#[kani::proof]
+fn range_from() {
+    let elem: Wrapper<RangeFrom<u8>> = kani::any();
+    assert!(elem.0.start < 100);
+}
+
+#[kani::proof]
+fn range_inclusive() {
+    let elem: Wrapper<RangeInclusive<u8>> = kani::any();
+    assert!(*elem.0.start() < 100);
+    assert!(*elem.0.end() < 100);
+}
+
+#[kani::proof]
+fn range_to() {
+    let elem: Wrapper<RangeTo<u8>> = kani::any();
+    assert!(elem.0.end < 100);
+}
+
+#[kani::proof]
+fn range_to_inclusive() {
+    let elem: Wrapper<RangeToInclusive<u8>> = kani::any();
+    assert!(elem.0.end < 100);
+}
+
+struct Wrapper<T>(T);
+
+impl kani::Arbitrary for Wrapper<Bound<u8>> {
+    fn any() -> Self {
+        let val = kani::any();
+        match val {
+            Bound::Included(elem) => {
+                kani::assume(elem < 100);
+            }
+            Bound::Excluded(elem) => {
+                kani::assume(elem < 100);
+            }
+            Bound::Unbounded => {}
+        }
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<Range<u8>> {
+    fn any() -> Self {
+        let val = kani::any()..kani::any();
+        kani::assume(val.start < 100);
+        kani::assume(val.end < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeFrom<u8>> {
+    fn any() -> Self {
+        let val = kani::any()..;
+        kani::assume(val.start < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeInclusive<u8>> {
+    fn any() -> Self {
+        let val = kani::any()..=kany::any();
+        kani::assume(*val.start() < 100);
+        kani::assume(*val.end() < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeTo<u8>> {
+    fn any() -> Self {
+        let val = ..kany::any();
+        kani::assume(val.end < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeToInclusive<u8>> {
+    fn any() -> Self {
+        let val = ..=kany::any();
+        kani::assume(val.end < 100);
+        Self(val)
+    }
+}