Revert "Temporarily remove most perf tests to debug failure"

This reverts commit 63f6028.

.gitmodules

@@ -1,3 +1,7 @@
 [submodule "firecracker"]
 	path = firecracker
 	url = https://github.com/firecracker-microvm/firecracker.git
+[submodule "tests/perf/s2n-quic"]
+	path = tests/perf/s2n-quic
+	url = https://github.com/aws/s2n-quic
+	branch = main

tests/perf/btreeset/insert_any/Cargo.toml

@@ -0,0 +1,16 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "insert_any"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_any/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/perf/btreeset/insert_any/src/main.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of pushing onto a BTreeSet
+//! The test is from https://github.com/model-checking/kani/issues/705.
+//! Pre CBMC 5.72.0, it ran out of memory
+//! With CBMC 5.72.0, it takes ~10 seconds and consumes ~255 MB of memory.
+
+use std::collections::BTreeSet;
+
+#[kani::proof]
+#[kani::unwind(3)]
+fn main() {
+    let mut set = BTreeSet::<u32>::new();
+    let x = kani::any();
+    set.insert(x);
+    assert!(set.contains(&x));
+}

tests/perf/btreeset/insert_multi/Cargo.toml

@@ -0,0 +1,16 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "insert_multi"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_multi/expected

@@ -0,0 +1,2 @@
+** 2 of 2 cover properties satisfied
+VERIFICATION:- SUCCESSFUL

tests/perf/btreeset/insert_multi/src/main.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of pushing multiple non-det elements onto a
+//! `BtreeSet`
+
+use kani::cover;
+use std::collections::BTreeSet;
+
+#[kani::proof]
+#[kani::unwind(3)]
+#[kani::solver(cadical)]
+fn insert_multi() {
+    const N: usize = 2;
+    let mut set: BTreeSet<i32> = BTreeSet::new();
+    for _i in 0..N {
+        set.insert(kani::any());
+    }
+    assert!(!set.is_empty());
+    // all elements are the same
+    cover!(set.len() == 1);
+    // two unique elements
+    cover!(set.len() == 2);
+}
+
+fn main() {}

tests/perf/btreeset/insert_same/Cargo.toml

@@ -0,0 +1,16 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "insert_same"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_same/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/perf/btreeset/insert_same/src/main.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of pushing the same element onto a `BTreeSet`
+//! The test is from <https://github.com/model-checking/kani/issues/2022>
+//! With CBMC's default solver (minisat), it takes ~517 seconds
+//! With Kissat 3.0.0, it takes ~22 seconds
+
+use std::collections::BTreeSet;
+
+#[kani::proof]
+#[kani::unwind(3)]
+#[kani::solver(minisat)]
+fn main() {
+    let mut set: BTreeSet<i32> = BTreeSet::new();
+    let x = kani::any();
+    set.insert(x);
+    set.insert(x);
+    assert!(set.len() == 1);
+}

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 test captures the performance regression introduced by the toolchain upgrade in <https://github.com/model-checking/kani/pull/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);
+}

tests/perf/hashset/Cargo.toml

@@ -0,0 +1,19 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "hashset"
+version = "0.1.0"
+edition = "2021"
+description = "Verify HashSet basic behavior"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+[package.metadata.kani.unstable]
+stubbing = true
+
+# Temporarily ignore the handling of storage markers till
+# https://github.com/model-checking/kani/issues/3099 is fixed
+[package.metadata.kani]
+flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/hashset/expected

@@ -0,0 +1 @@
+3 successfully verified harnesses, 0 failures, 3 total

tests/perf/hashset/src/lib.rs

