diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 90a2ae5e4c82..3ef474b65364 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -193,6 +193,74 @@ macro_rules! generate_arbitrary { pub mod slice { kani_core::slice_generator!(); } + + mod range_structures { + use super::{ + Arbitrary, + core_path::{ + mem, + ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive}, + }, + }; + + impl Arbitrary for Bound + where + T: Arbitrary, + { + fn any() -> Self { + match u8::any() { + 0 => Bound::Included(T::any()), + 1 => Bound::Excluded(T::any()), + _ => Bound::Unbounded, + } + } + } + + impl Arbitrary for Range + where + T: Arbitrary, + { + fn any() -> Self { + T::any()..T::any() + } + } + + impl Arbitrary for RangeFrom + where + T: Arbitrary, + { + fn any() -> Self { + T::any().. + } + } + + impl Arbitrary for RangeInclusive + where + T: Arbitrary, + { + fn any() -> Self { + T::any()..=T::any() + } + } + + impl Arbitrary for RangeTo + where + T: Arbitrary, + { + fn any() -> Self { + ..T::any() + } + } + + impl Arbitrary for RangeToInclusive + where + T: Arbitrary, + { + fn any() -> Self { + ..=T::any() + } + } + } }; } diff --git a/tests/kani/Arbitrary/ops.rs b/tests/kani/Arbitrary/ops.rs new file mode 100644 index 000000000000..6ae97b2335f4 --- /dev/null +++ b/tests/kani/Arbitrary/ops.rs @@ -0,0 +1,114 @@ +// 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> = kani::any(); + match elem.0 { + Bound::Included(elem) => { + assert!(elem < 100); + } + Bound::Excluded(elem) => { + assert!(elem < 100); + } + Bound::Unbounded => {} + } +} + +#[kani::proof] +fn range() { + let elem: Wrapper> = kani::any(); + assert!(elem.0.start < 100); + assert!(elem.0.end < 100); +} + +#[kani::proof] +fn range_from() { + let elem: Wrapper> = kani::any(); + assert!(elem.0.start < 100); +} + +#[kani::proof] +fn range_inclusive() { + let elem: Wrapper> = kani::any(); + assert!(*elem.0.start() < 100); + assert!(*elem.0.end() < 100); +} + +#[kani::proof] +fn range_to() { + let elem: Wrapper> = kani::any(); + assert!(elem.0.end < 100); +} + +#[kani::proof] +fn range_to_inclusive() { + let elem: Wrapper> = kani::any(); + assert!(elem.0.end < 100); +} + +struct Wrapper(T); + +impl kani::Arbitrary for Wrapper> { + 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> { + 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> { + fn any() -> Self { + let val = kani::any()..; + kani::assume(val.start < 100); + Self(val) + } +} + +impl kani::Arbitrary for Wrapper> { + 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> { + fn any() -> Self { + let val = ..kani::any(); + kani::assume(val.end < 100); + Self(val) + } +} + +impl kani::Arbitrary for Wrapper> { + fn any() -> Self { + let val = ..=kani::any(); + kani::assume(val.end < 100); + Self(val) + } +}