Slow performance with the Display trait

[zhassan-aws]

I tried this code:

use std::fmt::Display;

enum Foo {
    A(String),
    B(String),
}

impl Display for Foo {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let s = match self {
            Foo::A(s) => format!("A.{s}"),
            Foo::B(s) => format!("B.{s}"),
        };
        write!(f, "{s}")?;
        Ok(())
    }
}

#[kani::proof]
#[kani::unwind(6)]
fn fast() {
    let a = Foo::A(String::from("foo"));
    let s = match a {
        Foo::A(s) => format!("A.{s}"),
        Foo::B(s) => format!("B.{s}"),
    };
    assert_eq!(s, "A.foo");
}

#[kani::proof]
#[kani::unwind(6)]
fn slow() {
    let a = Foo::A(String::from("foo"));
    let s = a.to_string();
    assert_eq!(s, "A.foo");
}

using the following command line invocation:

kani str_from.rs --harness fast
kani str_from.rs --harness slow

with Kani version: 71b9d0e

I expected to see this happen: Verification time is about the same for the two harnesses.

Instead, this happened: The fast harness completes in less than 4 seconds, but the slow harness runs for over 60 minutes without terminating (and consumes close to 6 GB of memory).

[tautschnig]

The combination of diffblue/cbmc#7569 and diffblue/cbmc#7570 makes both harnesses complete in 2-3 seconds.

[zhassan-aws]

Awesome! Thanks @tautschnig!