Merge branch 'main' into unify-intrinsics

model-checking · Aug 9, 2024 · 8d0d9f3 · 8d0d9f3
2 parents 807e606 + bec5fd1
commit 8d0d9f3
Show file tree

Hide file tree

Showing 14 changed files with 137 additions and 23 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,46 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.54.0]
+
+### Major Changes
+* We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts.
+* We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros.
+* We enabled support for concrete playback for harness that contains stubs or function contracts.
+* We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.
+
+### Breaking Changes
+* The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.
+
+## What's Changed
+* Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332
+* Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323
+* Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295
+* Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344
+* Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348
+* Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283
+* Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305
+* Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373
+* Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995
+* Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270
+* Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389
+* Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120
+* Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363
+* Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001
+* Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999
+* Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002
+* Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000
+* Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417
+* Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374
+* Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333
+* Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426
+* Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri
+
+## New Contributors
+* @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0
+
 ## [0.53.0]
 
 ### Major Changes

diff --git a/Cargo.lock b/Cargo.lock
@@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -234,7 +234,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -432,15 +432,15 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "kani_core",
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -461,7 +461,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -489,7 +489,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "anyhow",
  "home",
@@ -498,14 +498,14 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -515,7 +515,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -1034,7 +1034,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "kani",
 ]

diff --git a/Cargo.toml b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"

diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"

diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_core"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
@@ -5,7 +5,7 @@
 # Note: this package is intentionally named std to make sure the names of
 # standard library symbols are preserved
 name = "std"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh
@@ -21,10 +21,83 @@ git clone \
 
 pushd "${WORK_DIR}"
 
-mkdir build
-git submodule update --init
+# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is
+# properly fixed in CBMC
+cat > varargs.patch << "EOF"
+--- a/src/ansi-c/library/stdio.c
++++ b/src/ansi-c/library/stdio.c
+@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
 
-cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+-        __CPROVER_OBJECT_SIZE(arg))
++        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+   {
+     void *a = va_arg(arg, void *);
+     __CPROVER_havoc_object(a);
+@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf(
+
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+-        __CPROVER_OBJECT_SIZE(args))
++        __CPROVER_OBJECT_SIZE(*(void **)&args))
+   {
+     void *a = va_arg(args, void *);
+     __CPROVER_havoc_object(a);
+@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
+   (void)*s;
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+-        __CPROVER_OBJECT_SIZE(arg))
++        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+   {
+     void *a = va_arg(arg, void *);
+     __CPROVER_havoc_object(a);
+@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf(
+   (void)*s;
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+-        __CPROVER_OBJECT_SIZE(args))
++        __CPROVER_OBJECT_SIZE(*(void **)&args))
+   {
+     void *a = va_arg(args, void *);
+     __CPROVER_havoc_object(a);
+@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
+   (void)*fmt;
+
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+-        __CPROVER_OBJECT_SIZE(ap))
++        __CPROVER_OBJECT_SIZE(*(void **)&ap))
+
+   {
+     (void)va_arg(ap, int);
+     __CPROVER_precondition(
+-      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
++      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
+       "vsnprintf object overlap");
+   }
+
+@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk(
+   (void)*fmt;
+
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+-        __CPROVER_OBJECT_SIZE(ap))
++        __CPROVER_OBJECT_SIZE(*(void **)&ap))
+
+   {
+     (void)va_arg(ap, int);
+     __CPROVER_precondition(
+-      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
++      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
+       "vsnprintf object overlap");
+   }
+
+EOF
+
+cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
+  -DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \
+  -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
+  -DCMAKE_CXX_FLAGS=-Wno-error=register
 cmake3 --build build -- -j$(nproc)
 sudo make -C build install
 

diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh
@@ -11,6 +11,7 @@ set -eu
 DEPS=(
   cmake
   cmake3
+  gcc10-c++
   git
   openssl-devel
   python3-pip

diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"