Skip to content

Commit 15ec42f

Browse files
author
Daniel Kroening
committed
use the builtins factory in the C frontend
1 parent 1711345 commit 15ec42f

9 files changed

+217
-152
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

+45-24
Original file line numberDiff line numberDiff line change
@@ -49,15 +49,24 @@ CLEANFILES = ansi-c$(LIBEXT) \
4949
ansi_c_y.output \
5050
library/converter$(EXEEXT) cprover_library.inc \
5151
file_converter$(EXEEXT) library_check \
52-
gcc_builtin_headers_generic.inc gcc_builtin_headers_ia32.inc \
53-
arm_builtin_headers.inc cw_builtin_headers.inc \
54-
gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \
55-
gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \
56-
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
57-
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
58-
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
52+
arm_builtin_headers.inc \
53+
clang_builtin_headers.inc \
54+
cw_builtin_headers.inc \
55+
gcc_builtin_headers_alpha.inc \
56+
gcc_builtin_headers_arm.inc \
57+
gcc_builtin_headers_generic.inc \
58+
gcc_builtin_headers_ia32-2.inc \
59+
gcc_builtin_headers_ia32-3.inc \
60+
gcc_builtin_headers_ia32-4.inc \
61+
gcc_builtin_headers_ia32.inc \
62+
gcc_builtin_headers_math.inc \
5963
gcc_builtin_headers_mem_string.inc \
60-
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
64+
gcc_builtin_headers_mips.inc \
65+
gcc_builtin_headers_omp.inc \
66+
gcc_builtin_headers_power.inc \
67+
gcc_builtin_headers_tm.inc \
68+
gcc_builtin_headers_types.inc \
69+
gcc_builtin_headers_ubsan.inc
6170

6271
all: ansi-c$(LIBEXT)
6372

@@ -103,34 +112,46 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c
103112

104113
cprover_library.cpp: cprover_library.inc
105114

115+
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
116+
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc
117+
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
118+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
119+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
106120
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
107-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
108121
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
109122
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
110123
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
111-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
112-
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
124+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
113125
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
114126
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc
115127
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc
116128
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc
117129
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc
118130
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc
131+
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_types.inc
119132
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc
120-
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
121-
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
122-
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc
123133

124-
generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
125-
gcc_builtin_headers_ia32.inc gcc_builtin_headers_alpha.inc \
126-
gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \
127-
gcc_builtin_headers_power.inc arm_builtin_headers.inc \
128-
cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \
129-
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
130-
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
131-
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
132-
gcc_builtin_headers_mem_string.inc \
133-
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
134+
generated_files: \
135+
ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \
136+
arm_builtin_headers.inc \
137+
clang_builtin_headers.inc \
138+
cprover_library.inc \
139+
cw_builtin_headers.inc \
140+
gcc_builtin_headers_alpha.inc \
141+
gcc_builtin_headers_arm.inc \
142+
gcc_builtin_headers_generic.inc \
143+
gcc_builtin_headers_ia32-2.inc \
144+
gcc_builtin_headers_ia32-3.inc \
145+
gcc_builtin_headers_ia32-4.inc \
146+
gcc_builtin_headers_ia32.inc \
147+
gcc_builtin_headers_math.inc \
148+
gcc_builtin_headers_mem_string.inc \
149+
gcc_builtin_headers_mips.inc \
150+
gcc_builtin_headers_omp.inc \
151+
gcc_builtin_headers_power.inc \
152+
gcc_builtin_headers_tm.inc \
153+
gcc_builtin_headers_types.inc \
154+
gcc_builtin_headers_ubsan.inc
134155

135156
###############################################################################
136157

‎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

+1
Original file line numberDiff line numberDiff line change
@@ -32,5 +32,6 @@ extern const char gcc_builtin_headers_mips[];
3232
extern const char gcc_builtin_headers_power[];
3333
extern const char arm_builtin_headers[];
3434
extern const char cw_builtin_headers[];
35+
extern const char windows_builtin_headers[];
3536

3637
#endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H

‎src/ansi-c/builtin_factory.cpp

+86-24
Original file line numberDiff line numberDiff line change
@@ -12,14 +12,12 @@ Author: Daniel Kroening, [email protected]
1212
#include "ansi_c_parser.h"
1313
#include "ansi_c_typecheck.h"
1414

15+
#include <util/config.h>
16+
1517
#include <cstring>
1618
#include <ostream>
1719
#include <sstream>
1820

