Add support for f16 and f128 for toolchain upgrade to 6/28

cprover_bindings/src/goto_program/expr.rs

@@ -98,7 +98,11 @@ pub enum ExprValue {
     // {}
     EmptyUnion,
     /// `1.0f`
+    HalfConstant(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!(HalfConstant(c), Type::float16())
+    }
+
+    /// `3.14159265358979323846264338327950288L`
+    pub fn float128_constant(c: f128) -> Self {
+        expr!(Float128Constant(c), Type::float128())
+    }
+
+    /// `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)
+    }
+
+    /// `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/mod.rs

@@ -6,7 +6,6 @@
 // There are a fair number of constructs in this module that are better maintained as
 // explicit pattern matching versus using the `matches!` macro.
 #![allow(clippy::match_like_matches_macro)]
-
 mod builtin;
 mod expr;
 mod location;

cprover_bindings/src/goto_program/typ.rs

@@ -41,6 +41,10 @@ pub enum Type {
     FlexibleArray { typ: Box<Type> },
     /// `float`
     Float,
+    /// `Half float`
+    Float16,
+    /// `float 128`
+    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"),
@@ -577,6 +585,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -632,6 +642,8 @@ impl Type {
             | Double
             | Empty
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -918,6 +930,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -1042,6 +1056,14 @@ impl Type {
         FlexibleArray { typ: Box::new(self) }
     }
 
+    pub fn float16() -> Self {
+        Float16
+    }
+
+    pub fn float128() -> Self {
+        Float128
+    }
+
     pub fn float() -> Self {
         Float
     }
@@ -1309,6 +1331,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -1413,6 +1437,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 } => {

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,28 @@ impl ToIrep for ExprValue {
                     )],
                 }
             }
+            ExprValue::HalfConstant(i) => {
+                let c: u16 = i.to_bits();
+                Irep {
+                    id: IrepId::Constant,
+                    sub: vec![],
+                    named_sub: linear_map![(
+                        IrepId::Value,
+                        Irep::just_bitpattern_id(c, mm.float_width, 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, mm.float_width, false)
+                    )],
+                }
+            }
             ExprValue::FunctionCall { function, arguments } => side_effect_irep(
                 IrepId::FunctionCall,
                 vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
@@ -695,6 +717,24 @@ impl ToIrep for Type {
                     (IrepId::CCType, Irep::just_id(IrepId::Float)),
                 ],
             },
+            Type::Float16 => Irep {
+                id: IrepId::Floatbv,
+                sub: vec![],
+                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![],
+                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!(),

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;

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