From 8889078c9f8e578cb498933af59f829531ca1fa0 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Wed, 21 Jul 2021 19:51:42 +0000 Subject: [PATCH 1/4] support simd_extract intrinsic --- .../rustc_codegen_llvm/src/gotoc/intrinsic.rs | 5 +++++ src/test/cbmc/SIMD/Operators/main.rs | 15 +++++++++++++-- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 21384762c370..6e4fe988523b 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -375,6 +375,11 @@ impl<'tcx> GotocCtx<'tcx> { "simd_and" => codegen_intrinsic_binop!(bitand), "simd_div" => codegen_intrinsic_binop!(div), "simd_eq" => codegen_intrinsic_binop!(eq), + "simd_extract" => { + let vec = fargs.remove(0); + let index = fargs.remove(0); + self.codegen_expr_to_place(p, vec.index_array(index)) + } "simd_ge" => codegen_intrinsic_binop!(ge), "simd_gt" => codegen_intrinsic_binop!(gt), "simd_le" => codegen_intrinsic_binop!(le), diff --git a/src/test/cbmc/SIMD/Operators/main.rs b/src/test/cbmc/SIMD/Operators/main.rs index d9030338f864..a7da57e4d82f 100644 --- a/src/test/cbmc/SIMD/Operators/main.rs +++ b/src/test/cbmc/SIMD/Operators/main.rs @@ -18,6 +18,7 @@ extern "platform-intrinsic" { fn simd_and(x: T, y: T) -> T; fn simd_or(x: T, y: T) -> T; fn simd_xor(x: T, y: T) -> T; + fn simd_extract(x: T, idx: u32) -> U; } macro_rules! assert_op { @@ -35,14 +36,24 @@ fn main() { let z = i64x2(1, 2); let v = i64x2(1, 3); + // 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); + } + unsafe { assert_op!(res_add, simd_add, x, y, 0, 1); assert_op!(res_sub, simd_sub, x, y, 0, -1); assert_op!(res_mul, simd_mul, y, z, 0, 2); assert_op!(res_div, simd_div, v, z, 1, 1); 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); assert_op!(res_shr, simd_shr, z, y, 1, 1); assert_op!(res_and, simd_and, y, v, 0, 1); assert_op!(res_or, simd_or, x, y, 0, 1); From 36685dfc82d571425bde40bddd93a1ff090417b0 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Wed, 21 Jul 2021 21:17:39 +0000 Subject: [PATCH 2/4] support simd_insert intrinsic --- .../rustc_codegen_llvm/src/gotoc/intrinsic.rs | 16 ++++++++++++++++ src/test/cbmc/SIMD/Operators/main.rs | 5 +++++ 2 files changed, 21 insertions(+) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 6e4fe988523b..2f29cd9588fc 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -382,6 +382,22 @@ impl<'tcx> GotocCtx<'tcx> { } "simd_ge" => codegen_intrinsic_binop!(ge), "simd_gt" => codegen_intrinsic_binop!(gt), + "simd_insert" => { + let vec = fargs.remove(0); + let index = fargs.remove(0); + let newval = fargs.remove(0); + // Type checker should have ensured it's a vector type + let elem_ty = cbmc_ret_ty.base_type().unwrap().clone(); + let tmp = self.gen_temp_variable(cbmc_ret_ty, loc.clone()).to_expr(); + Stmt::block( + vec![ + Stmt::decl(tmp.clone(), Some(vec), loc.clone()), + tmp.clone().index_array(index).assign(newval.cast_to(elem_ty), loc.clone()), + self.codegen_expr_to_place(p, tmp), + ], + loc, + ) + } "simd_le" => codegen_intrinsic_binop!(le), "simd_lt" => codegen_intrinsic_binop!(lt), "simd_mul" => codegen_intrinsic_binop!(mul), diff --git a/src/test/cbmc/SIMD/Operators/main.rs b/src/test/cbmc/SIMD/Operators/main.rs index a7da57e4d82f..9dbd35850fb3 100644 --- a/src/test/cbmc/SIMD/Operators/main.rs +++ b/src/test/cbmc/SIMD/Operators/main.rs @@ -19,6 +19,7 @@ extern "platform-intrinsic" { fn simd_or(x: T, y: T) -> T; fn simd_xor(x: T, y: T) -> T; fn simd_extract(x: T, idx: u32) -> U; + fn simd_insert(x: T, idx: u32, b: U) -> T; } macro_rules! assert_op { @@ -45,6 +46,10 @@ fn main() { 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); } unsafe { From a8b38333662bd79d6fe0d0c86c6471d93f69b6f5 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Thu, 22 Jul 2021 21:14:19 +0000 Subject: [PATCH 3/4] move insert/extract tests to their own tile --- src/test/cbmc/SIMD/Construction/main.rs | 39 +++++++++++++++++++++++++ src/test/cbmc/SIMD/Operators/main.rs | 17 ----------- 2 files changed, 39 insertions(+), 17 deletions(-) create mode 100644 src/test/cbmc/SIMD/Construction/main.rs diff --git a/src/test/cbmc/SIMD/Construction/main.rs b/src/test/cbmc/SIMD/Construction/main.rs new file mode 100644 index 000000000000..48d7aa444035 --- /dev/null +++ b/src/test/cbmc/SIMD/Construction/main.rs @@ -0,0 +1,39 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, Eq)] +pub struct i64x2(i64, i64); + +extern "platform-intrinsic" { + fn simd_extract(x: T, idx: u32) -> U; + fn simd_insert(x: T, idx: u32, b: U) -> T; +} + +fn main() { + let y = i64x2(0, 1); + let z = i64x2(1, 2); + + // Indexing into the vectors + assert!(z.0 == 1); + assert!(z.1 == 2); + + { + // Intrinsic indexing + 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); + } + { + // Intrinsic updating + 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); + // Original unchanged + assert!(y.0 == 0 && y.1 == 1); + } +} diff --git a/src/test/cbmc/SIMD/Operators/main.rs b/src/test/cbmc/SIMD/Operators/main.rs index 9dbd35850fb3..c184f2bb32ec 100644 --- a/src/test/cbmc/SIMD/Operators/main.rs +++ b/src/test/cbmc/SIMD/Operators/main.rs @@ -18,8 +18,6 @@ extern "platform-intrinsic" { fn simd_and(x: T, y: T) -> T; fn simd_or(x: T, y: T) -> T; fn simd_xor(x: T, y: T) -> T; - fn simd_extract(x: T, idx: u32) -> U; - fn simd_insert(x: T, idx: u32, b: U) -> T; } macro_rules! assert_op { @@ -37,21 +35,6 @@ fn main() { let z = i64x2(1, 2); let v = i64x2(1, 3); - // 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); - } - unsafe { assert_op!(res_add, simd_add, x, y, 0, 1); assert_op!(res_sub, simd_sub, x, y, 0, -1); From fb1c5f54ba1521b006ab2482c51773333d240740 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Thu, 22 Jul 2021 21:58:26 +0000 Subject: [PATCH 4/4] extract codegen_intrinsic_simd_insert --- .../rustc_codegen_llvm/src/gotoc/intrinsic.rs | 46 ++++++++++++------- 1 file changed, 30 insertions(+), 16 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 2f29cd9588fc..109227f9097c 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -382,22 +382,7 @@ impl<'tcx> GotocCtx<'tcx> { } "simd_ge" => codegen_intrinsic_binop!(ge), "simd_gt" => codegen_intrinsic_binop!(gt), - "simd_insert" => { - let vec = fargs.remove(0); - let index = fargs.remove(0); - let newval = fargs.remove(0); - // Type checker should have ensured it's a vector type - let elem_ty = cbmc_ret_ty.base_type().unwrap().clone(); - let tmp = self.gen_temp_variable(cbmc_ret_ty, loc.clone()).to_expr(); - Stmt::block( - vec![ - Stmt::decl(tmp.clone(), Some(vec), loc.clone()), - tmp.clone().index_array(index).assign(newval.cast_to(elem_ty), loc.clone()), - self.codegen_expr_to_place(p, tmp), - ], - loc, - ) - } + "simd_insert" => self.codegen_intrinsic_simd_insert(fargs, p, cbmc_ret_ty, loc), "simd_le" => codegen_intrinsic_binop!(le), "simd_lt" => codegen_intrinsic_binop!(lt), "simd_mul" => codegen_intrinsic_binop!(mul), @@ -812,4 +797,33 @@ impl<'tcx> GotocCtx<'tcx> { } } } + + /// Insert is a generic update of a single value in a SIMD vector. + /// `P = simd_insert(vector, index, newval)` is here translated to + /// `{ T v = vector; v[index] = (cast)newval; P = v; }` + /// + /// CBMC does not currently seem to implement intrinsics like insert e.g.: + /// `**** WARNING: no body for function __builtin_ia32_vec_set_v4si` + pub fn codegen_intrinsic_simd_insert( + &mut self, + mut fargs: Vec, + p: &Place<'tcx>, + cbmc_ret_ty: Type, + loc: Location, + ) -> Stmt { + let vec = fargs.remove(0); + let index = fargs.remove(0); + let newval = fargs.remove(0); + // Type checker should have ensured it's a vector type + let elem_ty = cbmc_ret_ty.base_type().unwrap().clone(); + let tmp = self.gen_temp_variable(cbmc_ret_ty, loc.clone()).to_expr(); + Stmt::block( + vec![ + Stmt::decl(tmp.clone(), Some(vec), loc.clone()), + tmp.clone().index_array(index).assign(newval.cast_to(elem_ty), loc.clone()), + self.codegen_expr_to_place(p, tmp), + ], + loc, + ) + } }