Kani fails to use static string in assertion message

[danielsn]

I tried this code:

1. Checkout prost https://github.com/tokio-rs/prost at commit 963a2cf0bfad4adb4ce7945d5738f2bde5c49c0a
2. Follow the instructions to setup PropProof https://github.com/tokio-rs/prost/blob/master/KANI.md

3. cd prost-types; 
   cargo kani --tests --default-unwind 3 --output-format terse --harness "check_duration_roundtrip" --visualize 

   with Kani version: 0.20.0

I expected to see this happen: Kani uses static strings in panic messages

Instead, this happened: explanation

VERIFICATION RESULT:
 ** 3 of 330 failed (6 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/dsn/.rustup/toolchains/nightly-2022-12-11-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/time.rs", line 202, in std::time::Duration::new
Failed Checks: concat!
("assertion failed: ", stringify!
(matches!(time :: Duration :: try_from(neg_prost_duration),
    Err(DurationError :: NegativeDuration(d)) if d == std_duration,)))
 File: "/Users/dsn/ws/prost/prost-types/src/lib.rs", line 449, in tests::check_duration_roundtrip::{closure#0}
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/dsn/.rustup/toolchains/nightly-2022-12-11-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs", line 1791, in std::result::unwrap_failed

But the panic on line 202 in time.rs is given a static string: https://doc.rust-lang.org/stable/src/core/time.rs.html#202

    #[stable(feature = "duration", since = "1.3.0")]
    #[inline]
    #[must_use]
    #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")]
    pub const fn new(secs: u64, nanos: u32) -> Duration {
        let secs = match secs.checked_add((nanos / NANOS_PER_SEC) as u64) {
            Some(secs) => secs,
            None => panic!("overflow in Duration::new"),
        };
        let nanos = nanos % NANOS_PER_SEC;
        // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
        Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
    }

[celinval]

Please correct-me if I'm wrong. I think the error message is coming from std::result::unwrap_failed() which is defined here: https://doc.rust-lang.org/src/core/result.rs.html#1791

fn unwrap_failed(msg: &str, error: &dyn fmt::Debug) -> ! {
    panic!("{msg}: {error:?}")
}

That said, I really think we should improve this message. It sounds like a bug in Kani not a property failure.

[danielsn]

The message I was referring to was this one. Sorry if I was unclear.

Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/dsn/.rustup/toolchains/nightly-2022-12-11-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/time.rs", line 202, in std::time::Duration::new

[celinval]

Ah, too many of them. :)

[celinval]

Is that this statement? panic!("overflow in Duration::new").