Add #[verifier::allow(...)] to suppress warnings

[Chris-Hawblitzel]

This adds a #[verifier::allow(...)] attribute to suppress warnings generated by Verus. For now, the attribute is only implemented for items like functions and modules, not for expressions, so you have to suppress warnings across entire functions or modules.

Example:

#[derive(Clone)]
struct S;

This generates:

warning: Verus does not (yet) support autoderive Clone impl when the clone is not a copy; continuing, but without adding a specification for the derived Clone impl
  --> .\scratch.rs:55:10
   |
55 | #[derive(Clone)]
   |          ^^^^^
   |
   = help: to suppress this warning, use `#[verifier::allow(autoderive_clone_without_spec)]` on the surrounding function, datatype, or module or `#![verifier::allow(autoderive_clone_without_spec)]` in the module or crate

Rewriting the code as:

#[verifier::allow(autoderive_clone_without_spec)]
#[derive(Clone)]
struct S;

removes the warning.

The implementation works differently for rust_verify and vir. In rust_verify, for each warning, the implementation walks up the DefId tree on demand to look for matching verifier::allow attributes. For vir, the implementation preemptively walks up the DefId tree from each function during translation to vir, keeping all the verifier::allow attributes in a table for later reference, and then uses the table to handle any warnings generated inside vir.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[parno]

Thanks, this looks like an elegant framework. It'll be nice to silence some of the warnings that have persistently cluttered some of my projects for a while now.

[parno]

"known" -> "know"

[parno]

I think we might need a format!(...) here, so that the "<<{}>>" gets resolved properly

[tjhance]

should we use an enum instead of String for the warning names?

[Chris-Hawblitzel]

Ok, I switched it to an enum.