Skip to content

Commit

Permalink
Add support for f16 and f128 in float_to_int_unchecked intrinsic
Browse files Browse the repository at this point in the history
  • Loading branch information
@zhassan-aws
zhassan-aws committed Nov 9, 2024
1 parent 8400296 commit 9c4b070
Show file tree
Hide file tree
Showing 4 changed files with 255 additions and 2 deletions.
171 changes: 169 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,19 @@ pub fn codegen_in_range_expr(
mm: &MachineModel,
) -> Expr {
match float_ty {
FloatTy::F32 => {
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();
// Avoid unnecessary comparison against -∞ or ∞
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,24 @@ 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 +163,13 @@ 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
/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
///
Expand All @@ -135,6 +193,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 +217,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 +276,54 @@ 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 +381,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
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
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);
44 changes: 44 additions & 0 deletions tests/kani/Intrinsics/FloatToInt/float_to_int.rs
View file
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,32 @@ 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 +75,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);
}

0 comments on commit 9c4b070

Please sign in to comment.