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 1 commit
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
199 changes: 198 additions & 1 deletion 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 @@ -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();
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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<N>::MAX or u<N>::MAX
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
///
Expand All @@ -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<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 +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 {
Expand Down Expand Up @@ -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),
Expand Down Expand Up @@ -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::*;
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);
43 changes: 43 additions & 0 deletions tests/kani/Intrinsics/FloatToInt/float_to_int.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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);
Expand Down Expand Up @@ -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);
}
Loading