Improvement: report multiple errors whenever possible

[bsdinis]

One quite frustating experience users might run into is verus reporting one error, fixing them, just to find that another error, and another, and another are also behind that error.

This is in general a hard problem -- requiring holding as many errors as possible in the multiple phases (instead of just reporting the first one).

The intention of this issue is to collect cases where we are only reporting one error at a time. That allows us to track these cases. Examples of cases that cause the issues would be nice as well.

[bsdinis]

#1 cannot call function x with mode y

Example:

use vstd::prelude::*;

verus! {

proof fn test(v: &Vec<u64>)
    requires
        v.len() > 0
    ensures
        !v.is_empty()
{}

proof fn test2(v: &Vec<u64>)
    requires
        v.len() == 0
    ensures
        v.is_empty()
{}

} // verus!

This would require VirErr to have multiple messages, and check_expr_handle_mut_arg to report these messages.

[tjhance]

Reporting multiple errors is a long-needed improvement.

I would start with the checks in well_formed.rs which are all effectively independent, and which are implemented via a node visitor pattern that would make it easy to aggregate all the errors.

modes.rs is much trickier due to the stateful algorithm, so it's difficult to avoid failing fast; but functions are pretty much independent, so we could still check the next function in the event an error is encountered. This would give much of the benefit.

Likewise, for the rust_to_vir phase, we could fail fast on the item level but still move onto the next item; this would give much of the benefit. Though I also think it wouldn't be too unreasonable to aggregate errors over the course of the Expr traversal.

These are the 3 main phases that produce errors. There's also the external.rs phase that runs before rust_to_vir, though I think it already aggregates errors, it just lacks the ability to report all of them so it throws most of them away.

After modes.rs, there aren't very many checks (though there are a few).

[bsdinis]

Thanks for the context! It is very useful to know for improving error reporting.

I'm low on cycles to work on this right now (hence, this issue works as a way to report use cases where I see it happen so I don't forget).

[bsdinis]

#2 no variant <VARIANT> for this datatype

Example:

use vstd::prelude::*;

verus! {

enum Foo {
    Bar
}

spec fn foo(f: Foo) -> bool {
    f is Baz
}

spec fn baz(f: Foo) -> bool {
    f is Baz
}

} // verus!

This is being issued in check_variant_field (in fn_call_to_vir).
However, it seems like the place to aggregate would be crate_to_vir (in rust_to_vir.rs). It iterates over the crates items and checks them -- we can simply aggregate inside this for loop.

[tjhance]

I've made a bit of progress on multi-error reporting via 8f517fb and 93c39f8

[bsdinis]

#3: this function call takes a &mut ref of a field of a datatype with a user-defined type invariant ... no unwind

This happens whenever a type invarianted method calls into a function that is not marked no_unwind.
I think this comes from annotate_user_defined_invariants, in source/vir/src/user_defined_type_invariants.rs