Skip to content

Commit a108335

Browse files
tautschnigtautschnig
authored
Merge pull request #6707 from tautschnig/feature/clang-builtins-fetcher
Move and cleanup declarations of C compiler intrinsics
2 parents 8f8d169 + 371d886 commit a108335

26 files changed

+638
-337
lines changed

‎src/ansi-c/CMakeLists.txt

+42-40
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,9 @@ add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
1212
add_executable(file_converter file_converter.cpp)
1313

1414
function(make_inc name)
15+
get_filename_component(inc_path "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc" DIRECTORY)
1516
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc"
17+
COMMAND ${CMAKE_COMMAND} -E make_directory ${inc_path}
1618
COMMAND file_converter "${CMAKE_CURRENT_SOURCE_DIR}/${name}.h" > "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc"
1719
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${name}.h" file_converter
1820
)
@@ -52,51 +54,51 @@ endif()
5254

5355
################################################################################
5456

55-
make_inc(arm_builtin_headers)
56-
make_inc(clang_builtin_headers)
57+
make_inc(compiler_headers/arm_builtin_headers)
58+
make_inc(compiler_headers/clang_builtin_headers)
59+
make_inc(compiler_headers/cw_builtin_headers)
60+
make_inc(compiler_headers/gcc_builtin_headers_alpha)
61+
make_inc(compiler_headers/gcc_builtin_headers_arm)
62+
make_inc(compiler_headers/gcc_builtin_headers_generic)
63+
make_inc(compiler_headers/gcc_builtin_headers_ia32)
64+
make_inc(compiler_headers/gcc_builtin_headers_ia32-2)
65+
make_inc(compiler_headers/gcc_builtin_headers_ia32-3)
66+
make_inc(compiler_headers/gcc_builtin_headers_ia32-4)
67+
make_inc(compiler_headers/gcc_builtin_headers_ia32-5)
68+
make_inc(compiler_headers/gcc_builtin_headers_math)
69+
make_inc(compiler_headers/gcc_builtin_headers_mem_string)
70+
make_inc(compiler_headers/gcc_builtin_headers_mips)
71+
make_inc(compiler_headers/gcc_builtin_headers_omp)
72+
make_inc(compiler_headers/gcc_builtin_headers_power)
73+
make_inc(compiler_headers/gcc_builtin_headers_tm)
74+
make_inc(compiler_headers/gcc_builtin_headers_types)
75+
make_inc(compiler_headers/gcc_builtin_headers_ubsan)
76+
make_inc(compiler_headers/windows_builtin_headers)
5777
make_inc(cprover_builtin_headers)
58-
make_inc(cw_builtin_headers)
59-
make_inc(gcc_builtin_headers_alpha)
60-
make_inc(gcc_builtin_headers_arm)
61-
make_inc(gcc_builtin_headers_generic)
62-
make_inc(gcc_builtin_headers_ia32)
63-
make_inc(gcc_builtin_headers_ia32-2)
64-
make_inc(gcc_builtin_headers_ia32-3)
65-
make_inc(gcc_builtin_headers_ia32-4)
66-
make_inc(gcc_builtin_headers_ia32-5)
67-
make_inc(gcc_builtin_headers_math)
68-
make_inc(gcc_builtin_headers_mem_string)
69-
make_inc(gcc_builtin_headers_mips)
70-
make_inc(gcc_builtin_headers_omp)
71-
make_inc(gcc_builtin_headers_power)
72-
make_inc(gcc_builtin_headers_tm)
73-
make_inc(gcc_builtin_headers_types)
74-
make_inc(gcc_builtin_headers_ubsan)
75-
make_inc(windows_builtin_headers)
7678

