Introduce simd_shuffle intrinsic #417

tedinski · 2021-08-11T20:56:05Z

Description of changes:

Add CBMC's vector_exprt to our gotoc representation.
Add support for the simd_shuffle instrinsics.
Add a test of the above.

Resolved issues:

Resolves #309

Call-outs:

TODO: I need to create some new issues about future follow-ups (e.g. getting CBMC to expose shuffle_vector_exprt for us?) and possibly link to them from the code.
I still have a TODO in the code about the type of the array index expressions we generate. Currently, I use a signed index. Unsigned causes CBMC to object:

--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_mult.cpp:73 function: convert_mult
Condition: it->type() == expr.type()
Reason: multiplication operands should have same type as expression

I'm going to investigate this before merging. It's possible I should be picking the type in some other way, but this is difficult to diagnose because it seems to be internal to CBMC's transformations (e.g. I think we put "array index" in the symbol table, but them CBMC is transforming that into "pointer + index*size" internally, and that's where the "mult" is coming from. A guess, for now. Perplexing because it would seem to imply that the "sizeof" a type has signed type internally?)

Testing:

How is this change tested? Added 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.

avanhatt · 2021-08-13T14:11:32Z

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

Could this be integrated into the match below instead of its own code block?

i if i.strip_prefix("simd_shuffle") => ...

Apparently this is an "if let guard" and is marked as experimental currently: https://github.com/rust-lang/rfcs/blob/master/text/2294-if-let-guard.md

I'm going to leave it as-is for now.

Why not have it at the end of the match with an starts_with guard?

We need to extract the suffix still. This is what's done in the LLVM code as well.

I don't think including it in the match would be any better.

Still, you can match the prefix, then extract the suffix before calling the codegen function.

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

src/test/cbmc/SIMD/Construction/main.rs

avanhatt

LGTM, with one testing suggestion

adpaco-aws · 2021-08-16T14:15:30Z

src/test/cbmc/SIMD/Construction/main.rs

I would move simd_shuffle testing into its own file.

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs

adpaco-aws · 2021-08-16T14:23:05Z

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

Why do you need this?

I think I don't anymore, will fix...

adpaco-aws · 2021-08-16T14:25:59Z

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

Why not have it at the end of the match with an starts_with guard?

Co-authored-by: Adrian Palacios <[email protected]>

tedinski · 2021-08-16T22:38:47Z

I think this has addressed everything except the nits about the match vs preceding if. I think there isn't any obviously better choice (except "if let guards", which isn't stable yet), and this style is what appears in some of the llvm codegen crate. IMO, let's just go with it.

danielsn · 2021-08-17T02:18:43Z

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

    }

+    pub fn vector_expr(typ: Type, elems: Vec<Expr>) -> Self {
+        if let Type::Vector { size, typ: value_typ } = typ.clone() {


Why is the clone needed here

The use of value_typ later is a partial move out of the value.

danielsn · 2021-08-17T02:22:26Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/intrinsic.rs

+
+        // An unsigned type here causes an invariant violation in CBMC.
+        // Issue: https://github.com/diffblue/cbmc/issues/6298
+        let st_rep = Type::ssize_t();


It might be clearer to just use Type::ssize_t() wherever this is used.

I had that thought too, but I felt like keeping it since it created a place for the comment about the CBMC issue.

* introduce simd_shuffle intrinsic * add links to cbmc issues in simd_shuffle comments * add assert for arguments length to simd instrinsic functions * typo fix Co-authored-by: Adrian Palacios <[email protected]> * separate simd_shuffle test from other tests Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

avanhatt reviewed Aug 13, 2021

View reviewed changes

tedinski marked this pull request as ready for review August 13, 2021 22:55

avanhatt reviewed Aug 16, 2021

View reviewed changes

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs Outdated Show resolved Hide resolved

src/test/cbmc/SIMD/Construction/main.rs Outdated Show resolved Hide resolved

avanhatt approved these changes Aug 16, 2021

View reviewed changes

adpaco-aws reviewed Aug 16, 2021

View reviewed changes

tedinski and others added 5 commits August 16, 2021 22:28

introduce simd_shuffle intrinsic

9ad3225

add links to cbmc issues in simd_shuffle comments

7ab47de

add assert for arguments length to simd instrinsic functions

67c4c7b

typo fix

d6c24b3

Co-authored-by: Adrian Palacios <[email protected]>

separate simd_shuffle test from other tests

d15569a

tedinski force-pushed the simd-shuffle branch from 68a6c36 to d15569a Compare August 16, 2021 22:35

Merge branch 'main-154-2021-08-06' into simd-shuffle

9f6c6fb

danielsn reviewed Aug 17, 2021

View reviewed changes

adpaco-aws approved these changes Aug 17, 2021

View reviewed changes

adpaco-aws merged commit 122281b into model-checking:main-154-2021-08-06 Aug 17, 2021

adpaco-aws mentioned this pull request Aug 23, 2021

Codegen issues in rand crate #111

Closed

tedinski deleted the simd-shuffle branch July 8, 2022 22:32

github-actions bot mentioned this pull request Feb 11, 2025

Toolchain upgrade to nightly-2025-02-11 failed #3884

Closed

Introduce simd_shuffle intrinsic #417

Introduce simd_shuffle intrinsic #417

Uh oh!

Conversation

tedinski commented Aug 11, 2021

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

avanhatt Aug 13, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

avanhatt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tedinski commented Aug 16, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

avanhatt Aug 13, 2021 •

edited

Loading