From de4557fff6c2bf04e0979f1bd06afc3a34cda941 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Mar 2021 23:23:06 +0000 Subject: [PATCH] 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. --- regression/cbmc/gcc_vector3/main.c | 52 +++++++ regression/cbmc/gcc_vector3/test.desc | 8 ++ scripts/expected_doxygen_warnings.txt | 2 +- src/ansi-c/Makefile | 1 + src/ansi-c/c_expr.cpp | 64 +++++++++ src/ansi-c/c_expr.h | 93 +++++++++++++ src/ansi-c/c_typecheck_base.h | 2 + src/ansi-c/c_typecheck_expr.cpp | 18 +++ .../c_typecheck_gcc_polymorphic_builtins.cpp | 127 ++++++++++++++++++ src/ansi-c/clang_builtin_headers.h | 2 - src/util/irep_ids.def | 1 + 11 files changed, 367 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/gcc_vector3/main.c create mode 100644 regression/cbmc/gcc_vector3/test.desc create mode 100644 src/ansi-c/c_expr.cpp diff --git a/regression/cbmc/gcc_vector3/main.c b/regression/cbmc/gcc_vector3/main.c new file mode 100644 index 00000000000..85d45b3f724 --- /dev/null +++ b/regression/cbmc/gcc_vector3/main.c @@ -0,0 +1,52 @@ +#include + +#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 +} diff --git a/regression/cbmc/gcc_vector3/test.desc b/regression/cbmc/gcc_vector3/test.desc new file mode 100644 index 00000000000..39d9265e8a7 --- /dev/null +++ b/regression/cbmc/gcc_vector3/test.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index 154e4feef9e..67766e0c898 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/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. diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index b4163349e4a..07b396da0ee 100644 --- a/src/ansi-c/Makefile +++ b/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 \ diff --git a/src/ansi-c/c_expr.cpp b/src/ansi-c/c_expr.cpp new file mode 100644 index 00000000000..d89c05e9a8b --- /dev/null +++ b/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, kroening@kroening.com + +\*******************************************************************/ + +#include "c_expr.h" + +#include + +shuffle_vector_exprt::shuffle_vector_exprt( + exprt vector1, + optionalt 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(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()}; +} diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 3f81db6b301..3a53f6cb618 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -14,4 +14,97 @@ Author: Daniel Kroening, kroening@kroening.com #include +/// \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 vector2, + exprt::operandst indices); + + const vector_typet &type() const + { + return static_cast(multi_ary_exprt::type()); + } + + vector_typet &type() + { + return static_cast(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(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(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(expr); + validate_expr(ret); + return ret; +} + #endif // CPROVER_ANSI_C_C_EXPR_H diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 47b6cd77b05..d5ba9f1ba26 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/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); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 94ac93c1ec2..215992c9a5c 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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())) diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index c869e9cb832..bfb49377621 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "c_expr.h" + static symbol_exprt typecheck_sync_with_pointer_parameter( const irep_idt &identifier, const exprt::operandst &arguments, @@ -1377,3 +1379,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 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(indices_type.size()); + + exprt::operandst operands; + operands.reserve(indices_size); + + auto input_size = numeric_cast(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(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; +} diff --git a/src/ansi-c/clang_builtin_headers.h b/src/ansi-c/clang_builtin_headers.h index ebe4bd0acb8..1906a29d5cb 100644 --- a/src/ansi-c/clang_builtin_headers.h +++ b/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); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e78c3eac98d..ec411fedef5 100644 --- a/src/util/irep_ids.def +++ b/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