Merge pull request #5919 from tautschnig/fix-5903

Provide implementations of __builtin_ia32_vec_ext_*

Author: tautschnig

regression/cbmc/SIMD1/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#ifdef _MSC_VER
+#  include <intrin.h>
+#else
+#  include <immintrin.h>
+#endif
+
+int main()
+{
+  __m128i values = _mm_setr_epi32(0x1234, 0x2345, 0x3456, 0x4567);
+  int val1 = _mm_extract_epi32(values, 0);
+  assert(val1 == 0x1234);
+  return 0;
+}

regression/cbmc/SIMD1/test.desc

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

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();
 

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);

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);
+}

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 <intrin.h>
+#    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 <intrin.h>
+#    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 <intrin.h>
+#    define __CPROVER_INTRIN_H_INCLUDED
+#  endif
+
+inline int _mm_extract_epi32(__m128i a, const int imm8)
+{
+  return a.m128i_i32[imm8];
+}
+#endif

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);

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 &parameter : 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 &parameter : code_type.parameters())
+      remove_vector(parameter.type());
+  }
   else if(type.id()==ID_pointer ||
           type.id()==ID_complex ||
           type.id()==ID_array)