C front-end: __builtin_shuffle, __builtin_shufflevector

These are polymorphic built-ins supported by GCC and Clang,
respectively. Introduce a new shuffle_vector expression to handle these,
with type checking addressing the differences between the GCC/Clang
APIs.

Author: tautschnig

regression/cbmc/gcc_vector3/main.c

@@ -0,0 +1,52 @@
+#include <assert.h>
+
+#ifdef __GNUC__
+typedef int v4si __attribute__((vector_size(16)));
+
+typedef union {
+  v4si v;
+  int members[4];
+} vector_u;
+#endif
+
+int main()
+{
+#if defined(__GNUC__) && !defined(__clang__)
+  // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
+  v4si a = {1, 2, 3, 4};
+  v4si b = {5, 6, 7, 8};
+  v4si mask1 = {0, 1, 5, 3};
+  v4si mask2 = {0, 4, 2, 5};
+
+  vector_u res;
+
+  res.v = __builtin_shuffle(a, mask1);
+  assert(res.members[0] == 1);
+  assert(res.members[1] == 2);
+  assert(res.members[2] == 2);
+  assert(res.members[3] == 4);
+
+  res.v = __builtin_shuffle(a, b, mask2);
+  assert(res.members[0] == 1);
+  assert(res.members[1] == 5);
+  assert(res.members[2] == 3);
+  assert(res.members[3] == 6);
+#elif defined(__clang__)
+  v4si a = {1, 2, 3, 4};
+  v4si b = {5, 6, 7, 8};
+
+  vector_u res;
+
+  res.v = __builtin_shufflevector(a, a, 0, 1, -1, 3);
+  assert(res.members[0] == 1);
+  assert(res.members[1] == 2);
+  // res.members[2] is "don't care"
+  assert(res.members[3] == 4);
+
+  res.v = __builtin_shufflevector(a, b, 0, 4, 2, 5);
+  assert(res.members[0] == 1);
+  assert(res.members[1] == 5);
+  assert(res.members[2] == 3);
+  assert(res.members[3] == 6);
+#endif
+}

regression/cbmc/gcc_vector3/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_base.h

@@ -208,6 +208,8 @@ class c_typecheck_baset:
   virtual code_blockt instantiate_gcc_polymorphic_builtin(
     const irep_idt &identifier,
     const symbol_exprt &function_symbol);
+  virtual exprt
+  typecheck_shuffle_vector(const side_effect_expr_function_callt &expr);
 
   virtual void make_index_type(exprt &expr);
   virtual void make_constant(exprt &expr);

src/ansi-c/c_typecheck_expr.cpp

@@ -1927,6 +1927,24 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
         return;
       }
+      else if(
+        identifier == "__builtin_shuffle" &&
+        config.ansi_c.mode == configt::ansi_ct::flavourt::GCC)
+      {
+        exprt result = typecheck_shuffle_vector(expr);
+        expr.swap(result);
+
+        return;
+      }
+      else if(
+        identifier == "__builtin_shufflevector" &&
+        config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG)
+      {
+        exprt result = typecheck_shuffle_vector(expr);
+        expr.swap(result);
+
+        return;
+      }
       else if(
         auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
           identifier, expr.arguments(), f_op.source_location()))

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -1377,3 +1377,128 @@ code_blockt c_typecheck_baset::instantiate_gcc_polymorphic_builtin(
 
   return block;
 }
