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  out << "extern unsigned char "
76  << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n';
77 
78  // malloc
79  out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
80  out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
81  out << "const void *" CPROVER_PREFIX "malloc_object = 0;" << '\n';
82  out << "__CPROVER::size_t " CPROVER_PREFIX "malloc_size;" << '\n';
83  out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
84  << '\n';
85  out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
86  out << "void *" CPROVER_PREFIX "allocate("
87  << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
88 
89  // auxiliaries for new/delete
90  out << "void *__new(__CPROVER::size_t);" << '\n';
91  out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
92  out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
93  out << "void *__placement_new_array("
94  << "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
95  out << "void __delete(void *);" << '\n';
96  out << "void __delete_array(void *);" << '\n';
97 
98  // float
99  // TODO: should be thread_local
100  out << "int " CPROVER_PREFIX "rounding_mode = "
101  << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
102 
103  // pipes, write, read, close
104  out << "struct " CPROVER_PREFIX "pipet {\n"
105  << " bool widowed;\n"
106  << " char data[4];\n"
107  << " short next_avail;\n"
108  << " short next_unread;\n"
109  << "};\n";
110  out << "extern struct " CPROVER_PREFIX "pipet "
111  << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n';
112  // offset to make sure we don't collide with other fds
113  out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n';
114  out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n';
115 
116  // This function needs to be declared, or otherwise can't be called
117  // by the entry-point construction.
118  out << "void " INITIALIZE_FUNCTION "();" << '\n';
119 
120  // GCC junk stuff, also for CLANG and ARM
121  if(
125  {
127 
128  if(
129  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
130  config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
131  config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
132  config.ansi_c.arch == "ia64")
133  {
134  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
135  // For clang, __float128 is a keyword.
136  // For gcc, this is a typedef and not a keyword.
137  // C++ doesn't have _Float128.
139  out << "typedef " CPROVER_PREFIX "Float128 __float128;" << '\n';
140  }
141  else if(config.ansi_c.arch == "hppa")
142  {
143  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
144  // For clang, __float128 is a keyword.
145  // For gcc, this is a typedef and not a keyword.
146  // C++ doesn't have _Float128.
148  out << "typedef long double __float128;" << '\n';
149  }
150 
151  if(
152  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
153  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
154  {
155  // clang doesn't do __float80
156  // Note that __float80 is a typedef, and not a keyword,
157  // and that C++ doesn't have _Float64x.
159  out << "typedef " CPROVER_PREFIX "Float80 __float80;" << '\n';
160  }
161 
162  // On 64-bit systems, gcc has typedefs
163  // __int128_t und __uint128_t -- but not on 32 bit!
164  if(config.ansi_c.long_int_width >= 64)
165  {
166  out << "typedef signed __int128 __int128_t;" << '\n';
167  out << "typedef unsigned __int128 __uint128_t;" << '\n';
168  }
169  }
170 
171  // this is Visual C/C++ only
173  {
174  out << "int __noop(...);" << '\n';
175  out << "int __assume(int);" << '\n';
176  }
177 
178  // ARM stuff
180  out << c2cpp(arm_builtin_headers);
181 
182  // CW stuff
184  out << c2cpp(cw_builtin_headers);
185 
186  // string symbols to identify the architecture we have compiled for
187  std::string architecture_strings;
188  ansi_c_architecture_strings(architecture_strings);
189  out << c2cpp(architecture_strings);
190 
191  out << '}' << '\n'; // end extern "C"
192 
193  // Microsoft stuff
195  {
196  // type_info infrastructure -- the standard wants this to be in the
197  // std:: namespace, but MS has it in the root namespace
198  out << "class type_info;" << '\n';
199 
200  // this is the return type of __uuidof(...),
201  // in the root namespace
202  out << "struct _GUID;" << '\n';
203 
204  // MS ATL-related stuff
205  out << "namespace ATL; " << '\n';
206  out << "void ATL::AtlThrowImpl(long);" << '\n';
207  out << "void __stdcall ATL::AtlThrowLastWin32();" << '\n';
208  }
209 
210  out << std::flush;
211 }
struct configt::ansi_ct ansi_c
#define CPROVER_PREFIX
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const char gcc_builtin_headers_types[]
configt config
Definition: config.cpp:24
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
const char arm_builtin_headers[]
const char cw_builtin_headers[]
void cpp_internal_additions(std::ostream &out)
flavourt mode
Definition: config.h:115
std::string c2cpp(const std::string &s)
#define INITIALIZE_FUNCTION
irep_idt arch
Definition: config.h:84
void ansi_c_architecture_strings(std::string &code)
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:258
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
std::size_t long_int_width
Definition: config.h:31