Generate nondeterministic reference-count state for Rc/Arc Arbitrary

library/kani/src/arbitrary.rs

@@ -15,12 +15,27 @@ where
     }
 }
 
+/// Reference-count observers (`strong_count`, `weak_count`, `get_mut`, `try_unwrap`,
+/// `make_mut`) branch only on *uniqueness*: every documented count-dependent behavior of
+/// `Rc`/`Arc` is decided by whether `strong_count == 1` and whether `weak_count == 0`.
+/// A nondeterministic value therefore covers all behavioral equivalence classes of real
+/// reference-count states by generating one representative per class:
+/// `strong_count ∈ {1, 2}` (2 stands in for every shared count) and
+/// `weak_count ∈ {0, 1}`. Extra references are leaked, which is observationally identical
+/// to references held by a caller for the duration of the function under verification.
 impl<T> Arbitrary for std::rc::Rc<T>
 where
     T: Arbitrary,
 {
     fn any() -> Self {
-        std::rc::Rc::new(T::any())
+        let rc = std::rc::Rc::new(T::any());
+        if bool::any() {
+            std::mem::forget(rc.clone());
+        }
+        if bool::any() {
+            std::mem::forget(std::rc::Rc::downgrade(&rc));
+        }
+        rc
     }
 }
 
@@ -29,7 +44,14 @@ where
     T: Arbitrary,
 {
     fn any() -> Self {
-        std::sync::Arc::new(T::any())
+        let arc = std::sync::Arc::new(T::any());
+        if bool::any() {
+            std::mem::forget(arc.clone());
+        }
+        if bool::any() {
+            std::mem::forget(std::sync::Arc::downgrade(&arc));
+        }
+        arc
     }
 }
 
