C front-end: declare further GCC built-ins

These cover the set of functions reported as undefined while trying to
compile aws-c-common.

Author: tautschnig

src/ansi-c/CMakeLists.txt

@@ -72,6 +72,7 @@ make_inc(compiler_headers/gcc_builtin_headers_omp)
 make_inc(compiler_headers/gcc_builtin_headers_power)
 make_inc(compiler_headers/gcc_builtin_headers_tm)
 make_inc(compiler_headers/gcc_builtin_headers_types)
+make_inc(compiler_headers/gcc_builtin_headers_types_gcc7plus)
 make_inc(compiler_headers/gcc_builtin_headers_ubsan)
 make_inc(compiler_headers/windows_builtin_headers)
 make_inc(cprover_builtin_headers)
@@ -95,6 +96,7 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_power.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_tm.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types_gcc7plus.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ubsan.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/windows_builtin_headers.inc
     ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc

src/ansi-c/Makefile

@@ -68,6 +68,7 @@ BUILTIN_FILES = \
   compiler_headers/gcc_builtin_headers_power.inc \
   compiler_headers/gcc_builtin_headers_tm.inc \
   compiler_headers/gcc_builtin_headers_types.inc \
+  compiler_headers/gcc_builtin_headers_types_gcc7plus.inc \
   compiler_headers/gcc_builtin_headers_ubsan.inc \
   compiler_headers/windows_builtin_headers.inc
 

src/ansi-c/ansi_c_internal_additions.cpp

@@ -11,15 +11,23 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #include <linking/static_lifetime_init.h>
 
-#include <goto-programs/adjust_float_expressions.h>
+#include "ansi_c_parser.h"
 
 const char gcc_builtin_headers_types[] =
   "#line 1 \"gcc_builtin_headers_types.h\"\n"
 #include "compiler_headers/gcc_builtin_headers_types.inc" // IWYU pragma: keep
   ; // NOLINT(whitespace/semicolon)
 
+const char gcc_builtin_headers_types_gcc7plus[] =
+  "#line 1 \"gcc_builtin_headers_types_gcc7plus.h\"\n"
+// NOLINTNEXTLINE(whitespace/line_length)
+#include "compiler_headers/gcc_builtin_headers_types_gcc7plus.inc" // IWYU pragma: keep
+  ; // NOLINT(whitespace/semicolon)
+
 const char gcc_builtin_headers_generic[] =
   "#line 1 \"gcc_builtin_headers_generic.h\"\n"
 #include "compiler_headers/gcc_builtin_headers_generic.inc" // IWYU pragma: keep
@@ -229,6 +237,10 @@ void ansi_c_internal_additions(std::string &code)
     config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     code+=gcc_builtin_headers_types;
+    // check the parser and not config.ansi_c.ts_18661_3_Floatn_types to adjust
+    // behaviour depending on C or C++ context
+    if(ansi_c_parser.ts_18661_3_Floatn_types)
+      code += gcc_builtin_headers_types_gcc7plus;
 
     // there are many more, e.g., look at
     // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html

src/ansi-c/ansi_c_internal_additions.h

@@ -18,6 +18,7 @@ void ansi_c_architecture_strings(std::string &code);
 extern const char clang_builtin_headers[];
 extern const char cprover_builtin_headers[];
 extern const char gcc_builtin_headers_types[];
+extern const char gcc_builtin_headers_types_gcc7plus[];
 extern const char gcc_builtin_headers_generic[];
 extern const char gcc_builtin_headers_math[];
 extern const char gcc_builtin_headers_mem_string[];

src/ansi-c/compiler_headers/clang_builtin_headers.h

@@ -93,4 +93,8 @@ unsigned int __builtin_rotateright32(unsigned int, unsigned int);
 unsigned long long __builtin_rotateright64(unsigned long long, unsigned long long);
 
 void __builtin_assume(__CPROVER_bool);
+
+void __builtin_cpu_init(void);
+_Bool __builtin_cpu_is(const char *);
+_Bool __builtin_cpu_supports(const char *);
 // clang-format on

src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-5.h

@@ -309,6 +309,10 @@ __gcc_v2df __builtin_ia32_cvtsi642sd(__gcc_v2df, long long);
 __gcc_v4sf __builtin_ia32_cvtsd2ss(__gcc_v4sf, __gcc_v2df);
 __gcc_v2df __builtin_ia32_cvtss2sd(__gcc_v2df, __gcc_v4sf);
 void __builtin_ia32_clflush(const void*);
+void __builtin_ia32_cldemote(const void*);
+void __builtin_ia32_clflushopt(const void*);
+void __builtin_ia32_clwb(const void*);
+void __builtin_ia32_clzero(void*);
 void __builtin_ia32_lfence(void);
 void __builtin_ia32_mfence(void);
 __gcc_v16qi __builtin_ia32_loaddqu(const char*);

src/ansi-c/compiler_headers/gcc_builtin_headers_ia32.h

@@ -0,0 +1,3 @@
+typedef _Float16 __gcc_v8hf __attribute__((__vector_size__(16)));
+typedef _Float16 __gcc_v16hf __attribute__((__vector_size__(32)));
+typedef _Float16 __gcc_v32hf __attribute__((__vector_size__(64)));

src/ansi-c/compiler_headers/gcc_builtin_headers_types_gcc7plus.h

@@ -19,6 +19,7 @@
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/cprover_library.h>
+#include <ansi-c/gcc_version.h>
 #include <assembler/remove_asm.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/multi_path_symex_checker.h>
@@ -59,6 +60,13 @@ api_sessiont::api_sessiont(const api_optionst &options)
   config.set(cmdline);
   // Initialise C language mode
   register_language(new_ansi_c_language);
+  // configure gcc, if required -- get_goto_program will have set the config
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
 }
 
 api_sessiont::~api_sessiont() = default;