Create Arbitrary::any_array()

[feliperodri]

We can take advantage of any_raw_internal to set all values in an array to nondet.
Kani users may now use any_array() with a loop-free operation for trivial types,
which improves performance.

Signed-off-by: Felipe R. Monteiro [email protected]

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

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

[celinval]

I'm curious, how does that work?

[zhassan-aws]

Can you clarify what the new version of the PR is doing? Is it providing a new way to create non-det arrays:

let arr: [u8; 10] = kani::Arbitrary::any_array();

? If so, how does it compare to the existing one:

let arr: [u8; 10] = kani::any();

and are there any advantages to the new approach?

[celinval]

Weren't you planning to also make changes to any_slice?

[celinval]

Can you clarify what the new version of the PR is doing? Is it providing a new way to create non-det arrays:

let arr: [u8; 10] = kani::Arbitrary::any_array();

? If so, how does it compare to the existing one:

let arr: [u8; 10] = kani::any();

and are there any advantages to the new approach?

With the new approach, we can directly assign a nondet array without initializing each element individually for types where this operation is safe.

[zhassan-aws]

With the new approach, we can directly assign a nondet array without initializing each element individually for types where this operation is safe.

Can you clarify how this is achieved? The any_array implementation:

[(); MAX_ARRAY_LENGTH].map(|_| Self::any())

seems to be doing the same thing that the Arbitrary implementation for arrays was doing:

[(); N].map(|_| T::any())

[feliperodri]

Weren't you planning to also make changes to any_slice?

@celinval no changes to any_slice() on this PR. I want to focus this one only on implementing a version of any_array(). We can address any changes to any_slice() on a separate PR.

[feliperodri]

With the new approach, we can directly assign a nondet array without initializing each element individually for types where this operation is safe.

Can you clarify how this is achieved? The any_array implementation:

[(); MAX_ARRAY_LENGTH].map(|_| Self::any())

seems to be doing the same thing that the Arbitrary implementation for arrays was doing:

[(); N].map(|_| T::any())

@zhassan-aws you could see this is a refactoring, yes. Maybe I should update the description of this PR to make it more clear.

[celinval]

With the new approach, we can directly assign a nondet array without initializing each element individually for types where this operation is safe.

Can you clarify how this is achieved? The any_array implementation:

[(); MAX_ARRAY_LENGTH].map(|_| Self::any())

seems to be doing the same thing that the Arbitrary implementation for arrays was doing:

[(); N].map(|_| T::any())

The difference is in the implementation of arbitrary_trivial!() macro, which is how we define the implementation for the trivial types which have no contraint in their values:

            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
            where
                [(); { std::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:,
            {
                unsafe {
                    crate::any_raw_internal::<
                        [Self; MAX_ARRAY_LENGTH],
                        { std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() },
                    >()
                }

Note that we directly call any_raw_internal with the array type.

[zhassan-aws]

I see. Can you point out how any_slice will use it?

[celinval]

It looks good to me. Please address @zhassan-aws comments before merging.

[zhassan-aws]

Thanks. Please update the PR description as well.

[zhassan-aws]

Looks good. Thanks @feliperodri!

[zhassan-aws]

It would be useful to add a test (perhaps in a follow-up PR) that makes sure that a program involving an array of a primitive type does not involve loops. This can be verified by adding a #[unwind(0)] annotation so that the test would fail if a loop is generated.