Skip to content

Commit 8c19967

Browse files
zhassan-awszhassan-aws
committed
Add support for f16 and f128 in float_to_int_unchecked intrinsic
1 parent 26c078e commit 8c19967

File tree

4 files changed

+283
-1
lines changed

4 files changed

+283
-1
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs‎

Lines changed: 198 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,18 @@ pub fn codegen_in_range_expr(
4646
mm: &MachineModel,
4747
) -> Expr {
4848
match float_ty {
49+
FloatTy::F16 => {
50+
let (lower, upper) = get_bounds_f16(integral_ty, mm);
51+
let mut in_range = Expr::bool_true();
52+
// Avoid unnecessary comparison against -∞ or ∞
53+
if lower != f16::NEG_INFINITY {
54+
in_range = in_range.and(float_expr.clone().gt(Expr::float16_constant(lower)));
55+
}
56+
if upper != f16::INFINITY {
57+
in_range = in_range.and(float_expr.clone().lt(Expr::float16_constant(upper)));
58+
}
59+
in_range
60+
}
4961
FloatTy::F32 => {
5062
let (lower, upper) = get_bounds_f32(integral_ty, mm);
5163
let mut in_range = Expr::bool_true();
@@ -69,10 +81,31 @@ pub fn codegen_in_range_expr(
6981
}
7082
in_range
7183
}
72-
_ => unimplemented!(),
84+
FloatTy::F128 => {
85+
let (lower, upper) = get_bounds_f128(integral_ty, mm);
86+
let mut in_range = Expr::bool_true();
87+
if lower != f128::NEG_INFINITY {
88+
in_range = in_range.and(float_expr.clone().gt(Expr::float128_constant(lower)));
89+
}
90+
if upper != f128::INFINITY {
91+
in_range = in_range.and(float_expr.clone().lt(Expr::float128_constant(upper)));
92+
}
93+
in_range
94+
}
7395
}
7496
}
7597

98+
const F16_I8_LOWER: [u8; 2] = [0x08, 0xD8];
99+
const F16_I8_UPPER: [u8; 2] = [0x00, 0x58];
100+
const F16_I16_LOWER: [u8; 2] = [0x01, 0xF8];
101+
const F16_I16_UPPER: [u8; 2] = [0x00, 0x78];
102+
const F16_I32_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf
103+
const F16_I32_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
104+
const F16_I64_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf
105+
const F16_I64_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
106+
const F16_I128_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf
107+
const F16_I128_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
108+
76109
const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
77110
const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0
78111
const F32_I16_LOWER: [u8; 4] = [0x00, 0x01, 0x00, 0xC7]; // -32769.0
@@ -97,6 +130,44 @@ const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43];
97130
const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0
98131
const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0
99132

133+
const F128_I8_LOWER: [u8; 16] = [
134+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x06, 0xC0,
135+
];
136+
const F128_I8_UPPER: [u8; 16] = [
137+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x06, 0x40,
138+
];
139+
const F128_I16_LOWER: [u8; 16] = [
140+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x0E, 0xC0,
141+
];
142+
const F128_I16_UPPER: [u8; 16] = [
143+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0E, 0x40,
144+
];
145+
const F128_I32_LOWER: [u8; 16] = [
146+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x1E, 0xC0,
147+
];
148+
const F128_I32_UPPER: [u8; 16] = [
149+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x1E, 0x40,
150+
];
151+
const F128_I64_LOWER: [u8; 16] = [
152+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0xC0,
153+
];
154+
const F128_I64_UPPER: [u8; 16] = [
155+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0x40,
156+
];
157+
const F128_I128_LOWER: [u8; 16] = [
158+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0xC0,
159+
];
160+
const F128_I128_UPPER: [u8; 16] = [
161+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0x40,
162+
];
163+
164+
const F16_U_LOWER: [u8; 2] = [0x00, 0xBC];
165+
const F16_U8_UPPER: [u8; 2] = [0x00, 0x5C];
166+
const F16_U16_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
167+
const F16_U32_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
168+
const F16_U64_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
169+
const F16_U128_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
170+
100171
const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0
101172
const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
102173
const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
@@ -112,6 +183,25 @@ const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41];
112183
const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0
113184
const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0
114185

