-
Notifications
You must be signed in to change notification settings - Fork 119
Fix BigFloat.FromInt incorrectly using string constructor
#1037
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
Conversation
shazqadeer
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am approving the PR with low confidence since I am not an expert in floating point. Perhaps @zvonimir, who is familiar with both floating point and Boogie, can also take a look.
|
@fabiomadge : Thanks for the PR. Please look into why some of the regression tests are failing. |
|
On it, thanks! |
- Fix overly aggressive subnormal overflow detection that was incorrectly promoting valid subnormals to normal numbers - Add proper handling for 0.5 × smallest subnormal to round to zero per IEEE 754 round-to-nearest-even rules - Fix complete underflow path for values below minimum subnormal exponent - Add comprehensive test coverage for subnormal edge cases Also adds many unit tests.
… bigfloat_refactor
|
@shazqadeer I spoke with @zvonimir and he won't immediately get to it. If you're ok with it, I'd like to merge now and revisit this, in case we end up finding any issues. |
|
Approved. Thanks for the PR. |
|
I don't have a compelling explanation for what went wrong, but installing .NET 6 on the runner solved the build issue we encountered after merging the README.md changes. |
|
I have seen the CI to be flaky in the past occasionally. A retry can often do the job. Please retry after reverting your change to the runner. I would like to see if that fixes the problem. |
|
It took three retries, but as finally worked. |
This PR fixes a critical bug in
BigFloat.FromInt()where it improperly used the string constructor, causing arithmetic failures. The fix introduces IEEE 754-compliant conversions, removes redundant fields, and adds 177 comprehensive tests to ensure correctness.The Bug: FromInt Misused the String Constructor
The
valuefield in BigFloat was designed to store only special values ("NaN","+oo","-oo"), with empty string ("") indicating a normal numeric value. However,FromIntwas incorrectly implemented:This stored regular integers as strings in the value field (e.g.,
"42"), breaking the invariant that value should only contain special values or be empty. This caused arithmetic operations to fail because:value != "" and try to handle"42"as a special valueThe Fix
Other Improvements
This fix ensures that integer-to-float conversions work correctly and participate properly in arithmetic operations.