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