7779
set(extra_dependencies
78-
${CMAKE_CURRENT_BINARY_DIR}/arm_builtin_headers.inc
79-
${CMAKE_CURRENT_BINARY_DIR}/clang_builtin_headers.inc
80+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/arm_builtin_headers.inc
81+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/clang_builtin_headers.inc
82+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/cw_builtin_headers.inc
83+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_alpha.inc
84+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_arm.inc
85+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_generic.inc
86+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-2.inc
87+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-3.inc
88+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-4.inc
89+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-5.inc
90+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32.inc
91+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_math.inc
92+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mem_string.inc
93+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mips.inc
94+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_omp.inc
95+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_power.inc
96+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_tm.inc
97+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types.inc
98+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ubsan.inc
99+
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/windows_builtin_headers.inc
80100
${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
81101
${CMAKE_CURRENT_BINARY_DIR}/cprover_builtin_headers.inc
82-
${CMAKE_CURRENT_BINARY_DIR}/cw_builtin_headers.inc
83-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_alpha.inc
84-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_arm.inc
85-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_generic.inc
86-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
87-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
88-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
89-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-5.inc
90-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
91-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
92-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc
93-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mips.inc
94-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc
95-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc
96-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc
97-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_types.inc
98-
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
99-
${CMAKE_CURRENT_BINARY_DIR}/windows_builtin_headers.inc
100102
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
101103
)
102104

‎src/ansi-c/Makefile

+20-20
Original file line numberDiff line numberDiff line change
@@ -49,27 +49,27 @@ include ../config.inc
4949
include ../common
5050

5151
BUILTIN_FILES = \
52-
arm_builtin_headers.inc \
53-
clang_builtin_headers.inc \
5452
cprover_builtin_headers.inc \
55-
cw_builtin_headers.inc \
56-
gcc_builtin_headers_alpha.inc \
57-
gcc_builtin_headers_arm.inc \
58-
gcc_builtin_headers_generic.inc \
59-
gcc_builtin_headers_ia32-2.inc \
60-
gcc_builtin_headers_ia32-3.inc \
61-
gcc_builtin_headers_ia32-4.inc \
62-
gcc_builtin_headers_ia32-5.inc \
63-
gcc_builtin_headers_ia32.inc \
64-
gcc_builtin_headers_math.inc \
65-
gcc_builtin_headers_mem_string.inc \
66-
gcc_builtin_headers_mips.inc \
67-
gcc_builtin_headers_omp.inc \
68-
gcc_builtin_headers_power.inc \
69-
gcc_builtin_headers_tm.inc \
70-
gcc_builtin_headers_types.inc \
71-
gcc_builtin_headers_ubsan.inc \
72-
windows_builtin_headers.inc
53+
compiler_headers/arm_builtin_headers.inc \
54+
compiler_headers/clang_builtin_headers.inc \
55+
compiler_headers/cw_builtin_headers.inc \
56+
compiler_headers/gcc_builtin_headers_alpha.inc \
57+
compiler_headers/gcc_builtin_headers_arm.inc \
58+
compiler_headers/gcc_builtin_headers_generic.inc \
59+
compiler_headers/gcc_builtin_headers_ia32-2.inc \
60+
compiler_headers/gcc_builtin_headers_ia32-3.inc \
61+
compiler_headers/gcc_builtin_headers_ia32-4.inc \
62+
compiler_headers/gcc_builtin_headers_ia32-5.inc \
63+
compiler_headers/gcc_builtin_headers_ia32.inc \
64+
compiler_headers/gcc_builtin_headers_math.inc \
65+
compiler_headers/gcc_builtin_headers_mem_string.inc \
66+
compiler_headers/gcc_builtin_headers_mips.inc \
67+
compiler_headers/gcc_builtin_headers_omp.inc \
68+
compiler_headers/gcc_builtin_headers_power.inc \
69+
compiler_headers/gcc_builtin_headers_tm.inc \
70+
compiler_headers/gcc_builtin_headers_types.inc \
71+
compiler_headers/gcc_builtin_headers_ubsan.inc \
72+
compiler_headers/windows_builtin_headers.inc
7373

7474
CLEANFILES = ansi-c$(LIBEXT) \
7575
ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \

‎src/ansi-c/ansi_c_internal_additions.cpp

+41-40
Original file line numberDiff line numberDiff line change
@@ -17,92 +17,93 @@ Author: Daniel Kroening, [email protected]
1717

1818
const char gcc_builtin_headers_types[] =
1919
"#line 1 \"gcc_builtin_headers_types.h\"\n"
20-
#include "gcc_builtin_headers_types.inc" // IWYU pragma: keep
21-
; // NOLINT(whitespace/semicolon)
20+
#include "compiler_headers/gcc_builtin_headers_types.inc" // IWYU pragma: keep
21+
; // NOLINT(whitespace/semicolon)
2222

2323
const char gcc_builtin_headers_generic[] =
2424
"#line 1 \"gcc_builtin_headers_generic.h\"\n"
25-
#include "gcc_builtin_headers_generic.inc" // IWYU pragma: keep
26-
; // NOLINT(whitespace/semicolon)
25+
#include "compiler_headers/gcc_builtin_headers_generic.inc" // IWYU pragma: keep
26+
; // NOLINT(whitespace/semicolon)
2727

2828
const char gcc_builtin_headers_math[] =
2929
"#line 1 \"gcc_builtin_headers_math.h\"\n"
30-
#include "gcc_builtin_headers_math.inc" // IWYU pragma: keep
31-
; // NOLINT(whitespace/semicolon)
30+
#include "compiler_headers/gcc_builtin_headers_math.inc" // IWYU pragma: keep
31+
; // NOLINT(whitespace/semicolon)
3232

3333
const char gcc_builtin_headers_mem_string[] =
3434
"#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
35-
#include "gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
36-
; // NOLINT(whitespace/semicolon)
35+
// NOLINTNEXTLINE(whitespace/line_length)
36+
#include "compiler_headers/gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
37+
; // NOLINT(whitespace/semicolon)
3738

3839
const char gcc_builtin_headers_omp[] = "#line 1 \"gcc_builtin_headers_omp.h\"\n"
39-
#include "gcc_builtin_headers_omp.inc" // IWYU pragma: keep
40-
; // NOLINT(whitespace/semicolon)
40+
#include "compiler_headers/gcc_builtin_headers_omp.inc" // IWYU pragma: keep
41+
; // NOLINT(whitespace/semicolon)
4142

4243
const char gcc_builtin_headers_tm[] = "#line 1 \"gcc_builtin_headers_tm.h\"\n"
43-
#include "gcc_builtin_headers_tm.inc" // IWYU pragma: keep
44-
; // NOLINT(whitespace/semicolon)
44+
#include "compiler_headers/gcc_builtin_headers_tm.inc" // IWYU pragma: keep
45+
; // NOLINT(whitespace/semicolon)
4546

4647
const char gcc_builtin_headers_ubsan[] =
4748
"#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
48-
#include "gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
49-
; // NOLINT(whitespace/semicolon)
49+
#include "compiler_headers/gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
50+
; // NOLINT(whitespace/semicolon)
5051

5152
const char gcc_builtin_headers_ia32[] =
5253
"#line 1 \"gcc_builtin_headers_ia32.h\"\n"
53-
#include "gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
54-
; // NOLINT(whitespace/semicolon)
54+
#include "compiler_headers/gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
55+
; // NOLINT(whitespace/semicolon)
5556
const char gcc_builtin_headers_ia32_2[] =
56-
#include "gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
57-
; // NOLINT(whitespace/semicolon)
57+
#include "compiler_headers/gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
58+
; // NOLINT(whitespace/semicolon)
5859
const char gcc_builtin_headers_ia32_3[] =
59-
#include "gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
60-
; // NOLINT(whitespace/semicolon)
60+
#include "compiler_headers/gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
61+
; // NOLINT(whitespace/semicolon)
6162
const char gcc_builtin_headers_ia32_4[] =
62-
#include "gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
63-
; // NOLINT(whitespace/semicolon)
63+
#include "compiler_headers/gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
64+
; // NOLINT(whitespace/semicolon)
6465
const char gcc_builtin_headers_ia32_5[] =
65-
#include "gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
66-
; // NOLINT(whitespace/semicolon)
66+
#include "compiler_headers/gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
67+
; // NOLINT(whitespace/semicolon)
6768

6869
const char gcc_builtin_headers_alpha[] =
6970
"#line 1 \"gcc_builtin_headers_alpha.h\"\n"
70-
#include "gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
71-
; // NOLINT(whitespace/semicolon)
71+
#include "compiler_headers/gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
72+
; // NOLINT(whitespace/semicolon)
7273

7374
const char gcc_builtin_headers_arm[] = "#line 1 \"gcc_builtin_headers_arm.h\"\n"
74-
#include "gcc_builtin_headers_arm.inc" // IWYU pragma: keep
75-
; // NOLINT(whitespace/semicolon)
75+
#include "compiler_headers/gcc_builtin_headers_arm.inc" // IWYU pragma: keep
76+
; // NOLINT(whitespace/semicolon)
7677

7778
const char gcc_builtin_headers_mips[] =
7879
"#line 1 \"gcc_builtin_headers_mips.h\"\n"
79-
#include "gcc_builtin_headers_mips.inc" // IWYU pragma: keep
80-
; // NOLINT(whitespace/semicolon)
80+
#include "compiler_headers/gcc_builtin_headers_mips.inc" // IWYU pragma: keep
81+
; // NOLINT(whitespace/semicolon)
8182

8283
const char gcc_builtin_headers_power[] =
8384
"#line 1 \"gcc_builtin_headers_power.h\"\n"
84-
#include "gcc_builtin_headers_power.inc" // IWYU pragma: keep
85-
; // NOLINT(whitespace/semicolon)
85+
#include "compiler_headers/gcc_builtin_headers_power.inc" // IWYU pragma: keep
86+
; // NOLINT(whitespace/semicolon)
8687

8788
const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n"
88-
#include "arm_builtin_headers.inc" // IWYU pragma: keep
89-
; // NOLINT(whitespace/semicolon)
89+
#include "compiler_headers/arm_builtin_headers.inc" // IWYU pragma: keep
90+
; // NOLINT(whitespace/semicolon)
9091

9192
const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n"
92-
#include "cw_builtin_headers.inc" // IWYU pragma: keep
93-
; // NOLINT(whitespace/semicolon)
93+
#include "compiler_headers/cw_builtin_headers.inc" // IWYU pragma: keep
94+
; // NOLINT(whitespace/semicolon)
9495

9596
const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n"
96-
#include "clang_builtin_headers.inc" // IWYU pragma: keep
97-
; // NOLINT(whitespace/semicolon)
97+
#include "compiler_headers/clang_builtin_headers.inc" // IWYU pragma: keep
98+
; // NOLINT(whitespace/semicolon)
9899

99100
const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n"
100101
#include "cprover_builtin_headers.inc" // IWYU pragma: keep
101102
; // NOLINT(whitespace/semicolon)
102103

103104
const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n"
104-
#include "windows_builtin_headers.inc" // IWYU pragma: keep
105-
; // NOLINT(whitespace/semicolon)
105+
#include "compiler_headers/windows_builtin_headers.inc" // IWYU pragma: keep
106+
; // NOLINT(whitespace/semicolon)
106107

107108
static std::string architecture_string(const std::string &value, const char *s)
108109
{

‎src/ansi-c/arm_builtin_headers.h ‎src/ansi-c/compiler_headers/arm_builtin_headers.h

File renamed without changes.

‎src/ansi-c/clang_builtin_headers.h ‎src/ansi-c/compiler_headers/clang_builtin_headers.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ void __builtin_ia32_vp2intersect_d_128(__gcc_v4si, __gcc_v4si, unsigned char *,
2020

2121
__gcc_v16qi __builtin_ia32_selectb_128(unsigned short, __gcc_v16qi, __gcc_v16qi);
2222
__gcc_v32qi __builtin_ia32_selectb_256(unsigned int, __gcc_v32qi, __gcc_v32qi);
23-
__gcc_v64qi __builtin_ia32_selectb_512(unsigned long, __gcc_v64qi, __gcc_v64qi);
23+
__gcc_v64qi __builtin_ia32_selectb_512(unsigned long int, __gcc_v64qi, __gcc_v64qi);
2424
__gcc_v8hi __builtin_ia32_selectw_128(unsigned char, __gcc_v8hi, __gcc_v8hi);
2525
__gcc_v16hi __builtin_ia32_selectw_256(unsigned short, __gcc_v16hi, __gcc_v16hi);
2626
__gcc_v32hi __builtin_ia32_selectw_512(unsigned int, __gcc_v32hi, __gcc_v32hi);
@@ -70,7 +70,7 @@ void __builtin_ia32_tdpbsud(__tile, __tile, __tile);
7070
void __builtin_ia32_tdpbusd(__tile, __tile, __tile);
7171
void __builtin_ia32_tdpbuud(__tile, __tile, __tile);
7272
void __builtin_ia32_tdpbf16ps(__tile, __tile, __tile);
73-
void __builtin_ia32_ptwrite64(unsigned long long);
73+
void __builtin_ia32_ptwrite64(unsigned long long int);
7474

7575
void __builtin_nontemporal_store();
7676
void __builtin_nontemporal_load();

0 commit comments

Comments
 (0)