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 "# 1 \"gcc_builtin_headers_types.h\"\n"
18 #include "gcc_builtin_headers_types.inc"
19 ; // NOLINT(whitespace/semicolon)
20 
22 "# 1 \"gcc_builtin_headers_generic.h\"\n"
23 #include "gcc_builtin_headers_generic.inc"
24 ; // NOLINT(whitespace/semicolon)
25 
27 "# 1 \"gcc_builtin_headers_math.h\"\n"
28 #include "gcc_builtin_headers_math.inc"
29 ; // NOLINT(whitespace/semicolon)
30 
32 "# 1 \"gcc_builtin_headers_mem_string.h\"\n"
33 #include "gcc_builtin_headers_mem_string.inc"
34 ; // NOLINT(whitespace/semicolon)
35 
37 "# 1 \"gcc_builtin_headers_omp.h\"\n"
38 #include "gcc_builtin_headers_omp.inc"
39 ; // NOLINT(whitespace/semicolon)
40 
42 "# 1 \"gcc_builtin_headers_tm.h\"\n"
43 #include "gcc_builtin_headers_tm.inc"
44 ; // NOLINT(whitespace/semicolon)
45 
47 "# 1 \"gcc_builtin_headers_ubsan.h\"\n"
48 #include "gcc_builtin_headers_ubsan.inc"
49 ; // NOLINT(whitespace/semicolon)
50 
52 "# 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)
64 
66 "# 1 \"gcc_builtin_headers_alpha.h\"\n"
67 #include "gcc_builtin_headers_alpha.inc"
68 ; // NOLINT(whitespace/semicolon)
69 
71 "# 1 \"gcc_builtin_headers_arm.h\"\n"
72 #include "gcc_builtin_headers_arm.inc"
73 ; // NOLINT(whitespace/semicolon)
74 
76 "# 1 \"gcc_builtin_headers_mips.h\"\n"
77 #include "gcc_builtin_headers_mips.inc"
78 ; // NOLINT(whitespace/semicolon)
79 
81 "# 1 \"gcc_builtin_headers_power.h\"\n"
82 #include "gcc_builtin_headers_power.inc"
83 ; // NOLINT(whitespace/semicolon)
84 
85 const char arm_builtin_headers[]=
86 "# 1 \"arm_builtin_headers.h\"\n"
87 #include "arm_builtin_headers.inc"
88 ; // NOLINT(whitespace/semicolon)
89 
90 const char cw_builtin_headers[]=
91 "# 1 \"cw_builtin_headers.h\"\n"
92 #include "cw_builtin_headers.inc"
93 ; // NOLINT(whitespace/semicolon)
94 
95 const char clang_builtin_headers[]=
96 "# 1 \"clang_builtin_headers.h\"\n"
97 #include "clang_builtin_headers.inc"
98 ; // NOLINT(whitespace/semicolon)
99 
101 "# 1 \"cprover_builtin_headers.h\"\n"
102 #include "cprover_builtin_headers.inc"
103 ; // NOLINT(whitespace/semicolon)
104 
106 "# 1 \"windows_builtin_headers.h\"\n"
107 #include "windows_builtin_headers.inc"
108 ; // NOLINT(whitespace/semicolon)
109 
110 static std::string architecture_string(const std::string &value, const char *s)
111 {
112  return std::string("const char *__CPROVER_architecture_")+
113  std::string(s)+
114  "=\""+value+"\";\n";
115 }
116 
117 template <typename T>
118 static std::string architecture_string(T value, const char *s)
119 {
120  return std::string("const int __CPROVER_architecture_")+
121  std::string(s)+
122  "="+std::to_string(value)+";\n";
123 }
124 
125 void ansi_c_internal_additions(std::string &code)
126 {
127  // do the built-in types and variables
128  code+=
129  "# 1 \"<built-in-additions>\"\n"
130  "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
131  "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
132  " __CPROVER_ssize_t;\n"
133  "const unsigned __CPROVER_constant_infinity_uint;\n"
134  "typedef void __CPROVER_integer;\n"
135  "typedef void __CPROVER_rational;\n"
136  "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
137  // NOLINTNEXTLINE(whitespace/line_length)
138  "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
139  "unsigned long __CPROVER_next_thread_id=0;\n"
140  // NOLINTNEXTLINE(whitespace/line_length)
141  "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
142 
143  // malloc
144  "const void *__CPROVER_deallocated=0;\n"
145  "const void *__CPROVER_dead_object=0;\n"
146  "const void *__CPROVER_malloc_object=0;\n"
147  "__CPROVER_size_t __CPROVER_malloc_size;\n"
148  "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++
149  "const void *__CPROVER_memory_leak=0;\n"
150  "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
151 
152  // this is ANSI-C
153  // NOLINTNEXTLINE(whitespace/line_length)
154  "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
155 
156  // this is GCC
157  // NOLINTNEXTLINE(whitespace/line_length)
158  "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
159  // NOLINTNEXTLINE(whitespace/line_length)
160  "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
161 
162  // float stuff
163  "int __CPROVER_thread_local __CPROVER_rounding_mode="+
165 
166  // pipes, write, read, close
167  "struct __CPROVER_pipet {\n"
168  " _Bool widowed;\n"
169  " char data[4];\n"
170  " short next_avail;\n"
171  " short next_unread;\n"
172  "};\n"
173  // NOLINTNEXTLINE(whitespace/line_length)
174  "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
175  // offset to make sure we don't collide with other fds
176  "extern const int __CPROVER_pipe_offset;\n"
177  "unsigned __CPROVER_pipe_count=0;\n"
178  "\n"
179  // This function needs to be declared, or otherwise can't be called
180  // by the entry-point construction.
181  "void " INITIALIZE_FUNCTION "(void);\n"
182  "\n";
183 
184  // GCC junk stuff, also for CLANG and ARM
185  if(
189  {
191 
192  // there are many more, e.g., look at
193  // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
194 
195  if(
196  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
197  config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
198  config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
199  config.ansi_c.arch == "ia64")
200  {
201  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
202  // For clang, __float128 is a keyword.
203  // For gcc, this is a typedef and not a keyword.
205  code += "typedef __CPROVER_Float128 __float128;\n";
206  }
207  else if(config.ansi_c.arch == "hppa")
208  {
209  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
210  // For clang, __float128 is a keyword.
211  // For gcc, this is a typedef and not a keyword.
213  code+="typedef long double __float128;\n";
214  }
215 
216  if(
217  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
218  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
219  {
220  // clang doesn't do __float80
221  // Note that __float80 is a typedef, and not a keyword.
223  code += "typedef __CPROVER_Float64x __float80;\n";
224  }
225 
226  // On 64-bit systems, gcc has typedefs
227  // __int128_t und __uint128_t -- but not on 32 bit!
229  {
230  code+="typedef signed __int128 __int128_t;\n"
231  "typedef unsigned __int128 __uint128_t;\n";
232  }
233  }
234 
235  // this is Visual C/C++ only
237  code+="int __noop();\n"
238  "int __assume(int);\n";
239 
240  // ARM stuff
242  code+=arm_builtin_headers;
243 
244  // CW stuff
246  code+=cw_builtin_headers;
247 
248  // Architecture strings
250 }
251 
252 void ansi_c_architecture_strings(std::string &code)
253 {
254  // The following are CPROVER-specific.
255  // They allow identifying the architectural settings used
256  // at compile time from a goto-binary.
257 
258  code+="# 1 \"<builtin-architecture-strings>\"\n";
259 
260  code+=architecture_string(config.ansi_c.int_width, "int_width");
261  code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
262  code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
263  code+=architecture_string(config.ansi_c.bool_width, "bool_width");
264  code+=architecture_string(config.ansi_c.char_width, "char_width");
265  code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
266  code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
267  code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
268  code+=architecture_string(config.ansi_c.single_width, "single_width");
269  code+=architecture_string(config.ansi_c.double_width, "double_width");
270  code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
271  code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
272  code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
273  code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
274  code+=architecture_string(config.ansi_c.alignment, "alignment");
275  code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
276  code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
278  code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
279  code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
280 }
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_ubsan[]
std::size_t alignment
Definition: config.h:69
static std::string os_to_string(ost)
Definition: config.cpp:1042
const char gcc_builtin_headers_types[]
std::size_t single_width
Definition: config.h:37
endiannesst endianness
Definition: config.h:76
bool NULL_is_zero
Definition: config.h:87
const char gcc_builtin_headers_alpha[]
std::size_t double_width
Definition: config.h:38
configt config
Definition: config.cpp:23
std::size_t char_width
Definition: config.h:33
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
const char arm_builtin_headers[]
void ansi_c_internal_additions(std::string &code)
const char cw_builtin_headers[]
const char gcc_builtin_headers_omp[]
const char gcc_builtin_headers_mips[]
static std::string architecture_string(const std::string &value, const char *s)
std::size_t long_long_int_width
Definition: config.h:35
flavourt mode
Definition: config.h:114
const char cprover_builtin_headers[]
#define INITIALIZE_FUNCTION
irep_idt arch
Definition: config.h:84
void ansi_c_architecture_strings(std::string &code)
const char gcc_builtin_headers_generic[]
std::size_t int_width
Definition: config.h:30
const char windows_builtin_headers[]
const char gcc_builtin_headers_tm[]
const char gcc_builtin_headers_mem_string[]
std::size_t pointer_width
Definition: config.h:36
const char gcc_builtin_headers_ia32_4[]
bool char_is_unsigned
Definition: config.h:43
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:258
std::size_t wchar_t_width
Definition: config.h:40
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
const char clang_builtin_headers[]
const char gcc_builtin_headers_math[]
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const char gcc_builtin_headers_ia32[]
std::size_t memory_operand_size
Definition: config.h:73
const char gcc_builtin_headers_arm[]
std::size_t bool_width
Definition: config.h:32
bool wchar_t_is_unsigned
Definition: config.h:43
const char gcc_builtin_headers_ia32_2[]
std::size_t long_int_width
Definition: config.h:31
std::size_t short_int_width
Definition: config.h:34
std::size_t long_double_width
Definition: config.h:39
const char gcc_builtin_headers_power[]