@@ -52,14 +74,28 @@ pub fn any_box<T: Arbitrary>() -> Box<T> {
 #[inline(never)]
 #[doc(hidden)]
 pub fn any_rc<T: Arbitrary>() -> std::rc::Rc<T> {
-    std::rc::Rc::new(crate::any())
+    let rc: std::rc::Rc<T> = std::rc::Rc::new(crate::any());
+    if crate::any() {
+        std::mem::forget(rc.clone());
+    }
+    if crate::any() {
+        std::mem::forget(std::rc::Rc::downgrade(&rc));
+    }
+    rc
 }
 
 #[kanitool::fn_marker = "AnyArcModel"]
 #[inline(never)]
 #[doc(hidden)]
 pub fn any_arc<T: Arbitrary>() -> std::sync::Arc<T> {
-    std::sync::Arc::new(crate::any())
+    let arc: std::sync::Arc<T> = std::sync::Arc::new(crate::any());
+    if crate::any() {
+        std::mem::forget(arc.clone());
+    }
+    if crate::any() {
+        std::mem::forget(std::sync::Arc::downgrade(&arc));
+    }
+    arc
 }
 
 impl Arbitrary for std::time::Duration {

tests/kani/RefCount/nondet_rc_arc.rs

@@ -0,0 +1,106 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Nondeterministic `Rc<T>`/`Arc<T>` values must cover every behavioral equivalence class of
+//! reference-count state: unique vs. shared strong ownership, and presence vs. absence of weak
+//! references (https://github.com/model-checking/kani/issues/4752). Count observers only branch
+//! on uniqueness, so `strong_count == 2` represents every shared state and `weak_count == 1`
+//! every state with weak references.
+
+use std::rc::Rc;
+use std::sync::Arc;
+
+// --- Validity: the generated reference is always a valid, countable handle. ---
+
+#[kani::proof]
+fn rc_strong_count_at_least_one() {
+    let rc: Rc<u8> = kani::any();
+    assert!(Rc::strong_count(&rc) >= 1);
+}
+
+#[kani::proof]
+fn arc_strong_count_at_least_one() {
+    let arc: Arc<u8> = kani::any();
+    assert!(Arc::strong_count(&arc) >= 1);
+}
+
+// --- Reachability: shared ownership and weak references are both generated.
+// Each `should_panic` harness asserts the old (incomplete) behavior; it must FAIL, proving
+// the newly covered class is reachable.
+
+#[kani::proof]
+#[kani::should_panic]
+fn rc_shared_state_reachable() {
+    let rc: Rc<u8> = kani::any();
+    assert_eq!(Rc::strong_count(&rc), 1);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn rc_weak_state_reachable() {
+    let rc: Rc<u8> = kani::any();
+    assert_eq!(Rc::weak_count(&rc), 0);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn arc_shared_state_reachable() {
+    let arc: Arc<u8> = kani::any();
+    assert_eq!(Arc::strong_count(&arc), 1);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn arc_weak_state_reachable() {
+    let arc: Arc<u8> = kani::any();
+    assert_eq!(Arc::weak_count(&arc), 0);
+}
+
+// --- Count-dependent APIs observe both outcomes. ---
+
+#[kani::proof]
+#[kani::should_panic]
+fn rc_get_mut_can_fail() {
+    let mut rc: Rc<u8> = kani::any();
+    assert!(Rc::get_mut(&mut rc).is_some());
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn arc_get_mut_can_fail() {
+    let mut arc: Arc<u8> = kani::any();
+    assert!(Arc::get_mut(&mut arc).is_some());
+}
+
+// Uniqueness still implies exclusive access: the one case where `get_mut` must succeed.
+#[kani::proof]
+fn rc_get_mut_succeeds_when_unique() {
+    let mut rc: Rc<u8> = kani::any();
+    kani::assume(Rc::strong_count(&rc) == 1 && Rc::weak_count(&rc) == 0);
+    assert!(Rc::get_mut(&mut rc).is_some());
+}
+
+#[kani::proof]
+fn arc_get_mut_succeeds_when_unique() {
+    let mut arc: Arc<u8> = kani::any();
+    kani::assume(Arc::strong_count(&arc) == 1 && Arc::weak_count(&arc) == 0);
+    assert!(Arc::get_mut(&mut arc).is_some());
+}
+
+// --- The pointee remains fully nondeterministic under sharing. ---
+
+#[kani::proof]
+#[kani::should_panic]
+fn rc_pointee_extreme_values_generated() {
+    let rc: Rc<u8> = kani::any();
+    kani::cover!(*rc == 255);
+    assert!(*rc < 255);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn arc_pointee_extreme_values_generated() {
+    let arc: Arc<u8> = kani::any();
+    kani::cover!(*arc == 255);
+    assert!(*arc < 255);
+}

tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.expected

@@ -6,4 +6,6 @@
 | cargo_autoharness_smart_pointers | box_derived       | #[kani::proof]            | Success             |
 | cargo_autoharness_smart_pointers | rc_derivable      | #[kani::proof]            | Success             |
 | cargo_autoharness_smart_pointers | arc_assert        | #[kani::proof]            | Failure             |
-Complete - 4 successfully verified functions, 1 failures, 5 total.
+| cargo_autoharness_smart_pointers | arc_count         | #[kani::proof]            | Failure             |
+assertion failed: Arc::strong_count(&a) == 1
+Complete - 4 successfully verified functions, 2 failures, 6 total.

tests/script-based-pre/cargo_autoharness_smart_pointers/src/lib.rs

@@ -3,8 +3,10 @@
 
 // Test that the autoharness subcommand supports Box<T>, Rc<T>, and Arc<T> arguments, both for
 // pointee types that implement Arbitrary and for pointees whose Arbitrary implementation the
-// compiler derives (via the AnyBox/AnyRc/AnyArc models). These values are *unbounded*: a smart
-// pointer to T covers exactly the values of T, so no --bounded-arguments is needed.
+// compiler derives (via the AnyBox/AnyRc/AnyArc models). These values are *unbounded* in the
+// pointee: a smart pointer to T covers all values of T, so no --bounded-arguments is needed.
+// Nondeterministic Rc/Arc values additionally cover the reference-count classes (unique vs.
+// shared, with/without weak references), since count observers branch on uniqueness (#4752).
 // The "TEST NOTE" comments explain the expected result per function.
 
 use std::rc::Rc;
@@ -49,6 +51,12 @@ pub fn arc_assert(a: Arc<OnlyDerivable>) {
     assert!(a.x < 255);
 }
 
+// TEST NOTE: should FAIL: a nondeterministic Arc can be shared (strong_count > 1 reachable
+// through the AnyArc model), so uniqueness is not guaranteed (#4752).
+pub fn arc_count(a: Arc<OnlyDerivable>) {
+    assert!(Arc::strong_count(&a) == 1);
+}
+
 // TEST NOTE: skipped (gracefully, without crashing the compiler): unsized pointees are not
 // supported. `Box<str>` is used (rather than e.g. `Box<[u8]>`, which implements
 // `BoundedArbitrary`) so that the argument is genuinely unsupported without `--bounded-arguments`.