186+
const F128_U_LOWER: [u8; 16] = [
187+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xFF, 0xBF,
188+
];
189+
const F128_U8_UPPER: [u8; 16] = [
190+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x07, 0x40,
191+
];
192+
const F128_U16_UPPER: [u8; 16] = [
193+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0F, 0x40,
194+
];
195+
const F128_U32_UPPER: [u8; 16] = [
196+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x1F, 0x40,
197+
];
198+
const F128_U64_UPPER: [u8; 16] = [
199+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3F, 0x40,
200+
];
201+
const F128_U128_UPPER: [u8; 16] = [
202+
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0x40,
203+
];
204+
115205
/// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX or u<N>::MAX
116206
/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
117207
///
@@ -135,6 +225,14 @@ const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]
135225
///
136226
/// For all unsigned types, lower is -1.0 because the next higher number, when
137227
/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
228+
fn get_bounds_f16(integral_ty: RigidTy, mm: &MachineModel) -> (f16, f16) {
229+
match integral_ty {
230+
RigidTy::Int(int_ty) => get_bounds_f16_int(int_ty, mm),
231+
RigidTy::Uint(uint_ty) => get_bounds_f16_uint(uint_ty, mm),
232+
_ => unreachable!(),
233+
}
234+
}
235+
138236
fn get_bounds_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) {
139237
match integral_ty {
140238
RigidTy::Int(int_ty) => get_bounds_f32_int(int_ty, mm),
@@ -151,6 +249,31 @@ fn get_bounds_f64(integral_ty: RigidTy, mm: &MachineModel) -> (f64, f64) {
151249
}
152250
}
153251

252+
fn get_bounds_f128(integral_ty: RigidTy, mm: &MachineModel) -> (f128, f128) {
253+
match integral_ty {
254+
RigidTy::Int(int_ty) => get_bounds_f128_int(int_ty, mm),
255+
RigidTy::Uint(uint_ty) => get_bounds_f128_uint(uint_ty, mm),
256+
_ => unreachable!(),
257+
}
258+
}
259+
260+
fn get_bounds_f16_uint(uint_ty: UintTy, mm: &MachineModel) -> (f16, f16) {
261+
let lower: f16 = f16::from_le_bytes(F16_U_LOWER);
262+
let upper: f16 = match uint_ty {
263+
UintTy::U8 => f16::from_le_bytes(F16_U8_UPPER),
264+
UintTy::U16 => f16::from_le_bytes(F16_U16_UPPER),
265+
UintTy::U32 => f16::from_le_bytes(F16_U32_UPPER),
266+
UintTy::U64 => f16::from_le_bytes(F16_U64_UPPER),
267+
UintTy::U128 => f16::from_le_bytes(F16_U128_UPPER),
268+
UintTy::Usize => match mm.pointer_width {
269+
32 => f16::from_le_bytes(F16_U32_UPPER),
270+
64 => f16::from_le_bytes(F16_U64_UPPER),
271+
_ => unreachable!(),
272+
},
273+
};
274+
(lower, upper)
275+
}
276+
154277
fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
155278
let lower: f32 = f32::from_le_bytes(F32_U_LOWER);
156279
let upper: f32 = match uint_ty {
@@ -185,6 +308,52 @@ fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
185308
(lower, upper)
186309
}
187310

311+
fn get_bounds_f128_uint(uint_ty: UintTy, mm: &MachineModel) -> (f128, f128) {
312+
let lower = f128::from_le_bytes(F128_U_LOWER);
313+
let upper = match uint_ty {
314+
UintTy::U8 => f128::from_le_bytes(F128_U8_UPPER),
315+
UintTy::U16 => f128::from_le_bytes(F128_U16_UPPER),
316+
UintTy::U32 => f128::from_le_bytes(F128_U32_UPPER),
317+
UintTy::U64 => f128::from_le_bytes(F128_U64_UPPER),
318+
UintTy::U128 => f128::from_le_bytes(F128_U128_UPPER),
319+
UintTy::Usize => match mm.pointer_width {
320+
32 => f128::from_le_bytes(F128_U32_UPPER),
321+
64 => f128::from_le_bytes(F128_U64_UPPER),
322+
_ => unreachable!(),
323+
},
324+
};
325+
(lower, upper)
326+
}
327+
328+
fn get_bounds_f16_int(int_ty: IntTy, mm: &MachineModel) -> (f16, f16) {
329+
let lower = match int_ty {
330+
IntTy::I8 => f16::from_le_bytes(F16_I8_LOWER),
331+
IntTy::I16 => f16::from_le_bytes(F16_I16_LOWER),
332+
IntTy::I32 => f16::from_le_bytes(F16_I32_LOWER),
333+
IntTy::I64 => f16::from_le_bytes(F16_I64_LOWER),
334+
IntTy::I128 => f16::from_le_bytes(F16_I128_LOWER),
335+
IntTy::Isize => match mm.pointer_width {
336+
32 => f16::from_le_bytes(F16_I32_LOWER),
337+
64 => f16::from_le_bytes(F16_I64_LOWER),
338+
_ => unreachable!(),
339+
},
340+
};
341+
342+
let upper = match int_ty {
343+
IntTy::I8 => f16::from_le_bytes(F16_I8_UPPER),
344+
IntTy::I16 => f16::from_le_bytes(F16_I16_UPPER),
345+
IntTy::I32 => f16::from_le_bytes(F16_I32_UPPER),
346+
IntTy::I64 => f16::from_le_bytes(F16_I64_UPPER),
347+
IntTy::I128 => f16::from_le_bytes(F16_I128_UPPER),
348+
IntTy::Isize => match mm.pointer_width {
349+
32 => f16::from_le_bytes(F16_I32_UPPER),
350+
64 => f16::from_le_bytes(F16_I64_UPPER),
351+
_ => unreachable!(),
352+
},
353+
};
354+
(lower, upper)
355+
}
356+
188357
fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
189358
let lower = match int_ty {
190359
IntTy::I8 => f32::from_le_bytes(F32_I8_LOWER),
@@ -242,6 +411,34 @@ fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
242411
(lower, upper)
243412
}
244413

414+
fn get_bounds_f128_int(int_ty: IntTy, mm: &MachineModel) -> (f128, f128) {
415+
let lower = match int_ty {
416+
IntTy::I8 => f128::from_le_bytes(F128_I8_LOWER),
417+
IntTy::I16 => f128::from_le_bytes(F128_I16_LOWER),
418+
IntTy::I32 => f128::from_le_bytes(F128_I32_LOWER),
419+
IntTy::I64 => f128::from_le_bytes(F128_I64_LOWER),
420+
IntTy::I128 => f128::from_le_bytes(F128_I128_LOWER),
421+
IntTy::Isize => match mm.pointer_width {
422+
32 => f128::from_le_bytes(F128_I32_LOWER),
423+
64 => f128::from_le_bytes(F128_I64_LOWER),
424+
_ => unreachable!(),
425+
},
426+
};
427+
let upper = match int_ty {
428+
IntTy::I8 => f128::from_le_bytes(F128_I8_UPPER),
429+
IntTy::I16 => f128::from_le_bytes(F128_I16_UPPER),
430+
IntTy::I32 => f128::from_le_bytes(F128_I32_UPPER),
431+
IntTy::I64 => f128::from_le_bytes(F128_I64_UPPER),
432+
IntTy::I128 => f128::from_le_bytes(F128_I128_UPPER),
433+
IntTy::Isize => match mm.pointer_width {
434+
32 => f128::from_le_bytes(F128_I32_UPPER),
435+
64 => f128::from_le_bytes(F128_I64_UPPER),
436+
_ => unreachable!(),
437+
},
438+
};
439+
(lower, upper)
440+
}
441+
245442
#[cfg(test)]
246443
mod tests {
247444
use super::*;

‎tests/expected/intrinsics/float-to-int/oob_f128.expected‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
Verification failed for - check_cast_i16
2+
Verification failed for - check_cast_i128
3+
Verification failed for - check_cast_u8
4+
Verification failed for - check_cast_u32
5+
Verification failed for - check_cast_u64
6+
Verification failed for - check_cast_u16
7+
Verification failed for - check_cast_u128
8+
Verification failed for - check_cast_usize
9+
Verification failed for - check_cast_i8
10+
Verification failed for - check_cast_i64
11+
Verification failed for - check_cast_isize
12+
Verification failed for - check_cast_i32
13+
Complete - 0 successfully verified harnesses, 12 failures, 12 total.

‎tests/expected/intrinsics/float-to-int/oob_f128.rs‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
#![feature(f128)]
4+
5+
// Check that `f128::MAX` does not fit in some integer types
6+
7+
macro_rules! check_cast {
8+
($name:ident, $t:ty) => {
9+
#[kani::proof]
10+
fn $name() {
11+
let x = f128::MAX;
12+
let _u: $t = unsafe { x.to_int_unchecked() };
13+
}
14+
};
15+
}
16+
17+
check_cast!(check_cast_u8, u8);
18+
check_cast!(check_cast_u16, u16);
19+
check_cast!(check_cast_u32, u32);
20+
check_cast!(check_cast_u64, u64);
21+
check_cast!(check_cast_u128, u128);
22+
check_cast!(check_cast_usize, usize);
23+
24+
check_cast!(check_cast_i8, i8);
25+
check_cast!(check_cast_i16, i16);
26+
check_cast!(check_cast_i32, i32);
27+
check_cast!(check_cast_i64, i64);
28+
check_cast!(check_cast_i128, i128);
29+
check_cast!(check_cast_isize, isize);

‎tests/kani/Intrinsics/FloatToInt/float_to_int.rs‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
#![feature(core_intrinsics)]
4+
#![feature(f16)]
5+
#![feature(f128)]
46

57
// Check that the `float_to_int_unchecked` intrinsic works as expected
68

@@ -16,6 +18,31 @@ macro_rules! check_float_to_int_unchecked {
1618
};
1719
}
1820

21+
macro_rules! check_float_to_int_unchecked_no_assert {
22+
($float_ty:ty, $int_ty:ty) => {
23+
let f: $float_ty = kani::any_where(|f: &$float_ty| {
24+
f.is_finite() && *f > <$int_ty>::MIN as $float_ty && *f < <$int_ty>::MAX as $float_ty
25+
});
26+
let _u: $int_ty = unsafe { float_to_int_unchecked(f) };
27+
};
28+
}
29+
30+
#[kani::proof]
31+
fn check_f16_to_int_unchecked() {
32+
check_float_to_int_unchecked_no_assert!(f16, u8);
33+
check_float_to_int_unchecked_no_assert!(f16, u16);
34+
check_float_to_int_unchecked_no_assert!(f16, u32);
35+
check_float_to_int_unchecked_no_assert!(f16, u64);
36+
check_float_to_int_unchecked_no_assert!(f16, u128);
37+
check_float_to_int_unchecked_no_assert!(f16, usize);
38+
check_float_to_int_unchecked_no_assert!(f16, i8);
39+
check_float_to_int_unchecked_no_assert!(f16, i16);
40+
check_float_to_int_unchecked_no_assert!(f16, i32);
41+
check_float_to_int_unchecked_no_assert!(f16, i64);
42+
check_float_to_int_unchecked_no_assert!(f16, i128);
43+
check_float_to_int_unchecked_no_assert!(f16, isize);
44+
}
45+
1946
#[kani::proof]
2047
fn check_f32_to_int_unchecked() {
2148
check_float_to_int_unchecked!(f32, u8);
@@ -47,3 +74,19 @@ fn check_f64_to_int_unchecked() {
4774
check_float_to_int_unchecked!(f64, i128);
4875
check_float_to_int_unchecked!(f64, isize);
4976
}
77+
78+
#[kani::proof]
79+
fn check_f128_to_int_unchecked() {
80+
check_float_to_int_unchecked_no_assert!(f128, u8);
81+
check_float_to_int_unchecked_no_assert!(f128, u16);
82+
check_float_to_int_unchecked_no_assert!(f128, u32);
83+
check_float_to_int_unchecked_no_assert!(f128, u64);
84+
check_float_to_int_unchecked_no_assert!(f128, u128);
85+
check_float_to_int_unchecked_no_assert!(f128, usize);
86+
check_float_to_int_unchecked_no_assert!(f128, i8);
87+
check_float_to_int_unchecked_no_assert!(f128, i16);
88+
check_float_to_int_unchecked_no_assert!(f128, i32);
89+
check_float_to_int_unchecked_no_assert!(f128, i64);
90+
check_float_to_int_unchecked_no_assert!(f128, i128);
91+
check_float_to_int_unchecked_no_assert!(f128, isize);
92+
}

0 commit comments

Comments
 (0)