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

@@ -1593,7 +1593,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 +1617,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: