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
18#include "ansi_c_parser.h"
19
21 "#line 1 \"gcc_builtin_headers_types.h\"\n"
22#include "compiler_headers/gcc_builtin_headers_types.inc" // IWYU pragma: keep
23 ; // NOLINT(whitespace/semicolon)
24
26 "#line 1 \"gcc_builtin_headers_types_gcc7plus.h\"\n"
27// NOLINTNEXTLINE(whitespace/line_length)
28#include "compiler_headers/gcc_builtin_headers_types_gcc7plus.inc" // IWYU pragma: keep
29 ; // NOLINT(whitespace/semicolon)
30
32 "#line 1 \"gcc_builtin_headers_generic.h\"\n"
33#include "compiler_headers/gcc_builtin_headers_generic.inc" // IWYU pragma: keep
34 ; // NOLINT(whitespace/semicolon)
35
37 "#line 1 \"gcc_builtin_headers_math.h\"\n"
38#include "compiler_headers/gcc_builtin_headers_math.inc" // IWYU pragma: keep
39 ; // NOLINT(whitespace/semicolon)
40
42 "#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
43// NOLINTNEXTLINE(whitespace/line_length)
44#include "compiler_headers/gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
45 ; // NOLINT(whitespace/semicolon)
46
47const char gcc_builtin_headers_omp[] = "#line 1 \"gcc_builtin_headers_omp.h\"\n"
48#include "compiler_headers/gcc_builtin_headers_omp.inc" // IWYU pragma: keep
49 ; // NOLINT(whitespace/semicolon)
50
51const char gcc_builtin_headers_tm[] = "#line 1 \"gcc_builtin_headers_tm.h\"\n"
52#include "compiler_headers/gcc_builtin_headers_tm.inc" // IWYU pragma: keep
53 ; // NOLINT(whitespace/semicolon)
54
56 "#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
57#include "compiler_headers/gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
58 ; // NOLINT(whitespace/semicolon)
59
61 "#line 1 \"gcc_builtin_headers_ia32.h\"\n"
62#include "compiler_headers/gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
63 ; // NOLINT(whitespace/semicolon)
65#include "compiler_headers/gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
66 ; // NOLINT(whitespace/semicolon)
68#include "compiler_headers/gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
69 ; // NOLINT(whitespace/semicolon)
71#include "compiler_headers/gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
72 ; // NOLINT(whitespace/semicolon)
74#include "compiler_headers/gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
75 ; // NOLINT(whitespace/semicolon)
77#include "compiler_headers/gcc_builtin_headers_ia32-6.inc" // IWYU pragma: keep
78 ; // NOLINT(whitespace/semicolon)
79
81 "#line 1 \"gcc_builtin_headers_alpha.h\"\n"
82#include "compiler_headers/gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
83 ; // NOLINT(whitespace/semicolon)
84
85const char gcc_builtin_headers_arm[] = "#line 1 \"gcc_builtin_headers_arm.h\"\n"
86#include "compiler_headers/gcc_builtin_headers_arm.inc" // IWYU pragma: keep
87 ; // NOLINT(whitespace/semicolon)
88
90 "#line 1 \"gcc_builtin_headers_mips.h\"\n"
91#include "compiler_headers/gcc_builtin_headers_mips.inc" // IWYU pragma: keep
92 ; // NOLINT(whitespace/semicolon)
93
95 "#line 1 \"gcc_builtin_headers_power.h\"\n"
96#include "compiler_headers/gcc_builtin_headers_power.inc" // IWYU pragma: keep
97 ; // NOLINT(whitespace/semicolon)
98
99const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n"
100#include "compiler_headers/arm_builtin_headers.inc" // IWYU pragma: keep
101 ; // NOLINT(whitespace/semicolon)
102
103const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n"
104#include "compiler_headers/cw_builtin_headers.inc" // IWYU pragma: keep
105 ; // NOLINT(whitespace/semicolon)
106
107const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n"
108#include "compiler_headers/clang_builtin_headers.inc" // IWYU pragma: keep
109 ; // NOLINT(whitespace/semicolon)
110
111const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n"
112#include "cprover_builtin_headers.inc" // IWYU pragma: keep
113 ; // NOLINT(whitespace/semicolon)
114
115const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n"
116#include "compiler_headers/windows_builtin_headers.inc" // IWYU pragma: keep
117 ; // NOLINT(whitespace/semicolon)
118
119static std::string architecture_string(const std::string &value, const char *s)
120{
121 return std::string("const char *" CPROVER_PREFIX "architecture_") +
122 std::string(s) + "=\"" + value + "\";\n";
123}
124
125template <typename T>
126static std::string architecture_string(T value, const char *s)
127{
128 return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX
129 "architecture_") +
130 std::string(s) + "=" + std::to_string(value) + ";\n";
131}
132
147static mp_integer
148max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
149{
150 PRECONDITION(pointer_width >= 1);
151 PRECONDITION(object_bits < pointer_width);
152 PRECONDITION(object_bits >= 1);
153 const auto offset_bits = pointer_width - object_bits;
154 // We require the offset to be able to express upto allocation_size - 1,
155 // but also down to -allocation_size, therefore the size is allowable
156 // is number of bits, less the signed bit.
157 const auto bits_for_positive_offset = offset_bits - 1;
159}
160
161void ansi_c_internal_additions(std::string &code)
162{
163 // clang-format off
164 // do the built-in types and variables
165 code+=
166 "#line 1 \"<built-in-additions>\"\n"
167 "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
169 " " CPROVER_PREFIX "ssize_t;\n"
170 "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
171 "typedef void " CPROVER_PREFIX "integer;\n"
172 "typedef void " CPROVER_PREFIX "rational;\n"
173 "extern unsigned char " CPROVER_PREFIX "memory["
174 CPROVER_PREFIX "constant_infinity_uint];\n"
175
176 // malloc
177 "const void *" CPROVER_PREFIX "deallocated=0;\n"
178 "const void *" CPROVER_PREFIX "dead_object=0;\n"
179 "const void *" CPROVER_PREFIX "memory_leak=0;\n"
180 "void *" CPROVER_PREFIX "allocate("
181 CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
182 "void " CPROVER_PREFIX "deallocate(void *);\n"
183
184 CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
186 .bv_encoding.object_bits));
187 if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
188 code += "UL;\n";
189 else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
190 code += "ULL;\n";
191 else
192 code += "U;\n";
193
194 code+=
195 // this is ANSI-C
196 "extern " CPROVER_PREFIX "thread_local const char __func__["
197 CPROVER_PREFIX "constant_infinity_uint];\n"
198
199 // this is GCC
200 "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
201 CPROVER_PREFIX "constant_infinity_uint];\n"
202 "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
203 CPROVER_PREFIX "constant_infinity_uint];\n"
204
205 // float stuff
206 "int " CPROVER_PREFIX "thread_local " +
208 std::to_string(config.ansi_c.rounding_mode)+";\n"
209
210 // pipes, write, read, close
211 "struct " CPROVER_PREFIX "pipet {\n"
212 " _Bool widowed;\n"
213 " char data[4];\n"
214 " short next_avail;\n"
215 " short next_unread;\n"
216 "};\n"
217 "\n"
218 // This function needs to be declared, or otherwise can't be called
219 // by the entry-point construction.
220 "void " INITIALIZE_FUNCTION "(void);\n"
221 "\n"
222 // frame specifications for contracts
223 // Declares a range of bytes as assignable (internal representation)
224 "void " CPROVER_PREFIX "assignable(void *ptr,\n"
225 " " CPROVER_PREFIX "size_t size,\n"
226 " " CPROVER_PREFIX "bool is_ptr_to_ptr);\n"
227 // Declares a range of bytes as assignable
228 "void " CPROVER_PREFIX "object_upto(void *ptr, \n"
229 " " CPROVER_PREFIX "size_t size);\n"
230 // Declares bytes from ptr to the end of the object as assignable
231 "void " CPROVER_PREFIX "object_from(void *ptr);\n"
232 // Declares the whole object pointed to by ptr as assignable
233 "void " CPROVER_PREFIX "object_whole(void *ptr);\n"
234 // Declares a pointer as freeable
235 "void " CPROVER_PREFIX "freeable(void *ptr);\n"
236 // True iff ptr satisfies the preconditions of the free stdlib function
237 CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freeable(void *ptr);\n"
238 // True iff ptr was freed during function execution or loop execution
239 CPROVER_PREFIX "bool " CPROVER_PREFIX "was_freed(void *ptr);\n"
240 "\n";
241 // clang-format on
242
243 // GCC junk stuff, also for CLANG and ARM
244 if(
248 {
250 // check the parser and not config.ansi_c.ts_18661_3_Floatn_types to adjust
251 // behaviour depending on C or C++ context
254
255 // there are many more, e.g., look at
256 // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
257
258 if(
259 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
260 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
261 config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
262 {
263 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
264 // For clang, __float128 is a keyword.
265 // For gcc, this is a typedef and not a keyword.
266 if(
268 config.ansi_c.gcc__float128_type)
269 {
270 code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
271 }
272 }
273 else if(config.ansi_c.arch == "ppc64le")
274 {
275 // https://patchwork.ozlabs.org/patch/792295/
277 code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
278 }
279 else if(config.ansi_c.arch == "hppa")
280 {
281 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
282 // For clang, __float128 is a keyword.
283 // For gcc, this is a typedef and not a keyword.
284 if(
286 config.ansi_c.gcc__float128_type)
287 {
288 code+="typedef long double __float128;\n";
289 }
290 }
291
292 if(
293 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
294 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
295 {
296 // clang doesn't do __float80
297 // Note that __float80 is a typedef, and not a keyword.
299 code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
300 }
301
302 // On 64-bit systems, gcc has typedefs
303 // __int128_t und __uint128_t -- but not on 32 bit!
304 if(config.ansi_c.long_int_width>=64)
305 {
306 code+="typedef signed __int128 __int128_t;\n"
307 "typedef unsigned __int128 __uint128_t;\n";
308 }
309 }
310
311 // this is Visual C/C++ only
313 code += "int __assume(int);\n";
314
315 // ARM stuff
318
319 // CW stuff
321 code+=cw_builtin_headers;
322
323 // Architecture strings
325}
326
327void ansi_c_architecture_strings(std::string &code)
328{
329 // The following are CPROVER-specific.
330 // They allow identifying the architectural settings used
331 // at compile time from a goto-binary.
332
333 code += "#line 1 \"<builtin-architecture-strings>\"\n";
334
335 code+=architecture_string(config.ansi_c.int_width, "int_width");
336 code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
337 code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
338 code+=architecture_string(config.ansi_c.bool_width, "bool_width");
339 code+=architecture_string(config.ansi_c.char_width, "char_width");
340 code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
341 code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
342 code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
343 code+=architecture_string(config.ansi_c.single_width, "single_width");
344 code+=architecture_string(config.ansi_c.double_width, "double_width");
345 code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
346 code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
347 code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
348 code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
349 code+=architecture_string(config.ansi_c.alignment, "alignment");
350 code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
351 code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
352 code+=architecture_string(id2string(config.ansi_c.arch), "arch");
353 code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
354 code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
355}
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_ia32_6[]
const char gcc_builtin_headers_mips[]
const char clang_builtin_headers[]
const char gcc_builtin_headers_alpha[]
const char gcc_builtin_headers_types_gcc7plus[]
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...
ansi_c_parsert ansi_c_parser
configt config
Definition config.cpp:25
std::string c_type_as_string(const irep_idt &c_type)
Definition c_types.cpp:256
signedbv_typet signed_size_type()
Definition c_types.cpp:71
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
bool ts_18661_3_Floatn_types
struct configt::bv_encodingt bv_encoding
struct configt::ansi_ct ansi_c
#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:18
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INITIALIZE_FUNCTION
static std::string os_to_string(ost)
Definition config.cpp:1177