Fuzz-like testers for developing explicit-rep checkers #346
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We should consistently hew to the convenient fiction that floating point types do not lose precision.
chiphogg
added a commit
that referenced
this pull request
Dec 9, 2024
The core enabling feature is the new "static cast checkers" library target. For each source and destination type, this target provides separate checks for overflow and truncation when static casting. We continue with our usual policy of treating floating point types as "value preserving". I did initially explore the possibility of treating large integer inputs as "truncating" when converted to a floating point type that can't represent them exactly. However, I found this made the library somewhat harder to reason about, for questionable benefit. Additionally, I think it is fair to assume that users intentionally entering the floating point domain have already accepted a kind of "magnitude based reasoning", and trying to split hairs about preserving exact integer values just felt too cute. With these static cast checkers in hand, the explicit-rep runtime conversion checkers become simple. We check the static cast to the common type, the unit conversion, and the final narrowing static cast to the destination type. To figure out how to write all these functions, I used some "fuzz-ish" utilities, which generated random values of various integral and floating point types, and performed various explicit-rep conversions. I checked that the round-trip conversion changed the value if-and-only-if `is_conversion_lossy` was true. After also taking intermediate sign flips into account (to handle some signed/unsigned conversion edge cases), I got to a point where integral-to-integral conversions always gave the right result. This gives me confidence in the overall approach. When floating point values came into the picture, I wasn't able to design a fully satisfactory policy to avoid both false positives and false negatives. However, I did get to a point where the kinds of errors I saw were ones I found acceptable, relating to "the usual floating point error". This was also what led me to embrace the policy of simply treating floating point destination types as value-preserving, consistent with the rest of the library. This machinery is not ready for prime time, but I posted it for posterity in the abandoned PR #346. I also updated the documentation, including making the floating point policy explicit. Fixes #110.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This just saves my existing work for posterity.
I'm going to make a PR and then immediately abandon it.