fail harness if cover is not satisfied #2792
Description
Requested feature: fail harness
Use case:
I just realized that the current bolero integration allows a proof to go through, even if you've specified a generator that is impossible to satisfy:
#[test]
#[kani::proof]
fn my_test() {
bolero::check!().with_type::<u8>().filter(|_| false).for_each(|_| {
panic!();
});
}$ cargo kani --tests --harness my_test --output-format=terse
Checking harness my_test...
VERIFICATION RESULT:
** 0 of 255 failed
** 0 of 1 cover properties satisfied (1 unreachable) // <= this should ideally fail the proof
VERIFICATION:- SUCCESSFUL
Verification Time: 0.14628594s
Complete - 1 successfully verified harnesses, 0 failures, 1 total.
Ideally, we'd replace the call to kani::assume with a cover call that would force harness failure. This could be called something like kani::cover_or_fail! or kani::assert_cover!.
Doing a test with multiple harnesses, it seems to behave as one would expect and only applies to the individual harness:
#[test]
#[kani::proof]
fn my_test() {
bolero::check!().with_type::<u8>().for_each(|_| {
// noop
});
}
#[test]
#[kani::proof]
fn my_test() {
bolero::check!().with_type::<u8>().filter(|_| false).for_each(|_| {
panic!();
});
}
#[kani::proof]
fn my_kani_proof() {
assert_eq!(1 + 2, 3);
}$ cargo kani --tests --output-format=terse
VERIFICATION:- SUCCESSFUL
Verification Time: 0.89504564s
Checking harness add_test...
VERIFICATION RESULT:
** 0 of 1502 failed (69 unreachable)
** 1 of 1 cover properties satisfied // <= the generator produced at least 1 valid value
VERIFICATION:- SUCCESSFUL
Verification Time: 0.8548021s
Checking harness my_test...
VERIFICATION RESULT:
** 0 of 255 failed
** 0 of 1 cover properties satisfied (1 unreachable) // <= the generator was UNSAT; should fail the harness!
VERIFICATION:- SUCCESSFUL
Verification Time: 0.14286228s
Checking harness my_kani_proof...
VERIFICATION RESULT:
** 0 of 2 failed // <= this harness doesn't use bolero at all; no references to the cover property
VERIFICATION:- SUCCESSFUL
Verification Time: 0.024725173s