Skip to content

Add support to array-based SIMD#2633

Merged
celinval merged 3 commits into
model-checking:mainfrom
celinval:issue-2253-simd-array
Jul 31, 2023
Merged

Add support to array-based SIMD#2633
celinval merged 3 commits into
model-checking:mainfrom
celinval:issue-2253-simd-array

Conversation

@celinval
Copy link
Copy Markdown
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
Copy Markdown
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.

Comment thread kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Comment thread kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Comment thread kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Comment thread tests/kani/SIMD/array_simd_repr.rs Outdated
Comment thread tests/kani/SIMD/array_simd_repr.rs Outdated
Comment thread tests/kani/SIMD/multi_field_simd.rs Outdated
Comment thread kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@celinval celinval enabled auto-merge (squash) July 31, 2023 19:20
@celinval celinval merged commit c15294e into model-checking:main Jul 31, 2023
@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

Development

Successfully merging this pull request may close these issues.

ICE: Kani compiler crashes when initializing a SIMD struct Invalid projection on firecracker regression with the 2022-11-20 rust toolchain

2 participants