From 0dd05cc0da041ef04c279c498c09d037905e1ac4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 3 May 2024 17:00:15 -0700 Subject: [PATCH 01/11] Upgrade toolchain to 2024-04-22 --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 23 +++++++++++++++++++ .../src/kani_middle/transform/check_values.rs | 1 + rust-toolchain.toml | 2 +- 3 files changed, 25 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index cb78163fe99b..2b2c74c2e9cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -674,6 +674,29 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, ) } + AggregateKind::RawPtr(pointee_ty, _) => { + // We expect two operands: "data" and "meta" + assert!(operands.len() == 2); + let typ = self.codegen_ty_stable(res_ty); + let layout = self.layout_of_stable(res_ty); + assert!(layout.ty.is_unsafe_ptr()); + let data = self.codegen_operand_stable(&operands[0]); + //dbg!(pointee_ty.kind()); + match pointee_ty.kind() { + TyKind::RigidTy(RigidTy::Slice(inner_ty)) => { + let pointee_goto_typ = self.codegen_ty_stable(inner_ty); + // cast data to pointer with specified type + let data_cast = + data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); + let meta = self.codegen_operand_stable(&operands[1]); + slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) + } + _ => { + let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); + data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }) + } + } + } AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty), } } diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index d62b5807319e..4697c139b294 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -678,6 +678,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { AggregateKind::Array(_) | AggregateKind::Closure(_, _) | AggregateKind::Coroutine(_, _, _) + | AggregateKind::RawPtr(_, _) | AggregateKind::Tuple => {} }, Rvalue::AddressOf(_, _) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 70848743b686..e571e9eaff4f 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-04-21" +channel = "nightly-2024-04-22" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 2d2336513824966891d87e10830f5285032a7d7c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 10 May 2024 14:59:45 +0000 Subject: [PATCH 02/11] Support Wrapper --- .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 2b2c74c2e9cd..c3507fcd7a5c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -691,6 +691,15 @@ impl<'tcx> GotocCtx<'tcx> { let meta = self.codegen_operand_stable(&operands[1]); slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } + TyKind::RigidTy(RigidTy::Adt(..)) => { + let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); + let data_cast = + data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); + let meta = self.codegen_operand_stable(&operands[1]); + let vtable_expr = meta.member("vtable_ptr", &self.symbol_table).cast_to( + typ.lookup_field_type("vtable", &self.symbol_table).unwrap()); + dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + } _ => { let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }) From eeb6741616e876ef412f2e5544434b9765a2bdda Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 10 May 2024 15:02:16 +0000 Subject: [PATCH 03/11] fmt --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c3507fcd7a5c..1baad94cdbed 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -696,8 +696,9 @@ impl<'tcx> GotocCtx<'tcx> { let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); let meta = self.codegen_operand_stable(&operands[1]); - let vtable_expr = meta.member("vtable_ptr", &self.symbol_table).cast_to( - typ.lookup_field_type("vtable", &self.symbol_table).unwrap()); + let vtable_expr = meta + .member("vtable_ptr", &self.symbol_table) + .cast_to(typ.lookup_field_type("vtable", &self.symbol_table).unwrap()); dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) } _ => { From c8e20b3c9d9f2d65aca2e5531cd87a67276ded9b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 10 May 2024 15:17:31 +0000 Subject: [PATCH 04/11] Metadata can be empty --- .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 1baad94cdbed..f1ce780819d8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -696,10 +696,15 @@ impl<'tcx> GotocCtx<'tcx> { let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); let meta = self.codegen_operand_stable(&operands[1]); - let vtable_expr = meta - .member("vtable_ptr", &self.symbol_table) - .cast_to(typ.lookup_field_type("vtable", &self.symbol_table).unwrap()); - dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + if meta.typ().sizeof(&self.symbol_table) == 0 { + data_cast + } else { + let vtable_expr = + meta.member("vtable_ptr", &self.symbol_table).cast_to( + typ.lookup_field_type("vtable", &self.symbol_table).unwrap(), + ); + dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + } } _ => { let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); From ce23c188ace728a45846558aa5f9634107e64dbe Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 10 May 2024 11:19:20 -0700 Subject: [PATCH 05/11] Delete non-failing tests --- .github/workflows/bench.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index 12b08eba7c9c..817f97e64b46 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -58,6 +58,11 @@ jobs: - name: Copy benchmarks from new to old run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/ + - run: | + rm -rf old/tests/perf/btreeset old/tests/perf/format old/tests/perf/hashset old/tests/perf/kani-lib old/tests/perf/misc old/tests/perf/s2n-quic old/tests/perf/string + rm -rf new/tests/perf/btreeset new/tests/perf/format new/tests/perf/hashset new/tests/perf/kani-lib new/tests/perf/misc new/tests/perf/s2n-quic new/tests/perf/string + name: Delete all tests apart from failing one + - name: Run benchcomp run: | new/tools/benchcomp/bin/benchcomp \ From d140243e5fd97c458d414b1098b00aeba3f3ad9c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 13 May 2024 10:10:47 -0700 Subject: [PATCH 06/11] Remove comment --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f1ce780819d8..8a9aa4821ab6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -681,7 +681,6 @@ impl<'tcx> GotocCtx<'tcx> { let layout = self.layout_of_stable(res_ty); assert!(layout.ty.is_unsafe_ptr()); let data = self.codegen_operand_stable(&operands[0]); - //dbg!(pointee_ty.kind()); match pointee_ty.kind() { TyKind::RigidTy(RigidTy::Slice(inner_ty)) => { let pointee_goto_typ = self.codegen_ty_stable(inner_ty); From 63f6028324b80e515dd0f45963651eab0608a2b9 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 13 May 2024 10:12:34 -0700 Subject: [PATCH 07/11] Temporarily remove most perf tests to debug failure --- .gitmodules | 4 - tests/perf/btreeset/insert_any/Cargo.toml | 16 ---- tests/perf/btreeset/insert_any/expected | 1 - tests/perf/btreeset/insert_any/src/main.rs | 18 ---- tests/perf/btreeset/insert_multi/Cargo.toml | 16 ---- tests/perf/btreeset/insert_multi/expected | 2 - tests/perf/btreeset/insert_multi/src/main.rs | 26 ------ tests/perf/btreeset/insert_same/Cargo.toml | 16 ---- tests/perf/btreeset/insert_same/expected | 1 - tests/perf/btreeset/insert_same/src/main.rs | 20 ---- tests/perf/format/Cargo.toml | 11 --- tests/perf/format/expected | 1 - tests/perf/format/src/lib.rs | 20 ---- tests/perf/hashset/Cargo.toml | 19 ---- tests/perf/hashset/expected | 1 - tests/perf/hashset/src/lib.rs | 76 --------------- tests/perf/kani-lib/arbitrary/Cargo.toml | 13 --- .../kani-lib/arbitrary/src/check_arbitrary.rs | 92 ------------------- tests/perf/misc/array_fold/Cargo.toml | 11 --- tests/perf/misc/array_fold/expected | 1 - tests/perf/misc/array_fold/src/main.rs | 34 ------- tests/perf/misc/display_trait/Cargo.toml | 11 --- tests/perf/misc/display_trait/expected | 1 - tests/perf/misc/display_trait/src/main.rs | 42 --------- tests/perf/misc/struct_defs/Cargo.toml | 11 --- tests/perf/misc/struct_defs/expected | 1 - tests/perf/misc/struct_defs/src/main.rs | 88 ------------------ tests/perf/s2n-quic | 1 - tests/perf/string/expected | 2 - tests/perf/string/src/any_str.rs | 18 ---- 30 files changed, 574 deletions(-) delete mode 100644 tests/perf/btreeset/insert_any/Cargo.toml delete mode 100644 tests/perf/btreeset/insert_any/expected delete mode 100644 tests/perf/btreeset/insert_any/src/main.rs delete mode 100644 tests/perf/btreeset/insert_multi/Cargo.toml delete mode 100644 tests/perf/btreeset/insert_multi/expected delete mode 100644 tests/perf/btreeset/insert_multi/src/main.rs delete mode 100644 tests/perf/btreeset/insert_same/Cargo.toml delete mode 100644 tests/perf/btreeset/insert_same/expected delete mode 100644 tests/perf/btreeset/insert_same/src/main.rs delete mode 100644 tests/perf/format/Cargo.toml delete mode 100644 tests/perf/format/expected delete mode 100644 tests/perf/format/src/lib.rs delete mode 100644 tests/perf/hashset/Cargo.toml delete mode 100644 tests/perf/hashset/expected delete mode 100644 tests/perf/hashset/src/lib.rs delete mode 100644 tests/perf/kani-lib/arbitrary/Cargo.toml delete mode 100644 tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs delete mode 100644 tests/perf/misc/array_fold/Cargo.toml delete mode 100644 tests/perf/misc/array_fold/expected delete mode 100644 tests/perf/misc/array_fold/src/main.rs delete mode 100644 tests/perf/misc/display_trait/Cargo.toml delete mode 100644 tests/perf/misc/display_trait/expected delete mode 100644 tests/perf/misc/display_trait/src/main.rs delete mode 100644 tests/perf/misc/struct_defs/Cargo.toml delete mode 100644 tests/perf/misc/struct_defs/expected delete mode 100644 tests/perf/misc/struct_defs/src/main.rs delete mode 160000 tests/perf/s2n-quic delete mode 100644 tests/perf/string/expected delete mode 100644 tests/perf/string/src/any_str.rs diff --git a/.gitmodules b/.gitmodules index b02c263a898e..f7d8da6faa01 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,7 +1,3 @@ [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 diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml deleted file mode 100644 index 66d8ecdddeb1..000000000000 --- a/tests/perf/btreeset/insert_any/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -# 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 } diff --git a/tests/perf/btreeset/insert_any/expected b/tests/perf/btreeset/insert_any/expected deleted file mode 100644 index 34c886c358cb..000000000000 --- a/tests/perf/btreeset/insert_any/expected +++ /dev/null @@ -1 +0,0 @@ -VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_any/src/main.rs b/tests/perf/btreeset/insert_any/src/main.rs deleted file mode 100644 index cf9df6551ae4..000000000000 --- a/tests/perf/btreeset/insert_any/src/main.rs +++ /dev/null @@ -1,18 +0,0 @@ -// 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::::new(); - let x = kani::any(); - set.insert(x); - assert!(set.contains(&x)); -} diff --git a/tests/perf/btreeset/insert_multi/Cargo.toml b/tests/perf/btreeset/insert_multi/Cargo.toml deleted file mode 100644 index 44028f8c842d..000000000000 --- a/tests/perf/btreeset/insert_multi/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -# 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 } diff --git a/tests/perf/btreeset/insert_multi/expected b/tests/perf/btreeset/insert_multi/expected deleted file mode 100644 index b8278d86805d..000000000000 --- a/tests/perf/btreeset/insert_multi/expected +++ /dev/null @@ -1,2 +0,0 @@ -** 2 of 2 cover properties satisfied -VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_multi/src/main.rs b/tests/perf/btreeset/insert_multi/src/main.rs deleted file mode 100644 index 47969f1d9e12..000000000000 --- a/tests/perf/btreeset/insert_multi/src/main.rs +++ /dev/null @@ -1,26 +0,0 @@ -// 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 = 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() {} diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml deleted file mode 100644 index 465119c74fbe..000000000000 --- a/tests/perf/btreeset/insert_same/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -# 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 } diff --git a/tests/perf/btreeset/insert_same/expected b/tests/perf/btreeset/insert_same/expected deleted file mode 100644 index 34c886c358cb..000000000000 --- a/tests/perf/btreeset/insert_same/expected +++ /dev/null @@ -1 +0,0 @@ -VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_same/src/main.rs b/tests/perf/btreeset/insert_same/src/main.rs deleted file mode 100644 index d77dd0644cde..000000000000 --- a/tests/perf/btreeset/insert_same/src/main.rs +++ /dev/null @@ -1,20 +0,0 @@ -// 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 -//! 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 = BTreeSet::new(); - let x = kani::any(); - set.insert(x); - set.insert(x); - assert!(set.len() == 1); -} diff --git a/tests/perf/format/Cargo.toml b/tests/perf/format/Cargo.toml deleted file mode 100644 index 3fe392e07c04..000000000000 --- a/tests/perf/format/Cargo.toml +++ /dev/null @@ -1,11 +0,0 @@ -# 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 deleted file mode 100644 index 44572d1c72bf..000000000000 --- a/tests/perf/format/expected +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 1986a08222ba..000000000000 --- a/tests/perf/format/src/lib.rs +++ /dev/null @@ -1,20 +0,0 @@ -// 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 -//! See 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); -} diff --git a/tests/perf/hashset/Cargo.toml b/tests/perf/hashset/Cargo.toml deleted file mode 100644 index 464fba412e6d..000000000000 --- a/tests/perf/hashset/Cargo.toml +++ /dev/null @@ -1,19 +0,0 @@ -# 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 } diff --git a/tests/perf/hashset/expected b/tests/perf/hashset/expected deleted file mode 100644 index 1fbcbbd13c25..000000000000 --- a/tests/perf/hashset/expected +++ /dev/null @@ -1 +0,0 @@ -3 successfully verified harnesses, 0 failures, 3 total diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs deleted file mode 100644 index e2f1fc16666a..000000000000 --- a/tests/perf/hashset/src/lib.rs +++ /dev/null @@ -1,76 +0,0 @@ -// 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::()); - unsafe { transmute(keys) } -} - -#[kani::proof] -#[kani::stub(RandomState::new, concrete_state)] -#[kani::unwind(5)] -#[kani::solver(kissat)] -fn check_insert() { - let mut set: HashSet = 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 = 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 = 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 = HashSet::default(); - let first = 10; - let second = 20; - set.insert(first); - set.insert(second); - assert_eq!(set.len(), 2); - } -} diff --git a/tests/perf/kani-lib/arbitrary/Cargo.toml b/tests/perf/kani-lib/arbitrary/Cargo.toml deleted file mode 100644 index 62f7fcf5d1d1..000000000000 --- a/tests/perf/kani-lib/arbitrary/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -# 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] diff --git a/tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs b/tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs deleted file mode 100644 index 1833b0768833..000000000000 --- a/tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs +++ /dev/null @@ -1,92 +0,0 @@ -// 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 = 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 = 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)); -} diff --git a/tests/perf/misc/array_fold/Cargo.toml b/tests/perf/misc/array_fold/Cargo.toml deleted file mode 100644 index 673b7681e0c7..000000000000 --- a/tests/perf/misc/array_fold/Cargo.toml +++ /dev/null @@ -1,11 +0,0 @@ -# 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] diff --git a/tests/perf/misc/array_fold/expected b/tests/perf/misc/array_fold/expected deleted file mode 100644 index 643fbd2317ec..000000000000 --- a/tests/perf/misc/array_fold/expected +++ /dev/null @@ -1 +0,0 @@ -Complete - 0 successfully verified harnesses, 2 failures, 2 total. diff --git a/tests/perf/misc/array_fold/src/main.rs b/tests/perf/misc/array_fold/src/main.rs deleted file mode 100644 index d7953255612b..000000000000 --- a/tests/perf/misc/array_fold/src/main.rs +++ /dev/null @@ -1,34 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test checks the performance of fold, which uses iterators under the -//! hood. -//! The test is from https://github.com/model-checking/kani/issues/1823. -//! Pre CBMC 5.72.0, it took ~36 seconds and consumed ~3.6 GB of memory. -//! With CBMC 5.72.0, it takes ~11 seconds and consumes ~255 MB of memory. - -pub fn array_sum_fold(x: [usize; 100]) -> usize { - x.iter().fold(0, |accumulator, current| accumulator + current) -} - -pub fn array_sum_for(x: [usize; 100]) -> usize { - let mut accumulator: usize = 0; - for i in 0..100 { - accumulator = x[i] + accumulator - } - accumulator -} - -#[kani::proof] -fn array_sum_fold_proof() { - let x: [usize; 100] = kani::any(); - array_sum_fold(x); -} - -#[kani::proof] -fn array_sum_for_proof() { - let x: [usize; 100] = kani::any(); - array_sum_for(x); -} - -fn main() {} diff --git a/tests/perf/misc/display_trait/Cargo.toml b/tests/perf/misc/display_trait/Cargo.toml deleted file mode 100644 index ce31328c8834..000000000000 --- a/tests/perf/misc/display_trait/Cargo.toml +++ /dev/null @@ -1,11 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "display_trait" -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/misc/display_trait/expected b/tests/perf/misc/display_trait/expected deleted file mode 100644 index 4426ff6c02cd..000000000000 --- a/tests/perf/misc/display_trait/expected +++ /dev/null @@ -1 +0,0 @@ -Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/perf/misc/display_trait/src/main.rs b/tests/perf/misc/display_trait/src/main.rs deleted file mode 100644 index f2f3b91e3344..000000000000 --- a/tests/perf/misc/display_trait/src/main.rs +++ /dev/null @@ -1,42 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test checks the performance when adding in the Display trait. -//! The test is from https://github.com/model-checking/kani/issues/1996 -//! With CBMC 5.79.0, all harnesses take ~3 seconds -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"); -} diff --git a/tests/perf/misc/struct_defs/Cargo.toml b/tests/perf/misc/struct_defs/Cargo.toml deleted file mode 100644 index 095c719f2b4b..000000000000 --- a/tests/perf/misc/struct_defs/Cargo.toml +++ /dev/null @@ -1,11 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "struct_defs" -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/misc/struct_defs/expected b/tests/perf/misc/struct_defs/expected deleted file mode 100644 index 9427535ab675..000000000000 --- a/tests/perf/misc/struct_defs/expected +++ /dev/null @@ -1 +0,0 @@ -Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/perf/misc/struct_defs/src/main.rs b/tests/perf/misc/struct_defs/src/main.rs deleted file mode 100644 index bba599888b77..000000000000 --- a/tests/perf/misc/struct_defs/src/main.rs +++ /dev/null @@ -1,88 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test checks the performance with different struct definitions -//! The test is from https://github.com/model-checking/kani/issues/1958. -//! With CBMC 5.72.0, all harnesses take ~1 second - -#[derive(PartialEq, Eq)] -enum Expr { - A, - B(Box), - C(Box, Box), - D(Box, Box, Box), - E(Box, Box, Box, Box), -} - -#[derive(PartialEq, Eq)] -enum Result { - Ok(S), - Err(T), -} - -impl Result { - fn unwrap(&self) -> &S { - let x = match self { - Result::Ok(x) => x, - Result::Err(_) => panic!(), - }; - x - } -} - -enum Err { - A(X), - B(Y, Z), -} - -type Err1 = Err; -type Err2<'a> = Err; -type Err3<'a> = Err; -type Err4<'a> = Err; -type Err5<'a> = Err<&'a str, String, String>; -type Err6<'a> = Err<&'a str, &'a str, String>; -type Err7<'a> = Err<&'a str, String, &'a str>; -type Err8<'a> = Err<&'a str, &'a str, &'a str>; -type Err9<'a> = Err; -type Err10<'a> = Err, &'a str, String>; - -// Takes >10s -#[cfg_attr(kani, kani::proof, kani::unwind(2))] -fn slow_harness1() { - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); -} - -// Takes >10s -#[cfg_attr(kani, kani::proof, kani::unwind(2))] -fn slow_harness2() { - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); -} - -// Takes ~1s -#[cfg_attr(kani, kani::proof, kani::unwind(2))] -fn fast_harness() { - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); - let x: Result = Result::Ok(Expr::A); - assert_eq!(x.unwrap(), &Expr::A); -} - -fn main() {} diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic deleted file mode 160000 index 6dd41e09195b..000000000000 --- a/tests/perf/s2n-quic +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 6dd41e09195bc22dbac93a48f8ab35f8063726dc diff --git a/tests/perf/string/expected b/tests/perf/string/expected deleted file mode 100644 index ac9ef183fb2c..000000000000 --- a/tests/perf/string/expected +++ /dev/null @@ -1,2 +0,0 @@ -Failed Checks: Function `alloc::string::String::from_utf8_lossy` with missing definition is unreachable - diff --git a/tests/perf/string/src/any_str.rs b/tests/perf/string/src/any_str.rs deleted file mode 100644 index 3b58d56750a7..000000000000 --- a/tests/perf/string/src/any_str.rs +++ /dev/null @@ -1,18 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-flags: --enable-unstable --mir-linker -// -//! This test is to check MIR linker state of the art. -//! I.e.: Currently, this should fail with missing function definition. - -#[kani::proof] -#[kani::unwind(4)] -fn check_abs() { - let data: [u8; 3] = kani::any(); - let mut string = String::from_utf8_lossy(&data).to_string(); - let new_len = kani::any(); - kani::assume(new_len <= 2); - string.truncate(new_len); - assert!(string.len() <= 2); -} From a449d17329a9ad9314ce613733d50fb7734b9702 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 13 May 2024 11:14:42 -0700 Subject: [PATCH 08/11] Revert "Temporarily remove most perf tests to debug failure" This reverts commit 63f6028324b80e515dd0f45963651eab0608a2b9. --- .gitmodules | 4 + tests/perf/btreeset/insert_any/Cargo.toml | 16 ++++ tests/perf/btreeset/insert_any/expected | 1 + tests/perf/btreeset/insert_any/src/main.rs | 18 ++++ tests/perf/btreeset/insert_multi/Cargo.toml | 16 ++++ tests/perf/btreeset/insert_multi/expected | 2 + tests/perf/btreeset/insert_multi/src/main.rs | 26 ++++++ tests/perf/btreeset/insert_same/Cargo.toml | 16 ++++ tests/perf/btreeset/insert_same/expected | 1 + tests/perf/btreeset/insert_same/src/main.rs | 20 ++++ tests/perf/format/Cargo.toml | 11 +++ tests/perf/format/expected | 1 + tests/perf/format/src/lib.rs | 20 ++++ tests/perf/hashset/Cargo.toml | 19 ++++ tests/perf/hashset/expected | 1 + tests/perf/hashset/src/lib.rs | 76 +++++++++++++++ tests/perf/kani-lib/arbitrary/Cargo.toml | 13 +++ .../kani-lib/arbitrary/src/check_arbitrary.rs | 92 +++++++++++++++++++ tests/perf/misc/array_fold/Cargo.toml | 11 +++ tests/perf/misc/array_fold/expected | 1 + tests/perf/misc/array_fold/src/main.rs | 34 +++++++ tests/perf/misc/display_trait/Cargo.toml | 11 +++ tests/perf/misc/display_trait/expected | 1 + tests/perf/misc/display_trait/src/main.rs | 42 +++++++++ tests/perf/misc/struct_defs/Cargo.toml | 11 +++ tests/perf/misc/struct_defs/expected | 1 + tests/perf/misc/struct_defs/src/main.rs | 88 ++++++++++++++++++ tests/perf/s2n-quic | 1 + tests/perf/string/expected | 2 + tests/perf/string/src/any_str.rs | 18 ++++ 30 files changed, 574 insertions(+) create mode 100644 tests/perf/btreeset/insert_any/Cargo.toml create mode 100644 tests/perf/btreeset/insert_any/expected create mode 100644 tests/perf/btreeset/insert_any/src/main.rs create mode 100644 tests/perf/btreeset/insert_multi/Cargo.toml create mode 100644 tests/perf/btreeset/insert_multi/expected create mode 100644 tests/perf/btreeset/insert_multi/src/main.rs create mode 100644 tests/perf/btreeset/insert_same/Cargo.toml create mode 100644 tests/perf/btreeset/insert_same/expected create mode 100644 tests/perf/btreeset/insert_same/src/main.rs create mode 100644 tests/perf/format/Cargo.toml create mode 100644 tests/perf/format/expected create mode 100644 tests/perf/format/src/lib.rs create mode 100644 tests/perf/hashset/Cargo.toml create mode 100644 tests/perf/hashset/expected create mode 100644 tests/perf/hashset/src/lib.rs create mode 100644 tests/perf/kani-lib/arbitrary/Cargo.toml create mode 100644 tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs create mode 100644 tests/perf/misc/array_fold/Cargo.toml create mode 100644 tests/perf/misc/array_fold/expected create mode 100644 tests/perf/misc/array_fold/src/main.rs create mode 100644 tests/perf/misc/display_trait/Cargo.toml create mode 100644 tests/perf/misc/display_trait/expected create mode 100644 tests/perf/misc/display_trait/src/main.rs create mode 100644 tests/perf/misc/struct_defs/Cargo.toml create mode 100644 tests/perf/misc/struct_defs/expected create mode 100644 tests/perf/misc/struct_defs/src/main.rs create mode 160000 tests/perf/s2n-quic create mode 100644 tests/perf/string/expected create mode 100644 tests/perf/string/src/any_str.rs diff --git a/.gitmodules b/.gitmodules index f7d8da6faa01..b02c263a898e 100644 --- a/.gitmodules +++ b/.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 diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml new file mode 100644 index 000000000000..66d8ecdddeb1 --- /dev/null +++ b/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 } diff --git a/tests/perf/btreeset/insert_any/expected b/tests/perf/btreeset/insert_any/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/perf/btreeset/insert_any/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_any/src/main.rs b/tests/perf/btreeset/insert_any/src/main.rs new file mode 100644 index 000000000000..cf9df6551ae4 --- /dev/null +++ b/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::::new(); + let x = kani::any(); + set.insert(x); + assert!(set.contains(&x)); +} diff --git a/tests/perf/btreeset/insert_multi/Cargo.toml b/tests/perf/btreeset/insert_multi/Cargo.toml new file mode 100644 index 000000000000..44028f8c842d --- /dev/null +++ b/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 } diff --git a/tests/perf/btreeset/insert_multi/expected b/tests/perf/btreeset/insert_multi/expected new file mode 100644 index 000000000000..b8278d86805d --- /dev/null +++ b/tests/perf/btreeset/insert_multi/expected @@ -0,0 +1,2 @@ +** 2 of 2 cover properties satisfied +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_multi/src/main.rs b/tests/perf/btreeset/insert_multi/src/main.rs new file mode 100644 index 000000000000..47969f1d9e12 --- /dev/null +++ b/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 = 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() {} diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml new file mode 100644 index 000000000000..465119c74fbe --- /dev/null +++ b/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 } diff --git a/tests/perf/btreeset/insert_same/expected b/tests/perf/btreeset/insert_same/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/perf/btreeset/insert_same/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_same/src/main.rs b/tests/perf/btreeset/insert_same/src/main.rs new file mode 100644 index 000000000000..d77dd0644cde --- /dev/null +++ b/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 +//! 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 = BTreeSet::new(); + let x = kani::any(); + set.insert(x); + set.insert(x); + assert!(set.len() == 1); +} 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..1986a08222ba --- /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 test captures the performance regression introduced by the toolchain upgrade in +//! See 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); +} diff --git a/tests/perf/hashset/Cargo.toml b/tests/perf/hashset/Cargo.toml new file mode 100644 index 000000000000..464fba412e6d --- /dev/null +++ b/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 } diff --git a/tests/perf/hashset/expected b/tests/perf/hashset/expected new file mode 100644 index 000000000000..1fbcbbd13c25 --- /dev/null +++ b/tests/perf/hashset/expected @@ -0,0 +1 @@ +3 successfully verified harnesses, 0 failures, 3 total diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs new file mode 100644 index 000000000000..e2f1fc16666a --- /dev/null +++ b/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::()); + unsafe { transmute(keys) } +} + +#[kani::proof] +#[kani::stub(RandomState::new, concrete_state)] +#[kani::unwind(5)] +#[kani::solver(kissat)] +fn check_insert() { + let mut set: HashSet = 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 = 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 = 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 = HashSet::default(); + let first = 10; + let second = 20; + set.insert(first); + set.insert(second); + assert_eq!(set.len(), 2); + } +} diff --git a/tests/perf/kani-lib/arbitrary/Cargo.toml b/tests/perf/kani-lib/arbitrary/Cargo.toml new file mode 100644 index 000000000000..62f7fcf5d1d1 --- /dev/null +++ b/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] diff --git a/tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs b/tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs new file mode 100644 index 000000000000..1833b0768833 --- /dev/null +++ b/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 = 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 = 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)); +} diff --git a/tests/perf/misc/array_fold/Cargo.toml b/tests/perf/misc/array_fold/Cargo.toml new file mode 100644 index 000000000000..673b7681e0c7 --- /dev/null +++ b/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] diff --git a/tests/perf/misc/array_fold/expected b/tests/perf/misc/array_fold/expected new file mode 100644 index 000000000000..643fbd2317ec --- /dev/null +++ b/tests/perf/misc/array_fold/expected @@ -0,0 +1 @@ +Complete - 0 successfully verified harnesses, 2 failures, 2 total. diff --git a/tests/perf/misc/array_fold/src/main.rs b/tests/perf/misc/array_fold/src/main.rs new file mode 100644 index 000000000000..d7953255612b --- /dev/null +++ b/tests/perf/misc/array_fold/src/main.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of fold, which uses iterators under the +//! hood. +//! The test is from https://github.com/model-checking/kani/issues/1823. +//! Pre CBMC 5.72.0, it took ~36 seconds and consumed ~3.6 GB of memory. +//! With CBMC 5.72.0, it takes ~11 seconds and consumes ~255 MB of memory. + +pub fn array_sum_fold(x: [usize; 100]) -> usize { + x.iter().fold(0, |accumulator, current| accumulator + current) +} + +pub fn array_sum_for(x: [usize; 100]) -> usize { + let mut accumulator: usize = 0; + for i in 0..100 { + accumulator = x[i] + accumulator + } + accumulator +} + +#[kani::proof] +fn array_sum_fold_proof() { + let x: [usize; 100] = kani::any(); + array_sum_fold(x); +} + +#[kani::proof] +fn array_sum_for_proof() { + let x: [usize; 100] = kani::any(); + array_sum_for(x); +} + +fn main() {} diff --git a/tests/perf/misc/display_trait/Cargo.toml b/tests/perf/misc/display_trait/Cargo.toml new file mode 100644 index 000000000000..ce31328c8834 --- /dev/null +++ b/tests/perf/misc/display_trait/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "display_trait" +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/misc/display_trait/expected b/tests/perf/misc/display_trait/expected new file mode 100644 index 000000000000..4426ff6c02cd --- /dev/null +++ b/tests/perf/misc/display_trait/expected @@ -0,0 +1 @@ +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/perf/misc/display_trait/src/main.rs b/tests/perf/misc/display_trait/src/main.rs new file mode 100644 index 000000000000..f2f3b91e3344 --- /dev/null +++ b/tests/perf/misc/display_trait/src/main.rs @@ -0,0 +1,42 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance when adding in the Display trait. +//! The test is from https://github.com/model-checking/kani/issues/1996 +//! With CBMC 5.79.0, all harnesses take ~3 seconds +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"); +} diff --git a/tests/perf/misc/struct_defs/Cargo.toml b/tests/perf/misc/struct_defs/Cargo.toml new file mode 100644 index 000000000000..095c719f2b4b --- /dev/null +++ b/tests/perf/misc/struct_defs/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "struct_defs" +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/misc/struct_defs/expected b/tests/perf/misc/struct_defs/expected new file mode 100644 index 000000000000..9427535ab675 --- /dev/null +++ b/tests/perf/misc/struct_defs/expected @@ -0,0 +1 @@ +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/perf/misc/struct_defs/src/main.rs b/tests/perf/misc/struct_defs/src/main.rs new file mode 100644 index 000000000000..bba599888b77 --- /dev/null +++ b/tests/perf/misc/struct_defs/src/main.rs @@ -0,0 +1,88 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance with different struct definitions +//! The test is from https://github.com/model-checking/kani/issues/1958. +//! With CBMC 5.72.0, all harnesses take ~1 second + +#[derive(PartialEq, Eq)] +enum Expr { + A, + B(Box), + C(Box, Box), + D(Box, Box, Box), + E(Box, Box, Box, Box), +} + +#[derive(PartialEq, Eq)] +enum Result { + Ok(S), + Err(T), +} + +impl Result { + fn unwrap(&self) -> &S { + let x = match self { + Result::Ok(x) => x, + Result::Err(_) => panic!(), + }; + x + } +} + +enum Err { + A(X), + B(Y, Z), +} + +type Err1 = Err; +type Err2<'a> = Err; +type Err3<'a> = Err; +type Err4<'a> = Err; +type Err5<'a> = Err<&'a str, String, String>; +type Err6<'a> = Err<&'a str, &'a str, String>; +type Err7<'a> = Err<&'a str, String, &'a str>; +type Err8<'a> = Err<&'a str, &'a str, &'a str>; +type Err9<'a> = Err; +type Err10<'a> = Err, &'a str, String>; + +// Takes >10s +#[cfg_attr(kani, kani::proof, kani::unwind(2))] +fn slow_harness1() { + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); +} + +// Takes >10s +#[cfg_attr(kani, kani::proof, kani::unwind(2))] +fn slow_harness2() { + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); +} + +// Takes ~1s +#[cfg_attr(kani, kani::proof, kani::unwind(2))] +fn fast_harness() { + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); +} + +fn main() {} diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic new file mode 160000 index 000000000000..6dd41e09195b --- /dev/null +++ b/tests/perf/s2n-quic @@ -0,0 +1 @@ +Subproject commit 6dd41e09195bc22dbac93a48f8ab35f8063726dc diff --git a/tests/perf/string/expected b/tests/perf/string/expected new file mode 100644 index 000000000000..ac9ef183fb2c --- /dev/null +++ b/tests/perf/string/expected @@ -0,0 +1,2 @@ +Failed Checks: Function `alloc::string::String::from_utf8_lossy` with missing definition is unreachable + diff --git a/tests/perf/string/src/any_str.rs b/tests/perf/string/src/any_str.rs new file mode 100644 index 000000000000..3b58d56750a7 --- /dev/null +++ b/tests/perf/string/src/any_str.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: --enable-unstable --mir-linker +// +//! This test is to check MIR linker state of the art. +//! I.e.: Currently, this should fail with missing function definition. + +#[kani::proof] +#[kani::unwind(4)] +fn check_abs() { + let data: [u8; 3] = kani::any(); + let mut string = String::from_utf8_lossy(&data).to_string(); + let new_len = kani::any(); + kani::assume(new_len <= 2); + string.truncate(new_len); + assert!(string.len() <= 2); +} From 9e1541fec1de1f4794f1dedc82255164dab35bc3 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 13 May 2024 10:51:23 -0700 Subject: [PATCH 09/11] Do not run perf tests in parallel --- scripts/kani-perf.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh index a7e2710773aa..aaa1e250e3e9 100755 --- a/scripts/kani-perf.sh +++ b/scripts/kani-perf.sh @@ -27,7 +27,7 @@ done suite="perf" mode="cargo-kani-test" echo "Check compiletest suite=$suite mode=$mode" -cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast +RUST_TEST_THREADS=1 cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast exit_code=$? echo "Cleaning up..." From 07097b14481c248711ae6f21747fb12eb0545f3d Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 13 May 2024 13:09:42 -0700 Subject: [PATCH 10/11] Revert "Do not run perf tests in parallel" This reverts commit 9e1541fec1de1f4794f1dedc82255164dab35bc3. --- scripts/kani-perf.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh index aaa1e250e3e9..a7e2710773aa 100755 --- a/scripts/kani-perf.sh +++ b/scripts/kani-perf.sh @@ -27,7 +27,7 @@ done suite="perf" mode="cargo-kani-test" echo "Check compiletest suite=$suite mode=$mode" -RUST_TEST_THREADS=1 cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast +cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast exit_code=$? echo "Cleaning up..." From 41481736302a3e644ae1ba52e230f7cec8babfa7 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 14 May 2024 09:42:25 -0700 Subject: [PATCH 11/11] Remove step that was used for debugging --- .github/workflows/bench.yml | 5 ----- 1 file changed, 5 deletions(-) diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index 817f97e64b46..12b08eba7c9c 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -58,11 +58,6 @@ jobs: - name: Copy benchmarks from new to old run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/ - - run: | - rm -rf old/tests/perf/btreeset old/tests/perf/format old/tests/perf/hashset old/tests/perf/kani-lib old/tests/perf/misc old/tests/perf/s2n-quic old/tests/perf/string - rm -rf new/tests/perf/btreeset new/tests/perf/format new/tests/perf/hashset new/tests/perf/kani-lib new/tests/perf/misc new/tests/perf/s2n-quic new/tests/perf/string - name: Delete all tests apart from failing one - - name: Run benchcomp run: | new/tools/benchcomp/bin/benchcomp \