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
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.