From 8c19967085da0f76edbdbf58e9bf6a50f3389c41 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 8 Nov 2024 16:57:24 -0800 Subject: [PATCH 1/2] Add support for f16 and f128 in float_to_int_unchecked intrinsic --- .../utils/float_utils.rs | 199 +++++++++++++++++- .../intrinsics/float-to-int/oob_f128.expected | 13 ++ .../intrinsics/float-to-int/oob_f128.rs | 29 +++ .../Intrinsics/FloatToInt/float_to_int.rs | 43 ++++ 4 files changed, 283 insertions(+), 1 deletion(-) create mode 100644 tests/expected/intrinsics/float-to-int/oob_f128.expected create mode 100644 tests/expected/intrinsics/float-to-int/oob_f128.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs index a50353b7c96d..3944767c5e81 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs @@ -46,6 +46,18 @@ pub fn codegen_in_range_expr( mm: &MachineModel, ) -> Expr { match float_ty { + FloatTy::F16 => { + let (lower, upper) = get_bounds_f16(integral_ty, mm); + let mut in_range = Expr::bool_true(); + // Avoid unnecessary comparison against -∞ or ∞ + if lower != f16::NEG_INFINITY { + in_range = in_range.and(float_expr.clone().gt(Expr::float16_constant(lower))); + } + if upper != f16::INFINITY { + in_range = in_range.and(float_expr.clone().lt(Expr::float16_constant(upper))); + } + in_range + } FloatTy::F32 => { let (lower, upper) = get_bounds_f32(integral_ty, mm); let mut in_range = Expr::bool_true(); @@ -69,10 +81,31 @@ pub fn codegen_in_range_expr( } in_range } - _ => unimplemented!(), + FloatTy::F128 => { + let (lower, upper) = get_bounds_f128(integral_ty, mm); + let mut in_range = Expr::bool_true(); + if lower != f128::NEG_INFINITY { + in_range = in_range.and(float_expr.clone().gt(Expr::float128_constant(lower))); + } + if upper != f128::INFINITY { + in_range = in_range.and(float_expr.clone().lt(Expr::float128_constant(upper))); + } + in_range + } } } +const F16_I8_LOWER: [u8; 2] = [0x08, 0xD8]; +const F16_I8_UPPER: [u8; 2] = [0x00, 0x58]; +const F16_I16_LOWER: [u8; 2] = [0x01, 0xF8]; +const F16_I16_UPPER: [u8; 2] = [0x00, 0x78]; +const F16_I32_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf +const F16_I32_UPPER: [u8; 2] = [0x00, 0x7C]; // inf +const F16_I64_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf +const F16_I64_UPPER: [u8; 2] = [0x00, 0x7C]; // inf +const F16_I128_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf +const F16_I128_UPPER: [u8; 2] = [0x00, 0x7C]; // inf + const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0 const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0 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]; const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0 const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0 +const F128_I8_LOWER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x06, 0xC0, +]; +const F128_I8_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x06, 0x40, +]; +const F128_I16_LOWER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x0E, 0xC0, +]; +const F128_I16_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0E, 0x40, +]; +const F128_I32_LOWER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x1E, 0xC0, +]; +const F128_I32_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x1E, 0x40, +]; +const F128_I64_LOWER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0xC0, +]; +const F128_I64_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0x40, +]; +const F128_I128_LOWER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0xC0, +]; +const F128_I128_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0x40, +]; + +const F16_U_LOWER: [u8; 2] = [0x00, 0xBC]; +const F16_U8_UPPER: [u8; 2] = [0x00, 0x5C]; +const F16_U16_UPPER: [u8; 2] = [0x00, 0x7C]; // inf +const F16_U32_UPPER: [u8; 2] = [0x00, 0x7C]; // inf +const F16_U64_UPPER: [u8; 2] = [0x00, 0x7C]; // inf +const F16_U128_UPPER: [u8; 2] = [0x00, 0x7C]; // inf + const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0 const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0 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]; const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0 const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0 +const F128_U_LOWER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xFF, 0xBF, +]; +const F128_U8_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x07, 0x40, +]; +const F128_U16_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0F, 0x40, +]; +const F128_U32_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x1F, 0x40, +]; +const F128_U64_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3F, 0x40, +]; +const F128_U128_UPPER: [u8; 16] = [ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0x40, +]; + /// upper is the smallest `f32` that after truncation is strictly larger than i::MAX or u::MAX /// lower is the largest `f32` that after truncation is strictly smaller than i::MIN or u::MIN /// @@ -135,6 +225,14 @@ const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47] /// /// For all unsigned types, lower is -1.0 because the next higher number, when /// truncated is -0.0 (or 0.0) which is not strictly smaller than `u::MIN` +fn get_bounds_f16(integral_ty: RigidTy, mm: &MachineModel) -> (f16, f16) { + match integral_ty { + RigidTy::Int(int_ty) => get_bounds_f16_int(int_ty, mm), + RigidTy::Uint(uint_ty) => get_bounds_f16_uint(uint_ty, mm), + _ => unreachable!(), + } +} + fn get_bounds_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) { match integral_ty { 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) { } } +fn get_bounds_f128(integral_ty: RigidTy, mm: &MachineModel) -> (f128, f128) { + match integral_ty { + RigidTy::Int(int_ty) => get_bounds_f128_int(int_ty, mm), + RigidTy::Uint(uint_ty) => get_bounds_f128_uint(uint_ty, mm), + _ => unreachable!(), + } +} + +fn get_bounds_f16_uint(uint_ty: UintTy, mm: &MachineModel) -> (f16, f16) { + let lower: f16 = f16::from_le_bytes(F16_U_LOWER); + let upper: f16 = match uint_ty { + UintTy::U8 => f16::from_le_bytes(F16_U8_UPPER), + UintTy::U16 => f16::from_le_bytes(F16_U16_UPPER), + UintTy::U32 => f16::from_le_bytes(F16_U32_UPPER), + UintTy::U64 => f16::from_le_bytes(F16_U64_UPPER), + UintTy::U128 => f16::from_le_bytes(F16_U128_UPPER), + UintTy::Usize => match mm.pointer_width { + 32 => f16::from_le_bytes(F16_U32_UPPER), + 64 => f16::from_le_bytes(F16_U64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) { let lower: f32 = f32::from_le_bytes(F32_U_LOWER); let upper: f32 = match uint_ty { @@ -185,6 +308,52 @@ fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) { (lower, upper) } +fn get_bounds_f128_uint(uint_ty: UintTy, mm: &MachineModel) -> (f128, f128) { + let lower = f128::from_le_bytes(F128_U_LOWER); + let upper = match uint_ty { + UintTy::U8 => f128::from_le_bytes(F128_U8_UPPER), + UintTy::U16 => f128::from_le_bytes(F128_U16_UPPER), + UintTy::U32 => f128::from_le_bytes(F128_U32_UPPER), + UintTy::U64 => f128::from_le_bytes(F128_U64_UPPER), + UintTy::U128 => f128::from_le_bytes(F128_U128_UPPER), + UintTy::Usize => match mm.pointer_width { + 32 => f128::from_le_bytes(F128_U32_UPPER), + 64 => f128::from_le_bytes(F128_U64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + +fn get_bounds_f16_int(int_ty: IntTy, mm: &MachineModel) -> (f16, f16) { + let lower = match int_ty { + IntTy::I8 => f16::from_le_bytes(F16_I8_LOWER), + IntTy::I16 => f16::from_le_bytes(F16_I16_LOWER), + IntTy::I32 => f16::from_le_bytes(F16_I32_LOWER), + IntTy::I64 => f16::from_le_bytes(F16_I64_LOWER), + IntTy::I128 => f16::from_le_bytes(F16_I128_LOWER), + IntTy::Isize => match mm.pointer_width { + 32 => f16::from_le_bytes(F16_I32_LOWER), + 64 => f16::from_le_bytes(F16_I64_LOWER), + _ => unreachable!(), + }, + }; + + let upper = match int_ty { + IntTy::I8 => f16::from_le_bytes(F16_I8_UPPER), + IntTy::I16 => f16::from_le_bytes(F16_I16_UPPER), + IntTy::I32 => f16::from_le_bytes(F16_I32_UPPER), + IntTy::I64 => f16::from_le_bytes(F16_I64_UPPER), + IntTy::I128 => f16::from_le_bytes(F16_I128_UPPER), + IntTy::Isize => match mm.pointer_width { + 32 => f16::from_le_bytes(F16_I32_UPPER), + 64 => f16::from_le_bytes(F16_I64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) { let lower = match int_ty { 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) { (lower, upper) } +fn get_bounds_f128_int(int_ty: IntTy, mm: &MachineModel) -> (f128, f128) { + let lower = match int_ty { + IntTy::I8 => f128::from_le_bytes(F128_I8_LOWER), + IntTy::I16 => f128::from_le_bytes(F128_I16_LOWER), + IntTy::I32 => f128::from_le_bytes(F128_I32_LOWER), + IntTy::I64 => f128::from_le_bytes(F128_I64_LOWER), + IntTy::I128 => f128::from_le_bytes(F128_I128_LOWER), + IntTy::Isize => match mm.pointer_width { + 32 => f128::from_le_bytes(F128_I32_LOWER), + 64 => f128::from_le_bytes(F128_I64_LOWER), + _ => unreachable!(), + }, + }; + let upper = match int_ty { + IntTy::I8 => f128::from_le_bytes(F128_I8_UPPER), + IntTy::I16 => f128::from_le_bytes(F128_I16_UPPER), + IntTy::I32 => f128::from_le_bytes(F128_I32_UPPER), + IntTy::I64 => f128::from_le_bytes(F128_I64_UPPER), + IntTy::I128 => f128::from_le_bytes(F128_I128_UPPER), + IntTy::Isize => match mm.pointer_width { + 32 => f128::from_le_bytes(F128_I32_UPPER), + 64 => f128::from_le_bytes(F128_I64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + #[cfg(test)] mod tests { use super::*; diff --git a/tests/expected/intrinsics/float-to-int/oob_f128.expected b/tests/expected/intrinsics/float-to-int/oob_f128.expected new file mode 100644 index 000000000000..020299489786 --- /dev/null +++ b/tests/expected/intrinsics/float-to-int/oob_f128.expected @@ -0,0 +1,13 @@ +Verification failed for - check_cast_i16 +Verification failed for - check_cast_i128 +Verification failed for - check_cast_u8 +Verification failed for - check_cast_u32 +Verification failed for - check_cast_u64 +Verification failed for - check_cast_u16 +Verification failed for - check_cast_u128 +Verification failed for - check_cast_usize +Verification failed for - check_cast_i8 +Verification failed for - check_cast_i64 +Verification failed for - check_cast_isize +Verification failed for - check_cast_i32 +Complete - 0 successfully verified harnesses, 12 failures, 12 total. diff --git a/tests/expected/intrinsics/float-to-int/oob_f128.rs b/tests/expected/intrinsics/float-to-int/oob_f128.rs new file mode 100644 index 000000000000..b28cc0360d8a --- /dev/null +++ b/tests/expected/intrinsics/float-to-int/oob_f128.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(f128)] + +// Check that `f128::MAX` does not fit in some integer types + +macro_rules! check_cast { + ($name:ident, $t:ty) => { + #[kani::proof] + fn $name() { + let x = f128::MAX; + let _u: $t = unsafe { x.to_int_unchecked() }; + } + }; +} + +check_cast!(check_cast_u8, u8); +check_cast!(check_cast_u16, u16); +check_cast!(check_cast_u32, u32); +check_cast!(check_cast_u64, u64); +check_cast!(check_cast_u128, u128); +check_cast!(check_cast_usize, usize); + +check_cast!(check_cast_i8, i8); +check_cast!(check_cast_i16, i16); +check_cast!(check_cast_i32, i32); +check_cast!(check_cast_i64, i64); +check_cast!(check_cast_i128, i128); +check_cast!(check_cast_isize, isize); diff --git a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs index 4797669b9b61..b05fe1133ed8 100644 --- a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs +++ b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(core_intrinsics)] +#![feature(f16)] +#![feature(f128)] // Check that the `float_to_int_unchecked` intrinsic works as expected @@ -16,6 +18,31 @@ macro_rules! check_float_to_int_unchecked { }; } +macro_rules! check_float_to_int_unchecked_no_assert { + ($float_ty:ty, $int_ty:ty) => { + let f: $float_ty = kani::any_where(|f: &$float_ty| { + f.is_finite() && *f > <$int_ty>::MIN as $float_ty && *f < <$int_ty>::MAX as $float_ty + }); + let _u: $int_ty = unsafe { float_to_int_unchecked(f) }; + }; +} + +#[kani::proof] +fn check_f16_to_int_unchecked() { + check_float_to_int_unchecked_no_assert!(f16, u8); + check_float_to_int_unchecked_no_assert!(f16, u16); + check_float_to_int_unchecked_no_assert!(f16, u32); + check_float_to_int_unchecked_no_assert!(f16, u64); + check_float_to_int_unchecked_no_assert!(f16, u128); + check_float_to_int_unchecked_no_assert!(f16, usize); + check_float_to_int_unchecked_no_assert!(f16, i8); + check_float_to_int_unchecked_no_assert!(f16, i16); + check_float_to_int_unchecked_no_assert!(f16, i32); + check_float_to_int_unchecked_no_assert!(f16, i64); + check_float_to_int_unchecked_no_assert!(f16, i128); + check_float_to_int_unchecked_no_assert!(f16, isize); +} + #[kani::proof] fn check_f32_to_int_unchecked() { check_float_to_int_unchecked!(f32, u8); @@ -47,3 +74,19 @@ fn check_f64_to_int_unchecked() { check_float_to_int_unchecked!(f64, i128); check_float_to_int_unchecked!(f64, isize); } + +#[kani::proof] +fn check_f128_to_int_unchecked() { + check_float_to_int_unchecked_no_assert!(f128, u8); + check_float_to_int_unchecked_no_assert!(f128, u16); + check_float_to_int_unchecked_no_assert!(f128, u32); + check_float_to_int_unchecked_no_assert!(f128, u64); + check_float_to_int_unchecked_no_assert!(f128, u128); + check_float_to_int_unchecked_no_assert!(f128, usize); + check_float_to_int_unchecked_no_assert!(f128, i8); + check_float_to_int_unchecked_no_assert!(f128, i16); + check_float_to_int_unchecked_no_assert!(f128, i32); + check_float_to_int_unchecked_no_assert!(f128, i64); + check_float_to_int_unchecked_no_assert!(f128, i128); + check_float_to_int_unchecked_no_assert!(f128, isize); +} From 97a1d246acee9844e51bb81f598b8314eac2d23b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 11 Nov 2024 10:03:43 -0800 Subject: [PATCH 2/2] Clarify doc comments --- .../utils/float_utils.rs | 31 +++++++------------ 1 file changed, 12 insertions(+), 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs index 3944767c5e81..d220c02f2466 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs @@ -25,8 +25,9 @@ use stable_mir::ty::{FloatTy, IntTy, RigidTy, UintTy}; /// /// If we were to just use `MIN - 1`, the resulting expression may exclude values that are actually in range. /// For example, `float_expr > ((i32::MIN - 1) as f32)` would expand to `float_expr > -2147483649 as f32` which -/// would result in `float_expr > -2147483648.0`. This expression incorrectly exlcudes a valid `i32` -/// value: `i32::MIN` = -2147483648. +/// would result in `float_expr > -2147483648.0`. This expression incorrectly excludes a valid `i32` +/// value: `i32::MIN` = -2147483648. Note that CBMC for example uses the formula above which +/// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488 /// /// Thus, to determine the lower bound, we need to find the **largest** floating-point value that is /// less than or equal to `MIN - 1`. @@ -34,6 +35,10 @@ use stable_mir::ty::{FloatTy, IntTy, RigidTy, UintTy}; /// Similarly, to determine the upper bound, we need to find the smallest floating-point value that is /// greater than or equal to `MAX + 1`. /// +/// Note that generally, `MAX + 1` values (=2^x) can be precisely represented as floating-point numbers +/// Also, for all unsigned types, lower is -1.0 because the next higher number, when +/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u::MIN`. +/// /// An alternative approach would be to perform the float-to-int cast with a wider integer and /// then check if the wider integer value is in the range of the narrower integer value. /// This seems to be the approach used in MIRI: @@ -202,29 +207,17 @@ const F128_U128_UPPER: [u8; 16] = [ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0x40, ]; -/// upper is the smallest `f32` that after truncation is strictly larger than i::MAX or u::MAX -/// lower is the largest `f32` that after truncation is strictly smaller than i::MIN or u::MIN +/// For the `get_bounds_fXY` functions below (`get_bounds_f16`, `get_bounds_f32`, etc.): +/// upper is the smallest `fXY` that after truncation is strictly larger than i::MAX or u::MAX +/// lower is the largest `fXY` that after truncation is strictly smaller than i::MIN or u::MIN /// -/// For example, for `u8`, upper is 256.0 because the previous f32 (i.e. +/// For example, for `u8` and `f32`, upper is 256.0 because the previous f32 (i.e. /// `256_f32.next_down()` which is 255.9999847412109375) when truncated is 255.0, /// which is not strictly larger than `u8::MAX` /// -/// For `i16`, upper is 32768.0 because the previous f32 (i.e. +/// For `i16` and `f32`, upper is 32768.0 because the previous f32 (i.e. /// `32768_f32.next_down()`) when truncated is 32767, /// which is not strictly larger than `i16::MAX` -/// -/// Note that all upper bound values are 2^(w-1) which can be precisely -/// represented in f32 (verified using -/// https://www.h-schmidt.net/FloatConverter/IEEE754.html) -/// However, for lower bound values, which should be -2^(w-1)-1 (i.e. -/// i::MIN-1), not all of them can be represented in f32. -/// For instance, for w = 32, -2^(31)-1 = -2,147,483,649, but this number does -/// **not** have an f32 representation, and the next **smaller** number is -/// -2,147,483,904. Note that CBMC for example uses the formula above which -/// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488 -/// -/// For all unsigned types, lower is -1.0 because the next higher number, when -/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u::MIN` fn get_bounds_f16(integral_ty: RigidTy, mm: &MachineModel) -> (f16, f16) { match integral_ty { RigidTy::Int(int_ty) => get_bounds_f16_int(int_ty, mm),