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