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

Audit for truncf* #1250

Merged
merged 9 commits into from
Jun 8, 2022
Merged

Audit for truncf* #1250

merged 9 commits into from
Jun 8, 2022

Conversation

adpaco-aws
Copy link
Contributor

Description of changes:

Restores and completes the audit for the truncf32 (truncf) and truncf64 (trunc) intrinsics.

Resolved issues:

Part of #1163
Part of #1025

Call-outs:

Testing:

  • How is this change tested? Adds 2 tests.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

@adpaco-aws adpaco-aws requested a review from a team as a code owner June 3, 2022 21:32
@adpaco-aws adpaco-aws changed the title Audit trunc Audit for truncf* Jun 3, 2022
let trunc_res = unsafe { std::intrinsics::truncf32(x) };

// The expected result is the number minus its fractional part
let expected_res = x - x.fract();
Copy link
Contributor

Choose a reason for hiding this comment

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

Does fract use trunc under the hood?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes.

Copy link
Contributor

Choose a reason for hiding this comment

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

Is that a problem for the test, if it's just running (x - f) == (x - f)?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, it's probably better to avoid it altogether.

It's quite hard to test these functions with symbolic values. Because of that, I've broken the truncf32 test into a three harnesses: One that tests a property for all values and two other for concrete values.

Please let me know what you think! Any suggestions on other tests are welcome.

Copy link
Contributor

@tedinski tedinski left a comment

Choose a reason for hiding this comment

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

I'm not sure how to do better either, so LGTM

@danielsn
Copy link
Contributor

danielsn commented Jun 8, 2022

Can you test 0 <= x - trunc(x) < 1

@adpaco-aws
Copy link
Contributor Author

Thanks @danielsn , this is now testing that property and a few more concrete cases.

@adpaco-aws adpaco-aws merged commit dcb2992 into model-checking:main Jun 8, 2022
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.

3 participants