Merge pull request #7593 from tautschnig/bugfixes/avx

C front-end: declare further GCC built-ins

Author: tautschnig

src/ansi-c/CMakeLists.txt

@@ -65,13 +65,15 @@ make_inc(compiler_headers/gcc_builtin_headers_ia32-2)
 make_inc(compiler_headers/gcc_builtin_headers_ia32-3)
 make_inc(compiler_headers/gcc_builtin_headers_ia32-4)
 make_inc(compiler_headers/gcc_builtin_headers_ia32-5)
+make_inc(compiler_headers/gcc_builtin_headers_ia32-6)
 make_inc(compiler_headers/gcc_builtin_headers_math)
 make_inc(compiler_headers/gcc_builtin_headers_mem_string)
 make_inc(compiler_headers/gcc_builtin_headers_mips)
 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)
@@ -87,6 +89,7 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-3.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-4.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-5.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-6.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_math.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mem_string.inc
@@ -95,6 +98,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

@@ -60,6 +60,7 @@ BUILTIN_FILES = \
   compiler_headers/gcc_builtin_headers_ia32-3.inc \
   compiler_headers/gcc_builtin_headers_ia32-4.inc \
   compiler_headers/gcc_builtin_headers_ia32-5.inc \
+  compiler_headers/gcc_builtin_headers_ia32-6.inc \
   compiler_headers/gcc_builtin_headers_ia32.inc \
   compiler_headers/gcc_builtin_headers_math.inc \
   compiler_headers/gcc_builtin_headers_mem_string.inc \
@@ -68,6 +69,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, kroening@kroening.com
 #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
@@ -65,6 +73,9 @@ const char gcc_builtin_headers_ia32_4[] =
 const char gcc_builtin_headers_ia32_5[] =
 #include "compiler_headers/gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
   ; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_6[] =
+#include "compiler_headers/gcc_builtin_headers_ia32-6.inc" // IWYU pragma: keep
+  ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_alpha[] =
   "#line 1 \"gcc_builtin_headers_alpha.h\"\n"
@@ -229,6 +240,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[];
@@ -29,6 +30,7 @@ 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_ia32_6[];
 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

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

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/clang_builtins.py

@@ -43,7 +43,7 @@
         'v': 'void',
         'w': 'wchar_t',
         'x': '_Float16',
-        'y': '__bf16',
+        'y': '_Float16', # would be '__bf16', but we don't support that yet
         'z': '__CPROVER_size_t'
         }
 
@@ -209,7 +209,7 @@ def process_line(name, types, attributes):
     i = 0
     while i < len(types):
         (t, i_updated) = build_type(types, i)
-        assert i_updated > i, ('failed to parse type spec of' + name + ': ' +
+        assert i_updated > i, ('failed to parse type spec of ' + name + ': ' +
                                types[i:])
         i = i_updated
         type_specs.append(t)