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.

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 float_to_int_unchecked #3660

Merged
merged 12 commits into from
Nov 6, 2024

Conversation

zhassan-aws
Copy link
Contributor

@zhassan-aws zhassan-aws commented Oct 30, 2024

This PR adds support for the float_to_int_unchecked intrinsic for f32 and f64.

Towards #3629

Keeping it as draft till I add more tests.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Oct 30, 2024
@tautschnig
Copy link
Member

Please don't forget to update docs/src/rust-feature-support/intrinsics.md.

@zhassan-aws zhassan-aws marked this pull request as ready for review October 31, 2024 00:39
@zhassan-aws zhassan-aws requested a review from a team as a code owner October 31, 2024 00:39
@zhassan-aws
Copy link
Contributor Author

Please don't forget to update docs/src/rust-feature-support/intrinsics.md.

Thanks for the reminder. Added.

@zhassan-aws
Copy link
Contributor Author

This PR could use quite a bit of cleanup, especially around hard-coded values and unit tests. In particular, it's probably better to store the hard-coded values using their byte representation as opposed to their decimal one.

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we be worried about the cast using as logic?

@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented Oct 31, 2024

I did a fairly big overhaul of the PR in 08531f6:

  1. I've added all the constants using their byte representation. This is to avoid any questionable casts using as. These constants are now the single source of truth.
  2. I added unit tests that verify that all the values are indeed lower and upper bounds of the corresponding int/uint types. The tests use BigInt to guarantee they work for all int types.
  3. I removed the unit tests that were checking that the decimal value can be represented as f32/f64 because we're no longer using decimal values anywhere.

@celinval This should address some of your comments.

@celinval
Copy link
Contributor

celinval commented Nov 1, 2024

I'm really sorry, I think you might've misunderstood my comment about the as. I think we should be using as in the kani-compiler code since this is getting rustc's values as the source of truth.

My comment about the as is about Kani's implementation of casting float to integer using as. I would expect the same bounds to be used for both, but it sounds like we don't.

@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented Nov 1, 2024

I'm really sorry, I think you might've misunderstood my comment about the as. I think we should be using as in the kani-compiler code since this is getting rustc's values as the source of truth.

Not at all. I was planning to make this change before your comment. The reason is that casting a decimal value into a floating-point value can have surprising behavior. For example, this program:

    println!("{}", u32::MAX);
    let f1: f32 = u32::MAX as f32;
    let f2: f32 = u32::MAX as f32 + 1.0;
    let f3: f32 = (u32::MAX as u128 + 1) as f32;
    
    println!("{:.32}", f1);
    println!("{:.32}", f2);
    println!("{:.32}", f3);

prints:

4294967295
4294967296.00000000000000000000000000000000
4294967296.00000000000000000000000000000000
4294967296.00000000000000000000000000000000

So casting the decimal value u32::MAX (4294967295) to a float results in a different number. This is because the cast operation rounds to the nearest number that can be represented as an f32. In other words, when assigning an f32 a decimal value, the actual value it stores may end up being different (could be smaller or larger). This calculator, which @tautschnig pointed out to me helped me determine the correct bounds:

https://www.h-schmidt.net/FloatConverter/IEEE754.html

One way to specify a floating-point value unambiguously is to use the byte representation. This is the reason I switched to it.

@zhassan-aws
Copy link
Contributor Author

I made a few final touches:

  1. Moved most of the code to a new float_utils module to avoid polluting intrinsics.rs (Thanks @celinval for the suggestion)
  2. I added the code I used to determine the bounds as a unit test. If run with --nocapture, it'll print the constants.
  3. I added a small optimization that skips the comparison if the bound is +/- infinity.

@tautschnig @celinval Let me know if you want to take another look. Otherwise, I'll go ahead and merge.

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's fine by me. Thanks!

@zhassan-aws zhassan-aws added this pull request to the merge queue Nov 6, 2024
Merged via the queue into model-checking:main with commit 0dc09a7 Nov 6, 2024
27 checks passed
@zhassan-aws zhassan-aws deleted the float-to-int-intrinsic branch November 6, 2024 06:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants