Skip to content

Commit a15b75f

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#1910 from diffblue/builtin-factory
on-demand definitions for compiler-built-in functions
2 parents 76b93e8 + 2c8ae92 commit a15b75f

11 files changed

+345
-142
lines changed

‎src/ansi-c/CMakeLists.txt

+2
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,7 @@ make_inc(gcc_builtin_headers_mips)
7272
make_inc(gcc_builtin_headers_omp)
7373
make_inc(gcc_builtin_headers_power)
7474
make_inc(gcc_builtin_headers_tm)
75+
make_inc(gcc_builtin_headers_types)
7576
make_inc(gcc_builtin_headers_ubsan)
7677

7778
set(extra_dependencies
@@ -92,6 +93,7 @@ set(extra_dependencies
9293
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc
9394
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc
9495
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc
96+
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_types.inc
9597
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
9698
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
9799
)

‎src/ansi-c/Makefile

+28-37
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ SRC = anonymous_member.cpp \
1010
ansi_c_scope.cpp \
1111
ansi_c_typecheck.cpp \
1212
ansi_c_y.tab.cpp \
13+
builtin_factory.cpp \
1314
c_misc.cpp \
1415
c_nondet_symbol_factory.cpp \
1516
c_preprocess.cpp \
@@ -43,20 +44,32 @@ INCLUDES= -I ..
4344
include ../config.inc
4445
include ../common
4546

47+
BUILTIN_FILES = \
48+
arm_builtin_headers.inc \
49+
clang_builtin_headers.inc \
50+
cw_builtin_headers.inc \
51+
gcc_builtin_headers_alpha.inc \
52+
gcc_builtin_headers_arm.inc \
53+
gcc_builtin_headers_generic.inc \
54+
gcc_builtin_headers_ia32-2.inc \
55+
gcc_builtin_headers_ia32-3.inc \
56+
gcc_builtin_headers_ia32-4.inc \
57+
gcc_builtin_headers_ia32.inc \
58+
gcc_builtin_headers_math.inc \
59+
gcc_builtin_headers_mem_string.inc \
60+
gcc_builtin_headers_mips.inc \
61+
gcc_builtin_headers_omp.inc \
62+
gcc_builtin_headers_power.inc \
63+
gcc_builtin_headers_tm.inc \
64+
gcc_builtin_headers_types.inc \
65+
gcc_builtin_headers_ubsan.inc
66+
4667
CLEANFILES = ansi-c$(LIBEXT) \
4768
ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \
4869
ansi_c_y.output \
4970
library/converter$(EXEEXT) cprover_library.inc \
5071
file_converter$(EXEEXT) library_check \
51-
gcc_builtin_headers_generic.inc gcc_builtin_headers_ia32.inc \
52-
arm_builtin_headers.inc cw_builtin_headers.inc \
53-
gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \
54-
gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \
55-
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
56-
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
57-
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
58-
gcc_builtin_headers_mem_string.inc \
59-
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
72+
$(BUILTIN_FILES)
6073

6174
all: ansi-c$(LIBEXT)
6275

@@ -102,34 +115,12 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c
102115

103116
cprover_library.cpp: cprover_library.inc
104117

105-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
106-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
107-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
108-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
109-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
110-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
111-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
112-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
113-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc
114-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc
115-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc
116-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc
117-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc
118-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc
119-
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
120-
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
121-
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc
122-
123-
generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
124-
gcc_builtin_headers_ia32.inc gcc_builtin_headers_alpha.inc \
125-
gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \
126-
gcc_builtin_headers_power.inc arm_builtin_headers.inc \
127-
cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \
128-
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
129-
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
130-
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
131-
gcc_builtin_headers_mem_string.inc \
132-
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
118+
ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES)
119+
120+
generated_files: \
121+
ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \
122+
cprover_library.inc \
123+
$(BUILTIN_FILES)
133124

134125
###############################################################################
135126

‎src/ansi-c/ansi_c_internal_additions.cpp

+10-38
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,11 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <util/config.h>
1212

