Fail verification if contract is vacuous

[carolynzech]

Description

Fail verification if a contract's preconditions are unsatisfiable or its postconditions are unreachable.
This solution introduces a new Kani intrinsic, kani::internal::cover_contract. We insert calls to this intrinsic during macro expansion after the the precondition and before the postcondition, e.g.:

kani::assume(precondition);
kani::internal::cover_contract(precondition, "The contract's precondition is satisfiable");
....
kani::internal::cover_contract(postcondition, "The contract's postcondition is reachable");
kani::assert(postcondition);

This intrinsic has the same codegen as kani::cover (i.e., assert(!cond)). Just as with kani::cover, the CBMC property renderer intercepts the results of these property checks and updates them before returning them to the user.

Call Outs

• I'd be curious if anyone can think of a simple solution to the never type fixme test that I included--if so, I'll fix it in this PR. Otherwise, I'll create an issue about it and link it in the test before merging.
• I'm changing the result of undetermined checks to failure if there's unwinding failures. My rationale is that in the case of code like this:

#[ensures(...)]
fn foo() { loop{} }

We know that the postcondition is unreachable, so we should say so. I think this approach makes sense, but also happy to keep it undetermined if we'd rather not treat one type of undetermined check differently from another.

Resolves #2793

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

[carolynzech]

Note that this fails the standard library job because a number of the unchecked_mul harnesses are restricted to ranges such that the precondition empties the search space. For example, verify::unchecked_mul_usize_edge performs lhs.unchecked_mul(rhs) on usizes between [u32::MAX / 2, u32::MAX], with a precondition that the product must not overflow. However, this product will always overflow, so the contract is vacuous and verification fails.
If we decide we're happy with this behavior, I can create a PR to update those harnesses before merging this PR (or ping the CMU team who authored them).

[celinval]

May I suggest a different approach? I think we should add 2 special cover statements to harnesses. One before we invoke the function and one after we leave the function. This would help us understand whether the pre-conditions are ever satisfied, and if the post-condition is ever checked.

Note that this fails the standard library job because a number of the unchecked_mul harnesses are restricted to ranges such that the precondition empties the search space. For example, verify::unchecked_mul_usize_edge performs lhs.unchecked_mul(rhs) on usizes between [u32::MAX / 2, u32::MAX], with a precondition that the product must not overflow. However, this product will always overflow, so the contract is vacuous and verification fails. If we decide we're happy with this behavior, I can create a PR to update those harnesses before merging this PR (or ping the CMU team who authored them).

hummm... that's an interesting point. I don't think the harness is incorrect though. I am not sure what the best approach is here to combine problem partitioning and the vacuous contract check. Maybe what we want is to combine harnesses that verify the same contract.

[celinval]

* I'm changing the result of undetermined checks to failure if there's unwinding failures. My rationale is that in the case of code like this:

I would prefer if we don't do that. We can discuss this further but I think it's out of scope of this PR.

[carolynzech]

Moving to draft for now -- we need to decide whether we want verification failure for these properties to be the default behavior, or a characteristic of the harness. This implementation has failure as the default behavior, but one could imagine that in the unchecked_mul case I mentioned above, you may want something like this:

#[requires(!self.overflowing_mul(rhs).1)]
pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
  ...
}

#[kani::proof_for_contract(unchecked_mul)]
// without this attribute, verification would fail because of a vacuous proof,
// but maybe you want to sanity check your precondition
// by having a separate harness with just invalid inputs
#[kani::allow_vacuity]
fn unchecked_mul_usize_edge() {
  let lhs: u32 = kani::any_where(|num| num >= u32::MAX / 2);
  let rhs: u32 = kani::any_where(|num| num >= u32::MAX / 2);
  lhs.unchecked_mul(rhs);
}

// This harness will fail for a vacuous proof by default
#[kani::proof_for_contract(unchecked_mul)]
fn unchecked_mul_middle() { ... }

Partitioning harnesses like this is a reasonable thing to do (and in fact, an approach we recommend and would like to implement as a feature) so failing by default could produce a bad experience for users. Introducing a harness-level attribute requires further discussion, however.