cprover
Loading...
Searching...
No Matches
ansi_c_internal_additions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include <util/c_types.h>
12#include <util/config.h>
13
15
17
19 "#line 1 \"gcc_builtin_headers_types.h\"\n"
20#include "gcc_builtin_headers_types.inc"
21 ; // NOLINT(whitespace/semicolon)
22
24 "#line 1 \"gcc_builtin_headers_generic.h\"\n"
25#include "gcc_builtin_headers_generic.inc"
26 ; // NOLINT(whitespace/semicolon)
27
29 "#line 1 \"gcc_builtin_headers_math.h\"\n"
30#include "gcc_builtin_headers_math.inc"
31 ; // NOLINT(whitespace/semicolon)
32
34 "#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
35#include "gcc_builtin_headers_mem_string.inc"
36 ; // NOLINT(whitespace/semicolon)
37
38const char gcc_builtin_headers_omp[] = "#line 1 \"gcc_builtin_headers_omp.h\"\n"
39#include "gcc_builtin_headers_omp.inc"
40 ; // NOLINT(whitespace/semicolon)
41
42const char gcc_builtin_headers_tm[] = "#line 1 \"gcc_builtin_headers_tm.h\"\n"
43#include "gcc_builtin_headers_tm.inc"
44 ; // NOLINT(whitespace/semicolon)
45
47 "#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
48#include "gcc_builtin_headers_ubsan.inc"
49 ; // NOLINT(whitespace/semicolon)
50
52 "#line 1 \"gcc_builtin_headers_ia32.h\"\n"
53#include "gcc_builtin_headers_ia32.inc"
54 ; // NOLINT(whitespace/semicolon)
56#include "gcc_builtin_headers_ia32-2.inc"
57; // NOLINT(whitespace/semicolon)
59#include "gcc_builtin_headers_ia32-3.inc"
60; // NOLINT(whitespace/semicolon)
62#include "gcc_builtin_headers_ia32-4.inc"
63; // NOLINT(whitespace/semicolon)
65#include "gcc_builtin_headers_ia32-5.inc"
66 ; // NOLINT(whitespace/semicolon)
67
69 "#line 1 \"gcc_builtin_headers_alpha.h\"\n"
70#include "gcc_builtin_headers_alpha.inc"
71 ; // NOLINT(whitespace/semicolon)
72
73const char gcc_builtin_headers_arm[] = "#line 1 \"gcc_builtin_headers_arm.h\"\n"
74#include "gcc_builtin_headers_arm.inc"
75 ; // NOLINT(whitespace/semicolon)
76
78 "#line 1 \"gcc_builtin_headers_mips.h\"\n"
79#include "gcc_builtin_headers_mips.inc"
80 ; // NOLINT(whitespace/semicolon)
81
83 "#line 1 \"gcc_builtin_headers_power.h\"\n"
84#include "gcc_builtin_headers_power.inc"
85 ; // NOLINT(whitespace/semicolon)
86
87const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n"
88#include "arm_builtin_headers.inc"
89 ; // NOLINT(whitespace/semicolon)
90
91const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n"
92#include "cw_builtin_headers.inc"
93 ; // NOLINT(whitespace/semicolon)
94
95const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n"
96#include "clang_builtin_headers.inc"
97 ; // NOLINT(whitespace/semicolon)
98
99const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n"
100#include "cprover_builtin_headers.inc"
101 ; // NOLINT(whitespace/semicolon)
102
103const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n"
104#include "windows_builtin_headers.inc"
105 ; // NOLINT(whitespace/semicolon)
106
107static std::string architecture_string(const std::string &value, const char *s)
108{
109 return std::string("const char *" CPROVER_PREFIX "architecture_") +
110 std::string(s) + "=\"" + value + "\";\n";
111}
112
113template <typename T>
114static std::string architecture_string(T value, const char *s)
115{
116 return std::string("const int " CPROVER_PREFIX "architecture_") +
117 std::string(s) + "=" + std::to_string(value) + ";\n";
118}
119
134static mp_integer
135max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
136{
137 PRECONDITION(pointer_width >= 1);
138 PRECONDITION(object_bits < pointer_width);
139 PRECONDITION(object_bits >= 1);
140 const auto offset_bits = pointer_width - object_bits;
141 // We require the offset to be able to express upto allocation_size - 1,
142 // but also down to -allocation_size, therefore the size is allowable
143 // is number of bits, less the signed bit.
144 const auto bits_for_positive_offset = offset_bits - 1;
146}
147
148void ansi_c_internal_additions(std::string &code)
149{
150 // clang-format off
151 // do the built-in types and variables
152 code+=
153 "#line 1 \"<built-in-additions>\"\n"
154 "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
156 " " CPROVER_PREFIX "ssize_t;\n"
157 "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
158 "typedef void " CPROVER_PREFIX "integer;\n"
159 "typedef void " CPROVER_PREFIX "rational;\n"
160 CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
161 CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
162 CPROVER_PREFIX "constant_infinity_uint];\n"
163 "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
164 CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys["
165 CPROVER_PREFIX "constant_infinity_uint];\n"
166 CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors["
167 CPROVER_PREFIX "constant_infinity_uint])(void *);\n"
168 CPROVER_PREFIX "thread_local unsigned long "
169 CPROVER_PREFIX "next_thread_key = 0;\n"
170 "extern unsigned char " CPROVER_PREFIX "memory["
171 CPROVER_PREFIX "constant_infinity_uint];\n"
172
173 // malloc
174 "const void *" CPROVER_PREFIX "deallocated=0;\n"
175 "const void *" CPROVER_PREFIX "dead_object=0;\n"
176 "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
177 CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
178 "const void *" CPROVER_PREFIX "memory_leak=0;\n"
179 "void *" CPROVER_PREFIX "allocate("
180 CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
181 "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
182
183 CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
185 .bv_encoding.object_bits))+";\n"
186
187 // this is ANSI-C
188 "extern " CPROVER_PREFIX "thread_local const char __func__["
189 CPROVER_PREFIX "constant_infinity_uint];\n"
190
191 // this is GCC
192 "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
193 CPROVER_PREFIX "constant_infinity_uint];\n"
194 "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
195 CPROVER_PREFIX "constant_infinity_uint];\n"
196
197 // float stuff
198 "int " CPROVER_PREFIX "thread_local " +
200 std::to_string(config.ansi_c.rounding_mode)+";\n"
201
202 // pipes, write, read, close
203 "struct " CPROVER_PREFIX "pipet {\n"
204 " _Bool widowed;\n"
205 " char data[4];\n"
206 " short next_avail;\n"
207 " short next_unread;\n"
208 "};\n"
209 "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
210 CPROVER_PREFIX "constant_infinity_uint];\n"
211 // offset to make sure we don't collide with other fds
212 "extern const int " CPROVER_PREFIX "pipe_offset;\n"
213 "unsigned " CPROVER_PREFIX "pipe_count=0;\n"
214 "\n"
215 // This function needs to be declared, or otherwise can't be called
216 // by the entry-point construction.
217 "void " INITIALIZE_FUNCTION "(void);\n"
218 "\n";
219 // clang-format on
220
221 // GCC junk stuff, also for CLANG and ARM
222 if(
226 {
228
229 // there are many more, e.g., look at
230 // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
231
232 if(
233 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
234 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
235 config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
236 {
237 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
238 // For clang, __float128 is a keyword.
239 // For gcc, this is a typedef and not a keyword.
240 if(
242 config.ansi_c.gcc__float128_type)
243 {
244 code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
245 }
246 }
247 else if(config.ansi_c.arch == "ppc64le")
248 {
249 // https://patchwork.ozlabs.org/patch/792295/
251 code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
252 }
253 else if(config.ansi_c.arch == "hppa")
254 {
255 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
256 // For clang, __float128 is a keyword.
257 // For gcc, this is a typedef and not a keyword.
258 if(
260 config.ansi_c.gcc__float128_type)
261 {
262 code+="typedef long double __float128;\n";
263 }
264 }
265
266 if(
267 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
268 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
269 {
270 // clang doesn't do __float80
271 // Note that __float80 is a typedef, and not a keyword.
273 code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
274 }
275
276 // On 64-bit systems, gcc has typedefs
277 // __int128_t und __uint128_t -- but not on 32 bit!
278 if(config.ansi_c.long_int_width>=64)
279 {
280 code+="typedef signed __int128 __int128_t;\n"
281 "typedef unsigned __int128 __uint128_t;\n";
282 }
283 }
284
285 // this is Visual C/C++ only
287 code += "int __assume(int);\n";
288
289 // ARM stuff
292
293 // CW stuff
295 code+=cw_builtin_headers;
296
297 // Architecture strings
299}
300
301void ansi_c_architecture_strings(std::string &code)
302{
303 // The following are CPROVER-specific.
304 // They allow identifying the architectural settings used
305 // at compile time from a goto-binary.
306
307 code += "#line 1 \"<builtin-architecture-strings>\"\n";
308
309 code+=architecture_string(config.ansi_c.int_width, "int_width");
310 code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
311 code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
312 code+=architecture_string(config.ansi_c.bool_width, "bool_width");
313 code+=architecture_string(config.ansi_c.char_width, "char_width");
314 code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
315 code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
316 code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
317 code+=architecture_string(config.ansi_c.single_width, "single_width");
318 code+=architecture_string(config.ansi_c.double_width, "double_width");
319 code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
320 code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
321 code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
322 code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
323 code+=architecture_string(config.ansi_c.alignment, "alignment");
324 code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
325 code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
326 code+=architecture_string(id2string(config.ansi_c.arch), "arch");
327 code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
328 code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
329}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
static std::string architecture_string(const std::string &value, const char *s)
const char gcc_builtin_headers_types[]
const char cprover_builtin_headers[]
const char gcc_builtin_headers_ia32[]
const char gcc_builtin_headers_ia32_2[]
const char gcc_builtin_headers_ia32_5[]
const char gcc_builtin_headers_ubsan[]
const char windows_builtin_headers[]
const char gcc_builtin_headers_mem_string[]
const char gcc_builtin_headers_ia32_4[]
const char gcc_builtin_headers_generic[]
void ansi_c_internal_additions(std::string &code)
const char gcc_builtin_headers_tm[]
const char cw_builtin_headers[]
const char gcc_builtin_headers_math[]
const char gcc_builtin_headers_arm[]
const char gcc_builtin_headers_mips[]
const char clang_builtin_headers[]
const char gcc_builtin_headers_alpha[]
const char arm_builtin_headers[]
const char gcc_builtin_headers_omp[]
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_power[]
void ansi_c_architecture_strings(std::string &code)
static mp_integer max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
std::string c_type_as_string(const irep_idt &c_type)
Definition c_types.cpp:269
signedbv_typet signed_size_type()
Definition c_types.cpp:84
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
struct configt::bv_encodingt bv_encoding
struct configt::ansi_ct ansi_c
configt config
Definition config.cpp:25
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
BigInt mp_integer
Definition smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INITIALIZE_FUNCTION
static std::string os_to_string(ost)
Definition config.cpp:1175