Derive Macro Arbitrary
#[derive(Arbitrary)]
{
// Attributes available to this derive:
#[safety_constraint]
}
Expand description
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,
}