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