Add support for f16 and f128 for toolchain upgrade to 6/28 (model-che…

…cking#3306)

Adds support for f16 and f128, i.e 
1. adding translation to `irep` .
2. generating arbitrary values for the new types
3. generating basic invariants (checking if safe) for new types
4. Adds sanity testing for arbitrary on the new types.

Resolves model-checking#3303

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())

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());

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",

cprover_bindings/src/irep/to_irep.rs

@@ -254,6 +254,25 @@ impl ToIrep for ExprValue {
                     )],
                 }
             }
+            ExprValue::Float16Constant(i) => {
+                let c: u16 = i.to_bits();
+                Irep {
+                    id: IrepId::Constant,
+                    sub: vec![],
+                    named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))],
+                }
+            }
+            ExprValue::Float128Constant(i) => {
+                let c: u128 = i.to_bits();
+                Irep {
+                    id: IrepId::Constant,
+                    sub: vec![],
+                    named_sub: linear_map![(
+                        IrepId::Value,
+                        Irep::just_bitpattern_id(c, 128, false)
+                    )],
+                }
+            }
             ExprValue::FunctionCall { function, arguments } => side_effect_irep(
                 IrepId::FunctionCall,
                 vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
@@ -695,6 +714,30 @@ impl ToIrep for Type {
                     (IrepId::CCType, Irep::just_id(IrepId::Float)),
                 ],
             },
+            Type::Float16 => Irep {
+                id: IrepId::Floatbv,
+                sub: vec![],
+                // Fraction bits: 10
+                // Exponent width bits: 5
+                // Sign bit: 1
+                named_sub: linear_map![
+                    (IrepId::F, Irep::just_int_id(10)),
+                    (IrepId::Width, Irep::just_int_id(16)),
+                    (IrepId::CCType, Irep::just_id(IrepId::Float16)),
+                ],
+            },
+            Type::Float128 => Irep {
+                id: IrepId::Floatbv,
+                sub: vec![],
+                // Fraction bits: 112
+                // Exponent width bits: 15
+                // Sign bit: 1
+                named_sub: linear_map![
+                    (IrepId::F, Irep::just_int_id(112)),
+                    (IrepId::Width, Irep::just_int_id(128)),
+                    (IrepId::CCType, Irep::just_id(IrepId::Float128)),
+                ],
+            },
             Type::IncompleteStruct { tag } => Irep {
                 id: IrepId::Struct,
                 sub: vec![],

cprover_bindings/src/lib.rs

@@ -29,6 +29,9 @@
 //! Speical [irep::Irep::id]s include:
 //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
 
+#![feature(f128)]
+#![feature(f16)]
+
 mod env;
 pub mod goto_program;
 pub mod irep;

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

@@ -184,12 +184,18 @@ impl<'tcx> GotocCtx<'tcx> {
             // Instead, we use integers with the right width to represent the bit pattern.
             {
                 match k {
+                    FloatTy::F16 => Some(Expr::float16_constant_from_bitpattern(
+                        alloc.read_uint().unwrap() as u16,
+                    )),
                     FloatTy::F32 => Some(Expr::float_constant_from_bitpattern(
                         alloc.read_uint().unwrap() as u32,
                     )),
                     FloatTy::F64 => Some(Expr::double_constant_from_bitpattern(
                         alloc.read_uint().unwrap() as u64,
                     )),
+                    FloatTy::F128 => {
+                        Some(Expr::float128_constant_from_bitpattern(alloc.read_uint().unwrap()))
+                    }
                 }
             }
             TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _))

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

@@ -130,6 +130,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 Type::Empty => todo!(),
                 Type::FlexibleArray { .. } => todo!(),
                 Type::Float => write!(out, "f32")?,
+                Type::Float16 => write!(out, "f16")?,
+                Type::Float128 => write!(out, "f128")?,
                 Type::IncompleteStruct { .. } => todo!(),
                 Type::IncompleteUnion { .. } => todo!(),
                 Type::InfiniteArray { .. } => todo!(),
@@ -542,9 +544,8 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Float(k) => match k {
                 FloatTy::F32 => Type::float(),
                 FloatTy::F64 => Type::double(),
-                // `F16` and `F128` are not yet handled.
-                // Tracked here: <https://github.com/model-checking/kani/issues/3069>
-                FloatTy::F16 | FloatTy::F128 => unimplemented!(),
+                FloatTy::F16 => Type::float16(),
+                FloatTy::F128 => Type::float128(),
             },
             ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
             ty::Adt(def, subst) => {

kani-compiler/src/kani_middle/attributes.rs

@@ -1034,10 +1034,9 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
                     .intersperse("::")
                     .collect::<String>();
                 KaniAttributeKind::try_from(ident_str.as_str())
-                    .map_err(|err| {
+                    .inspect_err(|&err| {
                         debug!(?err, "attr_kind_failed");
                         tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
-                        err
                     })
                     .ok()
             } else {

kani-compiler/src/main.rs

@@ -13,6 +13,8 @@
 #![feature(more_qualified_paths)]
 #![feature(iter_intersperse)]
 #![feature(let_chains)]
+#![feature(f128)]
+#![feature(f16)]
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;

library/kani/src/arbitrary.rs

@@ -71,6 +71,10 @@ trivial_arbitrary!(isize);
 trivial_arbitrary!(f32);
 trivial_arbitrary!(f64);
 
+// Similarly, we do not constraint values for non-standard floating types.
+trivial_arbitrary!(f16);
+trivial_arbitrary!(f128);
+
 trivial_arbitrary!(());
 
 impl Arbitrary for bool {

library/kani/src/invariant.rs

@@ -96,6 +96,8 @@ trivial_invariant!(isize);
 // invariant that checks for NaN, infinite, or subnormal values.
 trivial_invariant!(f32);
 trivial_invariant!(f64);
+trivial_invariant!(f16);
+trivial_invariant!(f128);
 
 trivial_invariant!(());
 trivial_invariant!(bool);

library/kani/src/lib.rs

@@ -18,6 +18,8 @@
 #![allow(internal_features)]
 // Required for implementing memory predicates.
 #![feature(ptr_metadata)]
+#![feature(f16)]
+#![feature(f128)]
 
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]

library/kani_core/src/arbitrary.rs

@@ -88,6 +88,15 @@ macro_rules! generate_arbitrary {
         trivial_arbitrary!(i128);
         trivial_arbitrary!(isize);
 
+        // We do not constrain floating points values per type spec. Users must add assumptions to their
+        // verification code if they want to eliminate NaN, infinite, or subnormal.
+        trivial_arbitrary!(f32);
+        trivial_arbitrary!(f64);
+
+        // Similarly, we do not constraint values for non-standard floating types.
+        trivial_arbitrary!(f16);
+        trivial_arbitrary!(f128);
+
         nonzero_arbitrary!(NonZeroU8, u8);
         nonzero_arbitrary!(NonZeroU16, u16);
         nonzero_arbitrary!(NonZeroU32, u32);

library/kani_core/src/lib.rs

@@ -17,6 +17,8 @@
 
 #![feature(no_core)]
 #![no_core]
+#![feature(f16)]
+#![feature(f128)]
 
 mod arbitrary;
 mod mem;

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-06-27"
+channel = "nightly-2024-06-28"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]