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