Use CBMC's shuffle_vector expression

cprover_bindings/src/goto_program/expr.rs

@@ -139,6 +139,11 @@ pub enum ExprValue {
         op: SelfOperator,
         e: Expr,
     },
+    ShuffleVector {
+        vector1: Expr,
+        vector2: Expr,
+        indexes: Vec<Expr>,
+    },
     /// <https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html>
     /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })`
     /// `({ op1; op2; ...})`
@@ -371,6 +376,11 @@ impl Expr {
             If { c, t, e } => c.is_side_effect() || t.is_side_effect() || e.is_side_effect(),
             Index { array, index } => array.is_side_effect() || index.is_side_effect(),
             Member { lhs, field: _ } => lhs.is_side_effect(),
+            ShuffleVector { vector1, vector2, indexes } => {
+                vector1.is_side_effect()
+                    || vector2.is_side_effect()
+                    || indexes.iter().any(|e| e.is_side_effect())
+            }
             Struct { values } => values.iter().any(|e| e.is_side_effect()),
             Typecast(e) => e.is_side_effect(),
             Union { value, field: _ } => value.is_side_effect(),
@@ -990,6 +1000,18 @@ impl Expr {
         assert!(variable.is_symbol());
         expr!(Exists { variable, domain }, typ)
     }
+
+    pub fn shuffle_vector(vector1: Expr, vector2: Expr, indexes: Vec<Expr>) -> Expr {
+        assert!(vector1.typ.is_array_like());
+        assert!(vector2.typ.is_array_like());
+        expr!(
+            ShuffleVector { vector1, vector2, indexes },
+            Type::vector(
+                vector1.typ.base_type().unwrap().clone(),
+                indexes.len().try_into().unwrap()
+            )
+        )
+    }
 }
 
 /// Constructors for Binary Operations

cprover_bindings/src/irep/irep_id.rs

@@ -836,6 +836,7 @@ pub enum IrepId {
     VectorGt,
     VectorLt,
     FloatbvRoundToIntegral,
+    ShuffleVector,
 }
 
 impl IrepId {
@@ -1731,6 +1732,7 @@ impl IrepId {
             IrepId::VectorGt => "vector->",
             IrepId::VectorLt => "vector-<",
             IrepId::FloatbvRoundToIntegral => "floatbv_round_to_integral",
+            IrepId::ShuffleVector => "shuffle_vector",
         }
     }
 }

cprover_bindings/src/irep/to_irep.rs

@@ -408,6 +408,19 @@ impl ToIrep for ExprValue {
                 ],
                 named_sub: linear_map![],
             },
+            ExprValue::ShuffleVector { vector1, vector2, indexes } => Irep {
+                id: IrepId::ShuffleVector,
+                sub: vec![
+                    vector1.to_irep(mm),
+                    vector2.to_irep(mm),
+                    Irep {
+                        id: IrepId::EmptyString,
+                        sub: indexes.iter().map(|x| x.to_irep(mm)).collect(),
+                        named_sub: linear_map![],
+                    },
+                ],
+                named_sub: linear_map![],
+            },
         }
     }
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -1556,7 +1556,8 @@ impl GotocCtx<'_> {
     }
 
     /// `simd_shuffle` constructs a new vector from the elements of two input
-    /// vectors, choosing values according to an input array of indexes.
+    /// vectors, choosing values according to an input array of indexes. See
+    /// https://doc.rust-lang.org/std/intrinsics/simd/fn.simd_shuffle.html
     ///
     /// We check that:
     ///  1. The return type length is equal to the expected length (`n`) of the
@@ -1571,13 +1572,6 @@ impl GotocCtx<'_> {
     /// TODO: Check that `indexes` contains constant values which are within the
     /// expected bounds. See
     /// <https://github.com/model-checking/kani/issues/1960> for more details.
-    ///
-    /// This code mimics CBMC's `shuffle_vector_exprt::lower()` here:
-    /// <https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_expr.cpp>
-    ///
-    /// We can't use shuffle_vector_exprt because it's not understood by the CBMC backend,
-    /// it's immediately lowered by the C frontend.
-    /// Issue: <https://github.com/diffblue/cbmc/issues/6297>
     fn codegen_intrinsic_simd_shuffle(
         &mut self,
         mut fargs: Vec<Expr>,
@@ -1593,7 +1587,7 @@ impl GotocCtx<'_> {
         // [u32; n]: translated wrapped in a struct
         let indexes = fargs.remove(0);
 
-        let (in_type_len, vec_subtype) = self.simd_size_and_type(rust_arg_types[0]);
+        let (_, vec_subtype) = self.simd_size_and_type(rust_arg_types[0]);
         let (ret_type_len, ret_type_subtype) = self.simd_size_and_type(rust_ret_type);
         if ret_type_len != n {
             let err_msg = format!(
@@ -1617,24 +1611,20 @@ impl GotocCtx<'_> {
         // An unsigned type here causes an invariant violation in CBMC.
         // Issue: https://github.com/diffblue/cbmc/issues/6298
         let st_rep = Type::ssize_t();
-        let n_rep = Expr::int_constant(in_type_len, st_rep.clone());
 
-        // P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N])
         let elems = (0..n)
             .map(|i| {
                 let idx = Expr::int_constant(i, st_rep.clone());
                 // Must not use `indexes.index(i)` directly, because codegen wraps arrays in struct
-                let v = self.codegen_idx_array(indexes.clone(), idx).cast_to(st_rep.clone());
-                let cond = v.clone().lt(n_rep.clone());
-                let t = vec1.clone().index(v.clone());
-                let e = vec2.clone().index(v.sub(n_rep.clone()));
-                cond.ternary(t, e)
+                self.codegen_idx_array(indexes.clone(), idx).cast_to(st_rep.clone())
             })
             .collect();
         self.tcx.dcx().abort_if_errors();
         let cbmc_ret_ty = self.codegen_ty_stable(rust_ret_type);
         let loc = self.codegen_span_stable(span);
-        self.codegen_expr_to_place_stable(p, Expr::vector_expr(cbmc_ret_ty, elems), loc)
+        let shuffle_vector = Expr::shuffle_vector(vec1, vec2, elems);
+        assert_eq!(*shuffle_vector.typ(), cbmc_ret_ty);
+        self.codegen_expr_to_place_stable(p, shuffle_vector, loc)
     }
 
     /// A volatile load of a memory location: