Skip to content

Commit d55f25b

Browse files
jaisnanjaisnan
authored
Add support for f16 and f128 for toolchain upgrade to 6/28 (rust-lang#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 rust-lang#3303
1 parent 6f0c0b5 commit d55f25b

File tree

21 files changed

+240
-13
lines changed

21 files changed

+240
-13
lines changed

‎cprover_bindings/src/goto_program/expr.rs

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,11 @@ pub enum ExprValue {
9898
// {}
9999
EmptyUnion,
100100
/// `1.0f`
101+
Float16Constant(f16),
102+
/// `1.0f`
101103
FloatConstant(f32),
104+
/// `Float 128 example`
105+
Float128Constant(f128),
102106
/// `function(arguments)`
103107
FunctionCall {
104108
function: Expr,
@@ -581,6 +585,28 @@ impl Expr {
581585
expr!(EmptyUnion, typ)
582586
}
583587

588+
/// `3.14f`
589+
pub fn float16_constant(c: f16) -> Self {
590+
expr!(Float16Constant(c), Type::float16())
591+
}
592+
593+
/// `union {_Float16 f; uint16_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
594+
pub fn float16_constant_from_bitpattern(bp: u16) -> Self {
595+
let c = f16::from_bits(bp);
596+
Self::float16_constant(c)
597+
}
598+
599+
/// `3.14159265358979323846264338327950288L`
600+
pub fn float128_constant(c: f128) -> Self {
601+
expr!(Float128Constant(c), Type::float128())
602+
}
603+
604+
/// `union {_Float128 f; __uint128_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
605+
pub fn float128_constant_from_bitpattern(bp: u128) -> Self {
606+
let c = f128::from_bits(bp);
607+
Self::float128_constant(c)
608+
}
609+
584610
/// `1.0f`
585611
pub fn float_constant(c: f32) -> Self {
586612
expr!(FloatConstant(c), Type::float())

‎cprover_bindings/src/goto_program/typ.rs

Lines changed: 53 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,10 @@ pub enum Type {
4141
FlexibleArray { typ: Box<Type> },
4242
/// `float`
4343
Float,
44+
/// `_Float16`
45+
Float16,
46+
/// `_Float128`
47+
Float128,
4448
/// `struct x {}`
4549
IncompleteStruct { tag: InternedString },
4650
/// `union x {}`
@@ -166,6 +170,8 @@ impl DatatypeComponent {
166170
| Double
167171
| FlexibleArray { .. }
168172
| Float
173+
| Float16
174+
| Float128
169175
| Integer
170176
| Pointer { .. }
171177
| Signedbv { .. }
@@ -363,6 +369,8 @@ impl Type {
363369
Double => st.machine_model().double_width,
364370
Empty => 0,
365371
FlexibleArray { .. } => 0,
372+
Float16 => 16,
373+
Float128 => 128,
366374
Float => st.machine_model().float_width,
367375
IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
368376
IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
@@ -532,6 +540,22 @@ impl Type {
532540
}
533541
}
534542

543+
pub fn is_float_16(&self) -> bool {
544+
let concrete = self.unwrap_typedef();
545+
match concrete {
546+
Float16 => true,
547+
_ => false,
548+
}
549+
}
550+
551+
pub fn is_float_128(&self) -> bool {
552+
let concrete = self.unwrap_typedef();
553+
match concrete {
554+
Float128 => true,
555+
_ => false,
556+
}
557+
}
558+
535559
pub fn is_float(&self) -> bool {
536560
let concrete = self.unwrap_typedef();
537561
match concrete {
@@ -543,7 +567,7 @@ impl Type {
543567
pub fn is_floating_point(&self) -> bool {
544568
let concrete = self.unwrap_typedef();
545569
match concrete {
546-
Double | Float => true,
570+
Double | Float | Float16 | Float128 => true,
547571
_ => false,
548572
}
549573
}
@@ -577,6 +601,8 @@ impl Type {
577601
| CInteger(_)
578602
| Double
579603
| Float
604+
| Float16
605+
| Float128
580606
| Integer
581607
| Pointer { .. }
582608
| Signedbv { .. }
@@ -632,6 +658,8 @@ impl Type {
632658
| Double
633659
| Empty
634660
| Float
661+
| Float16
662+
| Float128
635663
| Integer
636664
| Pointer { .. }
637665
| Signedbv { .. }
@@ -918,6 +946,8 @@ impl Type {
918946
| CInteger(_)
919947
| Double
920948
| Float
949+
| Float16
950+
| Float128
921951
| Integer
922952
| Pointer { .. }
923953
| Signedbv { .. }
@@ -1042,6 +1072,14 @@ impl Type {
10421072
FlexibleArray { typ: Box::new(self) }
10431073
}
10441074

1075+
pub fn float16() -> Self {
1076+
Float16
1077+
}
1078+
1079+
pub fn float128() -> Self {
1080+
Float128
1081+
}
1082+
10451083
pub fn float() -> Self {
10461084
Float
10471085
}
@@ -1275,6 +1313,10 @@ impl Type {
12751313
Expr::c_true()
12761314
} else if self.is_float() {
12771315
Expr::float_constant(1.0)
1316+
} else if self.is_float_16() {
1317+
Expr::float16_constant(1.0)
1318+
} else if self.is_float_128() {
1319+
Expr::float128_constant(1.0)
12781320
} else if self.is_double() {
12791321
Expr::double_constant(1.0)
12801322
} else {
@@ -1291,6 +1333,10 @@ impl Type {
12911333
Expr::c_false()
12921334
} else if self.is_float() {
12931335
Expr::float_constant(0.0)
1336+
} else if self.is_float_16() {
1337+
Expr::float16_constant(0.0)
1338+
} else if self.is_float_128() {
1339+
Expr::float128_constant(0.0)
12941340
} else if self.is_double() {
12951341
Expr::double_constant(0.0)
12961342
} else if self.is_pointer() {
@@ -1309,6 +1355,8 @@ impl Type {
13091355
| CInteger(_)
13101356
| Double
13111357
| Float
1358+
| Float16
1359+
| Float128
13121360
| Integer
13131361
| Pointer { .. }
13141362
| Signedbv { .. }
@@ -1413,6 +1461,8 @@ impl Type {
14131461
Type::Empty => "empty".to_string(),
14141462
Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
14151463
Type::Float => "float".to_string(),
1464+
Type::Float16 => "float16".to_string(),
1465+
Type::Float128 => "float128".to_string(),
14161466
Type::IncompleteStruct { tag } => tag.to_string(),
14171467
Type::IncompleteUnion { tag } => tag.to_string(),
14181468
Type::InfiniteArray { typ } => {
@@ -1512,6 +1562,8 @@ mod type_tests {
15121562
assert_eq!(type_def.is_unsigned(&mm), src_type.is_unsigned(&mm));
15131563
assert_eq!(type_def.is_scalar(), src_type.is_scalar());
15141564
assert_eq!(type_def.is_float(), src_type.is_float());
1565+
assert_eq!(type_def.is_float_16(), src_type.is_float_16());
1566+
assert_eq!(type_def.is_float_128(), src_type.is_float_128());
15151567
assert_eq!(type_def.is_floating_point(), src_type.is_floating_point());
15161568
assert_eq!(type_def.width(), src_type.width());
15171569
assert_eq!(type_def.can_be_lvalue(), src_type.can_be_lvalue());

‎cprover_bindings/src/irep/irep_id.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -283,6 +283,8 @@ pub enum IrepId {
283283
Short,
284284
Long,
285285
Float,
286+
Float16,
287+
Float128,
286288
Double,
287289
Byte,
288290
Boolean,
@@ -1157,6 +1159,8 @@ impl Display for IrepId {
11571159
IrepId::Short => "short",
11581160
IrepId::Long => "long",
11591161
IrepId::Float => "float",
1162+
IrepId::Float16 => "float16",
1163+
IrepId::Float128 => "float128",
11601164
IrepId::Double => "double",
11611165
IrepId::Byte => "byte",
11621166
IrepId::Boolean => "boolean",

‎cprover_bindings/src/irep/to_irep.rs

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -254,6 +254,25 @@ impl ToIrep for ExprValue {
254254
)],
255255
}
256256
}
257+
ExprValue::Float16Constant(i) => {
258+
let c: u16 = i.to_bits();
259+
Irep {
260+
id: IrepId::Constant,
261+
sub: vec![],
262+
named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))],
263+
}
264+
}
265+
ExprValue::Float128Constant(i) => {
266+
let c: u128 = i.to_bits();
267+
Irep {
268+
id: IrepId::Constant,
269+
sub: vec![],
270+
named_sub: linear_map![(
271+
IrepId::Value,
272+
Irep::just_bitpattern_id(c, 128, false)
273+
)],
274+
}
275+
}
257276
ExprValue::FunctionCall { function, arguments } => side_effect_irep(
258277
IrepId::FunctionCall,
259278
vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
@@ -695,6 +714,30 @@ impl ToIrep for Type {
695714
(IrepId::CCType, Irep::just_id(IrepId::Float)),
696715
],
697716
},
717+
Type::Float16 => Irep {
718+
id: IrepId::Floatbv,
719+
sub: vec![],
720+
// Fraction bits: 10
721+
// Exponent width bits: 5
722+
// Sign bit: 1
723+
named_sub: linear_map![
724+
(IrepId::F, Irep::just_int_id(10)),
725+
(IrepId::Width, Irep::just_int_id(16)),
726+
(IrepId::CCType, Irep::just_id(IrepId::Float16)),
727+
],
728+
},
729+
Type::Float128 => Irep {
730+
id: IrepId::Floatbv,
731+
sub: vec![],
732+
// Fraction bits: 112
733+
// Exponent width bits: 15
734+
// Sign bit: 1
735+
named_sub: linear_map![
736+
(IrepId::F, Irep::just_int_id(112)),
737+
(IrepId::Width, Irep::just_int_id(128)),
738+
(IrepId::CCType, Irep::just_id(IrepId::Float128)),
739+
],
740+
},
698741
Type::IncompleteStruct { tag } => Irep {
699742
id: IrepId::Struct,
700743
sub: vec![],

‎cprover_bindings/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,9 @@
2929
//! Speical [irep::Irep::id]s include:
3030
//! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
3131
32+
#![feature(f128)]
33+
#![feature(f16)]
34+
3235
mod env;
3336
pub mod goto_program;
3437
pub mod irep;

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -184,12 +184,18 @@ impl<'tcx> GotocCtx<'tcx> {
184184
// Instead, we use integers with the right width to represent the bit pattern.
185185
{
186186
match k {
187+
FloatTy::F16 => Some(Expr::float16_constant_from_bitpattern(
188+
alloc.read_uint().unwrap() as u16,
189+
)),
187190
FloatTy::F32 => Some(Expr::float_constant_from_bitpattern(
188191
alloc.read_uint().unwrap() as u32,
189192
)),
190193
FloatTy::F64 => Some(Expr::double_constant_from_bitpattern(
191194
alloc.read_uint().unwrap() as u64,
192195
)),
196+
FloatTy::F128 => {
197+
Some(Expr::float128_constant_from_bitpattern(alloc.read_uint().unwrap()))
198+
}
193199
}
194200
}
195201
TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _))

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,8 @@ impl<'tcx> GotocCtx<'tcx> {
130130
Type::Empty => todo!(),
131131
Type::FlexibleArray { .. } => todo!(),
132132
Type::Float => write!(out, "f32")?,
133+
Type::Float16 => write!(out, "f16")?,
134+
Type::Float128 => write!(out, "f128")?,
133135
Type::IncompleteStruct { .. } => todo!(),
134136
Type::IncompleteUnion { .. } => todo!(),
135137
Type::InfiniteArray { .. } => todo!(),
@@ -542,9 +544,8 @@ impl<'tcx> GotocCtx<'tcx> {
542544
ty::Float(k) => match k {
543545
FloatTy::F32 => Type::float(),
544546
FloatTy::F64 => Type::double(),
545-
// `F16` and `F128` are not yet handled.
546-
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
547-
FloatTy::F16 | FloatTy::F128 => unimplemented!(),
547+
FloatTy::F16 => Type::float16(),
548+
FloatTy::F128 => Type::float128(),
548549
},
549550
ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
550551
ty::Adt(def, subst) => {

‎kani-compiler/src/kani_middle/attributes.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1034,10 +1034,9 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
10341034
.intersperse("::")
10351035
.collect::<String>();
10361036
KaniAttributeKind::try_from(ident_str.as_str())
1037-
.map_err(|err| {
1037+
.inspect_err(|&err| {
10381038
debug!(?err, "attr_kind_failed");
10391039
tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
1040-
err
10411040
})
10421041
.ok()
10431042
} else {

‎kani-compiler/src/main.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@
1313
#![feature(more_qualified_paths)]
1414
#![feature(iter_intersperse)]
1515
#![feature(let_chains)]
16+
#![feature(f128)]
17+
#![feature(f16)]
1618
extern crate rustc_abi;
1719
extern crate rustc_ast;
1820
extern crate rustc_ast_pretty;

‎library/kani/src/arbitrary.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,10 @@ trivial_arbitrary!(isize);
7171
trivial_arbitrary!(f32);
7272
trivial_arbitrary!(f64);
7373

74+
// Similarly, we do not constraint values for non-standard floating types.
75+
trivial_arbitrary!(f16);
76+
trivial_arbitrary!(f128);
77+
7478
trivial_arbitrary!(());
7579

7680
impl Arbitrary for bool {

‎library/kani/src/invariant.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,8 @@ trivial_invariant!(isize);
9696
// invariant that checks for NaN, infinite, or subnormal values.
9797
trivial_invariant!(f32);
9898
trivial_invariant!(f64);
99+
trivial_invariant!(f16);
100+
trivial_invariant!(f128);
99101

100102
trivial_invariant!(());
101103
trivial_invariant!(bool);

‎library/kani/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@
1818
#![allow(internal_features)]
1919
// Required for implementing memory predicates.
2020
#![feature(ptr_metadata)]
21+
#![feature(f16)]
22+
#![feature(f128)]
2123

2224
pub mod arbitrary;
2325
#[cfg(feature = "concrete_playback")]

‎library/kani_core/src/arbitrary.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,15 @@ macro_rules! generate_arbitrary {
8888
trivial_arbitrary!(i128);
8989
trivial_arbitrary!(isize);
9090

91+
// We do not constrain floating points values per type spec. Users must add assumptions to their
92+
// verification code if they want to eliminate NaN, infinite, or subnormal.
93+
trivial_arbitrary!(f32);
94+
trivial_arbitrary!(f64);
95+
96+
// Similarly, we do not constraint values for non-standard floating types.
97+
trivial_arbitrary!(f16);
98+
trivial_arbitrary!(f128);
99+
91100
nonzero_arbitrary!(NonZeroU8, u8);
92101
nonzero_arbitrary!(NonZeroU16, u16);
93102
nonzero_arbitrary!(NonZeroU32, u32);

‎library/kani_core/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@
1717
1818
#![feature(no_core)]
1919
#![no_core]
20+
#![feature(f16)]
21+
#![feature(f128)]
2022

2123
mod arbitrary;
2224
mod mem;

‎rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-06-27"
5+
channel = "nightly-2024-06-28"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)