diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index ce3c9fc1b7a2..a9e2740836e5 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -156,7 +156,7 @@ fabsf32 | Yes | | fabsf64 | Yes | | fadd_fast | Yes | | fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) | -float_to_int_unchecked | No | | +float_to_int_unchecked | Partial | [#3629](https://github.com/model-checking/kani/issues/3629) | floorf32 | Yes | | floorf64 | Yes | | fmaf32 | Partial | Results are overapproximated | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index c31dc6597a99..97b13e5f4185 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -384,6 +384,14 @@ impl GotocCtx<'_> { let binop_stmt = codegen_intrinsic_binop!(div); self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span) } + Intrinsic::FloatToIntUnchecked => self.codegen_float_to_int_unchecked( + intrinsic_str, + fargs.remove(0), + farg_types[0], + place, + ret_ty, + loc, + ), Intrinsic::FloorF32 => codegen_simple_intrinsic!(Floorf), Intrinsic::FloorF64 => codegen_simple_intrinsic!(Floor), Intrinsic::FmafF32 => codegen_simple_intrinsic!(Fmaf), @@ -1917,6 +1925,57 @@ impl GotocCtx<'_> { Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) } } + + /// Checks that the floating-point value is: + /// 1. Finite (i.e. neither infinite nor NaN) + /// 2. Its truncated value is in range of the target integer + /// then performs the cast to the target type + pub fn codegen_float_to_int_unchecked( + &mut self, + intrinsic: &str, + expr: Expr, + ty: Ty, + place: &Place, + res_ty: Ty, + loc: Location, + ) -> Stmt { + let finite_check = self.codegen_assert_assume( + expr.clone().is_finite(), + PropertyClass::ArithmeticOverflow, + format!("{intrinsic}: attempt to convert a non-finite value to an integer").as_str(), + loc, + ); + + assert!(res_ty.kind().is_integral()); + assert!(ty.kind().is_float()); + let TyKind::RigidTy(integral_ty) = res_ty.kind() else { + panic!( + "Expected intrinsic `{}` type to be `RigidTy`, but found: `{:?}`", + intrinsic, res_ty + ); + }; + let TyKind::RigidTy(RigidTy::Float(float_type)) = ty.kind() else { + panic!("Expected intrinsic `{}` type to be `Float`, but found: `{:?}`", intrinsic, ty); + }; + let mm = self.symbol_table.machine_model(); + let in_range = utils::codegen_in_range_expr(&expr, float_type, integral_ty, mm); + + let range_check = self.codegen_assert_assume( + in_range, + PropertyClass::ArithmeticOverflow, + format!("{intrinsic}: attempt to convert a value out of range of the target integer") + .as_str(), + loc, + ); + + let int_type = self.codegen_ty_stable(res_ty); + let cast = expr.cast_to(int_type); + + Stmt::block( + vec![finite_check, range_check, self.codegen_expr_to_place_stable(place, cast, loc)], + loc, + ) + } } fn instance_args(instance: &Instance) -> GenericArgs { diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs new file mode 100644 index 000000000000..a50353b7c96d --- /dev/null +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs @@ -0,0 +1,435 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains utilities related to floating-point types + +use cbmc::{MachineModel, goto_program::Expr}; +use stable_mir::ty::{FloatTy, IntTy, RigidTy, UintTy}; + +/// This function creates a boolean expression that the given `float_expr` when truncated is in the range of `integral_ty`. +/// +/// The expression it generates is in the form: +/// +/// `float_expr > lower_bound && float_expr < upper_bound` +/// +/// i.e., the comparison is performed in terms of floats +/// +/// Generally, the lower bound for an integral type is `MIN - 1` and the upper bound is `MAX + 1`. +/// For example, for `i16`, the lower bound is `i16::MIN - 1` (-32769) and the upper bound is `i16::MAX + 1` (32768) +/// Similarly, for `u8`, the lower bound is `u8::MIN - 1` (-1) and the upper bound is `u8::MAX + 1` (256) +/// +/// However, due to the floating-point imprecision, not every value has a representation. +/// For example, while `i16::MIN - 1` (-32769) and `u8::MAX + 1` (256) can be accurately represented as `f32` and `f64`, +/// `i32::MIN - 1` (-2147483649) cannot be represented in `f32` (the closest `f32` value is -2147483648). +/// See https://www.h-schmidt.net/FloatConverter/IEEE754.html +/// +/// 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. +/// +/// 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`. +/// +/// 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: +/// https://github.com/rust-lang/rust/blob/096277e989d6de11c3077472fc05778e261e7b8e/src/tools/miri/src/helpers.rs#L1003 +/// but it's not clear what it does for `i128` and `u128`. +pub fn codegen_in_range_expr( + float_expr: &Expr, + float_ty: FloatTy, + integral_ty: RigidTy, + mm: &MachineModel, +) -> Expr { + match float_ty { + FloatTy::F32 => { + let (lower, upper) = get_bounds_f32(integral_ty, mm); + let mut in_range = Expr::bool_true(); + // Avoid unnecessary comparison against -∞ or ∞ + if lower != f32::NEG_INFINITY { + in_range = in_range.and(float_expr.clone().gt(Expr::float_constant(lower))); + } + if upper != f32::INFINITY { + in_range = in_range.and(float_expr.clone().lt(Expr::float_constant(upper))); + } + in_range + } + FloatTy::F64 => { + let (lower, upper) = get_bounds_f64(integral_ty, mm); + let mut in_range = Expr::bool_true(); + if lower != f64::NEG_INFINITY { + in_range = in_range.and(float_expr.clone().gt(Expr::double_constant(lower))); + } + if upper != f64::INFINITY { + in_range = in_range.and(float_expr.clone().lt(Expr::double_constant(upper))); + } + in_range + } + _ => unimplemented!(), + } +} + +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 +const F32_I16_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x47]; // 32768.0 +const F32_I32_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xCF]; // -2147483904.0 +const F32_I32_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x4F]; // 2147483648.0 +const F32_I64_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xDF]; // -9223373136366403584.0 +const F32_I64_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x5F]; // 9223372036854775808.0 +// The next value is determined manually and not via test: +const F32_I128_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xFF]; // -170141203742878835383357727663135391744.0 +const F32_I128_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x7F]; // 170141183460469231731687303715884105728.0 + +const F64_I8_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x60, 0xC0]; // -129.0 +const F64_I8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x60, 0x40]; // 128.0 +const F64_I16_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0xE0, 0xC0]; // -32769.0 +const F64_I16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x40]; // 32768.0 +const F64_I32_LOWER: [u8; 8] = [0x00, 0x00, 0x20, 0x00, 0x00, 0x00, 0xE0, 0xC1]; // -2147483649.0 +const F64_I32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x41]; // 2147483648.0 +const F64_I64_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC3]; // -9223372036854777856.0 +const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43]; // 9223372036854775808.0 +// The next value is determined manually and not via test: +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 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 +const F32_U32_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x4F]; // 4294967296.0 +const F32_U64_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x5F]; // 18446744073709551616.0 +// The largest f32 value fits in a u128, so there is no upper bound +const F32_U128_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x7F]; // inf + +const F64_U_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0xBF]; // -1.0 +const F64_U8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x70, 0x40]; // 256.0 +const F64_U16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x40]; // 65536.0 +const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41]; // 4294967296.0 +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::MAX or u::MAX +/// lower is the largest `f32` 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. +/// `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. +/// `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_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) { + match integral_ty { + RigidTy::Int(int_ty) => get_bounds_f32_int(int_ty, mm), + RigidTy::Uint(uint_ty) => get_bounds_f32_uint(uint_ty, mm), + _ => unreachable!(), + } +} + +fn get_bounds_f64(integral_ty: RigidTy, mm: &MachineModel) -> (f64, f64) { + match integral_ty { + RigidTy::Int(int_ty) => get_bounds_f64_int(int_ty, mm), + RigidTy::Uint(uint_ty) => get_bounds_f64_uint(uint_ty, mm), + _ => unreachable!(), + } +} + +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 { + UintTy::U8 => f32::from_le_bytes(F32_U8_UPPER), + UintTy::U16 => f32::from_le_bytes(F32_U16_UPPER), + UintTy::U32 => f32::from_le_bytes(F32_U32_UPPER), + UintTy::U64 => f32::from_le_bytes(F32_U64_UPPER), + UintTy::U128 => f32::from_le_bytes(F32_U128_UPPER), + UintTy::Usize => match mm.pointer_width { + 32 => f32::from_le_bytes(F32_U32_UPPER), + 64 => f32::from_le_bytes(F32_U64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + +fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) { + let lower = f64::from_le_bytes(F64_U_LOWER); + let upper = match uint_ty { + UintTy::U8 => f64::from_le_bytes(F64_U8_UPPER), + UintTy::U16 => f64::from_le_bytes(F64_U16_UPPER), + UintTy::U32 => f64::from_le_bytes(F64_U32_UPPER), + UintTy::U64 => f64::from_le_bytes(F64_U64_UPPER), + UintTy::U128 => f64::from_le_bytes(F64_U128_UPPER), + UintTy::Usize => match mm.pointer_width { + 32 => f64::from_le_bytes(F64_U32_UPPER), + 64 => f64::from_le_bytes(F64_U64_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), + IntTy::I16 => f32::from_le_bytes(F32_I16_LOWER), + IntTy::I32 => f32::from_le_bytes(F32_I32_LOWER), + IntTy::I64 => f32::from_le_bytes(F32_I64_LOWER), + IntTy::I128 => f32::from_le_bytes(F32_I128_LOWER), + IntTy::Isize => match mm.pointer_width { + 32 => f32::from_le_bytes(F32_I32_LOWER), + 64 => f32::from_le_bytes(F32_I64_LOWER), + _ => unreachable!(), + }, + }; + + let upper = match int_ty { + IntTy::I8 => f32::from_le_bytes(F32_I8_UPPER), + IntTy::I16 => f32::from_le_bytes(F32_I16_UPPER), + IntTy::I32 => f32::from_le_bytes(F32_I32_UPPER), + IntTy::I64 => f32::from_le_bytes(F32_I64_UPPER), + IntTy::I128 => f32::from_le_bytes(F32_I128_UPPER), + IntTy::Isize => match mm.pointer_width { + 32 => f32::from_le_bytes(F32_I32_UPPER), + 64 => f32::from_le_bytes(F32_I64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + +fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) { + let lower = match int_ty { + IntTy::I8 => f64::from_le_bytes(F64_I8_LOWER), + IntTy::I16 => f64::from_le_bytes(F64_I16_LOWER), + IntTy::I32 => f64::from_le_bytes(F64_I32_LOWER), + IntTy::I64 => f64::from_le_bytes(F64_I64_LOWER), + IntTy::I128 => f64::from_le_bytes(F64_I128_LOWER), + IntTy::Isize => match mm.pointer_width { + 32 => f64::from_le_bytes(F64_I32_LOWER), + 64 => f64::from_le_bytes(F64_I64_LOWER), + _ => unreachable!(), + }, + }; + let upper = match int_ty { + IntTy::I8 => f64::from_le_bytes(F64_I8_UPPER), + IntTy::I16 => f64::from_le_bytes(F64_I16_UPPER), + IntTy::I32 => f64::from_le_bytes(F64_I32_UPPER), + IntTy::I64 => f64::from_le_bytes(F64_I64_UPPER), + IntTy::I128 => f64::from_le_bytes(F64_I128_UPPER), + IntTy::Isize => match mm.pointer_width { + 32 => f64::from_le_bytes(F64_I32_UPPER), + 64 => f64::from_le_bytes(F64_I64_UPPER), + _ => unreachable!(), + }, + }; + (lower, upper) +} + +#[cfg(test)] +mod tests { + use super::*; + use num::BigInt; + use num::FromPrimitive; + + macro_rules! check_lower_f32 { + ($val:ident, $min:expr) => { + let f = f32::from_le_bytes($val); + assert!(BigInt::from_f32(f.trunc()).unwrap() < BigInt::from($min)); + assert!(BigInt::from_f32(f.next_up().trunc()).unwrap() >= BigInt::from($min)); + }; + } + + macro_rules! check_upper_f32 { + ($val:ident, $max:expr) => { + let f = f32::from_le_bytes($val); + assert!(BigInt::from_f32(f.trunc()).unwrap() > BigInt::from($max)); + assert!(BigInt::from_f32(f.next_down().trunc()).unwrap() <= BigInt::from($max)); + }; + } + + #[test] + fn check_f32_bounds() { + // check that the bounds are correct, i.e. that for lower (upper) bounds: + // 1. the value when truncated is strictly smaller (larger) than i::MIN or u::MIN (i::MAX or u::MAX) + // 2. the next higher (lower) value when truncated is greater (smaller) than or equal to i::MIN or u::MIN (i::MAX or u::MAX) + + check_lower_f32!(F32_U_LOWER, u8::MIN); + + check_upper_f32!(F32_U8_UPPER, u8::MAX); + check_upper_f32!(F32_U16_UPPER, u16::MAX); + check_upper_f32!(F32_U32_UPPER, u32::MAX); + check_upper_f32!(F32_U64_UPPER, u64::MAX); + // 128 is not needed because the upper bounds is infinity + // Instead, check that `u128::MAX` is larger than the largest f32 value + assert!(f32::MAX < u128::MAX as f32); + + check_lower_f32!(F32_I8_LOWER, i8::MIN); + check_lower_f32!(F32_I16_LOWER, i16::MIN); + check_lower_f32!(F32_I32_LOWER, i32::MIN); + check_lower_f32!(F32_I64_LOWER, i64::MIN); + check_lower_f32!(F32_I128_LOWER, i128::MIN); + + check_upper_f32!(F32_I8_UPPER, i8::MAX); + check_upper_f32!(F32_I16_UPPER, i16::MAX); + check_upper_f32!(F32_I32_UPPER, i32::MAX); + check_upper_f32!(F32_I64_UPPER, i64::MAX); + check_upper_f32!(F32_I128_UPPER, i128::MAX); + } + + macro_rules! check_lower_f64 { + ($val:ident, $min:expr) => { + let f = f64::from_le_bytes($val); + assert!(BigInt::from_f64(f.trunc()).unwrap() < BigInt::from($min)); + assert!(BigInt::from_f64(f.next_up().trunc()).unwrap() >= BigInt::from($min)); + }; + } + + macro_rules! check_upper_f64 { + ($val:ident, $max:expr) => { + let f = f64::from_le_bytes($val); + assert!(BigInt::from_f64(f.trunc()).unwrap() > BigInt::from($max)); + assert!(BigInt::from_f64(f.next_down().trunc()).unwrap() <= BigInt::from($max)); + }; + } + + #[test] + fn check_f64_bounds() { + // check that the bounds are correct, i.e. that for lower (upper) bounds: + // 1. the value when truncated is strictly smaller (larger) than {i, u}::MIN ({i, u}::MAX) + // 2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}::MIN ({i, u}::MAX) + + check_lower_f64!(F64_U_LOWER, u8::MIN); + + check_upper_f64!(F64_U8_UPPER, u8::MAX); + check_upper_f64!(F64_U16_UPPER, u16::MAX); + check_upper_f64!(F64_U32_UPPER, u32::MAX); + check_upper_f64!(F64_U64_UPPER, u64::MAX); + check_upper_f64!(F64_U128_UPPER, u128::MAX); + + check_lower_f64!(F64_I8_LOWER, i8::MIN); + check_lower_f64!(F64_I16_LOWER, i16::MIN); + check_lower_f64!(F64_I32_LOWER, i32::MIN); + check_lower_f64!(F64_I64_LOWER, i64::MIN); + check_lower_f64!(F64_I128_LOWER, i128::MIN); + + check_upper_f64!(F64_I8_UPPER, i8::MAX); + check_upper_f64!(F64_I16_UPPER, i16::MAX); + check_upper_f64!(F64_I32_UPPER, i32::MAX); + check_upper_f64!(F64_I64_UPPER, i64::MAX); + check_upper_f64!(F64_I128_UPPER, i128::MAX); + } + + macro_rules! find_upper_fn { + ($fn_name:ident, $float_ty:ty) => { + fn $fn_name(start: u128) -> $float_ty { + let mut current = start + 1; + let mut f = current as $float_ty; + + while f.trunc() as u128 <= start { + let f1 = (current + 1) as $float_ty; + let f2 = f.next_up(); + f = if f1 > f2 { f1 } else { f2 }; + current = f as u128; + } + f + } + }; + } + + macro_rules! find_lower_fn { + ($fn_name:ident, $float_ty:ty) => { + fn $fn_name(start: i128) -> $float_ty { + let mut current = start - 1; + let mut f = current as $float_ty; + + while f.trunc() >= start as $float_ty { + let f1 = (current - 1) as $float_ty; + let f2 = f.next_down(); + f = if f1 < f2 { f1 } else { f2 }; + current = f as i128; + } + f + } + }; + } + + find_lower_fn!(find_lower_f32, f32); + find_upper_fn!(find_upper_f32, f32); + find_lower_fn!(find_lower_f64, f64); + find_upper_fn!(find_upper_f64, f64); + + macro_rules! find_and_print { + (f32, $var_name:expr, $fn_name:ident, $start:expr) => { + let f = $fn_name($start); + let bytes = f.to_le_bytes(); + println!("const {}: [u8; 4] = [0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}]; // {f:.1}", $var_name, bytes[0], bytes[1], bytes[2], bytes[3]); + }; + (f64, $var_name:expr, $fn_name:ident, $start:expr) => { + let f = $fn_name($start); + let bytes = f.to_le_bytes(); + println!("const {}: [u8; 8] = [0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}]; // {f:.1}", $var_name, bytes[0], bytes[1], bytes[2], bytes[3], bytes[4], bytes[5], bytes[6], bytes[7]); + }; + } + + #[test] + /// This test generates most of the bounds. To run it do: + /// `cargo test -p kani-compiler generate_bounds -- --nocapture` + fn generate_bounds() { + find_and_print!(f32, "F32_I8_LOWER", find_lower_f32, i8::MIN as i128); + find_and_print!(f32, "F32_I8_UPPER", find_upper_f32, i8::MAX as u128); + find_and_print!(f32, "F32_I16_LOWER", find_lower_f32, i16::MIN as i128); + find_and_print!(f32, "F32_I16_UPPER", find_upper_f32, i16::MAX as u128); + find_and_print!(f32, "F32_I32_LOWER", find_lower_f32, i32::MIN as i128); + find_and_print!(f32, "F32_I32_UPPER", find_upper_f32, i32::MAX as u128); + find_and_print!(f32, "F32_I64_LOWER", find_lower_f32, i64::MIN as i128); + find_and_print!(f32, "F32_I64_UPPER", find_upper_f32, i64::MAX as u128); + // cannot use because of overflow + //find_and_print!(f32, "F32_I128_LOWER", find_lower_f32, i128::MIN as i128); + find_and_print!(f32, "F32_I128_UPPER", find_upper_f32, i128::MAX as u128); + println!(); + find_and_print!(f64, "F64_I8_LOWER", find_lower_f64, i8::MIN as i128); + find_and_print!(f64, "F64_I8_UPPER", find_upper_f64, i8::MAX as u128); + find_and_print!(f64, "F64_I16_LOWER", find_lower_f64, i16::MIN as i128); + find_and_print!(f64, "F64_I16_UPPER", find_upper_f64, i16::MAX as u128); + find_and_print!(f64, "F64_I32_LOWER", find_lower_f64, i32::MIN as i128); + find_and_print!(f64, "F64_I32_UPPER", find_upper_f64, i32::MAX as u128); + find_and_print!(f64, "F64_I64_LOWER", find_lower_f64, i64::MIN as i128); + find_and_print!(f64, "F64_I64_UPPER", find_upper_f64, i64::MAX as u128); + // cannot use because of overflow + //find_and_print!(f64, "F64_I128_LOWER", find_lower_f64, i128::MIN as i128); + find_and_print!(f64, "F64_I128_UPPER", find_upper_f64, i128::MAX as u128); + println!(); + find_and_print!(f32, "F32_U_LOWER", find_lower_f32, u8::MIN as i128); + find_and_print!(f32, "F32_U8_UPPER", find_upper_f32, u8::MAX as u128); + find_and_print!(f32, "F32_U16_UPPER", find_upper_f32, u16::MAX as u128); + find_and_print!(f32, "F32_U32_UPPER", find_upper_f32, u32::MAX as u128); + find_and_print!(f32, "F32_U64_UPPER", find_upper_f32, u64::MAX as u128); + // cannot use because of overflow + //find_and_print!(f32, "F32_U128_UPPER", find_upper_f32, u128::MAX as u128); + println!(); + find_and_print!(f64, "F64_U_LOWER", find_lower_f64, u8::MIN as i128); + find_and_print!(f64, "F64_U8_UPPER", find_upper_f64, u8::MAX as u128); + find_and_print!(f64, "F64_U16_UPPER", find_upper_f64, u16::MAX as u128); + find_and_print!(f64, "F64_U32_UPPER", find_upper_f64, u32::MAX as u128); + find_and_print!(f64, "F64_U64_UPPER", find_upper_f64, u64::MAX as u128); + // cannot use because of overflow + //find_and_print!(f64, "F64_U128_UPPER", find_upper_f64, u128::MAX as u128); + } +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs index 9d832146e3e8..8f176510d348 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs @@ -4,12 +4,14 @@ //! This module provides utils used across Kani mod debug; +mod float_utils; mod names; #[allow(clippy::module_inception)] mod utils; // TODO clean this up +pub use float_utils::*; pub use names::*; pub use utils::*; diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 13a12751bd07..0121975b11a2 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -63,6 +63,7 @@ pub enum Intrinsic { FabsF64, FaddFast, FdivFast, + FloatToIntUnchecked, FloorF32, FloorF64, FmafF32, @@ -283,6 +284,14 @@ impl Intrinsic { assert_sig_matches!(sig, _, _ => _); Self::FdivFast } + "float_to_int_unchecked" => { + assert_sig_matches!(sig, RigidTy::Float(_) => _); + assert!(matches!( + sig.output().kind(), + TyKind::RigidTy(RigidTy::Int(_)) | TyKind::RigidTy(RigidTy::Uint(_)) + )); + Self::FloatToIntUnchecked + } "fmul_fast" => { assert_sig_matches!(sig, _, _ => _); Self::FmulFast diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 52b9331fb29d..9558b4159224 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -16,6 +16,7 @@ #![feature(f128)] #![feature(f16)] #![feature(non_exhaustive_omitted_patterns_lint)] +#![feature(float_next_up_down)] extern crate rustc_abi; extern crate rustc_ast; extern crate rustc_ast_pretty; diff --git a/tests/expected/intrinsics/float-to-int/non_finite.expected b/tests/expected/intrinsics/float-to-int/non_finite.expected new file mode 100644 index 000000000000..703853398bf2 --- /dev/null +++ b/tests/expected/intrinsics/float-to-int/non_finite.expected @@ -0,0 +1,5 @@ +Failed Checks: float_to_int_unchecked: attempt to convert a non-finite value to an integer +Verification failed for - check_neg_inf +Verification failed for - check_inf +Verification failed for - check_nan +Complete - 0 successfully verified harnesses, 3 failures, 3 total. diff --git a/tests/expected/intrinsics/float-to-int/non_finite.rs b/tests/expected/intrinsics/float-to-int/non_finite.rs new file mode 100644 index 000000000000..1aace2f7d403 --- /dev/null +++ b/tests/expected/intrinsics/float-to-int/non_finite.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(core_intrinsics)] + +//! Check that Kani flags a conversion of a NaN or INFINITY to an int via +//! `float_to_int_unchecked` + +#[kani::proof] +fn check_nan() { + let f: f32 = f32::NAN; + let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) }; +} + +#[kani::proof] +fn check_inf() { + let f: f32 = f32::INFINITY; + let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) }; +} + +#[kani::proof] +fn check_neg_inf() { + let f: f32 = f32::NEG_INFINITY; + let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) }; +} diff --git a/tests/expected/intrinsics/float-to-int/oob.expected b/tests/expected/intrinsics/float-to-int/oob.expected new file mode 100644 index 000000000000..f862df90f706 --- /dev/null +++ b/tests/expected/intrinsics/float-to-int/oob.expected @@ -0,0 +1,14 @@ +Failed Checks: float_to_int_unchecked: attempt to convert a value out of range of the target integer + +Verification failed for - check_u16_upper +Verification failed for - check_u64_upper +Verification failed for - check_usize_upper +Verification failed for - check_u32_upper +Verification failed for - check_u8_upper +Verification failed for - check_u128_lower +Verification failed for - check_u32_lower +Verification failed for - check_u8_lower +Verification failed for - check_u64_lower +Verification failed for - check_usize_lower +Verification failed for - check_u16_lower +Complete - 1 successfully verified harnesses, 11 failures, 12 total. diff --git a/tests/expected/intrinsics/float-to-int/oob.rs b/tests/expected/intrinsics/float-to-int/oob.rs new file mode 100644 index 000000000000..a49cf89ca82c --- /dev/null +++ b/tests/expected/intrinsics/float-to-int/oob.rs @@ -0,0 +1,41 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(core_intrinsics)] + +//! Check that Kani flags a conversion of an out-of-bounds float value to an int +//! via `float_to_int_unchecked` + +macro_rules! check_unsigned_lower { + ($name:ident, $t:ty) => { + #[kani::proof] + fn $name() { + let x: f32 = kani::any_where(|v: &f32| v.is_finite() && *v <= -1.0); + let _u: $t = unsafe { std::intrinsics::float_to_int_unchecked(x) }; + } + }; +} + +check_unsigned_lower!(check_u8_lower, u8); +check_unsigned_lower!(check_u16_lower, u16); +check_unsigned_lower!(check_u32_lower, u32); +check_unsigned_lower!(check_u64_lower, u64); +check_unsigned_lower!(check_u128_lower, u128); +check_unsigned_lower!(check_usize_lower, usize); + +macro_rules! check_unsigned_upper { + ($name:ident, $t:ty, $v:expr) => { + #[kani::proof] + fn $name() { + let x: f32 = kani::any_where(|v: &f32| v.is_finite() && *v >= $v); + let _u: $t = unsafe { std::intrinsics::float_to_int_unchecked(x) }; + } + }; +} + +check_unsigned_upper!(check_u8_upper, u8, (1u128 << 8) as f32); +check_unsigned_upper!(check_u16_upper, u16, (1u128 << 16) as f32); +check_unsigned_upper!(check_u32_upper, u32, (1u128 << 32) as f32); +check_unsigned_upper!(check_u64_upper, u64, (1u128 << 64) as f32); +// this harness should pass +check_unsigned_upper!(check_u128_upper, u128, f32::INFINITY); +check_unsigned_upper!(check_usize_upper, usize, (1u128 << 64) as f32); diff --git a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs new file mode 100644 index 000000000000..4797669b9b61 --- /dev/null +++ b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs @@ -0,0 +1,49 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(core_intrinsics)] + +// Check that the `float_to_int_unchecked` intrinsic works as expected + +use std::intrinsics::float_to_int_unchecked; + +macro_rules! check_float_to_int_unchecked { + ($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) }; + assert_eq!(u as $float_ty, f.trunc()); + }; +} + +#[kani::proof] +fn check_f32_to_int_unchecked() { + check_float_to_int_unchecked!(f32, u8); + check_float_to_int_unchecked!(f32, u16); + check_float_to_int_unchecked!(f32, u32); + check_float_to_int_unchecked!(f32, u64); + check_float_to_int_unchecked!(f32, u128); + check_float_to_int_unchecked!(f32, usize); + check_float_to_int_unchecked!(f32, i8); + check_float_to_int_unchecked!(f32, i16); + check_float_to_int_unchecked!(f32, i32); + check_float_to_int_unchecked!(f32, i64); + check_float_to_int_unchecked!(f32, i128); + check_float_to_int_unchecked!(f32, isize); +} + +#[kani::proof] +fn check_f64_to_int_unchecked() { + check_float_to_int_unchecked!(f64, u8); + check_float_to_int_unchecked!(f64, u16); + check_float_to_int_unchecked!(f64, u32); + check_float_to_int_unchecked!(f64, u64); + check_float_to_int_unchecked!(f64, u128); + check_float_to_int_unchecked!(f64, usize); + check_float_to_int_unchecked!(f64, i8); + check_float_to_int_unchecked!(f64, i16); + check_float_to_int_unchecked!(f64, i32); + check_float_to_int_unchecked!(f64, i64); + check_float_to_int_unchecked!(f64, i128); + check_float_to_int_unchecked!(f64, isize); +}