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 static std::string architecture_string(int value, const char *s)
118 {
119  return std::string("const int __CPROVER_architecture_")+
120  std::string(s)+
121  "="+std::to_string(value)+";\n";
122 }
123 
124 void ansi_c_internal_additions(std::string &code)
125 {
126  // do the built-in types and variables
127  code+=
128  "# 1 \"<built-in-additions>\"\n"
129  "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
130  "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
131  " __CPROVER_ssize_t;\n"
132  "const unsigned __CPROVER_constant_infinity_uint;\n"
133  "typedef void __CPROVER_integer;\n"
134  "typedef void __CPROVER_rational;\n"
135  "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
136  // NOLINTNEXTLINE(whitespace/line_length)
137  "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
138  "unsigned long __CPROVER_next_thread_id=0;\n"
139  // NOLINTNEXTLINE(whitespace/line_length)
140  "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
141 
142  // malloc
143  "const void *__CPROVER_deallocated=0;\n"
144  "const void *__CPROVER_dead_object=0;\n"
145  "const void *__CPROVER_malloc_object=0;\n"
146  "__CPROVER_size_t __CPROVER_malloc_size;\n"
147  "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++
148  "const void *__CPROVER_memory_leak=0;\n"
149  "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
150 
151  // this is ANSI-C
152  // NOLINTNEXTLINE(whitespace/line_length)
153  "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
154 
155  // this is GCC
156  // NOLINTNEXTLINE(whitespace/line_length)
157  "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
158  // NOLINTNEXTLINE(whitespace/line_length)
159  "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
160 
161  // float stuff
162  "int __CPROVER_thread_local __CPROVER_rounding_mode="+
164 
165  // pipes, write, read, close
166  "struct __CPROVER_pipet {\n"
167  " _Bool widowed;\n"
168  " char data[4];\n"
169  " short next_avail;\n"
170  " short next_unread;\n"
171  "};\n"
172  // NOLINTNEXTLINE(whitespace/line_length)
173  "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
174  // offset to make sure we don't collide with other fds
175  "extern const int __CPROVER_pipe_offset;\n"
176  "unsigned __CPROVER_pipe_count=0;\n"
177  "\n"
178  // This function needs to be declared, or otherwise can't be called
179  // by the entry-point construction.
180  "void " INITIALIZE_FUNCTION "(void);\n"
181  "\n";
182 
183  // GCC junk stuff, also for CLANG and ARM
187  {
189 
190  // there are many more, e.g., look at
191  // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
192 
193  if(config.ansi_c.arch=="i386" ||
194  config.ansi_c.arch=="x86_64" ||
195  config.ansi_c.arch=="x32")
196  {
198  code+="typedef double __float128;\n"; // clang doesn't do __float128
199  }
200 
201  // On 64-bit systems, gcc has typedefs
202  // __int128_t und __uint128_t -- but not on 32 bit!
204  {
205  code+="typedef signed __int128 __int128_t;\n"
206  "typedef unsigned __int128 __uint128_t;\n";
207  }
208  }
209 
210  // this is Visual C/C++ only
212  code+="int __noop();\n"
213  "int __assume(int);\n";
214 
215  // ARM stuff
217  code+=arm_builtin_headers;
218 
219  // CW stuff
221  code+=cw_builtin_headers;
222 
223  // Architecture strings
225 }
226 
227 void ansi_c_architecture_strings(std::string &code)
228 {
229  // The following are CPROVER-specific.
230  // They allow identifying the architectural settings used
231  // at compile time from a goto-binary.
232 
233  code+="# 1 \"<builtin-architecture-strings>\"\n";
234 
235  code+=architecture_string(config.ansi_c.int_width, "int_width");
236  code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
237  code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
238  code+=architecture_string(config.ansi_c.bool_width, "bool_width");
239  code+=architecture_string(config.ansi_c.char_width, "char_width");
240  code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
241  code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
242  code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
243  code+=architecture_string(config.ansi_c.single_width, "single_width");
244  code+=architecture_string(config.ansi_c.double_width, "double_width");
245  code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
246  code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
247  code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
248  code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
249  code+=architecture_string(config.ansi_c.alignment, "alignment");
250  code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
251  code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
253  code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
254  code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
255 }
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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:1041
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:106
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[]