Provide implementations of __builtin_ia32_vec_ext_*

These built-ins extract an element of a vector.

Fixes: #5903

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/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