Update GCC builtin declarations

These builtins match GCC revision 425afe1f0c907.

Author: tautschnig

src/ansi-c/CMakeLists.txt

@@ -63,6 +63,7 @@ make_inc(gcc_builtin_headers_ia32)
 make_inc(gcc_builtin_headers_ia32-2)
 make_inc(gcc_builtin_headers_ia32-3)
 make_inc(gcc_builtin_headers_ia32-4)
+make_inc(gcc_builtin_headers_ia32-5)
 make_inc(gcc_builtin_headers_math)
 make_inc(gcc_builtin_headers_mem_string)
 make_inc(gcc_builtin_headers_mips)
@@ -85,6 +86,7 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-5.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc

src/ansi-c/Makefile

@@ -58,6 +58,7 @@ BUILTIN_FILES = \
   gcc_builtin_headers_ia32-2.inc \
   gcc_builtin_headers_ia32-3.inc \
   gcc_builtin_headers_ia32-4.inc \
+  gcc_builtin_headers_ia32-5.inc \
   gcc_builtin_headers_ia32.inc \
   gcc_builtin_headers_math.inc \
   gcc_builtin_headers_mem_string.inc \

src/ansi-c/ansi_c_internal_additions.cpp

@@ -63,6 +63,9 @@ const char gcc_builtin_headers_ia32_3[]=
 const char gcc_builtin_headers_ia32_4[]=
 #include "gcc_builtin_headers_ia32-4.inc"
 ; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_5[] =
+#include "gcc_builtin_headers_ia32-5.inc"
+  ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_alpha[]=
 "# 1 \"gcc_builtin_headers_alpha.h\"\n"

src/ansi-c/ansi_c_internal_additions.h

@@ -28,6 +28,7 @@ extern const char gcc_builtin_headers_ia32[];
 extern const char gcc_builtin_headers_ia32_2[];
 extern const char gcc_builtin_headers_ia32_3[];
 extern const char gcc_builtin_headers_ia32_4[];
+extern const char gcc_builtin_headers_ia32_5[];
 extern const char gcc_builtin_headers_alpha[];
 extern const char gcc_builtin_headers_arm[];
 extern const char gcc_builtin_headers_mips[];

src/ansi-c/builtin_factory.cpp

@@ -175,6 +175,9 @@ bool builtin_factory(
 
       if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s))
         return convert(identifier, s, symbol_table, mh);
