cprover
cpp_internal_additions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
22std::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
45void cpp_internal_additions(std::ostream &out)
46{
47 out << "#line 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 "new_object = 0;" << '\n';
94 out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
95 << '\n';
96 out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
97 out << "void *" CPROVER_PREFIX "allocate("
98 << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
99 out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n';
100
101 // auxiliaries for new/delete
102 out << "void *__new(__CPROVER::size_t);" << '\n';
103 out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
104 out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
105 out << "void *__placement_new_array("
106 << "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
107 out << "void __delete(void *);" << '\n';
108 out << "void __delete_array(void *);" << '\n';
109
110 // float
111 // TODO: should be thread_local
112 out << "int " << rounding_mode_identifier() << " = "
113 << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
114
115 // pipes, write, read, close
116 out << "struct " CPROVER_PREFIX "pipet {\n"
117 << " bool widowed;\n"
118 << " char data[4];\n"
119 << " short next_avail;\n"
120 << " short next_unread;\n"
121 << "};\n";
122 out << "extern struct " CPROVER_PREFIX "pipet "
123 << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n';
124 // offset to make sure we don't collide with other fds
125 out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n';
126 out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n';
127
128 // This function needs to be declared, or otherwise can't be called
129 // by the entry-point construction.
130 out << "void " INITIALIZE_FUNCTION "();" << '\n';
131
132 // GCC junk stuff, also for CLANG and ARM
133 if(
137 {
139
140 if(
141 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
142 config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
143 config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
144 config.ansi_c.arch == "ia64")
145 {
146 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
147 // For clang, __float128 is a keyword.
148 // For gcc, this is a typedef and not a keyword.
149 // C++ doesn't have _Float128.
151 out << "typedef " CPROVER_PREFIX "Float128 __float128;" << '\n';
152 }
153 else if(config.ansi_c.arch == "hppa")
154 {
155 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
156 // For clang, __float128 is a keyword.
157 // For gcc, this is a typedef and not a keyword.
158 // C++ doesn't have _Float128.
160 out << "typedef long double __float128;" << '\n';
161 }
162
163 if(
164 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
165 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
166 {
167 // clang doesn't do __float80
168 // Note that __float80 is a typedef, and not a keyword,
169 // and that C++ doesn't have _Float64x.
171 out << "typedef " CPROVER_PREFIX "Float80 __float80;" << '\n';
172 }
173
174 // On 64-bit systems, gcc has typedefs
175 // __int128_t und __uint128_t -- but not on 32 bit!
177 {
178 out << "typedef signed __int128 __int128_t;" << '\n';
179 out << "typedef unsigned __int128 __uint128_t;" << '\n';
180 }
181 }
182
183 // this is Visual C/C++ only
185 {
186 out << "int __noop(...);" << '\n';
187 out << "int __assume(int);" << '\n';
188 }
189
190 // ARM stuff
193
194 // CW stuff
197
198 // string symbols to identify the architecture we have compiled for
199 std::string architecture_strings;
200 ansi_c_architecture_strings(architecture_strings);
201 out << c2cpp(architecture_strings);
202
203 out << '}' << '\n'; // end extern "C"
204
205 // Microsoft stuff
207 {
208 // type_info infrastructure -- the standard wants this to be in the
209 // std:: namespace, but MS has it in the root namespace
210 out << "class type_info;" << '\n';
211
212 // this is the return type of __uuidof(...),
213 // in the root namespace
214 out << "struct _GUID;" << '\n';
215
216 // MS ATL-related stuff
217 out << "namespace ATL; " << '\n';
218 out << "void ATL::AtlThrowImpl(long);" << '\n';
219 out << "void __stdcall ATL::AtlThrowLastWin32();" << '\n';
220 }
221
222 out << std::flush;
223}
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:269
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
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:191
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:151
std::size_t long_int_width
Definition: config.h:110
flavourt mode
Definition: config.h:222