From 51383e952ab605a0e4722be2a8b3027569ce6d2e Mon Sep 17 00:00:00 2001 From: hz2 Date: Thu, 9 Jul 2026 15:24:54 -0700 Subject: [PATCH 1/2] Implement BoundedArbitrary for BTreeMap and BTreeSet Add BoundedArbitrary implementations for BTreeMap and BTreeSet, following the same pattern as the existing HashMap and HashSet impls. BTreeMap and BTreeSet operations cause state-space explosion during verification due to tree rebalancing internals. Providing a bounded constructor via BoundedArbitrary gives users an idiomatic way to generate symbolic BTree collections with controlled size. Usage: let map: BTreeMap = kani::bounded_any::<_, 4>(); --- library/kani/src/bounded_arbitrary.rs | 31 +++++++++++++++++++ .../bounded-arbitrary/btree/btree.expected | 10 ++++++ .../expected/bounded-arbitrary/btree/btree.rs | 24 ++++++++++++++ 3 files changed, 65 insertions(+) create mode 100644 tests/expected/bounded-arbitrary/btree/btree.expected create mode 100644 tests/expected/bounded-arbitrary/btree/btree.rs diff --git a/library/kani/src/bounded_arbitrary.rs b/library/kani/src/bounded_arbitrary.rs index 55b5f03662c0..006b1aaf8f6c 100644 --- a/library/kani/src/bounded_arbitrary.rs +++ b/library/kani/src/bounded_arbitrary.rs @@ -76,3 +76,34 @@ where hash_set } } + +impl BoundedArbitrary for std::collections::BTreeMap +where + K: Arbitrary + std::cmp::Ord, + V: Arbitrary, +{ + fn bounded_any() -> Self { + let mut btree_map = std::collections::BTreeMap::new(); + for _ in 0..N { + if bool::any() { + btree_map.insert(K::any(), V::any()); + } + } + btree_map + } +} + +impl BoundedArbitrary for std::collections::BTreeSet +where + V: Arbitrary + std::cmp::Ord, +{ + fn bounded_any() -> Self { + let mut btree_set = std::collections::BTreeSet::new(); + for _ in 0..N { + if bool::any() { + btree_set.insert(V::any()); + } + } + btree_set + } +} diff --git a/tests/expected/bounded-arbitrary/btree/btree.expected b/tests/expected/bounded-arbitrary/btree/btree.expected new file mode 100644 index 000000000000..3a6ba3a7b4f6 --- /dev/null +++ b/tests/expected/bounded-arbitrary/btree/btree.expected @@ -0,0 +1,10 @@ +Checking harness check_btreeset... + + ** 3 of 3 cover properties satisfied + +Checking harness check_btreemap... + + ** 3 of 3 cover properties satisfied + +Manual Harness Summary: +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/bounded-arbitrary/btree/btree.rs b/tests/expected/bounded-arbitrary/btree/btree.rs new file mode 100644 index 000000000000..3a2448c12909 --- /dev/null +++ b/tests/expected/bounded-arbitrary/btree/btree.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This file tests whether we can generate a bounded BTreeMap/BTreeSet that has any possible size between 0-BOUND + +#[kani::proof] +#[kani::unwind(5)] +fn check_btreemap() { + const BOUND: usize = 2; + let btree_map: std::collections::BTreeMap = kani::bounded_any::<_, BOUND>(); + kani::cover!(btree_map.len() == 0); + kani::cover!(btree_map.len() == 1); + kani::cover!(btree_map.len() == 2); +} + +#[kani::proof] +#[kani::unwind(5)] +fn check_btreeset() { + const BOUND: usize = 2; + let btree_set: std::collections::BTreeSet = kani::bounded_any::<_, BOUND>(); + kani::cover!(btree_set.len() == 0); + kani::cover!(btree_set.len() == 1); + kani::cover!(btree_set.len() == 2); +} From afa39bef6b1202d97df2d4ca7453f9892dcc05e4 Mon Sep 17 00:00:00 2001 From: hz2 Date: Fri, 17 Jul 2026 13:46:26 -0700 Subject: [PATCH 2/2] Address review feedback on BTreeMap/BTreeSet BoundedArbitrary Note that duplicate arbitrary keys/values collapse cardinality, and assert the upper-bound invariant explicitly in the test harnesses. --- library/kani/src/bounded_arbitrary.rs | 4 ++++ tests/expected/bounded-arbitrary/btree/btree.rs | 2 ++ 2 files changed, 6 insertions(+) diff --git a/library/kani/src/bounded_arbitrary.rs b/library/kani/src/bounded_arbitrary.rs index 006b1aaf8f6c..7f51d7b81a6e 100644 --- a/library/kani/src/bounded_arbitrary.rs +++ b/library/kani/src/bounded_arbitrary.rs @@ -82,6 +82,8 @@ where K: Arbitrary + std::cmp::Ord, V: Arbitrary, { + // duplicate `K::any()` values overwrite earlier entries, so the reachable + // map sizes are `0..=N` rather than always equal to the number of insert branches taken fn bounded_any() -> Self { let mut btree_map = std::collections::BTreeMap::new(); for _ in 0..N { @@ -97,6 +99,8 @@ impl BoundedArbitrary for std::collections::BTreeSet where V: Arbitrary + std::cmp::Ord, { + // duplicate `V::any()` values collapse into one entry, so the reachable + // set sizes are `0..=N` rather than always equal to the number of insert branches taken fn bounded_any() -> Self { let mut btree_set = std::collections::BTreeSet::new(); for _ in 0..N { diff --git a/tests/expected/bounded-arbitrary/btree/btree.rs b/tests/expected/bounded-arbitrary/btree/btree.rs index 3a2448c12909..ea3b9c11c745 100644 --- a/tests/expected/bounded-arbitrary/btree/btree.rs +++ b/tests/expected/bounded-arbitrary/btree/btree.rs @@ -8,6 +8,7 @@ fn check_btreemap() { const BOUND: usize = 2; let btree_map: std::collections::BTreeMap = kani::bounded_any::<_, BOUND>(); + assert!(btree_map.len() <= BOUND); kani::cover!(btree_map.len() == 0); kani::cover!(btree_map.len() == 1); kani::cover!(btree_map.len() == 2); @@ -18,6 +19,7 @@ fn check_btreemap() { fn check_btreeset() { const BOUND: usize = 2; let btree_set: std::collections::BTreeSet = kani::bounded_any::<_, BOUND>(); + assert!(btree_set.len() <= BOUND); kani::cover!(btree_set.len() == 0); kani::cover!(btree_set.len() == 1); kani::cover!(btree_set.len() == 2);