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 <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 
38 const 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 
42 const 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 
73 const 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 
87 const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n"
88 #include "arm_builtin_headers.inc"
89  ; // NOLINT(whitespace/semicolon)
90 
91 const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n"
92 #include "cw_builtin_headers.inc"
93  ; // NOLINT(whitespace/semicolon)
94 
95 const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n"
96 #include "clang_builtin_headers.inc"
97  ; // NOLINT(whitespace/semicolon)
98 
99 const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n"
100 #include "cprover_builtin_headers.inc"
101  ; // NOLINT(whitespace/semicolon)
102 
103 const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n"
104 #include "windows_builtin_headers.inc"
105  ; // NOLINT(whitespace/semicolon)
106 
107 static 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 
113 template <typename T>
114 static 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 
134 static mp_integer
135 max_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;
145  return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
146 }
147 
148 void 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"
155  "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
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 " +
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(
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(
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!
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
291  code+=arm_builtin_headers;
292 
293  // CW stuff
295  code+=cw_builtin_headers;
296 
297  // Architecture strings
299 }
300 
301 void 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)
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
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t long_double_width
Definition: config.h:118
endiannesst endianness
Definition: config.h:177
bool wchar_t_is_unsigned
Definition: config.h:122
static std::string os_to_string(ost)
Definition: config.cpp:1175
std::size_t pointer_width
Definition: config.h:115
bool gcc__float128_type
Definition: config.h:125
irep_idt arch
Definition: config.h:191
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:151
std::size_t wchar_t_width
Definition: config.h:119
std::size_t double_width
Definition: config.h:117
bool char_is_unsigned
Definition: config.h:122
std::size_t alignment
Definition: config.h:165
std::size_t bool_width
Definition: config.h:111
std::size_t memory_operand_size
Definition: config.h:169
std::size_t long_long_int_width
Definition: config.h:114
bool NULL_is_zero
Definition: config.h:194
std::size_t long_int_width
Definition: config.h:110
std::size_t single_width
Definition: config.h:116
std::size_t short_int_width
Definition: config.h:113
std::size_t char_width
Definition: config.h:112
flavourt mode
Definition: config.h:222
std::size_t int_width
Definition: config.h:109
std::size_t object_bits
Definition: config.h:321