+
+exprt c_typecheck_baset::typecheck_shuffle_vector(
+  const side_effect_expr_function_callt &expr)
+{
+  const exprt &f_op = expr.function();
+  const source_locationt &source_location = expr.source_location();
+  const irep_idt &identifier = to_symbol_expr(f_op).get_identifier();
+
+  exprt::operandst arguments = expr.arguments();
+
+  if(identifier == "__builtin_shuffle")
+  {
+    // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html and
+    // https://github.com/OpenCL/man/blob/master/shuffle.adoc
+    if(arguments.size() != 2 && arguments.size() != 3)
+    {
+      error().source_location = f_op.source_location();
+      error() << "__builtin_shuffle expects two or three arguments" << eom;
+      throw 0;
+    }
+
+    for(exprt &arg : arguments)
+    {
+      if(arg.type().id() != ID_vector)
+      {
+        error().source_location = f_op.source_location();
+        error() << "__builtin_shuffle expects vector arguments" << eom;
+        throw 0;
+      }
+    }
+
+    const exprt &arg0 = arguments[0];
+    const vector_typet &input_vec_type = to_vector_type(arg0.type());
+
+    optionalt<exprt> arg1;
+    if(arguments.size() == 3)
+    {
+      if(arguments[1].type() != input_vec_type)
+      {
+        error().source_location = f_op.source_location();
+        error() << "__builtin_shuffle expects input vectors of the same type"
+                << eom;
+        throw 0;
+      }
+      arg1 = arguments[1];
+    }
+    const exprt &indices = arguments.back();
+    const vector_typet &indices_type = to_vector_type(indices.type());
+    const std::size_t indices_size =
+      numeric_cast_v<std::size_t>(indices_type.size());
+
+    exprt::operandst operands;
+    operands.reserve(indices_size);
+
+    auto input_size = numeric_cast<mp_integer>(input_vec_type.size());
+    CHECK_RETURN(input_size.has_value());
+    if(arg1.has_value())
+      input_size = *input_size * 2;
+    constant_exprt size = from_integer(*input_size, indices_type.subtype());
+
+    for(std::size_t i = 0; i < indices_size; ++i)
+    {
+      // only the least significant bits of each mask element are considered
+      mod_exprt mod_index{index_exprt{indices, from_integer(i, index_type())},
+                          size};
+      mod_index.add_source_location() = source_location;
+      operands.push_back(std::move(mod_index));
+    }
+
+    return shuffle_vector_exprt{arg0, arg1, std::move(operands)}.lower();
+  }
+  else if(identifier == "__builtin_shufflevector")
+  {
+    // https://clang.llvm.org/docs/LanguageExtensions.html#langext-builtin-shufflevector
+    if(arguments.size() < 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << "__builtin_shufflevector expects two or more arguments" << eom;
+      throw 0;
+    }
+
+    exprt::operandst operands;
+    operands.reserve(arguments.size() - 2);
+
+    for(std::size_t i = 0; i < arguments.size(); ++i)
+    {
+      exprt &arg_i = arguments[i];
+
+      if(i <= 1 && arg_i.type().id() != ID_vector)
+      {
+        error().source_location = f_op.source_location();
+        error() << "__builtin_shufflevector expects two vectors as argument"
+                << eom;
+        throw 0;
+      }
+      else if(i > 1)
+      {
+        if(!is_signed_or_unsigned_bitvector(arg_i.type()))
+        {
+          error().source_location = f_op.source_location();
+          error() << "__builtin_shufflevector expects integer index" << eom;
+          throw 0;
+        }
+
+        make_constant(arg_i);
+
+        const auto int_index = numeric_cast<mp_integer>(arg_i);
+        CHECK_RETURN(int_index.has_value());
+
+        if(*int_index == -1)
+        {
+          operands.push_back(from_integer(0, arg_i.type()));
+          operands.back().add_source_location() = source_location;
+        }
+        else
+          operands.push_back(arg_i);
+      }
+    }
+
+    return shuffle_vector_exprt{arguments[0], arguments[1], std::move(operands)}
+      .lower();
+  }
+  else
+    UNREACHABLE;
+}

src/ansi-c/clang_builtin_headers.h

@@ -1,5 +1,3 @@
-__gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...);
-
 __gcc_v2di __builtin_ia32_undef128(void);
 __gcc_v4di __builtin_ia32_undef256(void);
 __gcc_v8di __builtin_ia32_undef512(void);

src/util/irep_ids.def

@@ -849,6 +849,7 @@ IREP_ID_TWO(vector_ge, vector->=)
 IREP_ID_TWO(vector_le, vector-<=)
 IREP_ID_TWO(vector_gt, vector->)
 IREP_ID_TWO(vector_lt, vector-<)
+IREP_ID_ONE(shuffle_vector)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/std_expr.cpp

