From 3b336ba52a4922ed1630f82cf60508b052d4bcdb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Mar 2021 00:48:28 +0000 Subject: [PATCH 1/4] Provide declarations of Clang AVX intrinsics Additional declarations based on Clang's BuiltinsX86.def. For `__builtin_ia32_sqrtpd512` and `__builtin_ia32_sqrtps512`, Clang and GCC disagree about the number of parameters (GCC supports one, Clang supports two). --- src/ansi-c/clang_builtin_headers.h | 47 +++++++++++++++++++++++++ src/ansi-c/gcc_builtin_headers_ia32-2.h | 4 +-- 2 files changed, 49 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/clang_builtin_headers.h b/src/ansi-c/clang_builtin_headers.h index 1906a29d5cb..cc931b64c20 100644 --- a/src/ansi-c/clang_builtin_headers.h +++ b/src/ansi-c/clang_builtin_headers.h @@ -2,6 +2,53 @@ __gcc_v2di __builtin_ia32_undef128(void); __gcc_v4di __builtin_ia32_undef256(void); __gcc_v8di __builtin_ia32_undef512(void); +// clang-format off +__gcc_v8hi __builtin_ia32_cvtne2ps2bf16_128(__gcc_v4sf, __gcc_v4sf); +__gcc_v16hi __builtin_ia32_cvtne2ps2bf16_256(__gcc_v8sf, __gcc_v8sf); +__gcc_v32hi __builtin_ia32_cvtne2ps2bf16_512(__gcc_v16sf, __gcc_v16sf); +__gcc_v8hi __builtin_ia32_cvtneps2bf16_128_mask(__gcc_v4sf, __gcc_v8hi, unsigned char); +__gcc_v8hi __builtin_ia32_cvtneps2bf16_256_mask(__gcc_v8sf, __gcc_v8hi, unsigned char); +__gcc_v16si __builtin_ia32_cvtneps2bf16_512_mask(__gcc_v16sf, __gcc_v16hi, unsigned short); +__gcc_v4sf __builtin_ia32_dpbf16ps_128(__gcc_v4sf, __gcc_v4si, __gcc_v4si); +__gcc_v8sf __builtin_ia32_dpbf16ps_256(__gcc_v8sf, __gcc_v8si, __gcc_v8si); +__gcc_v16sf __builtin_ia32_dpbf16ps_512(__gcc_v16sf, __gcc_v16si, __gcc_v16si); +float __builtin_ia32_cvtsbf162ss_32(unsigned short); + +void __builtin_ia32_vp2intersect_d_512(__gcc_v16si, __gcc_v16si, unsigned short *, unsigned short *); +void __builtin_ia32_vp2intersect_d_256(__gcc_v8si, __gcc_v8si, unsigned char *, unsigned char *); +void __builtin_ia32_vp2intersect_d_128(__gcc_v4si, __gcc_v4si, unsigned char *, unsigned char *); + +__gcc_v16qi __builtin_ia32_selectb_128(unsigned short, __gcc_v16qi, __gcc_v16qi); +__gcc_v32qi __builtin_ia32_selectb_256(unsigned int, __gcc_v32qi, __gcc_v32qi); +__gcc_v64qi __builtin_ia32_selectb_512(unsigned long, __gcc_v64qi, __gcc_v64qi); +__gcc_v8hi __builtin_ia32_selectw_128(unsigned char, __gcc_v8hi, __gcc_v8hi); +__gcc_v16hi __builtin_ia32_selectw_256(unsigned short, __gcc_v16hi, __gcc_v16hi); +__gcc_v32hi __builtin_ia32_selectw_512(unsigned int, __gcc_v32hi, __gcc_v32hi); +__gcc_v4si __builtin_ia32_selectd_128(unsigned char, __gcc_v4si, __gcc_v4si); +__gcc_v8si __builtin_ia32_selectd_256(unsigned char, __gcc_v8si, __gcc_v8si); +__gcc_v16si __builtin_ia32_selectd_512(unsigned short, __gcc_v16si, __gcc_v16si); +__gcc_v4sf __builtin_ia32_selectps_128(unsigned char, __gcc_v4sf, __gcc_v4sf); +__gcc_v8sf __builtin_ia32_selectps_256(unsigned char, __gcc_v8sf, __gcc_v8sf); +__gcc_v16sf __builtin_ia32_selectps_512(unsigned short, __gcc_v16sf, __gcc_v16sf); +__gcc_v2df __builtin_ia32_selectpd_128(unsigned char, __gcc_v2df, __gcc_v2df); +__gcc_v4df __builtin_ia32_selectpd_256(unsigned char, __gcc_v4df, __gcc_v4df); +__gcc_v8df __builtin_ia32_selectpd_512(unsigned char, __gcc_v8df, __gcc_v8df); +__gcc_v4sf __builtin_ia32_selectss_128(unsigned char, __gcc_v4sf, __gcc_v4sf); +__gcc_v2df __builtin_ia32_selectsd_128(unsigned char, __gcc_v2df, __gcc_v2df); + +__gcc_v4sf __builtin_ia32_vfmaddss3_mask(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int); +__gcc_v4sf __builtin_ia32_vfmaddss3_maskz(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int); +__gcc_v4sf __builtin_ia32_vfmaddss3_mask3(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int); +__gcc_v2df __builtin_ia32_vfmaddsd3_mask(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int); +__gcc_v2df __builtin_ia32_vfmaddsd3_maskz(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int); +__gcc_v2df __builtin_ia32_vfmaddsd3_mask3(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int); +__gcc_v2df __builtin_ia32_vfmsubsd3_mask3(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int); +__gcc_v4sf __builtin_ia32_vfmsubss3_mask3(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int); + +__gcc_v4sf __builtin_ia32_cvtsd2ss_round_mask(__gcc_v4sf, __gcc_v2df, __gcc_v4sf, unsigned char, int); +__gcc_v2df __builtin_ia32_cvtss2sd_round_mask(__gcc_v2df, __gcc_v4sf, __gcc_v2df, unsigned char, int); +// clang-format on + void __builtin_nontemporal_store(); void __builtin_nontemporal_load(); diff --git a/src/ansi-c/gcc_builtin_headers_ia32-2.h b/src/ansi-c/gcc_builtin_headers_ia32-2.h index d5000ec19da..0283a0c084c 100644 --- a/src/ansi-c/gcc_builtin_headers_ia32-2.h +++ b/src/ansi-c/gcc_builtin_headers_ia32-2.h @@ -377,8 +377,8 @@ __gcc_v8di __builtin_ia32_pternlogq512_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, __gcc_v8di __builtin_ia32_pternlogq512_maskz(__gcc_v8di, __gcc_v8di, __gcc_v8di, int, unsigned char); __gcc_v16sf __builtin_ia32_copysignps512(__gcc_v16sf, __gcc_v16sf); __gcc_v8df __builtin_ia32_copysignpd512(__gcc_v8df, __gcc_v8df); -__gcc_v8df __builtin_ia32_sqrtpd512(__gcc_v8df); -__gcc_v16sf __builtin_ia32_sqrtps512(__gcc_v16sf); +__gcc_v8df __builtin_ia32_sqrtpd512(__gcc_v8df, ...); +__gcc_v16sf __builtin_ia32_sqrtps512(__gcc_v16sf, ...); __gcc_v16sf __builtin_ia32_exp2ps(__gcc_v16sf); __gcc_v16si __builtin_ia32_roundpd_az_vec_pack_sfix512(__gcc_v8df, __gcc_v8df); __gcc_v16si __builtin_ia32_floorpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df, const int); From b89c32c219be897a156260449fdd6995ec7b502a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Mar 2021 22:12:35 +0000 Subject: [PATCH 2/4] instructiont::transform applies to function in function call We previously only transformed the left-hand side and arguments, but skipped over the function itself. This omission became apparent when trying to run the upcoming SIMD1 test (added in a later commit, further bug fixes are necessary). --- src/goto-programs/goto_program.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 9cb648274a6..6aa849569a9 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -974,6 +974,13 @@ void goto_programt::instructiont::transform( change = true; } + auto new_function = f(new_call.function()); + if(new_function.has_value()) + { + new_call.function() = *new_function; + change = true; + } + for(auto &a : new_call.arguments()) { auto new_a = f(a); From 63c65575876fdc104fe76613fdd97846ac9f3c8e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Mar 2021 22:14:17 +0000 Subject: [PATCH 3/4] remove_vector also applies to code_typet This omission became apparent when trying to run the upcoming SIMD1 test (added in a later commit, further bug fixes are necessary). --- src/goto-programs/remove_vector.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 9314fe3a32b..1304cff6134 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -64,6 +64,18 @@ static bool have_to_remove_vector(const typet &type) if(have_to_remove_vector(c.type())) return true; } + else if(type.id() == ID_code) + { + const code_typet &code_type = to_code_type(type); + + if(have_to_remove_vector(code_type.return_type())) + return true; + for(auto ¶meter : code_type.parameters()) + { + if(have_to_remove_vector(parameter.type())) + return true; + } + } else if(type.id()==ID_pointer || type.id()==ID_complex || type.id()==ID_array) @@ -256,6 +268,14 @@ static void remove_vector(typet &type) remove_vector(it->type()); } } + else if(type.id() == ID_code) + { + code_typet &code_type = to_code_type(type); + + remove_vector(code_type.return_type()); + for(auto ¶meter : code_type.parameters()) + remove_vector(parameter.type()); + } else if(type.id()==ID_pointer || type.id()==ID_complex || type.id()==ID_array) From cce048bf978b40f1908aefb136c91a8a6931cc03 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Mar 2021 11:00:36 +0000 Subject: [PATCH 4/4] Provide implementations of __builtin_ia32_vec_ext_* These built-ins extract an element of a vector. Fixes: #5903 --- regression/cbmc/SIMD1/main.c | 14 +++++++++++ regression/cbmc/SIMD1/test.desc | 8 +++++++ src/ansi-c/library/gcc.c | 36 ++++++++++++++++++++++++++++ src/ansi-c/library/intrin.c | 42 +++++++++++++++++++++++++++++++++ 4 files changed, 100 insertions(+) create mode 100644 regression/cbmc/SIMD1/main.c create mode 100644 regression/cbmc/SIMD1/test.desc diff --git a/regression/cbmc/SIMD1/main.c b/regression/cbmc/SIMD1/main.c new file mode 100644 index 00000000000..3bd22ded54a --- /dev/null +++ b/regression/cbmc/SIMD1/main.c @@ -0,0 +1,14 @@ +#include +#ifdef _MSC_VER +# include +#else +# include +#endif + +int main() +{ + __m128i values = _mm_setr_epi32(0x1234, 0x2345, 0x3456, 0x4567); + int val1 = _mm_extract_epi32(values, 0); + assert(val1 == 0x1234); + return 0; +} diff --git a/regression/cbmc/SIMD1/test.desc b/regression/cbmc/SIMD1/test.desc new file mode 100644 index 00000000000..39d9265e8a7 --- /dev/null +++ b/regression/cbmc/SIMD1/test.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/library/gcc.c b/src/ansi-c/library/gcc.c index c9f736e45c6..e3c6fab0deb 100644 --- a/src/ansi-c/library/gcc.c +++ b/src/ansi-c/library/gcc.c @@ -191,3 +191,39 @@ __CPROVER_HIDE:; (void)ptr; return size <= sizeof(__CPROVER_size_t); } + +/* FUNCTION: __builtin_ia32_vec_ext_v4si */ + +typedef int __gcc_v4si __attribute__((__vector_size__(16))); + +int __builtin_ia32_vec_ext_v4si(__gcc_v4si vec, int offset) +{ + return *((int *)&vec + offset); +} + +/* FUNCTION: __builtin_ia32_vec_ext_v2di */ + +typedef long long __gcc_v2di __attribute__((__vector_size__(16))); + +long long __builtin_ia32_vec_ext_v2di(__gcc_v2di vec, int offset) +{ + return *((long long *)&vec + offset); +} + +/* FUNCTION: __builtin_ia32_vec_ext_v16qi */ + +typedef char __gcc_v16qi __attribute__((__vector_size__(16))); + +int __builtin_ia32_vec_ext_v16qi(__gcc_v16qi vec, int offset) +{ + return *((char *)&vec + offset); +} + +/* FUNCTION: __builtin_ia32_vec_ext_v4sf */ + +typedef float __gcc_v4sf __attribute__((__vector_size__(16))); + +float __builtin_ia32_vec_ext_v4sf(__gcc_v4sf vec, int offset) +{ + return *((float *)&vec + offset); +} diff --git a/src/ansi-c/library/intrin.c b/src/ansi-c/library/intrin.c index 34de9f548ee..3f4ea7d0ed8 100644 --- a/src/ansi-c/library/intrin.c +++ b/src/ansi-c/library/intrin.c @@ -342,3 +342,45 @@ inline char _InterlockedCompareExchange8(char volatile *p, char v1, char v2) __CPROVER_atomic_end(); return old; } + +/* FUNCTION: _mm_set_epi32 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_set_epi32(int e3, int e2, int e1, int e0) +{ + return (__m128i){.m128i_i32 = {e0, e1, e2, e3}}; +} +#endif + +/* FUNCTION: _mm_setr_epi32 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0) +{ + return (__m128i){.m128i_i32 = {e3, e2, e1, e0}}; +} +#endif + +/* FUNCTION: _mm_extract_epi32 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline int _mm_extract_epi32(__m128i a, const int imm8) +{ + return a.m128i_i32[imm8]; +} +#endif