rust_verify_test: support expected message in FAILS comment

[mmcloughlin]

This PR extends the testing mechanism that checks for FAILS comments to additionally allow an expected error message.

A comment of the form // FAILS just checks for an error. The form // FAILS: <expect> also confirms that <expect> appears in the diagnostic text.

This PR demonstrates the feature by also updating some of the integer_ring tests.

[mmcloughlin]

I'm not sure if this is a good idea, open to suggestions.

A simple alternative is something like a helper assert_one_fails_with_vir_error_msg. This inline comment approach could be nice for the multi-error case though.

If we are going to support this kind of extended // FAILS syntax, we might also want to think about enforcing a format for FAILS comments. At the moment there are some comments with notes attached to them, for example:

verus/source/rust_verify_test/tests/loops.rs

Line 616 in edb8f53

assert(!b); // FAILS (while converted to loop due to ensures)

verus/source/rust_verify_test/tests/integer_ring.rs

Line 217 in edb8f53

assert(a % a == 0); // FAILS , `x` shouldn't be zero

Perhaps we support both an expectation and a note?

// FAIL
// FAIL: <expect_msg>
// FAIL (<note>)
// FAIL: <expect_msg> (<note>)

[utaal]

Hi @mmcloughlin. Thank you for the PR.

I have a fairly strong preference for the alternative approach:

A simple alternative is something like a helper assert_one_fails_with_vir_error_msg.

The FAILS comment, in my mind, should just be a marker of the affected line, and I'd prefer we kept that as simple as possible. Multiple errors with FAILS are uncommon, because we generally will only reliably get one SMT failure (the earliest failing assertion), and so we don't generally write tests with multiple FAILS.

Support for info or warning would be useful, through the addition of other markers (there it would be more useful to have multiple -- and perhaps identify them by some "id" to match them with the expected message. In fact, we could also do this for "FAILS" in the uncommon case where there are multiple FAILS we want to handle, e.g.

use vstd::string::*;
fn get_char_fails() {
    let x = new_strlit("hello world");
    let val = x.get_char(0); // FAILS(0)
    assert(val === 'h'); // FAILS(1)
}

uses:

assert_fails_with_vir_msgs(err, [
    Level::Error, "invalid comparison operator `===`",
    Level::Error, "expected function, found macro `assert`",
])