@@ -143,3 +143,56 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
       "let bindings must be type consistent");
   }
 }
+
+shuffle_vector_exprt::shuffle_vector_exprt(
+  exprt vector1,
+  optionalt<exprt> vector2,
+  exprt::operandst indices)
+  : multi_ary_exprt(
+      ID_shuffle_vector,
+      {std::move(vector1), nil_exprt{}, exprt{}},
+      typet{})
+{
+  if(vector2.has_value())
+    op1() = std::move(*vector2);
+
+  const vector_typet &vt = to_vector_type(op0().type());
+  type() =
+    vector_typet{vt.subtype(), from_integer(indices.size(), vt.size().type())};
+
+  op2().operands().swap(indices);
+}
+
+vector_exprt shuffle_vector_exprt::lower() const
+{
+  PRECONDITION(
+    !has_two_input_vectors() || vector1().type() == vector2().type());
+
+  if(indices().empty())
+    return vector_exprt{exprt::operandst{}, type()};
+
+  auto input_size =
+    numeric_cast<mp_integer>(to_vector_type(vector1().type()).size());
+  CHECK_RETURN(input_size.has_value());
+
+  exprt::operandst operands;
+  operands.reserve(indices().size());
+
+  for(const exprt &index : indices())
+  {
+    if(has_two_input_vectors())
+    {
+      operands.push_back(if_exprt{
+        binary_predicate_exprt{
+          index, ID_lt, from_integer(*input_size, index.type())},
+        index_exprt{vector1(), index},
+        index_exprt{
+          vector2(),
+          minus_exprt{index, from_integer(*input_size, index.type())}}});
+    }
+    else
+      operands.push_back(index_exprt{vector1(), index});
+  }
+
+  return vector_exprt{std::move(operands), type()};
+}

src/util/std_expr.h

@@ -3202,4 +3202,97 @@ inline bool can_cast_expr<class_method_descriptor_exprt>(const exprt &base)
   return base.id() == ID_virtual_function;
 }
 
+/// \brief Shuffle elements of one or two vectors, modelled after Clang's
+/// __builtin_shufflevector.
+class shuffle_vector_exprt : public multi_ary_exprt
+{
+public:
+  shuffle_vector_exprt(
+    exprt vector1,
+    optionalt<exprt> vector2,
+    exprt::operandst indices);
+
+  const vector_typet &type() const
+  {
+    return static_cast<const vector_typet &>(multi_ary_exprt::type());
+  }
+
+  vector_typet &type()
+  {
+    return static_cast<vector_typet &>(multi_ary_exprt::type());
+  }
+
+  const exprt &vector1() const
+  {
+    return op0();
+  }
+
+  exprt &vector1()
+  {
+    return op0();
+  }
+
+  const exprt &vector2() const
+  {
+    return op1();
+  }
+
+  exprt &vector2()
+  {
+    return op1();
+  }
+
+  bool has_two_input_vectors() const
+  {
+    return vector2().is_not_nil();
+  }
+
+  const exprt::operandst &indices() const
+  {
+    return op2().operands();
+  }
+
+  exprt::operandst &indices()
+  {
+    return op2().operands();
+  }
+
+  vector_exprt lower() const;
+};
+
+template <>
+inline bool can_cast_expr<shuffle_vector_exprt>(const exprt &base)
+{
+  return base.id() == ID_shuffle_vector;
+}
+
+inline void validate_expr(const shuffle_vector_exprt &value)
+{
+  validate_operands(value, 3, "shuffle_vector must have three operands");
+}
+
+/// \brief Cast an exprt to a \ref shuffle_vector_exprt
+///
+/// \a expr must be known to be \ref shuffle_vector_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref shuffle_vector_exprt
+inline const shuffle_vector_exprt &to_shuffle_vector_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_shuffle_vector);
+  const shuffle_vector_exprt &ret =
+    static_cast<const shuffle_vector_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_shuffle_vector_expr(const exprt &)
+inline shuffle_vector_exprt &to_shuffle_vector_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_shuffle_vector);
+  shuffle_vector_exprt &ret = static_cast<shuffle_vector_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_STD_EXPR_H