@@ -0,0 +1,76 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z stubbing
+//! Try to verify HashSet basic behavior.
+
+use std::collections::{hash_map::RandomState, HashSet};
+use std::mem::{size_of, size_of_val, transmute};
+
+#[allow(dead_code)]
+fn concrete_state() -> RandomState {
+    let keys: [u64; 2] = [0, 0];
+    assert_eq!(size_of_val(&keys), size_of::<RandomState>());
+    unsafe { transmute(keys) }
+}
+
+#[kani::proof]
+#[kani::stub(RandomState::new, concrete_state)]
+#[kani::unwind(5)]
+#[kani::solver(kissat)]
+fn check_insert() {
+    let mut set: HashSet<i32> = HashSet::default();
+    let first = kani::any();
+    set.insert(first);
+    assert_eq!(set.len(), 1);
+    assert_eq!(set.iter().next(), Some(&first));
+}
+
+#[kani::proof]
+#[kani::stub(RandomState::new, concrete_state)]
+#[kani::unwind(5)]
+#[kani::solver(kissat)]
+fn check_contains() {
+    let first = kani::any();
+    let set: HashSet<i8> = HashSet::from([first]);
+    assert!(set.contains(&first));
+}
+
+#[kani::proof]
+#[kani::stub(RandomState::new, concrete_state)]
+#[kani::unwind(5)]
+#[kani::solver(kissat)]
+fn check_contains_str() {
+    let set = HashSet::from(["s"]);
+    assert!(set.contains(&"s"));
+}
+
+// too slow so don't run in the regression for now
+#[cfg(slow)]
+mod slow {
+    #[kani::proof]
+    #[kani::stub(RandomState::new, concrete_state)]
+    #[kani::unwind(5)]
+    fn check_insert_two_elements() {
+        let mut set: HashSet<i8> = HashSet::default();
+        let first = kani::any();
+        set.insert(first);
+
+        let second = kani::any();
+        set.insert(second);
+
+        if first == second { assert_eq!(set.len(), 1) } else { assert_eq!(set.len(), 2) }
+    }
+
+    #[kani::proof]
+    #[kani::stub(RandomState::new, concrete_state)]
+    #[kani::unwind(5)]
+    #[kani::solver(kissat)]
+    fn check_insert_two_concrete() {
+        let mut set: HashSet<i32> = HashSet::default();
+        let first = 10;
+        let second = 20;
+        set.insert(first);
+        set.insert(second);
+        assert_eq!(set.len(), 2);
+    }
+}

tests/perf/kani-lib/arbitrary/Cargo.toml

@@ -0,0 +1,13 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "arbitrary"
+version = "0.1.0"
+edition = "2021"
+description = "Performance tests for different implementations of arbitrary"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+[lib]
+path = "src/check_arbitrary.rs"
+
+[dependencies]

tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs

@@ -0,0 +1,92 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains performance checks for Arbitrary implementations that are included in the
+//! kani library.
+
+#[kani::proof]
+fn check_any_char() {
+    for _ in 0..100 {
+        let c: char = kani::any();
+        let n = c as u32;
+        assert!(n <= 0x10FFFF);
+    }
+
+    for _ in 0..100 {
+        let c: char = kani::any();
+        kani::assume(c.is_digit(10));
+        assert!(c.to_digit(10).is_some());
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(101)]
+fn check_any_char_array() {
+    let arr: [char; 100] = kani::any();
+    for i in 0..100 {
+        let c = arr[i];
+        let n = c as u32;
+        assert!(n <= 0x10FFFF);
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(101)]
+fn check_any_usize_array() {
+    let arr: [usize; 100] = kani::any();
+    for i in 0..100 {
+        let us = arr[i];
+        kani::assume(us < 100);
+        assert!(us < 1000);
+    }
+}
+
+#[kani::proof]
+fn check_any_usize_option() {
+    let mut all_none = true;
+    let mut all_some = true;
+    for _ in 0..100 {
+        let us: Option<usize> = kani::any();
+        all_none &= us.is_none();
+        all_some &= us.is_some();
+    }
+
+    assert!(!all_none || !all_some);
+}
+
+#[kani::proof]
+fn check_any_usize_result() {
+    let mut all_ok = true;
+    let mut all_err = true;
+    for _ in 0..100 {
+        let us: Result<usize, isize> = kani::any();
+        all_ok &= us.is_ok();
+        all_err &= us.is_err();
+    }
+
+    assert!(!all_ok || !all_err);
+}
+
+#[kani::proof]
+fn check_any_bool() {
+    let mut all_true = true;
+    let mut all_false = true;
+    for _ in 0..100 {
+        let val: bool = kani::any();
+        all_true &= val;
+        all_false &= !val;
+    }
+
+    assert!(!all_true || !all_false);
+}
+
+#[kani::proof]
+fn check_duration() {
+    let durations: [Duration; 10] = kani::any();
+    let (max, zero): (usize, usize) = kani::any();
+    kani::assume(max < durations.len() && zero < durations.len());
+    kani::assume(durations[max] == Duration::MAX);
+    kani::assume(durations[zero] == Duration::ZERO);
+    assert_eq!(durations.iter().min(), Some(&Duration::ZERO));
+    assert_eq!(durations.iter().max(), Some(&Duration::MAX));
+}

tests/perf/misc/array_fold/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "array_fold"
+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/misc/array_fold/expected

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