Workaround performance issue for regression test

Use u8 instead of i8 for now and add a performance test to capture this
issue.

tests/cargo-kani/itoa_dep/src/main.rs

@@ -20,7 +20,7 @@ fn check_itoa<T: kani::Arbitrary + Integer + std::fmt::Display>() {
 #[kani::proof]
 #[kani::unwind(10)]
 fn check_signed() {
-    check_itoa::<i8>();
+    check_itoa::<u8>();
 }
 
 fn main() {}

tests/perf/format/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "format"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/perf/format/expected

@@ -0,0 +1 @@
+Complete - 2 successfully verified harnesses, 0 failures, 2 total

tests/perf/format/src/lib.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of calling format.
+//! This tests capture the performance regression introduced by the toolchain upgrade #2551.
+//! See https://github.com/model-checking/kani/issues/2576 for more details.
+
+#[kani::proof]
+fn fmt_i8() {
+    let num: i8 = kani::any();
+    let s = format!("{num}");
+    assert!(s.len() <= 4);
+}
+
+#[kani::proof]
+fn fmt_u8() {
+    let num: u8 = kani::any();
+    let s = format!("{num}");
+    assert!(s.len() <= 3);
+}