Derive Macro kani::Arbitrary

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

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

When using #[derive(Arbitrary)] on a struct, the #[safety_constraint(<cond>)] attribute can be added to its fields to indicate a type safety invariant condition <cond>. Since kani::any() is always expected to produce type-safe values, adding #[safety_constraint(...)] to any 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);
}

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