Implement Arbitrary for Rc<T> and Arc<T> - #4697
Merged
Merged
Conversation
Box<T> has an Arbitrary implementation, but Rc<T> and Arc<T> did not, so functions taking reference-counted arguments could not be verified against nondeterministic inputs (and were skipped by 'kani autoharness' with 'Missing Arbitrary implementation'). Add the analogous implementations. Unlike slice or container arguments, these need no bound: a smart pointer to T covers exactly the values of T, so the generated values retain Kani's usual full-coverage guarantee. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
feliperodri
added a commit
to tautschnig/kani
that referenced
this pull request
Aug 24, 2026
…odel-checking#4698) ### Description **Stacked on model-checking#4697** (only the last commit is new; review that one). `Box<T>`/`Rc<T>`/`Arc<T>` arguments were only supported by autoharness when `T` itself implements `Arbitrary` (resolving the blanket impls). When `T` merely *can derive* `Arbitrary` — the common case for plain structs without kani annotations — such arguments were skipped. This PR adds three generation models (`any_box`/`any_rc`/`any_arc`) whose internal `kani::any::<T>()` call gets the compiler-synthesized `Arbitrary` implementation via `AutomaticArbitraryPass`, exactly as for direct arguments of such types. Two design points: - **Optional models.** The models require `alloc`, so they exist only in the `kani` library, not `core::kani`. This introduces `KaniModel::is_optional()`: `validate_kani_functions` tolerates their absence and the autoharness passes hold them as `Option<FnDef>`, gracefully rejecting smart-pointer arguments in flows where they're unavailable (`kani verify-std` re-validated with `--force-rerun` to make sure the run wasn't cached). - **Robust detection.** `Box` via `is_box()`, `Rc`/`Arc` via their rustc diagnostic items (no name matching), plus a return-type equality check on the resolved model instance — which also correctly rejects non-default allocators (`Box<T, A>`); an arity-based check would have wrongly rejected plain `Box<T>` (= `Box<T, Global>`). Per the bounded-features policy (model-checking#4691/model-checking#4693): these values are **unbounded** — a smart pointer to `T` covers exactly the values of `T` — so they need no `--bounded-arguments` gating and retain the full-coverage guarantee, demonstrated by a cover check in the test. ### Testing New script-based test `cargo_autoharness_smart_pointers`: `Box`/`Rc`/`Arc` of both implementing and only-derivable pointees (all verified), a full-coverage cover check on the pointee (SATISFIED) with a correctly failing assertion, and graceful skipping of a pointee that can neither implement nor derive `Arbitrary`. Full autoharness suite (14 tests), `verify_std_cmd`/`std_codegen` (force-rerun), and `kani-compiler` unit tests pass. Towards model-checking#3832 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Box<T>implementsArbitrary, butRc<T>andArc<T>did not, so functions taking reference-counted arguments could not be verified against nondeterministic inputs — and were skipped bykani autoharnesswith "Missing Arbitrary implementation" (smart-pointer receivers are among the largest skip classes in the top-100 crates.io evaluation). This PR adds the analogous implementations.Note that unlike slice/container arguments (#4691/#4693), these need no bound and no opt-in flag: a smart pointer to
Tcovers exactly the values ofT, so the generated values retain Kani's usual full-coverage guarantee.A follow-up will extend autoharness to smart pointers around types that only can-derive
Arbitrary(compiler-synthesized implementations); that requires compiler-side models that depend onallocand hence some optional-model plumbing for theno_coreflow.Testing
New test
tests/kani/Arbitrary/rc_arc.rswith cover checks proving extreme values, specific values, and nested smart pointers (Rc<Arc<u8>>) are all generated (all SATISFIED). TheArbitrarysuite andkanilibrary unit/doc tests pass; verified via autoharness thatRc<T>/Arc<T>-taking functions are now selected and verified.Towards #3832
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.