Question about corner cases for to_int_unchecked

[Yenyun035]

We observed some imprecisions in to_int_unchecked results when a float is an extreme value. For example, values around 2147483646.4 (around i32::MAX) or -2147483647.7 (around i32::MIN). We are thinking about a better way to verify the result and appreciate any insights or guidance for it. @celinval @zhassan-aws

The check we have now is:

// inside a macro
#[kani::proof_for_contract($floatType::to_int_unchecked)]
pub fn $harness_name() {
    let num1: $floatType = kani::any::<$floatType>();
    let result = unsafe { num1.to_int_unchecked::<$intType>() };

    assert_eq!(result, num1 as $intType); // Might have a better way
}

// Theoretically, the contract would be (according to Kani PR#3742 https://github.com/model-checking/kani/pull/3742):
#[requires(self.is_finite() && kani::float::float_to_int_in_range::<Self, Int>(self))]
pub unsafe fn to_int_unchecked<Int>(self) -> Int where Self: FloatToInt<Int>

Assume that num1 (f32) is 2147483646.4 (i32 Max), I would imagine that i32 can fit the value, so to_int_unchecked should return 2147483647. However, when I tried:

let num1: f32 = 2147483646.4;
let expected: i32 = num1 as i32; // expected to be 2147483646, but got 2147483647. Tried `num1.trunc() as i32` as well.
let result: i32 = unsafe { num1.to_int_unchecked::<i32>() }; // -2147483648...

Another negative corner case:

let num1: f32 = -2147483647.7;
// or f1.trunc() as i32
let expected: i32 = num1 as i32; // expected to be -2147483647, but got -2147483648
let result: i32 = unsafe { num1.to_int_unchecked::<i32>() }; // -2147483648...

[zhassan-aws]

Hi @Yenyun035. Great question. The tricky thing about floating-point numbers is that not every decimal value has a floating-point representation. So when a value is assigned to a float, the actual value that gets stored might be different. One way to check if a value can be represented as a floating-point number is this calculator: https://www.h-schmidt.net/FloatConverter/IEEE754.html.

For your example, the value 2147483646.4 cannot be represented, and the actual value that gets stored is 2147483648. This is greater than i32::MAX, so Kani should flag the failure.

Another way to check if the value can be represented is to print it, e.g. using this program: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=89e9abccf943d6af537c6297ea9d2536. For 2147483646.4, it prints 2147483648.00, which is the actual value that gets stored.

[Yenyun035]

Thank you for sharing this! That is a really interesting behavior. No wonder printing out those float values gives me a completely different value.

In this case, can I assume that the kani::float::float_to_int_in_range in the contract can correctly flag such cases, and that the assert!(result, num1 as $intType) check would behave correctly?

[zhassan-aws]

In this case, can I assume that the kani::float::float_to_int_in_range in the contract can correctly flag such cases and that the assert!(result, num1 as $intType) check would behave correctly?

Yes to both questions.