Introduce a kani macro for checking coverage

[zhassan-aws]

Description of changes:

Introduce a kani::cover macro that can be used for checking whether certain conditions can occur without causing verification to fail.

Resolved issues:

Resolves #696

Related RFC:

Optional #1905

Call-outs:

This PR does not yet introduce reachability checks for cover properties. Thus, both unreachable and reachable but unsatisfiable properties will be reported as "UNSATISFIABLE". I'm planning to introduce reachability checks in a follow-up PR because I didn't want to complicate this one too much.

Testing:

• How is this change tested? Added a few tests.

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

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

[tedinski]

Hmm, was this always going to be a macro, not just a function, and I missed that when I glanced at the RFC before?

Why a macro over just a function? Is it just the messages part? Is that essential?

I want to make sure the disadvantages of a macro (complexity, compile time, IDE autocomplete problems) are actually needed for this...

[zhassan-aws]

Hmm, was this always going to be a macro, not just a function, and I missed that when I glanced at the RFC before?

No, it was originally a function, but the discussion on the RFC led to introducing a macro. See #1906 (comment).

The function still exists though, and is public, so can be used directly.

[celinval]

Thanks for doing this!

[celinval]

Can we invert the report? I think we should report the number of covers that were satisfied.

[zhassan-aws]

I agree an inverted report is better (I made the change). The reason I didn't do it initially, is that an inverted report is a bit inconsistent with the report for normal checks where we reported the number of things that went wrong (failures) as opposed to those that were successful (similarly, the unsatisfiable covers are the ones that are unexpected).

I'm pro inverting the summary for normal checks as well (perhaps in a separate PR).

[celinval]

Thanks!