19-
const char windows_headers[]=
20-
"int __noop();\n"
21-
"int __assume(int);\n";
22-
2321
//! Advance to the next line
2422
static const char *next_line(const char *line)
2523
{
@@ -93,7 +91,8 @@ static bool convert(
9391

9492
symbol_tablet new_symbol_table;
9593

96-
// very recursive!
94+
// this is recursive -- builtin_factory is called
95+
// from the typechecker
9796
if(ansi_c_typecheck(
9897
ansi_c_parser.parse_tree,
9998
new_symbol_table,
@@ -137,33 +136,96 @@ bool builtin_factory(
137136
std::string code;
138137
ansi_c_internal_additions(code);
139138
s << code;
140-
141-
if(find_pattern(pattern, gcc_builtin_headers_generic, s))
142-
return convert(identifier, s, symbol_table, mh);
143139

144-
if(find_pattern(pattern, gcc_builtin_headers_mem_string, s))
145-
return convert(identifier, s, symbol_table, mh);
140+
// this is Visual C/C++ only
141+
if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN)
142+
{
143+
if(find_pattern(pattern, windows_builtin_headers, s))
144+
return convert(identifier, s, symbol_table, mh);
145+
}
146+
147+
// ARM stuff
148+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
149+
{
150+
if(find_pattern(pattern, arm_builtin_headers, s))
151+
return convert(identifier, s, symbol_table, mh);
152+
}
153+
154+
// CW stuff
155+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::CODEWARRIOR)
156+
{
157+
if(find_pattern(pattern, cw_builtin_headers, s))
158+
return convert(identifier, s, symbol_table, mh);
159+
}
160+
161+
// GCC junk stuff, also for CLANG and ARM
162+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
163+
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
164+
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
165+
{
166+
if(find_pattern(pattern, gcc_builtin_headers_generic, s))
167+
return convert(identifier, s, symbol_table, mh);
168+
169+
if(find_pattern(pattern, gcc_builtin_headers_math, s))
170+
return convert(identifier, s, symbol_table, mh);
171+
172+
if(find_pattern(pattern, gcc_builtin_headers_mem_string, s))
173+
return convert(identifier, s, symbol_table, mh);
174+
175+
if(find_pattern(pattern, gcc_builtin_headers_omp, s))
176+
return convert(identifier, s, symbol_table, mh);
146177

147-
if(find_pattern(pattern, gcc_builtin_headers_omp, s))
148-
return convert(identifier, s, symbol_table, mh);
178+
if(find_pattern(pattern, gcc_builtin_headers_tm, s))
179+
return convert(identifier, s, symbol_table, mh);
149180

150-
if(find_pattern(pattern, gcc_builtin_headers_tm, s))
151-
return convert(identifier, s, symbol_table, mh);
181+
if(find_pattern(pattern, gcc_builtin_headers_ubsan, s))
182+
return convert(identifier, s, symbol_table, mh);
152183

153-
if(find_pattern(pattern, gcc_builtin_headers_ubsan, s))
154-
return convert(identifier, s, symbol_table, mh);
184+
if(find_pattern(pattern, clang_builtin_headers, s))
185+
return convert(identifier, s, symbol_table, mh);
155186

156-
if(find_pattern(pattern, gcc_builtin_headers_ia32, s))
157-
return convert(identifier, s, symbol_table, mh);
187+
if(config.ansi_c.arch=="i386" ||
188+
config.ansi_c.arch=="x86_64" ||
189+
config.ansi_c.arch=="x32")
190+
{
191+
if(find_pattern(pattern, gcc_builtin_headers_ia32, s))
192+
return convert(identifier, s, symbol_table, mh);
158193

159-
if(find_pattern(pattern, gcc_builtin_headers_ia32_2, s))
160-
return convert(identifier, s, symbol_table, mh);
194+
if(find_pattern(pattern, gcc_builtin_headers_ia32_2, s))
195+
return convert(identifier, s, symbol_table, mh);
161196

162-
if(find_pattern(pattern, gcc_builtin_headers_ia32_3, s))
163-
return convert(identifier, s, symbol_table, mh);
197+
if(find_pattern(pattern, gcc_builtin_headers_ia32_3, s))
198+
return convert(identifier, s, symbol_table, mh);
164199

165-
if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s))
166-
return convert(identifier, s, symbol_table, mh);
200+
if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s))
201+
return convert(identifier, s, symbol_table, mh);
202+
}
203+
else if(config.ansi_c.arch=="arm64" ||
204+
config.ansi_c.arch=="armel" ||
205+
config.ansi_c.arch=="armhf" ||
206+
config.ansi_c.arch=="arm")
207+
{
208+
if(find_pattern(pattern, gcc_builtin_headers_arm, s))
209+
return convert(identifier, s, symbol_table, mh);
210+
}
211+
else if(config.ansi_c.arch=="mips64el" ||
212+
config.ansi_c.arch=="mipsn32el" ||
213+
config.ansi_c.arch=="mipsel" ||
214+
config.ansi_c.arch=="mips64" ||
215+
config.ansi_c.arch=="mipsn32" ||
216+
config.ansi_c.arch=="mips")
217+
{
218+
if(find_pattern(pattern, gcc_builtin_headers_mips, s))
219+
return convert(identifier, s, symbol_table, mh);
220+
}
221+
else if(config.ansi_c.arch=="powerpc" ||
222+
config.ansi_c.arch=="ppc64" ||
223+
config.ansi_c.arch=="ppc64le")
224+
{
225+
if(find_pattern(pattern, gcc_builtin_headers_power, s))
226+
return convert(identifier, s, symbol_table, mh);
227+
}
228+
}
167229

168230
return true;
169231
}

0 commit comments

Comments
 (0)