Improve error messages

[utaal]

This is intended to track confusing or misleading error messages.

Please add a new top-level comment for each error message.

[utaal]

Reported by @jaylorch:

A simple program a beginner may write:

#[allow(unused_imports)]
use builtin_macros::*;
#[allow(unused_imports)]
use builtin::*;

#[allow(unused_attributes)]
mod pervasive;

verus! {

fn main() {
    println!("Hello, world!");
}

} // verus!

the verifier produced the following output:

[rust_verify/src/rust_to_vir_expr.rs:2944] expr = Expr {
    hir_id: HirId {
        owner: DefId(0:1969 ~ test2[e612]::main),
        local_id: 13,
    },
    kind: Array(
        [
            Expr {
                hir_id: HirId {
                    owner: DefId(0:1969 ~ test2[e612]::main),
                    local_id: 12,
                },
                kind: Lit(
                    Spanned {
                        node: Str(
                            "Hello, world!\n",
                            Cooked,
                        ),
                        span: rust_verify/play/test2.rs:12:14: 12:29 (#0),
                    },
                ),
                span: rust_verify/play/test2.rs:12:14: 12:29 (#26888),
            },
        ],
    ),
    span: rust_verify/play/test2.rs:12:14: 12:29 (#26887),
}
error: The verifier does not yet support the following Rust feature: expression
  --> rust_verify/play/test2.rs:12:14
   |
12 |     println!("Hello, world!");
   |              ^^^^^^^^^^^^^^^

error: aborting due to previous error

The guide pointed @jaylorch to #[verifier(external_body) to solve this issue; which we don't believe is the ideal outcome:

As I was reading Chapter 1 of the guide, after getting Verus to verify getting_started.rs/, I tried adding the println! and got the error message. The very next section I read, Section 2.1 (https://verus-lang.github.io/verus/guide/requires_ensures.html), showed how you could get println! into a Verus program by annotating its function as unverified. It made it sound like all I/O was unverified when it said "...leave other aspects, such as input-output operations, unverified", [...]

@Chris-Hawblitzel suggested that:

Maybe one thing we can do in terms of detecting uses of unsupported features is get rid of the _ match cases in our translator and fill in a specific error for each individual feature we don't support. When the user encounters an unsupported feature or unsupported standard library function, we could suggest using #[verifier(external_body)].

[utaal]

Unfortunate error message for write to immutable variable.

Reported by @jonhnet:

isolate.zip

#395

[utaal]

From #334 by @jonhnet:

This code

#![allow(unused_imports)]
use builtin::*;
use builtin_macros::*;

verus! {
pub const RC_WIDTH: nat = 4 as nat;
}

fn main() { }

results in

error[E0605]: non-primitive cast: `i32` as `builtin::nat`
 --> rust_verify/example/scache/testcase.rs:6:27
  |
6 | pub const RC_WIDTH: nat = 4 as nat;
  |                           ^^^^^^^^ an `as` expression can only be used to convert between primitive types or to coerce to a specific trait object

error: aborting due to previous error

For more information about this error, try `rustc --explain E0605`.
verification results:: verified: 0 errors: 0

---

@tjhance notes:

The issue is that the as nat is a spec-only feature, so the const needs to be marked spec.

pub spec const RC_WIDTH: nat = 4 as nat;

Perhaps we could have a nicer error message in the syntax macro, though.

[utaal]

Postcondition failure on a match is reported with a misleading span #281

#[is_variant]
enum Enum {
    A,
    B,
}


fn test(a: u32) -> (res: Enum)
    ensures (match res {
        Enum::A => a <= 10,
        Enum::B => a > 10, // FAILS
    }) {

    Enum::B
}

results in this error message, which points to the wrong branch of the match, while it should just point to the entire match, I think:

error: postcondition not satisfied
  --> test.rs:24:8
   |
22 |           Enum::A => a <= 10,
   |           ------- failed this postcondition
23 |           Enum::B => a > 10, // FAILS
24 |       }) {
   |  ________^
25 | |
26 | |     Enum::B
27 | | }
   | |_^ at the end of the function body

Originally found by @matthias-brun.

---

• un-ignore test e726297

[utaal]

cc @tjhance

A type parameter on a struct made with struct_with_invariant! may, I believe, end up being unconstrained in one of the macro-generated items, and cause a confusing error that doesn't point to the macro as the culprit.
For those with access, here's an example: https://github.com/verus-lang/verus-systems-code/blob/4817d858428619df34a0ab9da959dce7b5ea0f49/nr/src/main.rs#L107

[utaal]

@tjhance: type errors related to verus_tmp are confusing
Moved from #468.

this code:

fn test() {
    let ghost x = 0;
}

gives a very cryptic error:

error[E0282]: type annotations needed
  --> test_gh.rs:12:1
   |
12 | / verus!{
13 | |
14 | |
15 | | fn test() {
...  |
23 | |
24 | | }
   | |_^ consider giving `verus_tmp` a type
   |
   = note: this error originates in the macro `verus` (in Nightly builds, run with -Z macro-backtrace for more info)

There are two things that can be fixed here.

1. Fixing the spans in the macro code should result in a better localized error message.

2. The verus_tmp variable is unnecessary in the first place. This is the expanded code:

fn test() {
    #[verus::internal(spec)]
    let mut verus_tmp;

    #[verifier(proof_block)]
    { verus_tmp = ::builtin::spec_literal_integer("0") };
    #[verus::internal(spec)]
    let mut x;

    #[verifier(proof_block)]
    {
        #[verus::internal(spec)]
        let verus_tmp_x = verus_tmp;
        x = verus_tmp_x;
    };
}

However, it should suffice to expand it to simply:

    #[verus::internal(spec)]
    let mut x;

    #[verifier(proof_block)]
    {
        x = ::builtin::spec_literal_integer("0");
    }

[utaal]

This is now better (after 177130d), but the help is weird. I'm not sure we can do better.

error[E0282]: type annotations needed
  --> rust_verify/example/playground.rs:31:5
   |
31 |     let ghost x = 0;
   |     ^^^^^^^^^^^^^^^^
   |
help: consider giving `verus_tmp` an explicit type
   |
31 |     let ghost x = 0;: /* Type */
   |                     ++++++++++++

[utaal]

@jonhnet: bogus recommendation not met feedback is misleading
Moved from #467

The file below produces, as its first attempt at helping me debug my assertion failures:

note: recommendation not met
   --> src/journal/PagedJournalRefinement_v.rs:244:21
    |
244 | ...   assert( Self::opt_rec_crop_head_records(small, bdy, 1) == smaller );    // spitting "note: recommendati...
    |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
   ::: src/journal/PagedJournal_v.rs:93:9
    |
93  |         Self::opt_rec_can_crop_head_records(ojr, boundary_lsn, depth),
    |         ------------------------------------------------------------- recommendation not met

However, that exact recommendation appears in an assert on the previous line (243), and that assert passes.

Repro:

git clone git@github.com:vmware-labs/verified-betrfs.git
git checkout 3a2d8c01b8991fb431335921ef8e4fb8fee91136
$verus/tools/rust-verify.sh src/bundle.rs --verify-module journal::PagedJournalRefinement_v --verify-module journal::PagedJournal_v --time --expand-errors --multiple-errors 5

[utaal]

Multiple trait implementations for the same outer type are now supported. I believe this is resolved.

[utaal]

@jonhnet: Improve error message for exec-mode use of spec-mode builtin types

Moved from: #505

This code:

use builtin_macros::*;

verus!{

fn foo() -> nat {
    4 as nat
}

}

gives this error message:

error[E0605]: non-primitive cast: `i32` as `builtin::nat`
 --> ironsht/src/test.rs:7:5
  |
7 |     4 as nat
  |     ^^^^^^^^ an `as` expression can only be used to convert between primitive types or to coerce to a specific trait object

which confuses even people who should know better. It should instead tell us something like nat isn't available in exec mode, and perhaps suggest adding spec modifier to fn.

[utaal]

#323 should address this, at least in part, once I get around to it.

[tjhance]

I'm not sure - this error occurs from Rust type-checking, right? It seems hard to do anything about it.

[utaal]

Oh, I had somewhat misinterpreted this; you're right. It may indirectly help by warning that the return type of foo is a spec type, though.

[jaylorch]

I often accidentally write assert_seqs_equal! outside of a proof block, since I'm used to assertions not having to be enclosed in a proof block. The error message when this happens is confusing:

error: exec code cannot initialize non-exec variables

The error message would be less confusing if it got to the heart of the problem. That is, I think it should just say that assert_seqs_equal! can't be used in exec mode.

An even better solution, of course, would be to allow assert_seqs_equal! to be used in exec mode.

All of the above applies to the other assert*! macros like assert_sets_equal!.

[tjhance]

Macros are a bit of a pain point right now due to the way exec & proof code are split up. I'm not really sure what to do about it right now but it would be a good idea to come up with a system that handles situations like this. (In my head I've been toying with the idea of marking macros as for-exec-code or for-proof-code, but there are a number of obstacles.)

[jaybosamiya]

One potential way around it is if proof blocks allowed for nested proof blocks inside them (where nesting is a no-op, so proof { proof { x } } == proof { x }); if we do that, then such macros could generate a proof { ... }, and it'd be fine, because the blocks could nest fine). It is possible I'm missing something though.

[utaal]

One option to consider here is the proposal (by @Chris-Hawblitzel, and others) to have an extensible language for assert (...) by (<strategy>), or similar, as discussed in a previous meeting with @verus-lang/devs and others. That may be a way to organise the various macro-based proof techniques we rely on now, and make it easier for the syntax macro to handle situations like the one @jaylorch encountered (in the same way asserts can already appear directly without the need for a proof block).

[utaal]

Addressed with 23ac0b0.

[utaal]

This currently passes:

        pub open spec fn foo() -> bool 
          recommends
          { true }

        proof fn test() {
            assert(foo());
        }

I suspect the issue came up in combination with something else in the original file; if it happens again, please bring it up again.

Added test for the minimized case in 7bd59f3

[utaal]

Addressed by #748

[utaal]

Fixed by 3b0f834

[utaal]

Rename proof mode to tracked mode everywhere?

[utaal]

Fixed with 96882b6

[jaylorch]

The following code:

    fn mytest(r: &Tracked<Q>)
    {
        let Tracked(q) = r;
    }

gives the following error, and I'm not sure what it means:

error: cannot move out of `*verus_tmp_q` which is behind a shared reference

One thing making it hard to understand is the reference to *verus_tmp_q, which doesn't appear in the source code. The other thing making it tricky is that the associated span is the space between Tracked(q) and =.

[tjhance]

The reference to verus_tmp_q is very confusing. This is especially confusing because the let Tracked(...) pattern syntax would ordinarily work with Rust references if this was a normal pattern.

By the way, it's generally recommended you use the following form:

    fn mytest(Tracked(q): Tracked<&Q>)
    {
    }

[utaal]

Pointing out that a function is uninterpreted in --expand-errors may be irrelevant for standard library functions whose semantics are given by the axiomatization.

[utaal]

. @jonhnet would like we reported all precondition failures for a function call (I agree we should): https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=96d5fee8b3ba89a5fd796c509b072c6b

[utaal]

. @jonhnet prefers reporting assertion failures in (line number) order. The trade-off is that this would require delaying the first report (while we search for an earlier failure), but that (1-2 sec delay) is shorter than the time it takes the user to parse the out-of-order output.

[utaal]

Report by @jonhnet:

error[E0401]: can't use generic parameters from outer function
  --> ironsht/src/verus_extra/seq_lib_v.rs:40:28
   |
16 | pub proof fn lemma_seq_fold_left_merge_right_assoc<A, B>(s: Seq<A>, init: B, f: FnSpec(A) -> B, g: FnSpec(B, B)...
   |                                                    - type parameter from outer function
...
40 |     reveal_with_fuel(Seq::<A>::fold_left::<B>, 2);
   |                     -      ^ use of generic parameter from outer function
   |                     |
   |                     help: try using a local generic parameter instead: `<A>`

This error message is misleading. It'd be nice to catch the unneeded generic params before they cause an error.

[matthias-brun]

spec fn foo(n: nat) -> bool;
fn bar()
    ensures forall|n: nat| #![trigger] foo(n)
{ }

results in this error message:

error: trigger group 0 does not cover variable n
 --> /st/verus/test.rs:8:13
  |
8 |     ensures forall|n: nat| #![trigger] foo(n)
  |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I accidentally used #![trigger] rather than #[trigger] and the error message doesn't help in spotting that mistake. (Does #![trigger] even mean anything reasonable?)

[utaal]

@tenzinhl #873: Add a Warning/Error when using =~~= on type without #[verifier::ext_equal] annotation

Currently when using the =~~= syntax on a user defined type, there is no warning when the #[verifier::ext_equal] annotation is not added to said type. Instead assertions will just always fail (even though to my understanding this is always a clear misuse to use =~~= operator without having the #[verifier::ext_equal] annotation on the compared types).

Would it be possible to add a compiler warning or error for this case? (I'd be interested in looking into this with some guidance).

[utaal]

I'd be happy to help you with this. Ping me on Zulip/Slack.

[matthias-brun]

use builtin_macros::*;

verus! {

fn foo() {
    let x: usize = 0;
    let _ = x << 1u64;
}

fn main() { }
}

ξ verus-release /st/verus/test2.rs --arch-word-bits 64

error: error: argument bit-width does not match. Left: architecture-dependent, Right: 64-bit
 --> /st/verus/test2.rs:7:13
  |
7 |     let _ = x << 1u64;
  |             ^^^^^^^^^

error: aborting due to previous error

This error message is confusing, since the --arch-word-bits 64 argument should tell the verifier that the bit-width does in fact match. However, as @utaal explained to me, it's currently a requirement for the bitvector reasoning that the operands have the same type. That is what the error message should be pointing out instead.

[matthias-brun]

use vstd::prelude::*;

verus!{

fn main() { }

#[verifier(external_body)]
struct S { }

spec fn bar(s: &S) -> bool;

fn foo(s: &mut S)
    requires bar(old(s))
{
}

}

ξ verus-release /st/verus/test.rs
error: a mutable reference is expected here
  --> /st/verus/test.rs:13:22
   |
13 |     requires bar(old(s))
   |                      ^

error: aborting due to previous error

The problem here is that the requires should be requires bar(&*old(s)) instead, which the error message doesn't exactly help in figuring out. @utaal notes: "It'll go away with prophecies.".

[Chris-Hawblitzel]

I'm relaying a feature request that someone else brought up: we could have --expand-errors distinguish between the underflow and overflow cases of "possible arithmetic underflow/overflow".

[utaal-b]

From #957 by @jonhnet:

+ /home/jonh/verus/source/target-verus/release/verus --time src/bundle.rs
error: in pub open spec function, cannot access any field of a datatype where one or more fields are private
   --> src/marshalling/SeqMarshalling_v.rs:358:11
    |
358 | ...   ((self.total_size - Self::spec_size_of_length_field()) / (self.config.spec_uni...
    |       

It might be helpful to enhance this error message to identify one or more non-pub fields. Something like "struct Foo has non-pub fields x, y, z, ...". In the fullness of time, perhaps a Rust-like suggestion inserting 'pub' into the field declaration.

[utaal]

use vstd::prelude::*;

verus! {
struct Concrete {
    a: u64,
}

struct Abstract {
    a: nat,
}

impl View for Concrete {
    type V = Abstract;

    fn view(&self) -> <Self as vstd::string::View>::V {
        Abstract { a: self.a as nat }
    }
}

} // verus!

This should warn about view that should be marked as spec if possible, instead of "an as expression can only be used to convert between primitive types or to coerce to a specific trait object".

[utaal]

@matthias-brun recently noticed that we are now counting non-recursive spec functions as successful VCs, although nothing was verified for them:

use vstd::prelude::*;
verus!{
spec fn foo() {
    ()
}
}

produces:

verification results:: 1 verified, 0 errors

[jaylorch]

The error message "datatype is opaque here" is rather vague. Can we add the name of the datatype that's opaque and the subexpression(s) with that datatype?