+
+      if(find_pattern(pattern, gcc_builtin_headers_ia32_5, s))
+        return convert(identifier, s, symbol_table, mh);
     }
     else if(config.ansi_c.arch=="arm64" ||
             config.ansi_c.arch=="armel" ||

src/ansi-c/gcc_builtin_headers_generic.h

@@ -1,6 +1,7 @@
 // clang-format off
 // stdarg
 void* __builtin_apply_args();
+void* __builtin_apply(void (*)(), void*, __CPROVER_size_t);
 void __builtin_ms_va_end(void *ap);
 void __builtin_ms_va_start(void *ap, ...);
 void* __builtin_next_arg();
@@ -21,46 +22,7 @@ int __builtin_execv(const char*, const char**);
 int __builtin_execve(const char*, const char**, const char**);
 int __builtin_execvp(const char*, const char**);
 void __builtin_exit(int);
-
-// stdio
-int __builtin___fprintf_chk(void*, int, const char*, ...);
-int __builtin___printf_chk(int, const char*, ...);
-int __builtin___snprintf_chk(char*, __CPROVER_size_t, int, __CPROVER_size_t, const char*, ...);
-int __builtin___sprintf_chk(char*, int, __CPROVER_size_t, const char*, ...);
-int __builtin___vfprintf_chk(void*, int, const char*, __builtin_va_list);
-int __builtin___vprintf_chk(int, const char*, __builtin_va_list);
-int __builtin___vsnprintf_chk (char *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
-int __builtin___vsnprintf_chk(char*, __CPROVER_size_t, int, __CPROVER_size_t, const char*, __builtin_va_list);
-int __builtin___vsprintf_chk(char*, int, __CPROVER_size_t, const char*, __builtin_va_list);
-long __builtin_expect(long, long);
-int __builtin_fprintf(void *stream, const char *fmt, ...);
-int __builtin_fprintf_unlocked(void*, const char*, ...);
-int __builtin_fputc(int, void*);
-int __builtin_fputc_unlocked(int, void*);
-int __builtin_fputs(const char *s, void *stream);
-int __builtin_fputs_unlocked(const char*, void*);
-int __builtin_fscanf(void *stream, const char *fmt, ...);
-__CPROVER_size_t __builtin_fwrite(const void*, __CPROVER_size_t, __CPROVER_size_t, void*);
-__CPROVER_size_t __builtin_fwrite_unlocked(const void*, __CPROVER_size_t, __CPROVER_size_t, void*);
-int __builtin_printf(const char*, ...);
-int __builtin_printf_unlocked(const char*, ...);
-int __builtin_putc(int, void*);
-int __builtin_putc_unlocked(int, void*);
-int __builtin_putchar(int);
-int __builtin_putchar_unlocked(int);
-int __builtin_puts(const char*);
-int __builtin_puts_unlocked(const char*);
-int __builtin_scanf(const char *str, const char *fmt, ...);
-int __builtin_snprintf(char*, __CPROVER_size_t, const char*, ...);
-int __builtin_sprintf(char*, const char*, ...);
-int __builtin_sscanf(const char*, const char*, ...);
-int __builtin_vfprintf(void*, const char*, __builtin_va_list);
-int __builtin_vfscanf(void*, const char*, __builtin_va_list);
-int __builtin_vprintf(const char*, __builtin_va_list);
-int __builtin_vscanf(const char*, __builtin_va_list);
-int __builtin_vsnprintf(char*, __CPROVER_size_t, const char*, __builtin_va_list);
-int __builtin_vsprintf(char*, const char*, __builtin_va_list);
-int __builtin_vsscanf(const char*, const char*, __builtin_va_list);
+pid_t __builtin_fork();
 
 // atomics
 void __sync_synchronize();
@@ -77,11 +39,16 @@ int __builtin_classify_type();
 int __builtin_constant_p(int);
 void __builtin_trap(void);
 void __builtin_unreachable(void);
+long __builtin_expect(long, long);
+long __builtin_expect_with_probability(long, long, double);
+void __builtin_clear_padding();
+void __builtin_speculation_safe_value();
+void* __builtin_speculation_safe_value_ptr(void*, ...);
 
 void* __builtin_dwarf_cfa();
 unsigned __builtin_dwarf_sp_column();
 int __builtin_eh_return_data_regno(int);
-void __builtin_init_dwarf_reg___CPROVER_size_table(void*);
+void __builtin_init_dwarf_reg_size_table(void*);
 void __builtin_unwind_init();
 
 const char* __builtin_FILE();

src/ansi-c/gcc_builtin_headers_ia32-2.h

@@ -94,9 +94,9 @@ void __builtin_ia32_pmovqw512mem_mask(__gcc_v8hi*, __gcc_v8di, unsigned char);
 void __builtin_ia32_pmovusdw512mem_mask(__gcc_v16hi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovsdw512mem_mask(__gcc_v16hi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovdw512mem_mask(__gcc_v16hi*, __gcc_v16si, unsigned short);
-void __builtin_ia32_pmovqb512mem_mask(__gcc_v16qi*, __gcc_v8di, unsigned char);
-void __builtin_ia32_pmovusqb512mem_mask(__gcc_v16qi*, __gcc_v8di, unsigned char);
-void __builtin_ia32_pmovsqb512mem_mask(__gcc_v16qi*, __gcc_v8di, unsigned char);
+void __builtin_ia32_pmovqb512mem_mask(unsigned long long*, __gcc_v8di, unsigned char);
+void __builtin_ia32_pmovusqb512mem_mask(unsigned long long*, __gcc_v8di, unsigned char);
+void __builtin_ia32_pmovsqb512mem_mask(unsigned long long*, __gcc_v8di, unsigned char);
 void __builtin_ia32_pmovusdb512mem_mask(__gcc_v16qi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovsdb512mem_mask(__gcc_v16qi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovdb512mem_mask(__gcc_v16qi*, __gcc_v16si, unsigned short);
@@ -129,36 +129,36 @@ __gcc_v4sf __builtin_ia32_copysignps(__gcc_v4sf, __gcc_v4sf);
 float __builtin_ia32_rsqrtf(float);
 __gcc_v2df __builtin_ia32_copysignpd(__gcc_v2df, __gcc_v2df);
 __gcc_v4si __builtin_ia32_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
-__gcc_v2df __builtin_ia32_floorpd(__gcc_v2df, const int);
-__gcc_v2df __builtin_ia32_ceilpd(__gcc_v2df, const int);
-__gcc_v2df __builtin_ia32_truncpd(__gcc_v2df, const int);
+__gcc_v2df __builtin_ia32_floorpd(__gcc_v2df);
+__gcc_v2df __builtin_ia32_ceilpd(__gcc_v2df);
+__gcc_v2df __builtin_ia32_truncpd(__gcc_v2df);
 __gcc_v2df __builtin_ia32_rintpd(__gcc_v2df, const int);
-__gcc_v4si __builtin_ia32_floorpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df, const int);
-__gcc_v4si __builtin_ia32_ceilpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df, const int);
+__gcc_v4si __builtin_ia32_floorpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
+__gcc_v4si __builtin_ia32_ceilpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
 __gcc_v2df __builtin_ia32_roundpd_az(__gcc_v2df);
 __gcc_v4si __builtin_ia32_roundpd_az_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
-__gcc_v4sf __builtin_ia32_floorps(__gcc_v4sf, const int);
-__gcc_v4sf __builtin_ia32_ceilps(__gcc_v4sf, const int);
-__gcc_v4sf __builtin_ia32_truncps(__gcc_v4sf, const int);
+__gcc_v4sf __builtin_ia32_floorps(__gcc_v4sf);
+__gcc_v4sf __builtin_ia32_ceilps(__gcc_v4sf);
+__gcc_v4sf __builtin_ia32_truncps(__gcc_v4sf);
 __gcc_v4sf __builtin_ia32_rintps(__gcc_v4sf, const int);
-__gcc_v4si __builtin_ia32_floorps_sfix(__gcc_v4sf, const int);
-__gcc_v4si __builtin_ia32_ceilps_sfix(__gcc_v4sf, const int);
+__gcc_v4si __builtin_ia32_floorps_sfix(__gcc_v4sf);
+__gcc_v4si __builtin_ia32_ceilps_sfix(__gcc_v4sf);
 __gcc_v4sf __builtin_ia32_roundps_az(__gcc_v4sf);
 __gcc_v4si __builtin_ia32_roundps_az_sfix(__gcc_v4sf);
-__gcc_v4df __builtin_ia32_floorpd256(__gcc_v4df, const int);
-__gcc_v4df __builtin_ia32_ceilpd256(__gcc_v4df, const int);
-__gcc_v4df __builtin_ia32_truncpd256(__gcc_v4df, const int);
+__gcc_v4df __builtin_ia32_floorpd256(__gcc_v4df);
+__gcc_v4df __builtin_ia32_ceilpd256(__gcc_v4df);
+__gcc_v4df __builtin_ia32_truncpd256(__gcc_v4df);
 __gcc_v4df __builtin_ia32_rintpd256(__gcc_v4df, const int);
 __gcc_v4df __builtin_ia32_roundpd_az256(__gcc_v4df);
 __gcc_v8si __builtin_ia32_roundpd_az_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
-__gcc_v8si __builtin_ia32_floorpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df, const int);
-__gcc_v8si __builtin_ia32_ceilpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df, const int);
-__gcc_v8sf __builtin_ia32_floorps256(__gcc_v8sf, const int);
-__gcc_v8sf __builtin_ia32_ceilps256(__gcc_v8sf, const int);
-__gcc_v8sf __builtin_ia32_truncps256(__gcc_v8sf, const int);
+__gcc_v8si __builtin_ia32_floorpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
+__gcc_v8si __builtin_ia32_ceilpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
+__gcc_v8sf __builtin_ia32_floorps256(__gcc_v8sf);
+__gcc_v8sf __builtin_ia32_ceilps256(__gcc_v8sf);
+__gcc_v8sf __builtin_ia32_truncps256(__gcc_v8sf);
 __gcc_v8sf __builtin_ia32_rintps256(__gcc_v8sf, const int);
-__gcc_v8si __builtin_ia32_floorps_sfix256(__gcc_v8sf, const int);
-__gcc_v8si __builtin_ia32_ceilps_sfix256(__gcc_v8sf, const int);
+__gcc_v8si __builtin_ia32_floorps_sfix256(__gcc_v8sf);
+__gcc_v8si __builtin_ia32_ceilps_sfix256(__gcc_v8sf);
 __gcc_v8sf __builtin_ia32_roundps_az256(__gcc_v8sf);
 __gcc_v8si __builtin_ia32_roundps_az_sfix256(__gcc_v8sf);
 __gcc_v8sf __builtin_ia32_copysignps256(__gcc_v8sf, __gcc_v8sf);
@@ -197,7 +197,7 @@ __gcc_v16si __builtin_ia32_broadcasti32x4_512(__gcc_v4si, __gcc_v16si, unsigned
 __gcc_v8di __builtin_ia32_broadcasti64x4_512(__gcc_v4di, __gcc_v8di, unsigned char);
 __gcc_v8df __builtin_ia32_broadcastsd512(__gcc_v2df, __gcc_v8df, unsigned char);
 __gcc_v16sf __builtin_ia32_broadcastss512(__gcc_v4sf, __gcc_v16sf, unsigned short);
-short __builtin_ia32_cmpd512_mask(__gcc_v16si, __gcc_v16si, int, short);
+unsigned short __builtin_ia32_cmpd512_mask(__gcc_v16si, __gcc_v16si, int, unsigned short);
 unsigned char __builtin_ia32_cmpq512_mask(__gcc_v8di, __gcc_v8di, int, unsigned char);
 __gcc_v8df __builtin_ia32_compressdf512_mask(__gcc_v8df, __gcc_v8df, unsigned char);
 __gcc_v16sf __builtin_ia32_compresssf512_mask(__gcc_v16sf, __gcc_v16sf, unsigned short);
@@ -296,22 +296,22 @@ __gcc_v8di __builtin_ia32_prorq512_mask(__gcc_v8di, int, __gcc_v8di, unsigned ch
 __gcc_v16si __builtin_ia32_prorvd512_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_prorvq512_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_pshufd512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
-__gcc_v16si __builtin_ia32_pslld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, short);
-__gcc_v16si __builtin_ia32_pslldi512_mask(__gcc_v16si, int, __gcc_v16si, short);
-__gcc_v8di __builtin_ia32_psllq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, char);
-__gcc_v8di __builtin_ia32_psllqi512_mask(__gcc_v8di, int, __gcc_v8di, char);
+__gcc_v16si __builtin_ia32_pslld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, unsigned short);
+__gcc_v16si __builtin_ia32_pslldi512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
+__gcc_v8di __builtin_ia32_psllq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, unsigned char);
+__gcc_v8di __builtin_ia32_psllqi512_mask(__gcc_v8di, int, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psllv16si_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_psllv8di_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
-__gcc_v16si __builtin_ia32_psrad512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, short);
-__gcc_v16si __builtin_ia32_psradi512_mask(__gcc_v16si, int, __gcc_v16si, short);
-__gcc_v8di __builtin_ia32_psraq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, char);
-__gcc_v8di __builtin_ia32_psraqi512_mask(__gcc_v8di, int, __gcc_v8di, char);
+__gcc_v16si __builtin_ia32_psrad512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, unsigned short);
+__gcc_v16si __builtin_ia32_psradi512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
+__gcc_v8di __builtin_ia32_psraq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, unsigned char);
+__gcc_v8di __builtin_ia32_psraqi512_mask(__gcc_v8di, int, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psrav16si_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_psrav8di_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
-__gcc_v16si __builtin_ia32_psrld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, short);
-__gcc_v16si __builtin_ia32_psrldi512_mask(__gcc_v16si, int, __gcc_v16si, short);
-__gcc_v8di __builtin_ia32_psrlq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, char);
-__gcc_v8di __builtin_ia32_psrlqi512_mask(__gcc_v8di, int, __gcc_v8di, char);
+__gcc_v16si __builtin_ia32_psrld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, unsigned short);
+__gcc_v16si __builtin_ia32_psrldi512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
+__gcc_v8di __builtin_ia32_psrlq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, unsigned char);
+__gcc_v8di __builtin_ia32_psrlqi512_mask(__gcc_v8di, int, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psrlv16si_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_psrlv8di_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psubd512_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
@@ -340,7 +340,7 @@ __gcc_v16sf __builtin_ia32_shuf_f32x4_mask(__gcc_v16sf, __gcc_v16sf, int, __gcc_
 __gcc_v8df __builtin_ia32_shuf_f64x2_mask(__gcc_v8df, __gcc_v8df, int, __gcc_v8df, unsigned char);
 __gcc_v16si __builtin_ia32_shuf_i32x4_mask(__gcc_v16si, __gcc_v16si, int, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_shuf_i64x2_mask(__gcc_v8di, __gcc_v8di, int, __gcc_v8di, unsigned char);
-short __builtin_ia32_ucmpd512_mask(__gcc_v16si, __gcc_v16si, int, short);
+unsigned short __builtin_ia32_ucmpd512_mask(__gcc_v16si, __gcc_v16si, int, unsigned short);
 unsigned char __builtin_ia32_ucmpq512_mask(__gcc_v8di, __gcc_v8di, int, unsigned char);
 __gcc_v8df __builtin_ia32_unpckhpd512_mask(__gcc_v8df, __gcc_v8df, __gcc_v8df, unsigned char);
 __gcc_v16sf __builtin_ia32_unpckhps512_mask(__gcc_v16sf, __gcc_v16sf, __gcc_v16sf, unsigned short);
@@ -382,8 +382,8 @@ __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);
-__gcc_v16si __builtin_ia32_ceilpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df, const int);
+__gcc_v16si __builtin_ia32_floorpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df);
+__gcc_v16si __builtin_ia32_ceilpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df);
 unsigned short __builtin_ia32_kandhi(unsigned short, unsigned short);
 unsigned short __builtin_ia32_kandnhi(unsigned short, unsigned short);
 unsigned short __builtin_ia32_knothi(unsigned short);