Update CBMC version to 5.79.0

- Re-enable tests that had to be disabled with the toolchain upgrade in
  model-checking#2149. Fixes model-checking#2286, fixes model-checking#2191.
- Do not generate non-NULL pointer constants. Together with the CBMC
  version update this avoids the need for an unwinding annotation in the
  mir-linker test. Fixes model-checking#1978.
- CBMC 5.79.0 ships simplifier improvements that enable constant
  propagation to avoid slow-down with the Display trait. Fixes model-checking#1996.
- CBMC 5.79.0 ships SMT back-end fixes. Fixes model-checking#2002.

Co-authored-by: Zyad Hassan <[email protected]>

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