13+
const char gcc_builtin_headers_types[]=
14+
"# 1 \"gcc_builtin_headers_types.h\"\n"
15+
#include "gcc_builtin_headers_types.inc"
16+
; // NOLINT(whitespace/semicolon)
17+
1318
const char gcc_builtin_headers_generic[]=
1419
"# 1 \"gcc_builtin_headers_generic.h\"\n"
1520
#include "gcc_builtin_headers_generic.inc"
@@ -89,6 +94,10 @@ const char clang_builtin_headers[]=
8994
#include "clang_builtin_headers.inc"
9095
; // NOLINT(whitespace/semicolon)
9196

97+
const char windows_builtin_headers[]=
98+
"int __noop();\n"
99+
"int __assume(int);\n";
100+
92101
static std::string architecture_string(const std::string &value, const char *s)
93102
{
94103
return std::string("const char *__CPROVER_architecture_")+
@@ -257,13 +266,7 @@ void ansi_c_internal_additions(std::string &code)
257266
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
258267
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
259268
{
260-
code+=gcc_builtin_headers_generic;
261-
code+=gcc_builtin_headers_math;
262-
code+=gcc_builtin_headers_mem_string;
263-
code+=gcc_builtin_headers_omp;
264-
code+=gcc_builtin_headers_tm;
265-
code+=gcc_builtin_headers_ubsan;
266-
code+=clang_builtin_headers;
269+
code+=gcc_builtin_headers_types;
267270

268271
// there are many more, e.g., look at
269272
// https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
@@ -274,37 +277,6 @@ void ansi_c_internal_additions(std::string &code)
274277
{
275278
if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
276279
code+="typedef double __float128;\n"; // clang doesn't do __float128
277-
278-
code+=gcc_builtin_headers_ia32;
279-
code+=gcc_builtin_headers_ia32_2;
280-
code+=gcc_builtin_headers_ia32_3;
281-
code+=gcc_builtin_headers_ia32_4;
282-
}
283-
else if(config.ansi_c.arch=="arm64" ||
284-
config.ansi_c.arch=="armel" ||
285-
config.ansi_c.arch=="armhf" ||
286-
config.ansi_c.arch=="arm")
287-
{
288-
code+=gcc_builtin_headers_arm;
289-
}
290-
else if(config.ansi_c.arch=="alpha")
291-
{
292-
code+=gcc_builtin_headers_alpha;
293-
}
294-
else if(config.ansi_c.arch=="mips64el" ||
295-
config.ansi_c.arch=="mipsn32el" ||
296-
config.ansi_c.arch=="mipsel" ||
297-
config.ansi_c.arch=="mips64" ||
298-
config.ansi_c.arch=="mipsn32" ||
299-
config.ansi_c.arch=="mips")
300-
{
301-
code+=gcc_builtin_headers_mips;
302-
}
303-
else if(config.ansi_c.arch=="powerpc" ||
304-
config.ansi_c.arch=="ppc64" ||
305-
config.ansi_c.arch=="ppc64le")
306-
{
307-
code+=gcc_builtin_headers_power;
308280
}
309281

310282
// On 64-bit systems, gcc has typedefs

‎src/ansi-c/ansi_c_internal_additions.h

+8-1
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,24 @@ Author: Daniel Kroening, [email protected]
1515
void ansi_c_internal_additions(std::string &code);
1616
void ansi_c_architecture_strings(std::string &code);
1717

18+
extern const char clang_builtin_headers[];
19+
extern const char gcc_builtin_headers_types[];
1820
extern const char gcc_builtin_headers_generic[];
1921
extern const char gcc_builtin_headers_math[];
2022
extern const char gcc_builtin_headers_mem_string[];
2123
extern const char gcc_builtin_headers_omp[];
2224
extern const char gcc_builtin_headers_tm[];
2325
extern const char gcc_builtin_headers_ubsan[];
24-
extern const char clang_builtin_headers[];
2526
extern const char gcc_builtin_headers_ia32[];
2627
extern const char gcc_builtin_headers_ia32_2[];
2728
extern const char gcc_builtin_headers_ia32_3[];
2829
extern const char gcc_builtin_headers_ia32_4[];
30+
extern const char gcc_builtin_headers_alpha[];
31+
extern const char gcc_builtin_headers_arm[];
32+
extern const char gcc_builtin_headers_mips[];
33+
extern const char gcc_builtin_headers_power[];
2934
extern const char arm_builtin_headers[];
35+
extern const char cw_builtin_headers[];
36+
extern const char windows_builtin_headers[];
3037

3138
#endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H

0 commit comments

Comments
 (0)