From 2df53b72b1cacb233a78b62b22d53d8f58e9a256 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 16:20:52 +0000 Subject: [PATCH 01/14] Toolchain upgrade to 6/26 --- cprover_bindings/src/goto_program/expr.rs | 24 +++++++++++ cprover_bindings/src/goto_program/mod.rs | 1 - cprover_bindings/src/goto_program/typ.rs | 26 ++++++++++++ cprover_bindings/src/irep/irep_id.rs | 4 ++ cprover_bindings/src/irep/to_irep.rs | 40 +++++++++++++++++++ cprover_bindings/src/lib.rs | 3 ++ .../codegen_cprover_gotoc/codegen/operand.rs | 6 +++ .../src/codegen_cprover_gotoc/codegen/typ.rs | 2 + kani-compiler/src/main.rs | 2 + rust-toolchain.toml | 2 +- tests/perf/s2n-quic | 2 +- 11 files changed, 109 insertions(+), 3 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 75eb18df0abb..d127ec67459d 100644 --- 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` + HalfConstant(f16), + /// `1.0f` FloatConstant(f32), + /// `Float 128 example` + Float128Constant(f128), /// `function(arguments)` FunctionCall { function: Expr, @@ -581,6 +585,26 @@ impl Expr { expr!(EmptyUnion, typ) } + pub fn float16_constant(c: f16) -> Self { + expr!(HalfConstant(c), Type::float16()) + } + + pub fn float128_constant(c: f128) -> Self { + expr!(Float128Constant(c), Type::float128()) + } + + /// `union {float f; uint32_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 {float f; uint32_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/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 8b61722344fb..4da20177ede8 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/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; diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index da943b26ab19..601fc52311d4 100644 --- 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 }, /// `float` Float, + /// `Half Float Constant` + 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 } => { diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 119aecb8887c..9d52f4ef32fa 100644 --- 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", diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 8716c16d88e0..ca80ffbcd887 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/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![], diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index cd87dffd75a6..e77b29a24ca2 100644 --- a/cprover_bindings/src/lib.rs +++ b/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; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 7388ca44a5b7..5fa48b300cdb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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() as u128, + )) } } TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 6d00bda5bce4..3d71cb7f0f31 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/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!(), diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index a5cfa347a85e..d2f8cf17e9e7 100644 --- a/kani-compiler/src/main.rs +++ b/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; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c620752b423a..5f02b82a51d2 100644 --- a/rust-toolchain.toml +++ b/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"] diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 37335c196fb5..59ef366af76e 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 37335c196fb5755dcbe2532e5a3820e46906d5ea +Subproject commit 59ef366af76edfb4f89bd39137865db2a1ad041d From 98567e204898fcc4beacccca17f1b8fa94cddaa5 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 16:23:07 +0000 Subject: [PATCH 02/14] formatting --- kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 5fa48b300cdb..620aebd4d3b9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -195,7 +195,7 @@ impl<'tcx> GotocCtx<'tcx> { )), FloatTy::F128 => Some(Expr::float128_constant_from_bitpattern( alloc.read_uint().unwrap() as u128, - )) + )), } } TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) From 2b1c74c6ab0b0c624f7ee7f145e602655155f5c7 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 16:42:35 +0000 Subject: [PATCH 03/14] Clippy fixes and comments --- cprover_bindings/src/goto_program/expr.rs | 6 ++++-- cprover_bindings/src/goto_program/typ.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 3 +-- 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index d127ec67459d..3049a934943b 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -585,21 +585,23 @@ 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 {float f; uint32_t bp} u = {.bp = 0x1234}; >>> u.f <<<` + /// `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 {float f; uint32_t bp} u = {.bp = 0x1234}; >>> u.f <<<` + /// `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) diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index 601fc52311d4..4518b1991ee9 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -41,7 +41,7 @@ pub enum Type { FlexibleArray { typ: Box }, /// `float` Float, - /// `Half Float Constant` + /// `Half float` Float16, /// `float 128` Float128, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 620aebd4d3b9..fa0983d6d98f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -194,7 +194,7 @@ impl<'tcx> GotocCtx<'tcx> { alloc.read_uint().unwrap() as u64, )), FloatTy::F128 => Some(Expr::float128_constant_from_bitpattern( - alloc.read_uint().unwrap() as u128, + alloc.read_uint().unwrap(), )), } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index b7d8feeee886..84ec8d627c59 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -1034,10 +1034,9 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { .intersperse("::") .collect::(); 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 { From 93414c03e303bbcad23bd349220375e43359e1f7 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 16:51:47 +0000 Subject: [PATCH 04/14] Formatting again --- kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index fa0983d6d98f..5549edcced25 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -193,9 +193,9 @@ impl<'tcx> GotocCtx<'tcx> { 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(), - )), + FloatTy::F128 => { + Some(Expr::float128_constant_from_bitpattern(alloc.read_uint().unwrap())) + } } } TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) From 7db7a78c060edd823ef8a8db83b1cef950c6fc86 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 17:13:50 +0000 Subject: [PATCH 05/14] Add and clarify comments --- cprover_bindings/src/goto_program/expr.rs | 4 ++-- cprover_bindings/src/irep/to_irep.rs | 15 +++++++++------ tests/perf/s2n-quic | 1 - 3 files changed, 11 insertions(+), 9 deletions(-) delete mode 160000 tests/perf/s2n-quic diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 3049a934943b..0ea7ea4f2864 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -98,7 +98,7 @@ pub enum ExprValue { // {} EmptyUnion, /// `1.0f` - HalfConstant(f16), + HalfFloatConstant(f16), /// `1.0f` FloatConstant(f32), /// `Float 128 example` @@ -587,7 +587,7 @@ impl Expr { /// `3.14f` pub fn float16_constant(c: f16) -> Self { - expr!(HalfConstant(c), Type::float16()) + expr!(HalfFloatConstant(c), Type::float16()) } /// `3.14159265358979323846264338327950288L` diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index ca80ffbcd887..52a448a507e0 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -254,15 +254,12 @@ impl ToIrep for ExprValue { )], } } - ExprValue::HalfConstant(i) => { + ExprValue::HalfFloatConstant(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) - )], + named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))], } } ExprValue::Float128Constant(i) => { @@ -272,7 +269,7 @@ impl ToIrep for ExprValue { sub: vec![], named_sub: linear_map![( IrepId::Value, - Irep::just_bitpattern_id(c, mm.float_width, false) + Irep::just_bitpattern_id(c, 128, false) )], } } @@ -720,12 +717,18 @@ impl ToIrep for Type { Type::Float16 => Irep { id: IrepId::Floatbv, sub: vec![], + // Fraction bits: 10 + // Precision 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)), ], }, + // Fraction bits: 112 + // Precision bits: 52 + // Sign bit: 1 Type::Float128 => Irep { id: IrepId::Floatbv, sub: vec![], diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic deleted file mode 160000 index 59ef366af76e..000000000000 --- a/tests/perf/s2n-quic +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 59ef366af76edfb4f89bd39137865db2a1ad041d From 73e71c3ebf30c5e8b2105916eb757b79c864b9a9 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 17:22:58 +0000 Subject: [PATCH 06/14] Add and clarify comments --- cprover_bindings/src/goto_program/expr.rs | 4 ++-- cprover_bindings/src/irep/to_irep.rs | 15 +++++++++------ 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 3049a934943b..0ea7ea4f2864 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -98,7 +98,7 @@ pub enum ExprValue { // {} EmptyUnion, /// `1.0f` - HalfConstant(f16), + HalfFloatConstant(f16), /// `1.0f` FloatConstant(f32), /// `Float 128 example` @@ -587,7 +587,7 @@ impl Expr { /// `3.14f` pub fn float16_constant(c: f16) -> Self { - expr!(HalfConstant(c), Type::float16()) + expr!(HalfFloatConstant(c), Type::float16()) } /// `3.14159265358979323846264338327950288L` diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index ca80ffbcd887..52a448a507e0 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -254,15 +254,12 @@ impl ToIrep for ExprValue { )], } } - ExprValue::HalfConstant(i) => { + ExprValue::HalfFloatConstant(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) - )], + named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))], } } ExprValue::Float128Constant(i) => { @@ -272,7 +269,7 @@ impl ToIrep for ExprValue { sub: vec![], named_sub: linear_map![( IrepId::Value, - Irep::just_bitpattern_id(c, mm.float_width, false) + Irep::just_bitpattern_id(c, 128, false) )], } } @@ -720,12 +717,18 @@ impl ToIrep for Type { Type::Float16 => Irep { id: IrepId::Floatbv, sub: vec![], + // Fraction bits: 10 + // Precision 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)), ], }, + // Fraction bits: 112 + // Precision bits: 52 + // Sign bit: 1 Type::Float128 => Irep { id: IrepId::Floatbv, sub: vec![], From 70fd84a78d6764ad2c7401ecc390efcc9e6a80a5 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 17:39:12 +0000 Subject: [PATCH 07/14] Fix s2n-quic submodule being tracked --- tests/perf/s2n-quic | 1 + 1 file changed, 1 insertion(+) create mode 160000 tests/perf/s2n-quic diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic new file mode 160000 index 000000000000..59ef366af76e --- /dev/null +++ b/tests/perf/s2n-quic @@ -0,0 +1 @@ +Subproject commit 59ef366af76edfb4f89bd39137865db2a1ad041d From 2136a206200e49d2135abf8f03a5458486cebb25 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 17:46:59 +0000 Subject: [PATCH 08/14] Update s2n-quic from main --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 59ef366af76e..37335c196fb5 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 59ef366af76edfb4f89bd39137865db2a1ad041d +Subproject commit 37335c196fb5755dcbe2532e5a3820e46906d5ea From ac1b75e8428912368fd4cd4f3fd214010fd7f5ac Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 17:50:38 +0000 Subject: [PATCH 09/14] Update to `Float16Constant` --- cprover_bindings/src/goto_program/expr.rs | 4 ++-- cprover_bindings/src/irep/to_irep.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 0ea7ea4f2864..770b4f51dd52 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -98,7 +98,7 @@ pub enum ExprValue { // {} EmptyUnion, /// `1.0f` - HalfFloatConstant(f16), + Float16Constant(f16), /// `1.0f` FloatConstant(f32), /// `Float 128 example` @@ -587,7 +587,7 @@ impl Expr { /// `3.14f` pub fn float16_constant(c: f16) -> Self { - expr!(HalfFloatConstant(c), Type::float16()) + expr!(Float16Constant(c), Type::float16()) } /// `3.14159265358979323846264338327950288L` diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 52a448a507e0..eb6359463398 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -254,7 +254,7 @@ impl ToIrep for ExprValue { )], } } - ExprValue::HalfFloatConstant(i) => { + ExprValue::Float16Constant(i) => { let c: u16 = i.to_bits(); Irep { id: IrepId::Constant, From 549292764a83ddc83697725026459127da3427fc Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 17:58:34 +0000 Subject: [PATCH 10/14] Address comments --- cprover_bindings/src/goto_program/mod.rs | 1 + cprover_bindings/src/goto_program/typ.rs | 4 ++-- cprover_bindings/src/irep/to_irep.rs | 6 +++--- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 4da20177ede8..8b61722344fb 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -6,6 +6,7 @@ // 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; diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index 4518b1991ee9..e11bce386e6c 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -41,9 +41,9 @@ pub enum Type { FlexibleArray { typ: Box }, /// `float` Float, - /// `Half float` + /// `_Float16` Float16, - /// `float 128` + /// `_Float128` Float128, /// `struct x {}` IncompleteStruct { tag: InternedString }, diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index eb6359463398..fc08de05251f 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -726,12 +726,12 @@ impl ToIrep for Type { (IrepId::CCType, Irep::just_id(IrepId::Float16)), ], }, - // Fraction bits: 112 - // Precision bits: 52 - // Sign bit: 1 Type::Float128 => Irep { id: IrepId::Floatbv, sub: vec![], + // Fraction bits: 112 + // Precision bits: 52 + // Sign bit: 1 named_sub: linear_map![ (IrepId::F, Irep::just_int_id(112)), (IrepId::Width, Irep::just_int_id(128)), From 3e889c542fe71152d224cd7cd93a0e761c46dffd Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 18:00:33 +0000 Subject: [PATCH 11/14] Re-order to keep consistency --- cprover_bindings/src/goto_program/expr.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 770b4f51dd52..16f33115e0ff 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -590,17 +590,17 @@ impl Expr { expr!(Float16Constant(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) } + /// `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); From 14c40632c64fc43fdf9d6e8ce5f270853d1049cb Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 18:51:06 +0000 Subject: [PATCH 12/14] Add methods to check for new f16 and f128 types --- cprover_bindings/src/goto_program/typ.rs | 28 +++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index e11bce386e6c..d0cc8821a447 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -540,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 { @@ -551,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, } } @@ -1297,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 { @@ -1313,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() { @@ -1538,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()); From b3a06c5bd305dcf2edd21a4fdeacf853d3070c2b Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 19:57:11 +0000 Subject: [PATCH 13/14] Fix comment to say 15 bits --- cprover_bindings/src/irep/to_irep.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index fc08de05251f..4b5c86350172 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -718,7 +718,7 @@ impl ToIrep for Type { id: IrepId::Floatbv, sub: vec![], // Fraction bits: 10 - // Precision bits: 5 + // Exponent width bits: 5 // Sign bit: 1 named_sub: linear_map![ (IrepId::F, Irep::just_int_id(10)), @@ -730,7 +730,7 @@ impl ToIrep for Type { id: IrepId::Floatbv, sub: vec![], // Fraction bits: 112 - // Precision bits: 52 + // Exponent width bits: 15 // Sign bit: 1 named_sub: linear_map![ (IrepId::F, Irep::just_int_id(112)), From 86ea6b0b16bd0d9d552fbf15745416874e06a018 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 28 Jun 2024 21:57:38 +0000 Subject: [PATCH 14/14] Add testing for f16 and f128 --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 5 ++- library/kani/src/arbitrary.rs | 4 +++ library/kani/src/invariant.rs | 2 ++ library/kani/src/lib.rs | 2 ++ library/kani_core/src/arbitrary.rs | 9 ++++++ library/kani_core/src/lib.rs | 2 ++ .../floats/non_standard_floats/expected | 31 +++++++++++++++++++ .../floats/non_standard_floats/main.rs | 27 ++++++++++++++++ .../floats/{ => standard_floats}/expected | 2 -- .../floats/{ => standard_floats}/main.rs | 11 ++++--- tests/kani/FloatingPoint/main.rs | 6 ++++ tests/kani/Invariant/invariant_impls.rs | 7 +++++ 12 files changed, 99 insertions(+), 9 deletions(-) create mode 100644 tests/expected/arbitrary/floats/non_standard_floats/expected create mode 100644 tests/expected/arbitrary/floats/non_standard_floats/main.rs rename tests/expected/arbitrary/floats/{ => standard_floats}/expected (99%) rename tests/expected/arbitrary/floats/{ => standard_floats}/main.rs (74%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 3d71cb7f0f31..6e6547295ff9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -544,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: - 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) => { diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 3f1adc787b79..424ca2485d57 100644 --- a/library/kani/src/arbitrary.rs +++ b/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 { diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs index f118f94e995c..068cdedc277e 100644 --- a/library/kani/src/invariant.rs +++ b/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); diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index acf1e08e0441..0a52a9516398 100644 --- a/library/kani/src/lib.rs +++ b/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")] diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index d202df4ead1d..a8271ad758cf 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/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); diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index de808ffaf918..143fbb7ef825 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -17,6 +17,8 @@ #![feature(no_core)] #![no_core] +#![feature(f16)] +#![feature(f128)] mod arbitrary; mod mem; diff --git a/tests/expected/arbitrary/floats/non_standard_floats/expected b/tests/expected/arbitrary/floats/non_standard_floats/expected new file mode 100644 index 000000000000..26db615201a6 --- /dev/null +++ b/tests/expected/arbitrary/floats/non_standard_floats/expected @@ -0,0 +1,31 @@ +Checking harness check_f128... + +Status: SATISFIED\ +Description: "This may be true"\ +in function check_f128 + +Status: SATISFIED\ +Description: "This may also be true"\ +in function check_f128 + +Status: SATISFIED\ +Description: "NaN should be valid float"\ +in function check_f128 + +Checking harness check_f16... + +Status: SATISFIED\ +Description: "This may be true"\ +in function check_f16 + +Status: SATISFIED\ +Description: "This may also be true"\ +in function check_f16 + +Status: SATISFIED\ +Description: "NaN should be valid float"\ +in function check_f16 + +VERIFICATION:- SUCCESSFUL + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/arbitrary/floats/non_standard_floats/main.rs b/tests/expected/arbitrary/floats/non_standard_floats/main.rs new file mode 100644 index 000000000000..ebea6535b3d5 --- /dev/null +++ b/tests/expected/arbitrary/floats/non_standard_floats/main.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that kani::any and kani::any_raw can be used with non-standard floats i.e f16 and f128. + +#![feature(f16)] +#![feature(f128)] + +macro_rules! test_non_standard_floats { + ( $type: ty ) => {{ + let v1 = kani::any::<$type>(); + let v2 = kani::any::<$type>(); + kani::cover!(v1 == v2, "This may be true"); + kani::cover!(v1 != v2, "This may also be true"); + kani::cover!(v1.is_nan(), "NaN should be valid float"); + }}; +} + +#[kani::proof] +fn check_f16() { + test_non_standard_floats!(f16); +} + +#[kani::proof] +fn check_f128() { + test_non_standard_floats!(f128); +} diff --git a/tests/expected/arbitrary/floats/expected b/tests/expected/arbitrary/floats/standard_floats/expected similarity index 99% rename from tests/expected/arbitrary/floats/expected rename to tests/expected/arbitrary/floats/standard_floats/expected index 4bb2fadacd7f..de3b67f28578 100644 --- a/tests/expected/arbitrary/floats/expected +++ b/tests/expected/arbitrary/floats/standard_floats/expected @@ -51,10 +51,8 @@ Status: SATISFIED\ Description: "Non-finite numbers are valid float"\ in function check_f32 - ** 6 of 6 cover properties satisfied - VERIFICATION:- SUCCESSFUL Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/arbitrary/floats/main.rs b/tests/expected/arbitrary/floats/standard_floats/main.rs similarity index 74% rename from tests/expected/arbitrary/floats/main.rs rename to tests/expected/arbitrary/floats/standard_floats/main.rs index 1ad4de3ef3f7..c204643e9ab8 100644 --- a/tests/expected/arbitrary/floats/main.rs +++ b/tests/expected/arbitrary/floats/standard_floats/main.rs @@ -1,9 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// Ensure that kani::any and kani::any_raw can be used with floats. +// Ensure that kani::any and kani::any_raw can be used with standard floats i.e f32 and f64. -macro_rules! test { +#![feature(f16)] +#![feature(f128)] + +macro_rules! test_standard_floats { ( $type: ty ) => {{ let v1 = kani::any::<$type>(); let v2 = kani::any::<$type>(); @@ -18,10 +21,10 @@ macro_rules! test { #[kani::proof] fn check_f32() { - test!(f32); + test_standard_floats!(f32); } #[kani::proof] fn check_f64() { - test!(f64); + test_standard_floats!(f64); } diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs index c04bd9b305f8..f8ebccdac02a 100644 --- a/tests/kani/FloatingPoint/main.rs +++ b/tests/kani/FloatingPoint/main.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(f16)] +#![feature(f128)] + macro_rules! test_floats { ($ty:ty) => { let a: $ty = kani::any(); @@ -26,6 +30,8 @@ fn main() { assert!(1.1 == 1.1 * 1.0); assert!(1.1 != 1.11 / 1.0); + test_floats!(f16); test_floats!(f32); test_floats!(f64); + test_floats!(f128); } diff --git a/tests/kani/Invariant/invariant_impls.rs b/tests/kani/Invariant/invariant_impls.rs index 4f00f4134956..146c9731370d 100644 --- a/tests/kani/Invariant/invariant_impls.rs +++ b/tests/kani/Invariant/invariant_impls.rs @@ -3,6 +3,10 @@ //! Check the `Invariant` implementations that we include in the Kani library //! with respect to the underlying type invariants. + +#![feature(f16)] +#![feature(f128)] + extern crate kani; use kani::Invariant; @@ -29,6 +33,9 @@ fn check_safe_impls() { check_safe_type!(i128); check_safe_type!(isize); + check_safe_type!(f16); + check_safe_type!(f128); + check_safe_type!(f32); check_safe_type!(f64);