Add support for common proof options

[celinval]

Requested feature: We would like to allow users to customize rmc behavior for specific proof harnesses by adding attributes to the harnesses themselves. Today, users have to change how they invoke RMC.

Use case:

#[rmc::unwind(value=10)]
#[rmc::expect_failure("<message>")]
fn my_harness() {
    // code
}

Proposal: We should create macro attributes in our rmc_macros crate that allows the user to specify unwind values as well as proof expectations. Our compiler component will any proof harness attribute and dump it to the metadata file introduced in this PR: #668. Then we will use those values to control CBMC (for unwind) and the output results (for expect_failure).

If the user provides --unwind <value> argument, it should have precedence over the attribute.

Tasks breakdown:

• Add support to rmc::unwind.
• Add support to rmc::expect_failure.

[jaisnan]

Will look at this.

[adpaco-aws]

We had an exciting discussion about this today (cc @karkhaz ).

Let's assume for a moment that we have an annotation like #[rmc::expect_failure("<message>")] implemented. What would be its semantics?

1. All properties whose description contains message are expected to fail.
2. At least one property whose description contains message is expected to fail.

Now, let's discuss their usefulness:

• With (1), I suspect that the annotation wouldn't be useful to anyone since that'd require ALL properties with a given description to fail. For example, let's suppose we care about an overflow property in our code. We cannot expect all overflow properties to fail, and it'd be hard or impossible to even come up with such a program (even more with Kani, since it'll attempt to block executions from any failure).
• (2) would probably be more useful than (1), since we can detect that a particular failure happened. But this presents some problems: what "verification result" do we return if there are other failures? what if the code changes so the failure persists, but its origin is different?

The #[should_fail(...)] annotation for Rust unit tests doesn't have these problems because the "error" comes from a single execution path, and there will always be at most one error in your code, so matching it with the panic message is a good idea.

But execution paths in the context of verification work differently: conditions will split them, potentially generating multiple failures for a program. So we should consider a set of messages, instead of a single one.

Now, should we consider a string message? That's also not clear to me. Character strings aren't reliable in general.

In principle, we've identified three levels of granularity for this feature:

1. the proof fails (no need for arguments).
2. the proof fails and a given property fails.
3. the proof fails and a property related to a given line of code fails.

Note that (2) talks about a property/check, while (3) is talking about the line of code where it comes from. Even if we had some classification for the different errors you can get from Kani (which I'll be proposing in a new output format), I'm not clear on the best way to use it here (because of the first problem). In principle, we could do (1) and decide how to extend the functionality later depending on other output-related issues we have at the moment.