Add support for simd insert/extract intrinsics #354
Conversation
There was a problem hiding this comment.
Code looks great but after reading #308 I would like to make sure that there is no support for these builtins in CBMC before we try to implement them ourselves. This is not easy to do, but for instance looking at this file I can tell there exists support for shuffle builtins. In that case, the right thing to do would be to:
- Add a constructor for vector shuffle expressions.
- Define how vector shuffle expressions are converted into the associated ireps.
- Test that the verification results are the ones that we expect.
In some cases, we may ask CBMC developers for support via ireps if there are good reasons.
As an example, you can take a look to the count intrinsics (ctlz, cttz & friends) defined there. We do not handle them ourselves but rather we let CBMC process them by emitting an irep and nothing else.
src/test/cbmc/SIMD/Operators/main.rs
Outdated
| // Indexing into the vectors | ||
| assert!(z.1 == 2); | ||
| assert!(z.0 == 1); | ||
|
|
||
| { | ||
| let y_0: i64 = unsafe { simd_extract(y, 0) }; | ||
| let y_1: i64 = unsafe { simd_extract(y, 1) }; | ||
| assert!(y_0 == 0); | ||
| assert!(y_1 == 1); | ||
| let m = unsafe { simd_insert(y, 0, 1) }; | ||
| let n = unsafe { simd_insert(y, 1, 5) }; | ||
| assert!(m.0 == 1 && m.1 == 1); | ||
| assert!(n.0 == 0 && n.1 == 5); | ||
| } |
There was a problem hiding this comment.
I would create another folder in SIMD and put this test in there.
| assert_op!(res_rem, simd_rem, v, z, 0, 1); | ||
| assert_op!(res_rem, simd_rem, v, z, 0, 1); | ||
| assert_op!(res_shr, simd_shl, z, z, 2, 8); | ||
| assert_op!(res_shl, simd_shl, z, z, 2, 8); |
| } | ||
| "simd_ge" => codegen_intrinsic_binop!(ge), | ||
| "simd_gt" => codegen_intrinsic_binop!(gt), | ||
| "simd_insert" => { |
There was a problem hiding this comment.
Maybe put this code into a function? So we can keep one-liners for SIMD intrinsics. But first let's talk about what support does CBMC provide for them.
|
After entirely too much investigation, I've got this example: CBMC outputs: Which I believe is confirmation that CBMC doesn't implement these kinds of intrinsics (inserts). This makes sense as I'm guessing the idiomatic C code is to just do the assignment ( |
|
Yes, your example shows that the insert/extract builtins are not implemented. But array indices seem to be working well so I am happy with this proposal. Thanks for the investigation! |
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <[email protected]>
2 participants
Description of changes:
Adds support for two new intrinsics:
simd_extractandsimd_insert.Resolved issues:
Resolves #308
Call-outs:
cast_toto thesimd_inserttranslation to avoid[main.assertion.5] line 50 Reached assignment statement with unequal types Signedbv { width: 64 } Signedbv { width: 32 }: FAILUREfrom CBMC.simd_insertbut I did justunwrapthe base type in there, and I'm not sure if there's a better way to do that that would aid debugging later.P = simd_insert(e, i, v)asT tmp; tmp = e; e[i] = v; P=tmpwherePis our inputPlace. We could maybe doP=e; P[i] = v;if that's not violating any assumptions of the translation. Would get rid of a temp.Testing:
How is this change tested? Added to an existing test case.
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.