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_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_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_integer;" << '\n';
67  out << "typedef void __CPROVER_rational;" << '\n';
68  // TODO
69  // out << "thread_local unsigned long __CPROVER_thread_id = 0;" << '\n';
70  out << "__CPROVER_bool "
71  << "__CPROVER_threads_exited[__CPROVER::constant_infinity_uint];" << '\n';
72  out << "unsigned long __CPROVER_next_thread_id = 0;" << '\n';
73  out << "extern unsigned char "
74  << "__CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';
75 
76  // malloc
77  out << "const void *__CPROVER_deallocated = 0;" << '\n';
78  out << "const void *__CPROVER_dead_object = 0;" << '\n';
79  out << "const void *__CPROVER_malloc_object = 0;" << '\n';
80  out << "__CPROVER::size_t __CPROVER_malloc_size;" << '\n';
81  out << "__CPROVER_bool __CPROVER_malloc_is_new_array = 0;" << '\n';
82  out << "const void *__CPROVER_memory_leak = 0;" << '\n';
83  out << "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);"
84  << '\n';
85 
86  // auxiliaries for new/delete
87  out << "void *__new(__CPROVER::size_t);" << '\n';
88  out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
89  out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
90  out << "void *__placement_new_array("
91  << "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
92  out << "void __delete(void *);" << '\n';
93  out << "void __delete_array(void *);" << '\n';
94 
95  // float
96  // TODO: should the thread_local
97  out << "int __CPROVER_rounding_mode = "
98  << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
99 
100  // pipes, write, read, close
101  out << "struct __CPROVER_pipet {\n"
102  << " bool widowed;\n"
103  << " char data[4];\n"
104  << " short next_avail;\n"
105  << " short next_unread;\n"
106  << "};\n";
107  out << "extern struct __CPROVER_pipet "
108  << "__CPROVER_pipes[__CPROVER::constant_infinity_uint];" << '\n';
109  // offset to make sure we don't collide with other fds
110  out << "extern const int __CPROVER_pipe_offset;" << '\n';
111  out << "unsigned __CPROVER_pipe_count=0;" << '\n';
112 
113  // This function needs to be declared, or otherwise can't be called
114  // by the entry-point construction.
115  out << "void " INITIALIZE_FUNCTION "();" << '\n';
116 
117  // GCC junk stuff, also for CLANG and ARM
121  {
123 
124  if(
125  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
126  config.ansi_c.arch == "x32")
127  {
128  // clang doesn't do __float128
130  out << "typedef double __float128;" << '\n';
131  }
132 
133  // On 64-bit systems, gcc has typedefs
134  // __int128_t und __uint128_t -- but not on 32 bit!
135  if(config.ansi_c.long_int_width >= 64)
136  {
137  out << "typedef signed __int128 __int128_t;" << '\n';
138  out << "typedef unsigned __int128 __uint128_t;" << '\n';
139  }
140  }
141 
142  // this is Visual C/C++ only
144  {
145  out << "int __noop(...);" << '\n';
146  out << "int __assume(int);" << '\n';
147  }
148 
149  // ARM stuff
151  out << c2cpp(arm_builtin_headers);
152 
153  // CW stuff
155  out << c2cpp(cw_builtin_headers);
156 
157  // string symbols to identify the architecture we have compiled for
158  std::string architecture_strings;
159  ansi_c_architecture_strings(architecture_strings);
160  out << c2cpp(architecture_strings);
161 
162  out << '}' << '\n'; // end extern "C"
163 
164  // Microsoft stuff
166  {
167  // type_info infrastructure -- the standard wants this to be in the
168  // std:: namespace, but MS has it in the root namespace
169  out << "class type_info;" << '\n';
170 
171  // this is the return type of __uuidof(...),
172  // in the root namespace
173  out << "struct _GUID;" << '\n';
174 
175  // MS ATL-related stuff
176  out << "namespace ATL; " << '\n';
177  out << "void ATL::AtlThrowImpl(long);" << '\n';
178  out << "void __stdcall ATL::AtlThrowLastWin32();" << '\n';
179  }
180 
181  out << std::flush;
182 }
struct configt::ansi_ct ansi_c
const char gcc_builtin_headers_types[]
configt config
Definition: config.cpp:23
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:106
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::string to_string(const string_constraintt &expr)
Used for debug printing.
std::size_t long_int_width
Definition: config.h:31