Implement derive macro for Arbitrary #2016
Conversation
|
I want to make it clear I don't object, but do we want to duplicate stuff like this ourselves versus directing people towards Bolero and |
|
I see your point, but I don't think we should have a hard dependency on |
library/kani_macros/src/derive.rs
Outdated
| /// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` | ||
| /// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` | ||
| /// For unit field, generate an empty initialization. | ||
| fn init_item(ident: &Ident, fields: &Fields) -> TokenStream { |
There was a problem hiding this comment.
Rename to construct_symbolic_item or construct_nondet_item? The init gives an impression that it's getting initialized to some (concrete) value.
There was a problem hiding this comment.
Is init_symbolic_item OK?
library/kani_macros/src/derive.rs
Outdated
| /// Generate the body of the function `any()` for structures. | ||
| fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream { | ||
| if data.variants.is_empty() { | ||
| abort!(Span::call_site(), "Cannot derive `Arbitrary` for `{}`", ident; |
There was a problem hiding this comment.
Should we make this case a no-op? It seems the compiler doesn't complain about zero-variant enums, e.g.:
#[derive(Debug)]
enum Foo {}
fn main() {}$ rustc enum.rs && ./enum
$
There was a problem hiding this comment.
But invoking kany::any::<Foo>() would an error with a not so friendly message.
There was a problem hiding this comment.
I see. I guess it doesn't matter much.
library/kani_macros/src/derive.rs
Outdated
| note = ident.span() => "`{}` has zero variants and cannot be instantiated", ident | ||
| ); | ||
| } | ||
| let arms = data.variants.iter().enumerate().map(|(idx, variant)| { |
There was a problem hiding this comment.
I think I see what this is doing, but can you add to the function documentation an example of the output?
library/kani_macros/src/derive.rs
Outdated
| }); | ||
|
|
||
| quote! { | ||
| match kani::any() { |
There was a problem hiding this comment.
Is this guaranteed to use a type that is wide enough for the number of variants?
There was a problem hiding this comment.
Yes. Because the type will be decided based on the number of match conditions
| @@ -0,0 +1,11 @@ | |||
| // Copyright Kani Contributors | |||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | |||
| //! Check that Kani can automatically derive an empty Arbitrary enum. | |||
There was a problem hiding this comment.
"cannot" instead of "can"? But see my comment on making those a no-op.
There was a problem hiding this comment.
I guess it can now.
|
|
||
| Checking harness check_enum_wrapper... | ||
|
|
||
| SUCCESS\ |
There was a problem hiding this comment.
Are you relying on this being reported as "UNREACHABLE" if the variant is not possible? If so, you might want to use the brand new cover macro instead :)
There was a problem hiding this comment.
Yes. I was thinking about that while writing all these tests. =)
| fn check_arbitrary_point() { | ||
| let point: Point<i32, i8> = kani::any(); | ||
| if kani::any() { | ||
| assert!(point.x >= 0); |
There was a problem hiding this comment.
Might want to use cover instead.
There was a problem hiding this comment.
Yes! I will rewrite them.
Co-authored-by: Zyad Hassan <[email protected]>
3 participants
Description of changes:
Introduce a
derivemacro that allows users to annotate their structs and enums with#[derive(kani::Arbitray)]. This will allow users to easily generate implementation of theArbitrarytypes for their custom structs and enums when their arbitrary value is a combination of its fields arbitrary values.Resolved issues:
Resolves #726
Related RFC:
Call-outs:
cfg_attrto actually use the derive in production code. I.e.:#[cfg_attr(kani, derive(kani::Arbitrary))]Testing:
How is this change tested? New tests
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.