From 640f521c517e2d0733003c6222eaa6386c8696da Mon Sep 17 00:00:00 2001 From: Caio Date: Thu, 31 Oct 2024 08:16:07 -0300 Subject: [PATCH 1/2] Implement `Arbitrary` for `Range*` --- library/kani_core/src/arbitrary.rs | 81 ++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 90a2ae5e4c82..b73c33aafa68 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -193,6 +193,87 @@ 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() % 3 { + 0 => Bound::Included(T::any()), + 1 => Bound::Excluded(T::any()), + _ => Bound::Unbounded, + } + } + } + + impl Arbitrary for Range + where + T: Arbitrary + PartialOrd, + { + fn any() -> Self { + let (mut first, mut second) = (T::any(), T::any()); + adjust(&mut first, &mut second); + first..second + } + } + + impl Arbitrary for RangeFrom + where + T: Arbitrary, + { + fn any() -> Self { + T::any().. + } + } + + impl Arbitrary for RangeInclusive + where + T: Arbitrary + PartialOrd, + { + fn any() -> Self { + let (mut first, mut second) = (T::any(), T::any()); + adjust(&mut first, &mut second); + first..=second + } + } + + impl Arbitrary for RangeTo + where + T: Arbitrary, + { + fn any() -> Self { + ..T::any() + } + } + + impl Arbitrary for RangeToInclusive + where + T: Arbitrary, + { + fn any() -> Self { + ..=T::any() + } + } + + fn adjust(first: &mut T, second: &mut T) + where + T: PartialOrd, + { + if first > second { + mem::swap(first, second); + } + } + } }; } From f2780e77c8e3b9b2bb9979bfd5201a2d8487ec96 Mon Sep 17 00:00:00 2001 From: Caio Date: Sat, 2 Nov 2024 15:28:05 -0300 Subject: [PATCH 2/2] Address comments --- library/kani_core/src/arbitrary.rs | 23 ++---- tests/kani/Arbitrary/ops.rs | 114 +++++++++++++++++++++++++++++ 2 files changed, 119 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 Arbitrary for Range 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 Arbitrary for RangeInclusive 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(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..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) + } +}