Span of type error in contracts could be narrowed

[pnkfelix]

I was having a go at transcribing the example from the recent blog post, and I encountered a sub-optimal diagnostic issue.

Test case:

#[kani::ensures(a % result && b % result == 0 && result != 0)]
fn gcd(a: u64, b: u64) -> u64 {
    0
}

The above currently generates the following from Kani:

error[E0308]: mismatched types
 --> src/main.rs:1:1
  |
1 | #[kani::ensures(a % result && b % result == 0 && result != 0)]
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `u64`
  |
  = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0308]: mismatched types
 --> src/main.rs:1:1
  |
1 | #[kani::ensures(a % result && b % result == 0 && result != 0)]
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `u64`
  |
  = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to 2 previous errors

(I'm not sure why it prints two copies of the error message.)

I had a hard time seeing what was wrong, since the highlighted span was overly broad.

If you were to encode the contract as an assertion at the end of the method body and then invoke rustc, it produces a more precise diagnostic message:

error[E0308]: mismatched types
  --> src/main.rs:13:13
   |
13 | ...t!(a % result &&...
   |       ^^^^^^^^^^ expected `bool`, found `u64`

error: aborting due to 1 previous error

You can see how this more immediately reveals the source of the problem.

[pnkfelix]

(Oh, I should try with -Z macro-backtrace and see if that's any better... but, no, Kani does not support passing that flag along...)

[zhassan-aws]

Indeed, the error message is pretty vague.

Oh, I should try with -Z macro-backtrace and see if that's any better... but, no, Kani does not support passing that flag along...)

It supports it, but the extra diags are not that helpful either:

$ RUSTFLAGS="-Zmacro-backtrace" kani iss3009.rs 
Kani Rust Verifier 0.45.0 (standalone)
error[E0308]: mismatched types
   --> iss3009.rs:1:1
    |
1   | #[kani::ensures(a % result && b % result == 0 && result != 0)]
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    | |
    | expected `bool`, found `u64`
    | in this procedural macro expansion
    |
   ::: /home/ubuntu/git/kani/library/kani_macros/src/lib.rs:135:1
    |
135 | pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
    | ------------------------------------------------------------------- in this expansion of `#[kani::ensures]`

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0308`.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 1

[JustusAdam]

I can answer why it come up twice. Kani code-generates two functions from your contract, one that checks it and one that can be used to replace it. Both use the code in your contract so by the time that the rust type checker gets to it your code exists in two places ;)