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

fix: use saturating casts in lean_float_to_uint8 to avoid UB #1458

Merged
merged 1 commit into from Aug 11, 2022

Conversation

digama0
Copy link
Collaborator

@digama0 digama0 commented Aug 11, 2022

The C Standard, 6.3.1.4, paragraph 1 [ISO/IEC 9899:2011], says,

When a finite value of real floating type is converted to an integer type other than _Bool, the fractional part is discarded (i.e., the value is truncated toward zero). If the value of the integral part cannot be represented by the integer type, the behavior is undefined.

This means that the simple implementation uint8_t f(double d) { return (uint8_t)d; } is undefined behavior for large values of d. The correct version is to check that the value would truncate to a value in the range of the target type, that is, 0 <= d < 2^8. We have to write out 2^8 as a double constant though since this doesn't appear in any standard headers.

This changes the observable behavior of the cast from wrapping modulo 2^8 to saturating, but I think this behavior is more defensible (and it's also what rust did when they hit the same issue).

See also the Zulip thread.

@Kha
Copy link
Member

Kha commented Aug 11, 2022

This should probably documented in docstrings...? :)

@digama0
Copy link
Collaborator Author

digama0 commented Aug 11, 2022

I assure you, the float functions will all be documented extensively. That will be another PR though.

@leodemoura leodemoura merged commit d8c6c82 into leanprover:master Aug 11, 2022
@digama0 digama0 deleted the float_saturate branch August 11, 2022 20:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants