Update CBMC dependency to 6.10.0 (#4619)

Upgrading to 6.9.0 requires changes as described below. Upgrading from
6.9.0 to 6.10.0 does not require any further changes.

Changes in CBMC's set of static objects require retuning shadow-memory
object-count test: The `unsupported_num_objects` test depends on CBMC's
internal object-ID numbering: it creates N objects and expects the
(N+k)-th object's ID to cross Kani's 1024-object shadow-memory limit.
Newer CBMC allocates one fewer auxiliary object, so the previous N
values (1019 pass / 1020 fail) no longer straddle the limit -- the fail
harness verified successfully instead of failing.

Bump the thresholds by one (1020 pass / 1021 fail) to restore the
boundary, update the explanatory comment, and note that these counts are
sensitive to CBMC's object numbering and may need adjusting on future
CBMC upgrades.

CBMC 6.10 makes the `slow` harness's Display/`to_string` formatting path
far more memory-heavy: the original `"foo"`/unwind(6) version peaks at
~26 GB with Kani's default Cadical solver and deterministically
OOM-kills the 16 GB GitHub-hosted `perf` runner ("runner has received a
shutdown signal"). No solver is both under 16 GB and fast enough
(minisat2/kissat stay ~8 GB but do not finish in >15 min), so the
harness itself must shrink.

Use an empty payload (formatted result `"A."`) and unwind(3) -- the
smallest bound that still fully unrolls the formatting loops. This keeps
peak memory to ~11 GB while still exercising the trait/formatting path
the test guards. Both harnesses verify successfully.

Resolves: #4605
Resolves: #4617

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

kani-dependencies

@@ -1,5 +1,5 @@
 CBMC_MAJOR="6"
-CBMC_MINOR="8"
-CBMC_VERSION="6.8.0"
+CBMC_MINOR="10"
+CBMC_VERSION="6.10.0"
 
 KISSAT_VERSION="4.0.1"

tests/expected/shadow/unsupported_num_objects/test.rs

@@ -9,11 +9,14 @@ static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(fals
 
 fn check_max_objects<const N: usize>() {
     let mut i = 0;
-    // A dummy loop that creates `N`` objects.
-    // After the loop, CBMC's object ID counter should be at `N` + 3:
+    // A dummy loop that creates `N` objects.
+    // After the loop, CBMC's object ID counter should be at `N` + 2:
     // - `N` created in the loop +
     // - the NULL pointer whose object ID is 0, and
     // - objects for i, have_42
+    // Note: the exact object count depends on CBMC's internal object
+    // numbering, so the `N` thresholds below may need to be adjusted when
+    // upgrading CBMC.
     let mut have_42 = false;
     while i < N {
         let x: Box<usize> = Box::new(kani::any());
@@ -23,7 +26,7 @@ fn check_max_objects<const N: usize>() {
         i += 1;
     }
 
-    // create a new object whose ID is `N` + 4
+    // create a new object whose ID is `N` + 3
     let x: i32 = have_42 as i32;
     assert_eq!(x, have_42 as i32);
     // the following call to `set` would fail if the object ID for `x` exceeds
@@ -35,10 +38,10 @@ fn check_max_objects<const N: usize>() {
 
 #[kani::proof]
 fn check_max_objects_pass() {
-    check_max_objects::<1019>();
+    check_max_objects::<1020>();
 }
 
 #[kani::proof]
 fn check_max_objects_fail() {
-    check_max_objects::<1020>();
+    check_max_objects::<1021>();
 }

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

@@ -4,6 +4,14 @@
 //! This test checks the performance when adding in the Display trait.
 //! The test is from https://github.com/model-checking/kani/issues/1996
 //! With CBMC 5.79.0, all harnesses take ~3 seconds
+//!
+//! The input string and `kani::unwind` bound are deliberately minimal. The
+//! `slow` harness exercises the `Display`/`to_string` formatting path, whose
+//! SAT encoding is memory-heavy on newer CBMC: the original `"foo"`/unwind(6)
+//! version peaked at ~26 GB on CBMC 6.10 and OOM-killed the 16 GB `perf`
+//! runner. An empty payload (formatted result `"A."`) with the smallest unwind
+//! that still fully unrolls the formatting loops keeps peak memory to ~11 GB
+//! while still covering the trait/formatting path this test is meant to guard.
 use std::fmt::Display;
 
 enum Foo {
@@ -23,20 +31,20 @@ impl Display for Foo {
 }
 
 #[kani::proof]
-#[kani::unwind(6)]
+#[kani::unwind(3)]
 fn fast() {
-    let a = Foo::A(String::from("foo"));
+    let a = Foo::A(String::from(""));
     let s = match a {
         Foo::A(s) => format!("A.{s}"),
         Foo::B(s) => format!("B.{s}"),
     };
-    assert_eq!(s, "A.foo");
+    assert_eq!(s, "A.");
 }
 
 #[kani::proof]
-#[kani::unwind(6)]
+#[kani::unwind(3)]
 fn slow() {
-    let a = Foo::A(String::from("foo"));
+    let a = Foo::A(String::from(""));
     let s = a.to_string();
-    assert_eq!(s, "A.foo");
+    assert_eq!(s, "A.");
 }