C front-end: __builtin_shuffle, __builtin_shufflevector

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

scripts/expected_doxygen_warnings.txt

@@ -21,7 +21,7 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (142), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/ansi-c/Makefile

@@ -11,6 +11,7 @@ SRC = anonymous_member.cpp \
       ansi_c_typecheck.cpp \
       ansi_c_y.tab.cpp \
       builtin_factory.cpp \
+      c_expr.cpp \
       c_misc.cpp \
       c_nondet_symbol_factory.cpp \
       c_object_factory_parameters.cpp \

src/ansi-c/c_expr.cpp

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+Module: API to expression classes that are internal to the C frontend
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "c_expr.h"
+
+#include <util/arith_tools.h>
+
+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/ansi-c/c_expr.h

@@ -14,4 +14,97 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_code.h>
 
+/// \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_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_base.h

@@ -203,6 +203,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()))