Merge branch 'main' into modifies_fat

model-checking · Jul 8, 2024 · e5bf457 · e5bf457
2 parents 1fd0849 + fcc9d8b
commit e5bf457
Show file tree

Hide file tree

Showing 84 changed files with 2,826 additions and 136 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,44 @@ 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.53.0]
+
+### Major Changes
+* The `--visualize` option is being deprecated and will be removed in a future release. Consider using the `--concrete-playback` option instead.
+* The `-Z ptr-to-ref-cast-checks` option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
+* The `-Z uninit-checks` option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the `-Z ghost-state` option.
+
+### Breaking Changes
+* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278
+* Remove deprecated `--enable-stubbing` by @celinval in https://github.com/model-checking/kani/pull/3309
+
+### What's Changed
+
+* Change ensures into closures by @pi314mm in https://github.com/model-checking/kani/pull/3207
+* (Re)introduce `Invariant` trait by @adpaco-aws in https://github.com/model-checking/kani/pull/3190
+* Remove empty box creation from contracts impl by @celinval in https://github.com/model-checking/kani/pull/3233
+* Add a new verify-std subcommand to Kani by @celinval in https://github.com/model-checking/kani/pull/3231
+* Inject pointer validity check when casting raw pointers to references by @artemagvanian in https://github.com/model-checking/kani/pull/3221
+* Do not turn trivially diverging loops into assume(false) by @tautschnig in https://github.com/model-checking/kani/pull/3223
+* Fix "unused mut" warnings created by generated code. by @jsalzbergedu in https://github.com/model-checking/kani/pull/3247
+* Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in https://github.com/model-checking/kani/pull/3245
+* Use cfg=kani_host for host crates by @tautschnig in https://github.com/model-checking/kani/pull/3244
+* Add intrinsics and Arbitrary support for no_core by @jaisnan in https://github.com/model-checking/kani/pull/3230
+* Contracts: Avoid attribute duplication and `const` function generation for constant function by @celinval in https://github.com/model-checking/kani/pull/3255
+* Fix contract of constant fn with effect feature by @celinval in https://github.com/model-checking/kani/pull/3259
+* Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256
+* Add a `#[derive(Invariant)]` macro by @adpaco-aws in https://github.com/model-checking/kani/pull/3250
+* Contracts: History Expressions via "old" monad by @pi314mm in https://github.com/model-checking/kani/pull/3232
+* Function Contracts: remove instances of _renamed by @pi314mm in https://github.com/model-checking/kani/pull/3274
+* Deprecate `--visualize` in favor of concrete playback by @celinval in https://github.com/model-checking/kani/pull/3281
+* Fix operand in fat pointer comparison by @pi314mm in https://github.com/model-checking/kani/pull/3297
+* Function Contracts: Closure Type Inference by @pi314mm in https://github.com/model-checking/kani/pull/3307
+* Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in https://github.com/model-checking/kani/pull/3306
+* Towards Proving Memory Initialization by @artemagvanian in https://github.com/model-checking/kani/pull/3264
+* Rust toolchain upgraded to `nightly-2024-07-01` by @tautschnig @celinval @jaisnan @adpaco-aws
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.52.0...kani-0.53.0
+
 ## [0.52.0]
 
 ## What's Changed

diff --git a/Cargo.lock b/Cargo.lock
@@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -228,7 +228,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -405,14 +405,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -433,7 +433,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -461,7 +461,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "home",
@@ -470,14 +470,14 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -487,7 +487,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -992,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani",
 ]

