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_PREFIX "architecture_") +
113  std::string(s) + "=\"" + value + "\";\n";
114 }
115 
116 template <typename T>
117 static std::string architecture_string(T value, const char *s)
118 {
119  return std::string("const int " CPROVER_PREFIX "architecture_") +
120  std::string(s) + "=" + std::to_string(value) + ";\n";
121 }
122 
123 void ansi_c_internal_additions(std::string &code)
124 {
125  // clang-format off
126  // do the built-in types and variables
127  code+=
128  "# 1 \"<built-in-additions>\"\n"
129  "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
130  "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
131  " " CPROVER_PREFIX "ssize_t;\n"
132  "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
133  "typedef void " CPROVER_PREFIX "integer;\n"
134  "typedef void " CPROVER_PREFIX "rational;\n"
135  CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
136  CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
137  CPROVER_PREFIX "constant_infinity_uint];\n"
138  "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
139  CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys["
140  CPROVER_PREFIX "constant_infinity_uint];\n"
141  CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors["
142  CPROVER_PREFIX "constant_infinity_uint])(void *);\n"
143  CPROVER_PREFIX "thread_local unsigned long "
144  CPROVER_PREFIX "next_thread_key = 0;\n"
145  "extern unsigned char " CPROVER_PREFIX "memory["
146  CPROVER_PREFIX "constant_infinity_uint];\n"
147 
148  // malloc
149  "const void *" CPROVER_PREFIX "deallocated=0;\n"
150  "const void *" CPROVER_PREFIX "dead_object=0;\n"
151  "const void *" CPROVER_PREFIX "malloc_object=0;\n"
152  CPROVER_PREFIX "size_t " CPROVER_PREFIX "malloc_size;\n"
153  CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
154  "const void *" CPROVER_PREFIX "memory_leak=0;\n"
155  "void *" CPROVER_PREFIX "allocate("
156  CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
157  "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
158 
159  // this is ANSI-C
160  "extern " CPROVER_PREFIX "thread_local const char __func__["
161  CPROVER_PREFIX "constant_infinity_uint];\n"
162 
163  // this is GCC
164  "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
165  CPROVER_PREFIX "constant_infinity_uint];\n"
166  "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
167  CPROVER_PREFIX "constant_infinity_uint];\n"
168 
169  // float stuff
170  "int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+
172 
173  // pipes, write, read, close
174  "struct " CPROVER_PREFIX "pipet {\n"
175  " _Bool widowed;\n"
176  " char data[4];\n"
177  " short next_avail;\n"
178  " short next_unread;\n"
179  "};\n"
180  "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
181  CPROVER_PREFIX "constant_infinity_uint];\n"
182  // offset to make sure we don't collide with other fds
183  "extern const int " CPROVER_PREFIX "pipe_offset;\n"
184  "unsigned " CPROVER_PREFIX "pipe_count=0;\n"
185  "\n"
186  // This function needs to be declared, or otherwise can't be called
187  // by the entry-point construction.
188  "void " INITIALIZE_FUNCTION "(void);\n"
189  "\n";
190  // clang-format on
191 
192  // GCC junk stuff, also for CLANG and ARM
193  if(
197  {
199 
200  // there are many more, e.g., look at
201  // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
202 
203  if(
204  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
205  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
206  config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
207  {
208  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
209  // For clang, __float128 is a keyword.
210  // For gcc, this is a typedef and not a keyword.
211  if(
214  {
215  code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
216  }
217  }
218  else if(config.ansi_c.arch == "ppc64le")
219  {
220  // https://patchwork.ozlabs.org/patch/792295/
222  code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
223  }
224  else if(config.ansi_c.arch == "hppa")
225  {
226  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
227  // For clang, __float128 is a keyword.
228  // For gcc, this is a typedef and not a keyword.
229  if(
232  {
233  code+="typedef long double __float128;\n";
234  }
235  }
236 
237  if(
238  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
239  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
240  {
241  // clang doesn't do __float80
242  // Note that __float80 is a typedef, and not a keyword.
244  code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
245  }
246 
247  // On 64-bit systems, gcc has typedefs
248  // __int128_t und __uint128_t -- but not on 32 bit!
250  {
251  code+="typedef signed __int128 __int128_t;\n"
252  "typedef unsigned __int128 __uint128_t;\n";
253  }
254  }
255 
256  // this is Visual C/C++ only
258  code+="int __noop();\n"
259  "int __assume(int);\n";
260 
261  // ARM stuff
263  code+=arm_builtin_headers;
264 
265  // CW stuff
267  code+=cw_builtin_headers;
268 
269  // Architecture strings
271 }
272 
273 void ansi_c_architecture_strings(std::string &code)
274 {
275  // The following are CPROVER-specific.
276  // They allow identifying the architectural settings used
277  // at compile time from a goto-binary.
278 
279  code+="# 1 \"<builtin-architecture-strings>\"\n";
280 
281  code+=architecture_string(config.ansi_c.int_width, "int_width");
282  code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
283  code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
284  code+=architecture_string(config.ansi_c.bool_width, "bool_width");
285  code+=architecture_string(config.ansi_c.char_width, "char_width");
286  code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
287  code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
288  code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
289  code+=architecture_string(config.ansi_c.single_width, "single_width");
290  code+=architecture_string(config.ansi_c.double_width, "double_width");
291  code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
292  code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
293  code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
294  code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
295  code+=architecture_string(config.ansi_c.alignment, "alignment");
296  code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
297  code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
299  code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
300  code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
301 }
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:36
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:70
architecture_string
static std::string architecture_string(const std::string &value, const char *s)
Definition: ansi_c_internal_additions.cpp:110
configt::ansi_ct::flavourt::CODEWARRIOR
@ CODEWARRIOR
windows_builtin_headers
const char windows_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:105
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:273
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:31
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:46
clang_builtin_headers
const char clang_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:95
gcc_builtin_headers_types
const char gcc_builtin_headers_types[]
Definition: ansi_c_internal_additions.cpp:16
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
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:51
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:123
gcc_builtin_headers_ia32_2
const char gcc_builtin_headers_ia32_2[]
Definition: ansi_c_internal_additions.cpp:55
cw_builtin_headers
const char cw_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:90
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:1099
arm_builtin_headers
const char arm_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:85
config
configt config
Definition: config.cpp:24
gcc_builtin_headers_mips
const char gcc_builtin_headers_mips[]
Definition: ansi_c_internal_additions.cpp:75
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
cprover_builtin_headers
const char cprover_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:100
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:80
gcc_builtin_headers_ia32_3
const char gcc_builtin_headers_ia32_3[]
Definition: ansi_c_internal_additions.cpp:58
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:41
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:61
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:65
gcc_builtin_headers_generic
const char gcc_builtin_headers_generic[]
Definition: ansi_c_internal_additions.cpp:21
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
gcc_builtin_headers_math
const char gcc_builtin_headers_math[]
Definition: ansi_c_internal_additions.cpp:26