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

Add support to array-based SIMD #2633

Merged
merged 3 commits into from
Jul 31, 2023

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Jul 28, 2023

Description of changes:

Originally, repr(simd) supported only multi-field form. An array based version was later added and it's likely to become the only supported way (rust-lang/compiler-team#621).

The array-based version is currently used in the standard library, and it is used to implement portable-simd. This change adds support to instantiating and using the array-based version.

Resolved issues:

Resolves #2590
Resolves #1926

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

We should still add more tests to check if all simd operations that Kani supports works with the array-based SIMD. I'm planning on doing that in a follow up PR.

Testing:

  • How is this change tested? New tests

  • Is this a refactor change?

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.

Originally, repr(simd) supported only multi-field form. An array
based version was later added and it's likely to become the only
supported way.

The array-based version is currently used in the standard library, and
to implement `portable-simd`. This change adds support to instantiating
and using the array-based version.

We should still add more tests to check if all simd operations that Kani
supports works with the array-based SIMD.
@celinval celinval requested a review from a team as a code owner July 28, 2023 01:39
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

Looks good, I'm just a little confused about what is it that the tests are doing.

tests/kani/SIMD/array_simd_repr.rs Outdated Show resolved Hide resolved
tests/kani/SIMD/array_simd_repr.rs Outdated Show resolved Hide resolved
tests/kani/SIMD/multi_field_simd.rs Outdated Show resolved Hide resolved
@celinval celinval enabled auto-merge (squash) July 31, 2023 19:20
@celinval celinval merged commit c15294e into model-checking:main Jul 31, 2023
12 checks passed
@celinval celinval mentioned this pull request Aug 3, 2023
4 tasks
celinval added a commit that referenced this pull request Aug 4, 2023
Change #2633 was incomplete and it doesn't work in the context of generic functions. This PR fixes that.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants