Bump CBMC to version 5.72.0

kani-dependencies

@@ -1,3 +1,3 @@
-CBMC_VERSION="5.70.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"

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 72
 check-cbmc-viewer-version.py --major 3 --minor 5
 
 # Formatting check

tests/cargo-kani/mir-linker/src/lib.rs

@@ -4,7 +4,12 @@
 //! 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() {
     let next_major: u64 = kani::any();
     let next_minor: u64 = kani::any();

tests/expected/loop-backedge/expected

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

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);
+        }
+    }
+}

tests/kani/CopyNonOverlapping/copy.rs

@@ -0,0 +1,33 @@
+// 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(&param, &mut data.array[start..start + 4]);
+    assert!(data.t == Type::Apple);
+}

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]

tests/perf/btreeset/insert_any/expected

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

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

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

tests/perf/misc/array_fold/Cargo.toml

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

tests/perf/misc/array_fold/expected

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

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() {}

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]

tests/perf/misc/struct_defs/expected

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

tests/perf/misc/struct_defs/src/main.rs

@@ -0,0 +1,88 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance with different struct definitions
+//! The test is from https://github.com/model-checking/kani/issues/1958.
+//! With CBMC 5.72.0, all harnesses take ~1 second
+
+#[derive(PartialEq, Eq)]
+enum Expr {
+    A,
+    B(Box<Expr>),
+    C(Box<Expr>, Box<Expr>),
+    D(Box<Expr>, Box<Expr>, Box<Expr>),
+    E(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>),
+}
+
+#[derive(PartialEq, Eq)]
+enum Result<S, T> {
+    Ok(S),
+    Err(T),
+}
+
+impl<S, T> Result<S, T> {
+    fn unwrap(&self) -> &S {
+        let x = match self {
+            Result::Ok(x) => x,
+            Result::Err(_) => panic!(),
+        };
+        x
+    }
+}
+
+enum Err<X, Y, Z> {
+    A(X),
+    B(Y, Z),
+}
+
+type Err1 = Err<String, String, String>;
+type Err2<'a> = Err<String, &'a str, String>;
+type Err3<'a> = Err<String, String, &'a str>;
+type Err4<'a> = Err<String, &'a str, &'a str>;
+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<Expr, &'a str, String>;
+type Err10<'a> = Err<Box<Expr>, &'a str, String>;
+
+// Takes >10s
+#[cfg_attr(kani, kani::proof, kani::unwind(2))]
+fn slow_harness1() {
+    let x: Result<Expr, Err2> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+}
+
+// Takes >10s
+#[cfg_attr(kani, kani::proof, kani::unwind(2))]
+fn slow_harness2() {
+    let x: Result<Expr, Err9> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+}
+
+// Takes ~1s
+#[cfg_attr(kani, kani::proof, kani::unwind(2))]
+fn fast_harness() {
+    let x: Result<Expr, Err1> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err2> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err3> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err4> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err5> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err6> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err7> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err8> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err9> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+    let x: Result<Expr, Err10> = Result::Ok(Expr::A);
+    assert_eq!(x.unwrap(), &Expr::A);
+}
+
+fn main() {}

tests/perf/vec/box_dyn/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[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]

tests/perf/vec/box_dyn/expected

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

tests/perf/vec/box_dyn/src/main.rs

@@ -0,0 +1,52 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of pushing onto a vector of Box<dyn _>.
+//! 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;
+
+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<Box<dyn T>> = Vec::new();
+    a.push(Box::new(A { x: 9 }));
+    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;
+    }
+    assert_eq!(val as usize, 9 * M);
+}

tests/perf/vec/string/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[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]

tests/perf/vec/string/expected

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

tests/perf/vec/string/src/main.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// 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;
+
+#[kani::proof]
+#[kani::unwind(10)]
+fn main() {
+    let mut v: Vec<String> = 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");
+}

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]

tests/perf/vec/vec/expected

@@ -0,0 +1,4 @@
+Status: SUCCESS\
+Description: "assertion failed: v2 == vec![1]"
+
+VERIFICATION:- SUCCESSFUL