diff --git a/Cargo.toml b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.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.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
@@ -98,7 +98,11 @@ pub enum ExprValue {
     // {}
     EmptyUnion,
     /// `1.0f`
+    Float16Constant(f16),
+    /// `1.0f`
     FloatConstant(f32),
+    /// `Float 128 example`
+    Float128Constant(f128),
     /// `function(arguments)`
     FunctionCall {
         function: Expr,
@@ -581,6 +585,28 @@ impl Expr {
         expr!(EmptyUnion, typ)
     }
 
+    /// `3.14f`
+    pub fn float16_constant(c: f16) -> Self {
+        expr!(Float16Constant(c), Type::float16())
+    }
+
+    /// `union {_Float16 f; uint16_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
+    pub fn float16_constant_from_bitpattern(bp: u16) -> Self {
+        let c = f16::from_bits(bp);
+        Self::float16_constant(c)
+    }
+
+    /// `3.14159265358979323846264338327950288L`
+    pub fn float128_constant(c: f128) -> Self {
+        expr!(Float128Constant(c), Type::float128())
+    }
+
+    /// `union {_Float128 f; __uint128_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
+    pub fn float128_constant_from_bitpattern(bp: u128) -> Self {
+        let c = f128::from_bits(bp);
+        Self::float128_constant(c)
+    }
+
     /// `1.0f`
     pub fn float_constant(c: f32) -> Self {
         expr!(FloatConstant(c), Type::float())

diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -41,6 +41,10 @@ pub enum Type {
     FlexibleArray { typ: Box<Type> },
     /// `float`
     Float,
+    /// `_Float16`
+    Float16,
+    /// `_Float128`
+    Float128,
     /// `struct x {}`
     IncompleteStruct { tag: InternedString },
     /// `union x {}`
@@ -166,6 +170,8 @@ impl DatatypeComponent {
             | Double
             | FlexibleArray { .. }
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -363,6 +369,8 @@ impl Type {
             Double => st.machine_model().double_width,
             Empty => 0,
             FlexibleArray { .. } => 0,
+            Float16 => 16,
+            Float128 => 128,
             Float => st.machine_model().float_width,
             IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
             IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
@@ -532,6 +540,22 @@ impl Type {
         }
     }
 
+    pub fn is_float_16(&self) -> bool {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            Float16 => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_float_128(&self) -> bool {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            Float128 => true,
+            _ => false,
+        }
+    }
+
     pub fn is_float(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
@@ -543,7 +567,7 @@ impl Type {
     pub fn is_floating_point(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
-            Double | Float => true,
+            Double | Float | Float16 | Float128 => true,
             _ => false,
         }
     }
@@ -577,6 +601,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -632,6 +658,8 @@ impl Type {
             | Double
             | Empty
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -918,6 +946,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -1042,6 +1072,14 @@ impl Type {
         FlexibleArray { typ: Box::new(self) }
     }
 
+    pub fn float16() -> Self {
+        Float16
+    }
+
+    pub fn float128() -> Self {
+        Float128
+    }
+
     pub fn float() -> Self {
         Float
     }
@@ -1275,6 +1313,10 @@ impl Type {
             Expr::c_true()
         } else if self.is_float() {
             Expr::float_constant(1.0)
+        } else if self.is_float_16() {
+            Expr::float16_constant(1.0)
+        } else if self.is_float_128() {
+            Expr::float128_constant(1.0)
         } else if self.is_double() {
             Expr::double_constant(1.0)
         } else {
@@ -1291,6 +1333,10 @@ impl Type {
             Expr::c_false()
         } else if self.is_float() {
             Expr::float_constant(0.0)
+        } else if self.is_float_16() {
+            Expr::float16_constant(0.0)
+        } else if self.is_float_128() {
+            Expr::float128_constant(0.0)
         } else if self.is_double() {
             Expr::double_constant(0.0)
         } else if self.is_pointer() {
@@ -1309,6 +1355,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -1413,6 +1461,8 @@ impl Type {
             Type::Empty => "empty".to_string(),
             Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
             Type::Float => "float".to_string(),
+            Type::Float16 => "float16".to_string(),
+            Type::Float128 => "float128".to_string(),
             Type::IncompleteStruct { tag } => tag.to_string(),
             Type::IncompleteUnion { tag } => tag.to_string(),
             Type::InfiniteArray { typ } => {
@@ -1512,6 +1562,8 @@ mod type_tests {
         assert_eq!(type_def.is_unsigned(&mm), src_type.is_unsigned(&mm));
         assert_eq!(type_def.is_scalar(), src_type.is_scalar());
         assert_eq!(type_def.is_float(), src_type.is_float());
+        assert_eq!(type_def.is_float_16(), src_type.is_float_16());
+        assert_eq!(type_def.is_float_128(), src_type.is_float_128());
         assert_eq!(type_def.is_floating_point(), src_type.is_floating_point());
         assert_eq!(type_def.width(), src_type.width());
         assert_eq!(type_def.can_be_lvalue(), src_type.can_be_lvalue());

diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs
@@ -283,6 +283,8 @@ pub enum IrepId {
     Short,
     Long,
     Float,
+    Float16,
+    Float128,
     Double,
     Byte,
     Boolean,
@@ -1157,6 +1159,8 @@ impl Display for IrepId {
             IrepId::Short => "short",
             IrepId::Long => "long",
             IrepId::Float => "float",
+            IrepId::Float16 => "float16",
+            IrepId::Float128 => "float128",
             IrepId::Double => "double",
             IrepId::Byte => "byte",
             IrepId::Boolean => "boolean",