Skip to content

Support for fast math intrinsics#804

Merged
adpaco-aws merged 9 commits intomodel-checking:mainfrom
adpaco-aws:fast-math
Feb 9, 2022
Merged

Support for fast math intrinsics#804
adpaco-aws merged 9 commits intomodel-checking:mainfrom
adpaco-aws:fast-math

Conversation

@adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Feb 7, 2022

Description of changes:

Models fast math intrinsics as regular floating point operations. Includes function to check inputs are finite arguments. Adds 16 new test cases (8 positive, 8 negative) for testing fast math intrinsics.

Resolved issues:

Resolves #788

Call-outs:

Testing:

  • How is this change tested? Existing regression + 16 new 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 February 7, 2022 23:24
}
}

pub fn get_stmts(&self) -> Option<&Vec<Stmt>> {
Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is part of an earlier version where the intrinsics where encoded in a block statement, so I needed to retrieve statements within in order to prepend the finite checks. This version does not use it, but I figured it could be useful for something else. We can remove it otherwise.

Copy link
Contributor

Choose a reason for hiding this comment

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

If you do keep it, can you please add a comment?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Added a comment.

@adpaco-aws adpaco-aws changed the title Fast math Support for fast math intrinsics Feb 7, 2022
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Nice test coverage! Just minor comments.

(false, false) => kani::assume(x > f64::MIN - y),
_ => (),
}
let _z = unsafe { std::intrinsics::fadd_fast(x, y) };
Copy link
Contributor

Choose a reason for hiding this comment

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

Can you please assert that the result is equal to regular add? The same for the other tests.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Changed it so we assert it in the case of addition and substraction, as other operations show serious performance issues. Created #809 to revisit this.

}
}

pub fn get_stmts(&self) -> Option<&Vec<Stmt>> {
Copy link
Contributor

Choose a reason for hiding this comment

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

If you do keep it, can you please add a comment?

@adpaco-aws
Copy link
Contributor Author

Some changes I made:

  1. Added tests for f32 values so we now cover all floating point types.
  2. Changed tests to assert equality (w.r.t. regular operations) in the case of addition and substraction, but other operations show serious performance issues. Created Some fast math results cannot be practically compared #809 to revisit this topic later.
  3. Dropped support for frem_fast because testing showed unexpected results. Created Unimplemented intrinsic: frem_fast #810 to explain the issue and tackle it in the future.

@adpaco-aws adpaco-aws merged commit 1a41434 into model-checking:main Feb 9, 2022
@adpaco-aws adpaco-aws mentioned this pull request Feb 9, 2022
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Support for fast math intrinsics

* Add (failing) positive test for `fadd_fast`

* Undo change in `typecheck_binop_args`

* Encode fast math intrinsics as regular binops

* Add all tests for fast math intrinsics

* Add tests for 32-bit values and compare results

* Drop support for `frem_fast`

* Add comment to `get_stmts`
tedinski pushed a commit that referenced this pull request Apr 27, 2022
* Support for fast math intrinsics

* Add (failing) positive test for `fadd_fast`

* Undo change in `typecheck_binop_args`

* Encode fast math intrinsics as regular binops

* Add all tests for fast math intrinsics

* Add tests for 32-bit values and compare results

* Drop support for `frem_fast`

* Add comment to `get_stmts`
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.

Unimplemented intrinsics: Fast math for floating point numbers

2 participants