Update CBMC version to 5.79.0 (model-checking#2301)

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -284,7 +284,8 @@ impl<'tcx> GotocCtx<'tcx> {
  unreachable!("ZST is no longer represented as a scalar")
  }
  (Scalar::Int(_), ty::RawPtr(tm)) => {
- Expr::pointer_constant(s.to_u64().unwrap(), self.codegen_ty(tm.ty).to_pointer())
+ Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64))
+ .cast_to(self.codegen_ty(tm.ty).to_pointer())
  }
  // TODO: Removing this doesn't cause any regressions to fail.
  // We need a regression for this case.

kani-dependencies

@@ -1,4 +1,4 @@
-CBMC_VERSION="5.78.0"
+CBMC_VERSION="5.79.0"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"
 KISSAT_VERSION="3.0.0"

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 78
+check-cbmc-version.py --major 5 --minor 79
 check-cbmc-viewer-version.py --major 3 --minor 8
 check_kissat_version.sh
 

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

@@ -4,12 +4,7 @@
 //! 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/perf/misc/display_trait/Cargo.toml

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

tests/perf/misc/display_trait/expected

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

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

@@ -0,0 +1,42 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance when adding in the Display trait.
+//! The test is from https://github.com/model-checking/kani/issues/1996
+//! With CBMC 5.79.0, all harnesses take ~3 seconds
+use std::fmt::Display;
+
+enum Foo {
+ A(String),
+ B(String),
+}
+
+impl Display for Foo {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ let s = match self {
+ Foo::A(s) => format!("A.{s}"),
+ Foo::B(s) => format!("B.{s}"),
+ };
+ write!(f, "{s}")?;
+ Ok(())
+ }
+}
+
+#[kani::proof]
+#[kani::unwind(6)]
+fn fast() {
+ let a = Foo::A(String::from("foo"));
+ let s = match a {
+ Foo::A(s) => format!("A.{s}"),
+ Foo::B(s) => format!("B.{s}"),
+ };
+ assert_eq!(s, "A.foo");
+}
+
+#[kani::proof]
+#[kani::unwind(6)]
+fn slow() {
+ let a = Foo::A(String::from("foo"));
+ let s = a.to_string();
+ assert_eq!(s, "A.foo");
+}