Skip to content

Audit for truncf*#1250

Merged
adpaco-aws merged 9 commits intomodel-checking:mainfrom
adpaco-aws:audit-trunc
Jun 8, 2022
Merged

Audit for truncf*#1250
adpaco-aws merged 9 commits intomodel-checking:mainfrom
adpaco-aws:audit-trunc

Conversation

@adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Jun 3, 2022

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
tedinski
tedinski reviewed Jun 7, 2022
View reviewed changes
tests/kani/Intrinsics/Math/Rounding/Trunc/truncf32.rs Outdated
Copy link
Contributor

@tedinski tedinski Jun 7, 2022

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

@adpaco-aws adpaco-aws Jun 7, 2022

Choose a reason for hiding this comment

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

Yes.

Copy link
Contributor

@tedinski tedinski Jun 7, 2022

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

@adpaco-aws adpaco-aws Jun 7, 2022

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.

tedinski
tedinski approved these changes Jun 7, 2022
View reviewed changes
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
danielsn approved these changes Jun 8, 2022
View reviewed changes
@danielsn
Copy link
Contributor

danielsn commented Jun 8, 2022 •
edited
Loading

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

@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Jun 8, 2022

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
This was referenced Jun 8, 2022
Merged
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

2 more reviewers

@tedinski tedinski tedinski approved these changes

@danielsn danielsn danielsn approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@adpaco-aws @danielsn @tedinski