From 1e12c967c7f149a8609a06cfffa743ca415f74bd Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 28 Nov 2022 10:43:51 -0800 Subject: [PATCH 01/13] Bump CBMC to version 5.71.0 --- kani-dependencies | 2 +- scripts/kani-regression.sh | 2 +- tests/expected/loop-backedge/expected | 5 +++ tests/expected/loop-backedge/test.rs | 17 ++++++++++ tests/kani/CopyNonOverlapping/copy.rs | 36 ++++++++++++++++++++ tests/perf/vec/box_dyn/Cargo.toml | 8 +++++ tests/perf/vec/box_dyn/expected | 1 + tests/perf/vec/box_dyn/src/main.rs | 48 +++++++++++++++++++++++++++ tests/perf/vec/string/Cargo.toml | 8 +++++ tests/perf/vec/string/expected | 1 + tests/perf/vec/string/src/main.rs | 20 +++++++++++ 11 files changed, 146 insertions(+), 2 deletions(-) create mode 100644 tests/expected/loop-backedge/expected create mode 100644 tests/expected/loop-backedge/test.rs create mode 100644 tests/kani/CopyNonOverlapping/copy.rs create mode 100644 tests/perf/vec/box_dyn/Cargo.toml create mode 100644 tests/perf/vec/box_dyn/expected create mode 100644 tests/perf/vec/box_dyn/src/main.rs create mode 100644 tests/perf/vec/string/Cargo.toml create mode 100644 tests/perf/vec/string/expected create mode 100644 tests/perf/vec/string/src/main.rs diff --git a/kani-dependencies b/kani-dependencies index 6e658bafcdd3..72f93e32c684 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,3 +1,3 @@ -CBMC_VERSION="5.70.0" +CBMC_VERSION="5.71.0" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_VERSION="3.6" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index a870f9b225ca..83f1af552e61 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -22,7 +22,7 @@ KANI_DIR=$SCRIPT_DIR/.. export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true" # Required dependencies -check-cbmc-version.py --major 5 --minor 69 +check-cbmc-version.py --major 5 --minor 71 check-cbmc-viewer-version.py --major 3 --minor 5 # Formatting check diff --git a/tests/expected/loop-backedge/expected b/tests/expected/loop-backedge/expected new file mode 100644 index 000000000000..21a488cd2644 --- /dev/null +++ b/tests/expected/loop-backedge/expected @@ -0,0 +1,5 @@ +Status: SUCCESS\ +Description: "unwinding assertion loop 0" + +Status: SUCCESS\ +Description: "unwinding assertion loop 1" diff --git a/tests/expected/loop-backedge/test.rs b/tests/expected/loop-backedge/test.rs new file mode 100644 index 000000000000..91ef689880a5 --- /dev/null +++ b/tests/expected/loop-backedge/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that the unwinding assertions pass for nested loops for +//! which there's a backedge into the middle of the loop + +#[kani::proof] +#[kani::unwind(3)] +fn check_unwind_assertion() { + let a: &[i32] = &[0, 0]; + for &e in a { + assert_eq!(e, 0); + for i in e..1 { + assert_eq!(i, 0); + } + } +} diff --git a/tests/kani/CopyNonOverlapping/copy.rs b/tests/kani/CopyNonOverlapping/copy.rs new file mode 100644 index 000000000000..373a468c3738 --- /dev/null +++ b/tests/kani/CopyNonOverlapping/copy.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test verifies that std::ptr::copy_nonoverlapping works correctly +//! (originates from fixed bug https://github.com/model-checking/kani/issues/1911) + +pub struct Data { + pub t: Type, + pub array: [u8; 8], +} + +#[derive(PartialEq, Eq)] +pub enum Type { + Apple, + Banana, +} + +fn copy_from_slice(src: &[u8], dst: &mut [u8]) { + assert_eq!(src.len(), dst.len()); + unsafe { + std::ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), dst.len()); + } +} + +#[kani::proof] +fn proof_harness() { + let mut data = Data { + t: Type::Apple, + array: [0; 8], + }; + let coin = kani::any(); + let param = [0, 0, 0, 0]; + let start = if coin { 4 } else { 0 }; + copy_from_slice(¶m, &mut data.array[start..start+4]); + assert!(data.t == Type::Apple || data.t == Type::Banana); +} diff --git a/tests/perf/vec/box_dyn/Cargo.toml b/tests/perf/vec/box_dyn/Cargo.toml new file mode 100644 index 000000000000..9e2ea0c9c289 --- /dev/null +++ b/tests/perf/vec/box_dyn/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "box_dyn" +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/vec/box_dyn/expected b/tests/perf/vec/box_dyn/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/perf/vec/box_dyn/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/vec/box_dyn/src/main.rs b/tests/perf/vec/box_dyn/src/main.rs new file mode 100644 index 000000000000..43fb157fcb51 --- /dev/null +++ b/tests/perf/vec/box_dyn/src/main.rs @@ -0,0 +1,48 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of pushing onto a vector of Box + +const N: usize = 4; +const M: usize = N+1; + +trait T { + fn foo(&self) -> i32; +} + +struct A { + x: i32, +} + +impl T for A { + fn foo(&self) -> i32 { + self.x + } +} + +struct B { + x: i32, +} + +impl T for B { + fn foo(&self) -> i32 { + self.x + } +} + +#[kani::proof] +#[kani::unwind(6)] +fn main() { + let mut a: Vec> = Vec::new(); + a.push(Box::new(A { x: 5 })); + for i in 1..N { + a.push(Box::new(B { x: 9 })); + } + let mut val: i32 = 0; + for _i in 0..M { + let index: usize = kani::any(); + kani::assume(index < a.len()); + let x = a[index].as_mut().foo(); + val += x; + } +} diff --git a/tests/perf/vec/string/Cargo.toml b/tests/perf/vec/string/Cargo.toml new file mode 100644 index 000000000000..9eed48f08007 --- /dev/null +++ b/tests/perf/vec/string/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "string" +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/vec/string/expected b/tests/perf/vec/string/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/perf/vec/string/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/vec/string/src/main.rs b/tests/perf/vec/string/src/main.rs new file mode 100644 index 000000000000..af606b253e85 --- /dev/null +++ b/tests/perf/vec/string/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 onto a vector of strings + +const N: usize = 9; + +#[kani::proof] +#[kani::unwind(10))] +fn main() { + let mut v: Vec = Vec::new(); + for _i in 0..N { + v.push(String::from("ABC")); + } + assert_eq!(v.len(), N); + let index: usize = kani::any(); + kani::assume(index < v.len()); + let x = &v[index]; + assert_eq!(*x, "ABC"); +} From 4c2619cb15e846641e4876c48e88e7dcaacfab42 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 28 Nov 2022 11:18:11 -0800 Subject: [PATCH 02/13] Fix format --- tests/kani/CopyNonOverlapping/copy.rs | 7 ++----- tests/perf/vec/box_dyn/src/main.rs | 2 +- tests/perf/vec/string/src/main.rs | 2 +- 3 files changed, 4 insertions(+), 7 deletions(-) diff --git a/tests/kani/CopyNonOverlapping/copy.rs b/tests/kani/CopyNonOverlapping/copy.rs index 373a468c3738..87af5dd6bc15 100644 --- a/tests/kani/CopyNonOverlapping/copy.rs +++ b/tests/kani/CopyNonOverlapping/copy.rs @@ -24,13 +24,10 @@ fn copy_from_slice(src: &[u8], dst: &mut [u8]) { #[kani::proof] fn proof_harness() { - let mut data = Data { - t: Type::Apple, - array: [0; 8], - }; + let mut data = Data { t: Type::Apple, array: [0; 8] }; let coin = kani::any(); let param = [0, 0, 0, 0]; let start = if coin { 4 } else { 0 }; - copy_from_slice(¶m, &mut data.array[start..start+4]); + copy_from_slice(¶m, &mut data.array[start..start + 4]); assert!(data.t == Type::Apple || data.t == Type::Banana); } diff --git a/tests/perf/vec/box_dyn/src/main.rs b/tests/perf/vec/box_dyn/src/main.rs index 43fb157fcb51..5ad0ddecc053 100644 --- a/tests/perf/vec/box_dyn/src/main.rs +++ b/tests/perf/vec/box_dyn/src/main.rs @@ -4,7 +4,7 @@ //! This test checks the performance of pushing onto a vector of Box const N: usize = 4; -const M: usize = N+1; +const M: usize = N + 1; trait T { fn foo(&self) -> i32; diff --git a/tests/perf/vec/string/src/main.rs b/tests/perf/vec/string/src/main.rs index af606b253e85..89f4ba44c23a 100644 --- a/tests/perf/vec/string/src/main.rs +++ b/tests/perf/vec/string/src/main.rs @@ -6,7 +6,7 @@ const N: usize = 9; #[kani::proof] -#[kani::unwind(10))] +#[kani::unwind(10)] fn main() { let mut v: Vec = Vec::new(); for _i in 0..N { From bd7e78c76eff40d4de01cdf8fe83acdcfcdf85ed Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 28 Nov 2022 11:34:21 -0800 Subject: [PATCH 03/13] Add copyright to Cargo.toml --- tests/perf/vec/box_dyn/Cargo.toml | 3 +++ tests/perf/vec/string/Cargo.toml | 3 +++ 2 files changed, 6 insertions(+) diff --git a/tests/perf/vec/box_dyn/Cargo.toml b/tests/perf/vec/box_dyn/Cargo.toml index 9e2ea0c9c289..8c05707d4e79 100644 --- a/tests/perf/vec/box_dyn/Cargo.toml +++ b/tests/perf/vec/box_dyn/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "box_dyn" version = "0.1.0" diff --git a/tests/perf/vec/string/Cargo.toml b/tests/perf/vec/string/Cargo.toml index 9eed48f08007..b94ad94b428f 100644 --- a/tests/perf/vec/string/Cargo.toml +++ b/tests/perf/vec/string/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "string" version = "0.1.0" From 5cae8bc38c677340db930cc9396deb408c9285f9 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 28 Nov 2022 11:56:29 -0800 Subject: [PATCH 04/13] Reference GitHub issues and add performance information --- tests/perf/vec/box_dyn/src/main.rs | 5 ++++- tests/perf/vec/string/src/main.rs | 3 +++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/tests/perf/vec/box_dyn/src/main.rs b/tests/perf/vec/box_dyn/src/main.rs index 5ad0ddecc053..d0c0f7979fac 100644 --- a/tests/perf/vec/box_dyn/src/main.rs +++ b/tests/perf/vec/box_dyn/src/main.rs @@ -1,7 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This test checks the performance of pushing onto a vector of Box +//! This test checks the performance of pushing onto a vector of Box. +//! The test is from https://github.com/model-checking/kani/issues/1657. +//! Pre CBMC 5.71.0, it took 3 minutes and consumed more than 14 GB of memory. +//! With CBMC 5.71.0, it takes ~3 seconds and consumes ~150 MB of memory. const N: usize = 4; const M: usize = N + 1; diff --git a/tests/perf/vec/string/src/main.rs b/tests/perf/vec/string/src/main.rs index 89f4ba44c23a..1e982ae2987b 100644 --- a/tests/perf/vec/string/src/main.rs +++ b/tests/perf/vec/string/src/main.rs @@ -2,6 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This test checks the performance of pushing onto a vector of strings +//! The test is from https://github.com/model-checking/kani/issues/1673. +//! Pre CBMC 5.71.0, it took ~8.5 minutes and consumed ~27 GB of memory. +//! With CBMC 5.71.0, it takes ~70 seconds and consumes ~255 MB of memory. const N: usize = 9; From 00940c69e066e5d1d08a0e14bae3584e73caf40e Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 08:38:05 -0800 Subject: [PATCH 05/13] Bump version to 5.72 --- kani-dependencies | 2 +- scripts/kani-regression.sh | 2 +- tests/expected/loop-backedge/expected | 6 +- tests/expected/loop-backedge/see | 654 ++++++++++++++++++++++++++ 4 files changed, 657 insertions(+), 7 deletions(-) create mode 100644 tests/expected/loop-backedge/see diff --git a/kani-dependencies b/kani-dependencies index 72f93e32c684..49e3b94da9cc 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,3 +1,3 @@ -CBMC_VERSION="5.71.0" +CBMC_VERSION="5.72.0" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_VERSION="3.6" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 83f1af552e61..f9315cdde83d 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -22,7 +22,7 @@ KANI_DIR=$SCRIPT_DIR/.. export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true" # Required dependencies -check-cbmc-version.py --major 5 --minor 71 +check-cbmc-version.py --major 5 --minor 72 check-cbmc-viewer-version.py --major 3 --minor 5 # Formatting check diff --git a/tests/expected/loop-backedge/expected b/tests/expected/loop-backedge/expected index 21a488cd2644..34c886c358cb 100644 --- a/tests/expected/loop-backedge/expected +++ b/tests/expected/loop-backedge/expected @@ -1,5 +1 @@ -Status: SUCCESS\ -Description: "unwinding assertion loop 0" - -Status: SUCCESS\ -Description: "unwinding assertion loop 1" +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-backedge/see b/tests/expected/loop-backedge/see new file mode 100644 index 000000000000..44cfecdc308e --- /dev/null +++ b/tests/expected/loop-backedge/see @@ -0,0 +1,654 @@ +Checking harness check_unwind_assertion... +CBMC 5.72.0 (cbmc-5.72.0) +CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux +Reading GOTO program from file test.for-check_unwind_assertion.out +Generating GOTO Program +Adding CPROVER library (x86_64) +Removal of function pointers and virtual functions +Generic Property Instrumentation +Running with 16 object bits, 48 offset bits (user-specified) +Starting Bounded Model Checking +aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 +Unwinding loop test::check_unwind_assertion.0 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 +Unwinding loop test::check_unwind_assertion.1 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 +aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 +Unwinding loop test::check_unwind_assertion.0 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 +Unwinding loop test::check_unwind_assertion.1 iteration 2 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 +aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs line 38 column 15 function std::ptr::mut_ptr::::is_null thread 0 +aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 +Runtime Symex: 0.074707s +size of program expression: 2737 steps +slicing removed 1810 assignments +Generated 350 VCC(s), 76 remaining after simplification +Runtime Postprocess Equation: 0.000470442s +Passing problem to propositional reduction +converting SSA +Runtime Convert SSA: 0.00704614s +Running propositional reduction +Post-processing +Runtime Post-process: 5.37e-06s +Solving with MiniSAT 2.2.1 with simplifier +7849 variables, 11571 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00362767s +Runtime decision procedure: 0.010891s +Running propositional reduction +Solving with MiniSAT 2.2.1 with simplifier +7849 variables, 274 clauses +SAT checker: instance is UNSATISFIABLE +Runtime Solver: 0.00043837s +Runtime decision procedure: 0.000479132s + +RESULTS: +Check 1: std::ptr::write::.safety_check.1 + - Status: SUCCESS + - Description: "`src` must be properly aligned" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: + +Check 2: std::ptr::write::.safety_check.2 + - Status: SUCCESS + - Description: "`dst` must be properly aligned" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: + +Check 3: std::ptr::write::.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: + +Check 4: std::ptr::const_ptr::::is_null.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:39:15 in function std::ptr::const_ptr::::is_null + +Check 5: std::ptr::mut_ptr::::is_null.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:38:15 in function std::ptr::mut_ptr::::is_null + +Check 6: check_unwind_assertion.assertion.1 + - Status: SUCCESS + - Description: "assertion failed: e == 0" + - Location: test.rs:12:9 in function check_unwind_assertion + +Check 7: check_unwind_assertion.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: test.rs:11:15 in function check_unwind_assertion + +Check 8: check_unwind_assertion.assertion.2 + - Status: SUCCESS + - Description: "assertion failed: i == 0" + - Location: test.rs:14:13 in function check_unwind_assertion + +Check 9: check_unwind_assertion.unreachable.2 + - Status: SUCCESS + - Description: "unreachable code" + - Location: test.rs:13:18 in function check_unwind_assertion + +Check 10: core::num::::unchecked_add.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "attempt to compute unchecked_add which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/int_macros.rs:460:22 in function core::num::::unchecked_add + +Check 11: std::ptr::const_ptr::::offset.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "offset: attempt to compute number in bytes which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:456:18 in function std::ptr::const_ptr::::offset + +Check 12: std::ptr::const_ptr::::offset.arithmetic_overflow.2 + - Status: SUCCESS + - Description: "attempt to compute offset which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:456:18 in function std::ptr::const_ptr::::offset + +Check 13: std::slice::Iter::<'_, i32>::new.assume.1 + - Status: SUCCESS + - Description: "assumption failed" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:92:13 in function std::slice::Iter::<'_, i32>::new + +Check 14: std::ptr::mut_ptr::::offset.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "offset: attempt to compute number in bytes which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:470:18 in function std::ptr::mut_ptr::::offset + +Check 15: std::ptr::mut_ptr::::offset.arithmetic_overflow.2 + - Status: SUCCESS + - Description: "attempt to compute offset which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:470:18 in function std::ptr::mut_ptr::::offset + +Check 16: as std::iter::Iterator>::next.assume.1 + - Status: SUCCESS + - Description: "assumption failed" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:21 in function as std::iter::Iterator>::next + +Check 17: as std::iter::Iterator>::next.assume.2 + - Status: SUCCESS + - Description: "assumption failed" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:25 in function as std::iter::Iterator>::next + +Check 18: std::ptr::const_ptr::::wrapping_offset.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "arith_offset: attempt to compute number in bytes which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:538:18 in function std::ptr::const_ptr::::wrapping_offset + +Check 19: std::ptr::const_ptr::::wrapping_offset.arithmetic_overflow.2 + - Status: SUCCESS + - Description: "attempt to compute offset which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:538:18 in function std::ptr::const_ptr::::wrapping_offset + +Check 20: std::ptr::read::.safety_check.1 + - Status: SUCCESS + - Description: "`src` must be properly aligned" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: + +Check 21: std::ptr::read::.safety_check.2 + - Status: SUCCESS + - Description: "`dst` must be properly aligned" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: + +Check 22: std::ptr::read::.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: + +Check 23: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 24: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 25: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 26: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 27: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 28: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 29: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 30: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 31: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 32: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 33: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 34: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 35: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 36: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 37: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 38: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 39: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 40: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 41: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.19 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 42: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.20 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 43: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.21 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 44: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.22 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 45: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.23 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 46: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.24 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 47: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.25 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 48: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.26 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 49: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.27 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 50: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.28 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 51: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.29 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 52: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.30 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 53: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.31 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 54: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.32 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 55: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.33 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 56: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.34 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 57: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.35 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 58: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.36 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start + +Check 59: memcpy.pointer.1 + - Status: SUCCESS + - Description: "same object violation" + - Location: :33 in function memcpy + +Check 60: memcpy.pointer.2 + - Status: SUCCESS + - Description: "same object violation" + - Location: :34 in function memcpy + +Check 61: std::ptr::read::.precondition_instance.1 + - Status: SUCCESS + - Description: "memcpy src/dst overlap" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: + +Check 62: std::ptr::read::.precondition_instance.2 + - Status: SUCCESS + - Description: "memcpy source region readable" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: + +Check 63: std::ptr::read::.precondition_instance.3 + - Status: SUCCESS + - Description: "memcpy destination region writeable" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: + +Check 64: memcpy.pointer.3 + - Status: SUCCESS + - Description: "same object violation" + - Location: :33 in function memcpy + +Check 65: memcpy.pointer.4 + - Status: SUCCESS + - Description: "same object violation" + - Location: :34 in function memcpy + +Check 66: std::ptr::write::.precondition_instance.1 + - Status: SUCCESS + - Description: "memcpy src/dst overlap" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: + +Check 67: std::ptr::write::.precondition_instance.2 + - Status: SUCCESS + - Description: "memcpy source region readable" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: + +Check 68: std::ptr::write::.precondition_instance.3 + - Status: SUCCESS + - Description: "memcpy destination region writeable" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: + +Check 69: std::ptr::const_ptr::::is_null.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:39:15 in function std::ptr::const_ptr::::is_null + +Check 70: std::ptr::const_ptr::::guaranteed_eq.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:819:18 in function std::ptr::const_ptr::::guaranteed_eq + +Check 71: std::cmp::impls::::lt.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt + +Check 72: std::cmp::impls::::lt.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt + +Check 73: std::cmp::impls::::lt.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt + +Check 74: std::cmp::impls::::lt.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt + +Check 75: std::cmp::impls::::lt.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt + +Check 76: std::cmp::impls::::lt.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt + +Check 77: std::cmp::impls::::lt.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt + +Check 78: std::cmp::impls::::lt.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt + +Check 79: std::cmp::impls::::lt.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt + +Check 80: std::cmp::impls::::lt.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt + +Check 81: std::cmp::impls::::lt.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt + +Check 82: std::cmp::impls::::lt.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt + +Check 83: as std::iter::Iterator>::next.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next + +Check 84: as std::iter::Iterator>::next.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next + +Check 85: as std::iter::Iterator>::next.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next + +Check 86: as std::iter::Iterator>::next.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next + +Check 87: as std::iter::Iterator>::next.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next + +Check 88: as std::iter::Iterator>::next.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next + +Check 89: as std::iter::Iterator>::next.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next + +Check 90: as std::iter::Iterator>::next.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next + +Check 91: as std::iter::Iterator>::next.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next + +Check 92: as std::iter::Iterator>::next.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next + +Check 93: as std::iter::Iterator>::next.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next + +Check 94: as std::iter::Iterator>::next.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next + +Check 95: as std::iter::Iterator>::next.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next + +Check 96: as std::iter::Iterator>::next.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next + +Check 97: as std::iter::Iterator>::next.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next + +Check 98: as std::iter::Iterator>::next.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next + +Check 99: as std::iter::Iterator>::next.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next + +Check 100: as std::iter::Iterator>::next.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next + +Check 101: as std::iter::Iterator>::next.pointer_dereference.19 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next + +Check 102: as std::iter::Iterator>::next.pointer_dereference.20 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next + +Check 103: as std::iter::Iterator>::next.pointer_dereference.21 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next + +Check 104: as std::iter::Iterator>::next.pointer_dereference.22 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next + +Check 105: as std::iter::Iterator>::next.pointer_dereference.23 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next + +Check 106: as std::iter::Iterator>::next.pointer_dereference.24 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next + +Check 107: as std::iter::Iterator>::next.pointer_dereference.25 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:147:25 in function as std::iter::Iterator>::next + +Check 108: check_unwind_assertion.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: test.rs:11:15 in function check_unwind_assertion + +Check 109: check_unwind_assertion.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: test.rs:11:10 in function check_unwind_assertion + +Check 110: check_unwind_assertion.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: test.rs:11:10 in function check_unwind_assertion + +Check 111: check_unwind_assertion.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: test.rs:11:10 in function check_unwind_assertion + +Check 112: check_unwind_assertion.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: test.rs:11:10 in function check_unwind_assertion + +Check 113: check_unwind_assertion.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: test.rs:11:10 in function check_unwind_assertion + +Check 114: check_unwind_assertion.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: test.rs:11:10 in function check_unwind_assertion + +Check 115: std::clone::impls::::clone.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone + +Check 116: std::clone::impls::::clone.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone + +Check 117: std::clone::impls::::clone.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone + +Check 118: std::clone::impls::::clone.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone + +Check 119: std::clone::impls::::clone.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone + +Check 120: std::clone::impls::::clone.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone + +Check 121: std::ptr::mut_ptr::::is_null.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:38:15 in function std::ptr::mut_ptr::::is_null + + +SUMMARY: + ** 0 of 121 failed + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.178895s + From a3fb14c8dc7cd78f5885558b0329ec3bacae9aad Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 09:43:59 -0800 Subject: [PATCH 06/13] Add test for #705 --- tests/expected/loop-backedge/see | 654 --------------------- tests/perf/btreeset/insert_any/Cargo.toml | 11 + tests/perf/btreeset/insert_any/expected | 1 + tests/perf/btreeset/insert_any/src/main.rs | 16 + 4 files changed, 28 insertions(+), 654 deletions(-) delete mode 100644 tests/expected/loop-backedge/see 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 diff --git a/tests/expected/loop-backedge/see b/tests/expected/loop-backedge/see deleted file mode 100644 index 44cfecdc308e..000000000000 --- a/tests/expected/loop-backedge/see +++ /dev/null @@ -1,654 +0,0 @@ -Checking harness check_unwind_assertion... -CBMC 5.72.0 (cbmc-5.72.0) -CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux -Reading GOTO program from file test.for-check_unwind_assertion.out -Generating GOTO Program -Adding CPROVER library (x86_64) -Removal of function pointers and virtual functions -Generic Property Instrumentation -Running with 16 object bits, 48 offset bits (user-specified) -Starting Bounded Model Checking -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 -Unwinding loop test::check_unwind_assertion.0 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -Unwinding loop test::check_unwind_assertion.1 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 -Unwinding loop test::check_unwind_assertion.0 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -Unwinding loop test::check_unwind_assertion.1 iteration 2 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs line 38 column 15 function std::ptr::mut_ptr::::is_null thread 0 -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 -Runtime Symex: 0.074707s -size of program expression: 2737 steps -slicing removed 1810 assignments -Generated 350 VCC(s), 76 remaining after simplification -Runtime Postprocess Equation: 0.000470442s -Passing problem to propositional reduction -converting SSA -Runtime Convert SSA: 0.00704614s -Running propositional reduction -Post-processing -Runtime Post-process: 5.37e-06s -Solving with MiniSAT 2.2.1 with simplifier -7849 variables, 11571 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00362767s -Runtime decision procedure: 0.010891s -Running propositional reduction -Solving with MiniSAT 2.2.1 with simplifier -7849 variables, 274 clauses -SAT checker: instance is UNSATISFIABLE -Runtime Solver: 0.00043837s -Runtime decision procedure: 0.000479132s - -RESULTS: -Check 1: std::ptr::write::.safety_check.1 - - Status: SUCCESS - - Description: "`src` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 2: std::ptr::write::.safety_check.2 - - Status: SUCCESS - - Description: "`dst` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 3: std::ptr::write::.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 4: std::ptr::const_ptr::::is_null.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:39:15 in function std::ptr::const_ptr::::is_null - -Check 5: std::ptr::mut_ptr::::is_null.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:38:15 in function std::ptr::mut_ptr::::is_null - -Check 6: check_unwind_assertion.assertion.1 - - Status: SUCCESS - - Description: "assertion failed: e == 0" - - Location: test.rs:12:9 in function check_unwind_assertion - -Check 7: check_unwind_assertion.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: test.rs:11:15 in function check_unwind_assertion - -Check 8: check_unwind_assertion.assertion.2 - - Status: SUCCESS - - Description: "assertion failed: i == 0" - - Location: test.rs:14:13 in function check_unwind_assertion - -Check 9: check_unwind_assertion.unreachable.2 - - Status: SUCCESS - - Description: "unreachable code" - - Location: test.rs:13:18 in function check_unwind_assertion - -Check 10: core::num::::unchecked_add.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "attempt to compute unchecked_add which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/int_macros.rs:460:22 in function core::num::::unchecked_add - -Check 11: std::ptr::const_ptr::::offset.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "offset: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:456:18 in function std::ptr::const_ptr::::offset - -Check 12: std::ptr::const_ptr::::offset.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:456:18 in function std::ptr::const_ptr::::offset - -Check 13: std::slice::Iter::<'_, i32>::new.assume.1 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:92:13 in function std::slice::Iter::<'_, i32>::new - -Check 14: std::ptr::mut_ptr::::offset.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "offset: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:470:18 in function std::ptr::mut_ptr::::offset - -Check 15: std::ptr::mut_ptr::::offset.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:470:18 in function std::ptr::mut_ptr::::offset - -Check 16: as std::iter::Iterator>::next.assume.1 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:21 in function as std::iter::Iterator>::next - -Check 17: as std::iter::Iterator>::next.assume.2 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:25 in function as std::iter::Iterator>::next - -Check 18: std::ptr::const_ptr::::wrapping_offset.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "arith_offset: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:538:18 in function std::ptr::const_ptr::::wrapping_offset - -Check 19: std::ptr::const_ptr::::wrapping_offset.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:538:18 in function std::ptr::const_ptr::::wrapping_offset - -Check 20: std::ptr::read::.safety_check.1 - - Status: SUCCESS - - Description: "`src` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 21: std::ptr::read::.safety_check.2 - - Status: SUCCESS - - Description: "`dst` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 22: std::ptr::read::.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 23: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 24: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 25: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 26: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 27: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 28: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 29: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 30: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 31: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 32: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 33: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 34: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 35: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 36: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 37: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 38: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 39: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 40: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 41: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 42: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 43: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 44: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 45: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 46: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 47: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.25 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 48: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.26 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 49: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.27 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 50: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.28 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 51: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.29 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 52: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.30 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 53: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.31 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 54: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.32 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 55: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.33 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 56: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.34 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 57: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.35 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 58: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.36 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 59: memcpy.pointer.1 - - Status: SUCCESS - - Description: "same object violation" - - Location: :33 in function memcpy - -Check 60: memcpy.pointer.2 - - Status: SUCCESS - - Description: "same object violation" - - Location: :34 in function memcpy - -Check 61: std::ptr::read::.precondition_instance.1 - - Status: SUCCESS - - Description: "memcpy src/dst overlap" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 62: std::ptr::read::.precondition_instance.2 - - Status: SUCCESS - - Description: "memcpy source region readable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 63: std::ptr::read::.precondition_instance.3 - - Status: SUCCESS - - Description: "memcpy destination region writeable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 64: memcpy.pointer.3 - - Status: SUCCESS - - Description: "same object violation" - - Location: :33 in function memcpy - -Check 65: memcpy.pointer.4 - - Status: SUCCESS - - Description: "same object violation" - - Location: :34 in function memcpy - -Check 66: std::ptr::write::.precondition_instance.1 - - Status: SUCCESS - - Description: "memcpy src/dst overlap" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 67: std::ptr::write::.precondition_instance.2 - - Status: SUCCESS - - Description: "memcpy source region readable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 68: std::ptr::write::.precondition_instance.3 - - Status: SUCCESS - - Description: "memcpy destination region writeable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 69: std::ptr::const_ptr::::is_null.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:39:15 in function std::ptr::const_ptr::::is_null - -Check 70: std::ptr::const_ptr::::guaranteed_eq.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:819:18 in function std::ptr::const_ptr::::guaranteed_eq - -Check 71: std::cmp::impls::::lt.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 72: std::cmp::impls::::lt.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 73: std::cmp::impls::::lt.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 74: std::cmp::impls::::lt.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 75: std::cmp::impls::::lt.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 76: std::cmp::impls::::lt.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 77: std::cmp::impls::::lt.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 78: std::cmp::impls::::lt.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 79: std::cmp::impls::::lt.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 80: std::cmp::impls::::lt.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 81: std::cmp::impls::::lt.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 82: std::cmp::impls::::lt.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 83: as std::iter::Iterator>::next.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 84: as std::iter::Iterator>::next.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 85: as std::iter::Iterator>::next.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 86: as std::iter::Iterator>::next.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 87: as std::iter::Iterator>::next.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 88: as std::iter::Iterator>::next.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 89: as std::iter::Iterator>::next.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 90: as std::iter::Iterator>::next.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 91: as std::iter::Iterator>::next.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 92: as std::iter::Iterator>::next.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 93: as std::iter::Iterator>::next.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 94: as std::iter::Iterator>::next.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 95: as std::iter::Iterator>::next.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 96: as std::iter::Iterator>::next.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 97: as std::iter::Iterator>::next.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 98: as std::iter::Iterator>::next.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 99: as std::iter::Iterator>::next.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 100: as std::iter::Iterator>::next.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 101: as std::iter::Iterator>::next.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 102: as std::iter::Iterator>::next.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 103: as std::iter::Iterator>::next.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 104: as std::iter::Iterator>::next.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 105: as std::iter::Iterator>::next.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 106: as std::iter::Iterator>::next.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 107: as std::iter::Iterator>::next.pointer_dereference.25 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:147:25 in function as std::iter::Iterator>::next - -Check 108: check_unwind_assertion.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: test.rs:11:15 in function check_unwind_assertion - -Check 109: check_unwind_assertion.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 110: check_unwind_assertion.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 111: check_unwind_assertion.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 112: check_unwind_assertion.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 113: check_unwind_assertion.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 114: check_unwind_assertion.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 115: std::clone::impls::::clone.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 116: std::clone::impls::::clone.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 117: std::clone::impls::::clone.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 118: std::clone::impls::::clone.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 119: std::clone::impls::::clone.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 120: std::clone::impls::::clone.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 121: std::ptr::mut_ptr::::is_null.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:38:15 in function std::ptr::mut_ptr::::is_null - - -SUMMARY: - ** 0 of 121 failed - -VERIFICATION:- SUCCESSFUL -Verification Time: 0.178895s - diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml new file mode 100644 index 000000000000..41fa0a2db3ba --- /dev/null +++ b/tests/perf/btreeset/insert_any/Cargo.toml @@ -0,0 +1,11 @@ +# 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] 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..198970037b36 --- /dev/null +++ b/tests/perf/btreeset/insert_any/src/main.rs @@ -0,0 +1,16 @@ +// 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(); + set.insert(kani::any()); +} From 06e05643e2a9e52cbbaab78af9827c9e3596da8f Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 10:33:00 -0800 Subject: [PATCH 07/13] Add test for #1226 --- tests/perf/vec/vec/Cargo.toml | 11 +++++++++++ tests/perf/vec/vec/expected | 4 ++++ tests/perf/vec/vec/src/main.rs | 16 ++++++++++++++++ 3 files changed, 31 insertions(+) create mode 100644 tests/perf/vec/vec/Cargo.toml create mode 100644 tests/perf/vec/vec/expected create mode 100644 tests/perf/vec/vec/src/main.rs diff --git a/tests/perf/vec/vec/Cargo.toml b/tests/perf/vec/vec/Cargo.toml new file mode 100644 index 000000000000..77e60e006a35 --- /dev/null +++ b/tests/perf/vec/vec/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "vec" +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/vec/vec/expected b/tests/perf/vec/vec/expected new file mode 100644 index 000000000000..1ccbba770b35 --- /dev/null +++ b/tests/perf/vec/vec/expected @@ -0,0 +1,4 @@ +Status: SUCCESS\ +Description: "assertion failed: v2 == vec![1]" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/vec/vec/src/main.rs b/tests/perf/vec/vec/src/main.rs new file mode 100644 index 000000000000..c3feaa48b6d6 --- /dev/null +++ b/tests/perf/vec/vec/src/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of 2d-vectors +//! The test is from https://github.com/model-checking/kani/issues/1226. +//! Pre CBMC 5.72.0, it ran out of memory. +//! With CBMC 5.72.0, it takes ~2 seconds and consumes a few hundred MB of memory. + +#[kani::proof] +#[kani::unwind(5)] +fn main() { + let v1: Vec> = vec![vec![1], vec![]]; + + let v2: Vec = v1.into_iter().flatten().collect(); + assert_eq!(v2, vec![1]); +} From b504445a71210b22cecd7f1be42fd7461317958d Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 11:34:28 -0800 Subject: [PATCH 08/13] Add test for #1823 --- tests/perf/misc/array_fold/Cargo.toml | 11 +++++++++ tests/perf/misc/array_fold/expected | 1 + tests/perf/misc/array_fold/src/main.rs | 34 ++++++++++++++++++++++++++ 3 files changed, 46 insertions(+) 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 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..62eeba9864db --- /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() {} From ba61ab9d203f79cc48632ee87b49f1fac1bffa7d Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 11:35:36 -0800 Subject: [PATCH 09/13] Add an unwind annotation --- tests/cargo-kani/mir-linker/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs index a1514d454828..f33a61399564 100644 --- a/tests/cargo-kani/mir-linker/src/lib.rs +++ b/tests/cargo-kani/mir-linker/src/lib.rs @@ -5,6 +5,7 @@ use semver::{BuildMetadata, Prerelease, Version}; #[kani::proof] +#[kani::unwind(2)] fn check_version() { let next_major: u64 = kani::any(); let next_minor: u64 = kani::any(); From b67defb2e815707fc22c44446aa511b9c0d18787 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 11:46:50 -0800 Subject: [PATCH 10/13] Add test for #1958 --- tests/perf/misc/struct_defs/Cargo.toml | 11 +++++ tests/perf/misc/struct_defs/expected | 1 + tests/perf/misc/struct_defs/src/main.rs | 64 +++++++++++++++++++++++++ 3 files changed, 76 insertions(+) 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 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..3a0824122498 --- /dev/null +++ b/tests/perf/misc/struct_defs/src/main.rs @@ -0,0 +1,64 @@ +// 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 + +enum Expr { + A, + B(Box), + C(Box, Box), + D(Box, Box, Box), + E(Box, Box, Box, Box), +} + +enum Result { + Ok(S), + Err(T), +} + +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 _: Result = Result::Ok(Expr::A); +} + +// Takes >10s +#[cfg_attr(kani, kani::proof, kani::unwind(2))] +fn slow_harness2() { + let _: Result = Result::Ok(Expr::A); +} + +// Takes ~1s +#[cfg_attr(kani, kani::proof, kani::unwind(2))] +fn fast_harness() { + let _: Result = Result::Ok(Expr::A); + //let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); + //let _: Result = Result::Ok(Expr::A); + let _: Result = Result::Ok(Expr::A); +} + +fn main() {} From 5c58885da82f5e62997966f4e55411459a414d96 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 8 Dec 2022 13:58:41 -0800 Subject: [PATCH 11/13] Reference issue to investigate why an unwind annotation is now needed --- tests/cargo-kani/mir-linker/src/lib.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs index f33a61399564..bfad87b9e568 100644 --- a/tests/cargo-kani/mir-linker/src/lib.rs +++ b/tests/cargo-kani/mir-linker/src/lib.rs @@ -4,6 +4,10 @@ //! Dummy test to check --mir-linker runs on a cargo project. use semver::{BuildMetadata, Prerelease, Version}; +// Pre-CBMC 5.72.0, this test did not require an unwinding. +// TODO: figure out why it needs one now: +// https://github.com/model-checking/kani/issues/1978 + #[kani::proof] #[kani::unwind(2)] fn check_version() { From 2aebf1ba515ee70364c99dbb5cad0fe080bfac56 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 9 Dec 2022 09:01:59 -0800 Subject: [PATCH 12/13] Fix fmt --- tests/perf/misc/array_fold/src/main.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/perf/misc/array_fold/src/main.rs b/tests/perf/misc/array_fold/src/main.rs index 62eeba9864db..d7953255612b 100644 --- a/tests/perf/misc/array_fold/src/main.rs +++ b/tests/perf/misc/array_fold/src/main.rs @@ -7,14 +7,14 @@ //! 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 { +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; +pub fn array_sum_for(x: [usize; 100]) -> usize { + let mut accumulator: usize = 0; for i in 0..100 { - accumulator = x[i] + accumulator + accumulator = x[i] + accumulator } accumulator } From 895e4bb80cadbaf4c9fedebd08df85d4d4ffb97b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 9 Dec 2022 12:00:12 -0800 Subject: [PATCH 13/13] Add asserts --- tests/kani/CopyNonOverlapping/copy.rs | 2 +- tests/perf/btreeset/insert_any/src/main.rs | 4 +- tests/perf/misc/struct_defs/src/main.rs | 48 ++++++++++++++++------ tests/perf/vec/box_dyn/src/main.rs | 3 +- 4 files changed, 42 insertions(+), 15 deletions(-) diff --git a/tests/kani/CopyNonOverlapping/copy.rs b/tests/kani/CopyNonOverlapping/copy.rs index 87af5dd6bc15..a0e53eef2eb7 100644 --- a/tests/kani/CopyNonOverlapping/copy.rs +++ b/tests/kani/CopyNonOverlapping/copy.rs @@ -29,5 +29,5 @@ fn proof_harness() { let param = [0, 0, 0, 0]; let start = if coin { 4 } else { 0 }; copy_from_slice(¶m, &mut data.array[start..start + 4]); - assert!(data.t == Type::Apple || data.t == Type::Banana); + assert!(data.t == Type::Apple); } diff --git a/tests/perf/btreeset/insert_any/src/main.rs b/tests/perf/btreeset/insert_any/src/main.rs index 198970037b36..cf9df6551ae4 100644 --- a/tests/perf/btreeset/insert_any/src/main.rs +++ b/tests/perf/btreeset/insert_any/src/main.rs @@ -12,5 +12,7 @@ use std::collections::BTreeSet; #[kani::unwind(3)] fn main() { let mut set = BTreeSet::::new(); - set.insert(kani::any()); + let x = kani::any(); + set.insert(x); + assert!(set.contains(&x)); } diff --git a/tests/perf/misc/struct_defs/src/main.rs b/tests/perf/misc/struct_defs/src/main.rs index 3a0824122498..bba599888b77 100644 --- a/tests/perf/misc/struct_defs/src/main.rs +++ b/tests/perf/misc/struct_defs/src/main.rs @@ -5,6 +5,7 @@ //! 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), @@ -13,11 +14,22 @@ enum Expr { 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), @@ -37,28 +49,40 @@ type Err10<'a> = Err, &'a str, String>; // Takes >10s #[cfg_attr(kani, kani::proof, kani::unwind(2))] fn slow_harness1() { - let _: Result = Result::Ok(Expr::A); + 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 _: Result = Result::Ok(Expr::A); + 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 _: Result = Result::Ok(Expr::A); - //let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(Expr::A); - //let _: Result = Result::Ok(Expr::A); - let _: Result = Result::Ok(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); + let x: Result = Result::Ok(Expr::A); + assert_eq!(x.unwrap(), &Expr::A); } fn main() {} diff --git a/tests/perf/vec/box_dyn/src/main.rs b/tests/perf/vec/box_dyn/src/main.rs index d0c0f7979fac..f6c6299e80d5 100644 --- a/tests/perf/vec/box_dyn/src/main.rs +++ b/tests/perf/vec/box_dyn/src/main.rs @@ -37,7 +37,7 @@ impl T for B { #[kani::unwind(6)] fn main() { let mut a: Vec> = Vec::new(); - a.push(Box::new(A { x: 5 })); + a.push(Box::new(A { x: 9 })); for i in 1..N { a.push(Box::new(B { x: 9 })); } @@ -48,4 +48,5 @@ fn main() { let x = a[index].as_mut().foo(); val += x; } + assert_eq!(val as usize, 9 * M); }