From 07ba909ab045981d4dceb50400b4b4b8cd827f80 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Mar 2023 15:19:50 +0000 Subject: [PATCH] Update CBMC version to 5.79.0 - Re-enable tests that had to be disabled with the toolchain upgrade in #2149. Fixes #2286, fixes #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 #1978. - CBMC 5.79.0 ships simplifier improvements that enable constant propagation to avoid slow-down with the Display trait. Fixes #1996. - CBMC 5.79.0 ships SMT back-end fixes. Fixes #2002. Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .../codegen_cprover_gotoc/codegen/operand.rs | 3 +- kani-dependencies | 2 +- scripts/kani-regression.sh | 2 +- tests/cargo-kani/mir-linker/src/lib.rs | 5 --- .../Cargo.toml | 0 .../expected | 0 .../src/main.rs | 0 tests/perf/misc/display_trait/Cargo.toml | 11 +++++ tests/perf/misc/display_trait/expected | 1 + tests/perf/misc/display_trait/src/main.rs | 42 +++++++++++++++++++ .../vec/{ignore_string => string}/Cargo.toml | 0 .../box_dyn/Cargo.toml | 0 .../box_dyn/expected | 0 .../box_dyn/src/main.rs | 0 .../vec/{ignore_string => string}/expected | 0 .../vec/{ignore_string => string}/src/main.rs | 0 16 files changed, 58 insertions(+), 8 deletions(-) rename tests/perf/btreeset/{ignore_insert_same => insert_same}/Cargo.toml (100%) rename tests/perf/btreeset/{ignore_insert_same => insert_same}/expected (100%) rename tests/perf/btreeset/{ignore_insert_same => insert_same}/src/main.rs (100%) create mode 100644 tests/perf/misc/display_trait/Cargo.toml create mode 100644 tests/perf/misc/display_trait/expected create mode 100644 tests/perf/misc/display_trait/src/main.rs rename tests/perf/vec/{ignore_string => string}/Cargo.toml (100%) rename tests/perf/vec/{ignore_string => string}/box_dyn/Cargo.toml (100%) rename tests/perf/vec/{ignore_string => string}/box_dyn/expected (100%) rename tests/perf/vec/{ignore_string => string}/box_dyn/src/main.rs (100%) rename tests/perf/vec/{ignore_string => string}/expected (100%) rename tests/perf/vec/{ignore_string => string}/src/main.rs (100%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 5bb66a7dff76..417cf04baf5f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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. diff --git a/kani-dependencies b/kani-dependencies index e78a9da0bfbc..29a51b486a21 100644 --- a/kani-dependencies +++ b/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" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index fa09f0628aae..0331f2cbf2cb 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 78 +check-cbmc-version.py --major 5 --minor 79 check-cbmc-viewer-version.py --major 3 --minor 8 check_kissat_version.sh diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs index bfad87b9e568..a1514d454828 100644 --- a/tests/cargo-kani/mir-linker/src/lib.rs +++ b/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(); diff --git a/tests/perf/btreeset/ignore_insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml similarity index 100% rename from tests/perf/btreeset/ignore_insert_same/Cargo.toml rename to tests/perf/btreeset/insert_same/Cargo.toml diff --git a/tests/perf/btreeset/ignore_insert_same/expected b/tests/perf/btreeset/insert_same/expected similarity index 100% rename from tests/perf/btreeset/ignore_insert_same/expected rename to tests/perf/btreeset/insert_same/expected diff --git a/tests/perf/btreeset/ignore_insert_same/src/main.rs b/tests/perf/btreeset/insert_same/src/main.rs similarity index 100% rename from tests/perf/btreeset/ignore_insert_same/src/main.rs rename to tests/perf/btreeset/insert_same/src/main.rs diff --git a/tests/perf/misc/display_trait/Cargo.toml b/tests/perf/misc/display_trait/Cargo.toml new file mode 100644 index 000000000000..ce31328c8834 --- /dev/null +++ b/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] diff --git a/tests/perf/misc/display_trait/expected b/tests/perf/misc/display_trait/expected new file mode 100644 index 000000000000..4426ff6c02cd --- /dev/null +++ b/tests/perf/misc/display_trait/expected @@ -0,0 +1 @@ +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/perf/misc/display_trait/src/main.rs b/tests/perf/misc/display_trait/src/main.rs new file mode 100644 index 000000000000..f2f3b91e3344 --- /dev/null +++ b/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"); +} diff --git a/tests/perf/vec/ignore_string/Cargo.toml b/tests/perf/vec/string/Cargo.toml similarity index 100% rename from tests/perf/vec/ignore_string/Cargo.toml rename to tests/perf/vec/string/Cargo.toml diff --git a/tests/perf/vec/ignore_string/box_dyn/Cargo.toml b/tests/perf/vec/string/box_dyn/Cargo.toml similarity index 100% rename from tests/perf/vec/ignore_string/box_dyn/Cargo.toml rename to tests/perf/vec/string/box_dyn/Cargo.toml diff --git a/tests/perf/vec/ignore_string/box_dyn/expected b/tests/perf/vec/string/box_dyn/expected similarity index 100% rename from tests/perf/vec/ignore_string/box_dyn/expected rename to tests/perf/vec/string/box_dyn/expected diff --git a/tests/perf/vec/ignore_string/box_dyn/src/main.rs b/tests/perf/vec/string/box_dyn/src/main.rs similarity index 100% rename from tests/perf/vec/ignore_string/box_dyn/src/main.rs rename to tests/perf/vec/string/box_dyn/src/main.rs diff --git a/tests/perf/vec/ignore_string/expected b/tests/perf/vec/string/expected similarity index 100% rename from tests/perf/vec/ignore_string/expected rename to tests/perf/vec/string/expected diff --git a/tests/perf/vec/ignore_string/src/main.rs b/tests/perf/vec/string/src/main.rs similarity index 100% rename from tests/perf/vec/ignore_string/src/main.rs rename to tests/perf/vec/string/src/main.rs