Derive Macro Arbitrary

#[derive(Arbitrary)]
{
    // Attributes available to this derive:
    #[safety_constraint]
}

Allow users to auto generate Arbitrary implementations by using #[derive(Arbitrary)] macro.

Type safety specification with the #[safety_constraint(...)] attribute

When using #[derive(Arbitrary)] on a struct, the #[safety_constraint(<cond>)] attribute can be added to either the struct or its fields (but not both) to indicate a type safety invariant condition <cond>. Since kani::any() is always expected to produce type-safe values, adding #[safety_constraint(...)] to the struct or any of its fields will further constrain the objects generated with kani::any().

For example, the check_positive harness in this code is expected to pass:

#[derive(kani::Arbitrary)]
struct AlwaysPositive {
    #[safety_constraint(*inner >= 0)]
    inner: i32,
}

#[kani::proof]
fn check_positive() {
    let val: AlwaysPositive = kani::any();
    assert!(val.inner >= 0);
}

But using the #[safety_constraint(...)] attribute can lead to vacuous results when the values are over-constrained. For example, in this code the check_positive harness will pass too:

#[derive(kani::Arbitrary)]
struct AlwaysPositive {
    #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
    inner: i32,
}

#[kani::proof]
fn check_positive() {
    let val: AlwaysPositive = kani::any();
    assert!(val.inner >= 0);
}

Unfortunately, we made a mistake when specifying the condition because *inner >= 0 && *inner < i32::MIN is equivalent to false. This results in the relevant assertion being unreachable:

Check 1: check_positive.assertion.1
        - Status: UNREACHABLE
        - Description: "assertion failed: val.inner >= 0"
        - Location: src/main.rs:22:5 in function check_positive

As usual, we recommend users to defend against these behaviors by using kani::cover!(...) checks and watching out for unreachable assertions in their project’s code.

Adding #[safety_constraint(...)] to the struct as opposed to its fields

As mentioned earlier, the #[safety_constraint(...)] attribute can be added to either the struct or its fields, but not to both. Adding the #[safety_constraint(...)] attribute to both the struct and its fields will result in an error.

In practice, only one type of specification is need. If the condition for the type safety invariant involves a relation between two or more struct fields, the struct-level attribute should be used. Otherwise, using the #[safety_constraint(...)] on field(s) is recommended since it helps with readability.

For example, if we were defining a custom vector MyVector and wanted to specify that the inner vector’s length is always less than or equal to its capacity, we should do it as follows:

#[derive(Arbitrary)]
#[safety_constraint(vector.len() <= *capacity)]
struct MyVector<T> {
    vector: Vec<T>,
    capacity: usize,
}

However, if we were defining a struct whose fields are not related in any way, we would prefer using the #[safety_constraint(...)] attribute on its fields:

#[derive(Arbitrary)]
struct PositivePoint {
    #[safety_constraint(*x >= 0)]
    x: i32,
    #[safety_constraint(*y >= 0)]
    y: i32,
}