Generate nondeterministic reference-count state for Rc/Arc Arbitrary

[rbeauchamp]

Description

kani::any::<Rc<T>>() / kani::any::<Arc<T>>() (and the AnyRc/AnyArc autoharness models) always produced a fresh allocation: strong_count == 1 and weak_count == 0 on every generated value. A function observing reference-count state could be verified for states a real caller can violate — e.g. assert_eq!(Arc::strong_count(&a), 1) passed even though let _y = a.clone(); f(a) trips it at runtime. This is an input-space under-approximation (false-negative hazard) affecting strong_count, weak_count, get_mut, try_unwrap, make_mut, etc.

Design

Every documented count-dependent behavior of Rc/Arc branches only on uniqueness: strong_count == 1, and for get_mut/try_unwrap additionally weak_count == 0. The behavioral equivalence classes of real reference-count states are therefore exactly four — strong ∈ {1, ≥2} × weak ∈ {0, ≥1} — and the generator now covers all four with one representative each (strong_count ∈ {1, 2}, weak_count ∈ {0, 1}) by nondeterministically leaking a clone() and/or a downgrade(). A leaked reference is observationally identical to one held by a caller for the duration of the function under verification. Generation stays loop-free, so it needs no unwinding bound, and the pointee remains fully nondeterministic.

Note: this intentionally makes previously-"verified" uniqueness assertions fail — that is the soundness fix taking effect, not a regression.

Context

Surfaced in #4752 (during review of #4698). The issue offered two directions — model nondeterministic refcount state, or document the limitation; this PR implements the former, and the equivalence-class argument means the {1, 2} × {0, 1} representatives are behaviorally complete for the documented API surface rather than a lossy bound.

Manual testing

• New tests/kani/RefCount/nondet_rc_arc.rs (12 harnesses): count validity (strong_count >= 1), reachability of shared/weak states (#[kani::should_panic] on the old always-unique assertions — each now fails on exactly the count assertion), both get_mut outcomes, get_mut succeeds under assume(unique && no weak), and extreme pointee values (kani::cover!(*rc == 255) SATISFIED) under sharing.
• Extended tests/script-based-pre/cargo_autoharness_smart_pointers/ with arc_count, which fails through the AnyArc model path on assertion failed: Arc::strong_count(&a) == 1 (verifying the models carry the same semantics); .expected updated.
• Regression sweep of existing Rc/Arc-touching suites (FunctionContracts/receiver_contracts, SizeAndAlignOfDst, UnsizedCoercion, AsyncAwait, Drop): 28/28 pass.

Resolves #4752

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

🟡 Changes recommended

Restricting exact observable counts to {1,2} × {0,1} leaves an unsound input-space under-approximation while reporting generation as unbounded.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Expands nondeterministic Rc/Arc generation to include shared and weak-reference states.

Changes:

• Generates four representative reference-count states.
• Adds direct and autoharness regression tests.
• Updates expected autoharness failures.

File summaries

File	Description
library/kani/src/arbitrary.rs	Adds nondeterministic leaked strong/weak references.
tests/kani/RefCount/nondet_rc_arc.rs	Tests reference-count behavior and pointee coverage.
tests/script-based-pre/cargo_autoharness_smart_pointers/src/lib.rs	Adds an AnyArc count test.
tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.expected	Records the additional expected failure.

Review details

Suppressed comments (3)

library/kani/src/arbitrary.rs:52

• This also caps Arc at strong count 2 and weak count 1, although both count APIs reveal larger valid values exactly. A function that checks an incoming Arc has strong_count <= 2 or weak_count <= 1 can therefore be incorrectly verified; this needs full count modeling or explicit bounded semantics.

        if bool::any() {
            std::mem::forget(arc.clone());
        }
        if bool::any() {
            std::mem::forget(std::sync::Arc::downgrade(&arc));

library/kani/src/arbitrary.rs:82

• The AnyRc model has the same finite refcount cap, while autoharness still classifies smart-pointer models as unbounded ArgSupport::Arbitrary (kani-compiler/src/kani_middle/mod.rs:1169-1172, 1230-1236). Consequently, successful proofs about exact counts above 2/1 receive no bounded-result caveat. Either model every valid count or route this model through bounded-argument classification.

    if crate::any() {
        std::mem::forget(rc.clone());
    }
    if crate::any() {
        std::mem::forget(std::rc::Rc::downgrade(&rc));

library/kani/src/arbitrary.rs:96

• The AnyArc model is likewise finite but is reported by autoharness as unbounded. Exact count checks such as Arc::strong_count(&a) <= 2 can therefore produce an unsound successful result without requiring --bounded-arguments; please generate the full state space or classify this path as bounded.

    if crate::any() {
        std::mem::forget(arc.clone());
    }
    if crate::any() {
        std::mem::forget(std::sync::Arc::downgrade(&arc));

• Files reviewed: 4/4 changed files
• Comments generated: 2
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.