Autoharness: support smart pointers of compiler-derivable pointees - #4698
Open
tautschnig wants to merge 2 commits into
Open
Autoharness: support smart pointers of compiler-derivable pointees#4698tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
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>
Box<T>, Rc<T>, and Arc<T> arguments were only supported when T itself implements Arbitrary (resolving the smart pointer's blanket Arbitrary implementation). When T merely *can derive* Arbitrary -- the common case for plain structs without kani annotations -- such arguments were skipped. Add three generation models (any_box/any_rc/any_arc) whose internal kani::any::<T>() call is replaced with the compiler-synthesized Arbitrary implementation by AutomaticArbitraryPass, exactly as for direct arguments of such types. The models live in the kani library only: they require alloc and thus have no core::kani counterpart, so this introduces the notion of *optional* models (KaniModel::is_optional): validate_kani_functions tolerates their absence, and the autoharness passes hold them as Option<FnDef>, rejecting smart-pointer arguments in flows where the models are unavailable (e.g. kani verify-std). Smart-pointer detection uses is_box() and the Rc/Arc diagnostic items, plus a return-type equality check on the resolved model, which also correctly rejects non-default allocators (Box<T, A>). These values are unbounded -- a smart pointer to T covers exactly the values of T -- so they need no --bounded-arguments gating and retain Kani's usual full-coverage guarantee (demonstrated by a cover check in the test). Towards model-checking#3832 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
Stacked on #4697 (only the last commit is new; review that one).
Box<T>/Rc<T>/Arc<T>arguments were only supported by autoharness whenTitself implementsArbitrary(resolving the blanket impls). WhenTmerely can deriveArbitrary— 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 internalkani::any::<T>()call gets the compiler-synthesizedArbitraryimplementation viaAutomaticArbitraryPass, exactly as for direct arguments of such types.Two design points:
alloc, so they exist only in thekanilibrary, notcore::kani. This introducesKaniModel::is_optional():validate_kani_functionstolerates their absence and the autoharness passes hold them asOption<FnDef>, gracefully rejecting smart-pointer arguments in flows where they're unavailable (kani verify-stdre-validated with--force-rerunto make sure the run wasn't cached).Boxviais_box(),Rc/Arcvia 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 plainBox<T>(=Box<T, Global>).Per the bounded-features policy (#4691/#4693): these values are unbounded — a smart pointer to
Tcovers exactly the values ofT— so they need no--bounded-argumentsgating 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/Arcof 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 deriveArbitrary.Full autoharness suite (14 tests),
verify_std_cmd/std_codegen(force-rerun), andkani-compilerunit tests pass.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.