cprover
cpp_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 <ostream>
12 
13 #include <util/c_types.h>
14 #include <util/config.h>
15 
17 
19 
20 std::string c2cpp(const std::string &s)
21 {
22  std::string result;
23 
24  result.reserve(s.size());
25 
26  for(std::size_t i=0; i<s.size(); i++)
27  {
28  char ch=s[i];
29 
30  if(ch=='_' && std::string(s, i, 5)=="_Bool")
31  {
32  result.append("bool");
33  i+=4;
34  continue;
35  }
36 
37  result+=ch;
38  }
39 
40  return result;
41 }
42 
43 void cpp_internal_additions(std::ostream &out)
44 {
45  out << "# 1 \"<built-in-additions>\"" << '\n';
46 
47  // __CPROVER namespace
48  out << "namespace __CPROVER { }" << '\n';
49 
50  // types
51  out << "typedef __typeof__(sizeof(int)) __CPROVER::size_t;" << '\n';
52  out << "typedef __CPROVER::size_t " CPROVER_PREFIX "size_t;" << '\n';
53  out << "typedef "
54  << c_type_as_string(signed_size_type().get(ID_C_c_type))
55  << " __CPROVER::ssize_t;" << '\n';
56  out << "typedef __CPROVER::ssize_t " CPROVER_PREFIX "ssize_t;" << '\n';
57 
58  // new and delete are in the root namespace!
59  out << "void operator delete(void *);" << '\n';
60  out << "void *operator new(__CPROVER::size_t);" << '\n';
61 
62  out << "extern \"C\" {" << '\n';
63 
64  // CPROVER extensions
65  out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n';
66  out << "typedef void " CPROVER_PREFIX "integer;" << '\n';
67  out << "typedef void " CPROVER_PREFIX "rational;" << '\n';
68  // TODO: thread_local is still broken
69  // out << "thread_local unsigned long "
70  // << CPROVER_PREFIX "thread_id = 0;" << '\n';
71  out << CPROVER_PREFIX "bool "
72  << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];"
73  << '\n';
74  out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n';
75  // TODO: thread_local is still broken
76  out << "void* "
77  << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];"
78  << '\n';
79  // TODO: thread_local is still broken
80  out << "void (*"
81  << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])"
82  << "(void *);" << '\n';
83  // TODO: thread_local is still broken
84  out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n';
85  out << "extern unsigned char "
86  << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n';
87 
88  // malloc
89  out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
90  out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
91  out << "const void *" CPROVER_PREFIX "malloc_object = 0;" << '\n';
92  out << "__CPROVER::size_t " CPROVER_PREFIX "malloc_size;" << '\n';
93  out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
94  << '\n';
95  out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
96  out << "void *" CPROVER_PREFIX "allocate("
97  << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
98  out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n';
99 
100  // auxiliaries for new/delete
101  out << "void *__new(__CPROVER::size_t);" << '\n';
102  out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
103  out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
104  out << "void *__placement_new_array("
105  << "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
106  out << "void __delete(void *);" << '\n';
107  out << "void __delete_array(void *);" << '\n';
108 
109  // float
110  // TODO: should be thread_local
111  out << "int " CPROVER_PREFIX "rounding_mode = "
112  << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
113 
114  // pipes, write, read, close
115  out << "struct " CPROVER_PREFIX "pipet {\n"
116  << " bool widowed;\n"
117  << " char data[4];\n"
118  << " short next_avail;\n"
119  << " short next_unread;\n"
120  << "};\n";
121  out << "extern struct " CPROVER_PREFIX "pipet "
122  << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n';
123  // offset to make sure we don't collide with other fds
124  out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n';
125  out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n';
126 
127  // This function needs to be declared, or otherwise can't be called
128  // by the entry-point construction.
129  out << "void " INITIALIZE_FUNCTION "();" << '\n';
130 
131  // GCC junk stuff, also for CLANG and ARM
132  if(
136  {
138 
139  if(
140  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
141  config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
142  config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
143  config.ansi_c.arch == "ia64")
144  {
145  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
146  // For clang, __float128 is a keyword.
147  // For gcc, this is a typedef and not a keyword.
148  // C++ doesn't have _Float128.
150  out << "typedef " CPROVER_PREFIX "Float128 __float128;" << '\n';
151  }
152  else if(config.ansi_c.arch == "hppa")
153  {
154  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
155  // For clang, __float128 is a keyword.
156  // For gcc, this is a typedef and not a keyword.
157  // C++ doesn't have _Float128.
159  out << "typedef long double __float128;" << '\n';
160  }
161 
162  if(
163  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
164  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
165  {
166  // clang doesn't do __float80
167  // Note that __float80 is a typedef, and not a keyword,
168  // and that C++ doesn't have _Float64x.
170  out << "typedef " CPROVER_PREFIX "Float80 __float80;" << '\n';
171  }
172 
173  // On 64-bit systems, gcc has typedefs
174  // __int128_t und __uint128_t -- but not on 32 bit!
175  if(config.ansi_c.long_int_width >= 64)
176  {
177  out << "typedef signed __int128 __int128_t;" << '\n';
178  out << "typedef unsigned __int128 __uint128_t;" << '\n';
179  }
180  }
181 
182  // this is Visual C/C++ only
184  {
185  out << "int __noop(...);" << '\n';
186  out << "int __assume(int);" << '\n';
187  }
188 
189  // ARM stuff
191  out << c2cpp(arm_builtin_headers);
192 
193  // CW stuff
195  out << c2cpp(cw_builtin_headers);
196 
197  // string symbols to identify the architecture we have compiled for
198  std::string architecture_strings;
199  ansi_c_architecture_strings(architecture_strings);
200  out << c2cpp(architecture_strings);
201 
202  out << '}' << '\n'; // end extern "C"
203 
204  // Microsoft stuff
206  {
207  // type_info infrastructure -- the standard wants this to be in the
208  // std:: namespace, but MS has it in the root namespace
209  out << "class type_info;" << '\n';
210 
211  // this is the return type of __uuidof(...),
212  // in the root namespace
213  out << "struct _GUID;" << '\n';
214 
215  // MS ATL-related stuff
216  out << "namespace ATL; " << '\n';
217  out << "void ATL::AtlThrowImpl(long);" << '\n';
218  out << "void __stdcall ATL::AtlThrowLastWin32();" << '\n';
219  }
220 
221  out << std::flush;
222 }
configt::ansi_ct::flavourt::CODEWARRIOR
@ CODEWARRIOR
cpp_internal_additions
void cpp_internal_additions(std::ostream &out)
Definition: cpp_internal_additions.cpp:43
configt::ansi_ct::os
ost os
Definition: config.h:80
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
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
c2cpp
std::string c2cpp(const std::string &s)
Definition: cpp_internal_additions.cpp:20
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
cpp_internal_additions.h
configt::ansi_ct::flavourt::ARM
@ ARM
configt::ansi_ct::flavourt::CLANG
@ CLANG
gcc_builtin_headers_types
const char gcc_builtin_headers_types[]
Definition: ansi_c_internal_additions.cpp:18
ansi_c_internal_additions.h
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
signed_size_type
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
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
arm_builtin_headers
const char arm_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:87
config
configt config
Definition: config.cpp:24
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
c_type_as_string
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:259
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
config.h
configt::ansi_ct::flavourt::GCC
@ GCC
static_lifetime_init.h
c_types.h
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:32