From 8ef1847ab49d8f0ca443948c0a4bcd71f416ab58 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 21 Jun 2023 14:21:07 -0700
Subject: [PATCH] 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 |  2 +-
 tests/perf/format/Cargo.toml          | 11 +++++++++++
 tests/perf/format/expected            |  1 +
 tests/perf/format/src/lib.rs          | 20 ++++++++++++++++++++
 4 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 tests/perf/format/Cargo.toml
 create mode 100644 tests/perf/format/expected
 create mode 100644 tests/perf/format/src/lib.rs

diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs
index 9bda87de7339..ea729e7c1c20 100644
--- a/tests/cargo-kani/itoa_dep/src/main.rs
+++ b/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() {}
diff --git a/tests/perf/format/Cargo.toml b/tests/perf/format/Cargo.toml
new file mode 100644
index 000000000000..3fe392e07c04
--- /dev/null
+++ b/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]
diff --git a/tests/perf/format/expected b/tests/perf/format/expected
new file mode 100644
index 000000000000..44572d1c72bf
--- /dev/null
+++ b/tests/perf/format/expected
@@ -0,0 +1 @@
+Complete - 2 successfully verified harnesses, 0 failures, 2 total
diff --git a/tests/perf/format/src/lib.rs b/tests/perf/format/src/lib.rs
new file mode 100644
index 000000000000..ad14c6288e7c
--- /dev/null
+++ b/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);
+}