Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for f16 and f128 in float_to_int_unchecked intrinsic #3701

Merged
merged 3 commits into from
Nov 12, 2024
Merged

Add support for f16 and f128 in float_to_int_unchecked intrinsic #3701

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8c19967
Add support for f16 and f128 in float_to_int_unchecked intrinsic
zhassan-aws Nov 9, 2024
97a1d24
Clarify doc comments
zhassan-aws Nov 11, 2024
4709f82
Merge branch 'main' into float-to-int-f16-f128
zhassan-aws Nov 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
230 changes: 210 additions & 20 deletions kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,15 +25,20 @@ 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`.
/// For example, for `i32`, the largest such value is `-2147483904.0`
/// 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<N>::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:
Expand All @@ -46,6 +51,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();
Expand All @@ -69,10 +86,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
Expand All @@ -97,6 +135,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
Expand All @@ -112,29 +188,44 @@ 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

/// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX or u<N>::MAX
/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
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,
];

/// 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<N>::MAX or u<N>::MAX
/// lower is the largest `fXY` that after truncation is strictly smaller than i<N>::MIN or u<N>::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<N>::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<N>::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),
Expand All @@ -151,6 +242,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 {
Expand Down Expand Up @@ -185,6 +301,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),
Expand Down Expand Up @@ -242,6 +404,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::*;
Expand Down
13 changes: 13 additions & 0 deletions tests/expected/intrinsics/float-to-int/oob_f128.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
29 changes: 29 additions & 0 deletions tests/expected/intrinsics/float-to-int/oob_f128.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
Loading
Loading