cprover
cpp_convert_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Conversion
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_convert_type.h"
13 
14 #include <cassert>
15 
16 #include <util/config.h>
17 #include <util/arith_tools.h>
18 #include <util/std_types.h>
19 
20 #include <util/c_types.h>
21 
22 #include "cpp_declaration.h"
23 #include "cpp_name.h"
24 
26 {
27 public:
34 
35  void read(const typet &type);
36  void write(typet &type);
37 
38  std::list<typet> other;
39 
41  explicit cpp_convert_typet(const typet &type) { read(type); }
42 
43 protected:
44  void read_rec(const typet &type);
45  void read_function_type(const typet &type);
46  void read_template(const typet &type);
47 };
48 
49 void cpp_convert_typet::read(const typet &type)
50 {
57 
58  other.clear();
59 
60  #if 0
61  std::cout << "cpp_convert_typet::read: " << type.pretty() << '\n';
62  #endif
63 
64  read_rec(type);
65 }
66 
68 {
69  #if 0
70  std::cout << "cpp_convert_typet::read_rec: "
71  << type.pretty() << '\n';
72  #endif
73 
74  if(type.id()==ID_merged_type)
75  {
76  forall_subtypes(it, type)
77  read_rec(*it);
78  }
79  else if(type.id()==ID_signed)
80  signed_cnt++;
81  else if(type.id()==ID_unsigned)
82  unsigned_cnt++;
83  else if(type.id()==ID_volatile)
84  volatile_cnt++;
85  else if(type.id()==ID_char)
86  char_cnt++;
87  else if(type.id()==ID_int)
88  int_cnt++;
89  else if(type.id()==ID_short)
90  short_cnt++;
91  else if(type.id()==ID_long)
92  long_cnt++;
93  else if(type.id()==ID_double)
94  double_cnt++;
95  else if(type.id()==ID_float)
96  float_cnt++;
97  else if(type.id()==ID_gcc_float128)
98  float128_cnt++;
99  else if(type.id()==ID_gcc_int128)
100  int128_cnt++;
101  else if(type.id()==ID_complex)
102  complex_cnt++;
103  else if(type.id()==ID_bool)
104  cpp_bool_cnt++;
105  else if(type.id()==ID_proper_bool)
106  proper_bool_cnt++;
107  else if(type.id()==ID_wchar_t)
108  wchar_t_cnt++;
109  else if(type.id()==ID_char16_t)
110  char16_t_cnt++;
111  else if(type.id()==ID_char32_t)
112  char32_t_cnt++;
113  else if(type.id()==ID_int8)
114  int8_cnt++;
115  else if(type.id()==ID_int16)
116  int16_cnt++;
117  else if(type.id()==ID_int32)
118  int32_cnt++;
119  else if(type.id()==ID_int64)
120  int64_cnt++;
121  else if(type.id()==ID_ptr32)
122  ptr32_cnt++;
123  else if(type.id()==ID_ptr64)
124  ptr64_cnt++;
125  else if(type.id()==ID_const)
126  const_cnt++;
127  else if(type.id()==ID_restrict)
128  restrict_cnt++;
129  else if(type.id()==ID_constexpr)
130  constexpr_cnt++;
131  else if(type.id()==ID_extern)
132  extern_cnt++;
133  else if(type.id()==ID_function_type)
134  {
135  read_function_type(type);
136  }
137  else if(type.id()==ID_identifier)
138  {
139  // from parameters
140  }
141  else if(type.id()==ID_cpp_name)
142  {
143  // from typedefs
144  other.push_back(type);
145  }
146  else if(type.id()==ID_array)
147  {
148  other.push_back(type);
149  cpp_convert_plain_type(other.back().subtype());
150  }
151  else if(type.id()==ID_template)
152  {
153  read_template(type);
154  }
155  else if(type.id()==ID_void)
156  {
157  // we store 'void' as 'empty'
158  typet tmp=type;
159  tmp.id(ID_empty);
160  other.push_back(tmp);
161  }
162  else
163  {
164  other.push_back(type);
165  }
166 }
167 
169 {
170  other.push_back(type);
171  typet &t=other.back();
172 
174 
175  irept &arguments=t.add(ID_arguments);
176 
177  Forall_irep(it, arguments.get_sub())
178  {
179  exprt &decl=static_cast<exprt &>(*it);
180 
181  // may be type or expression
182  bool is_type=decl.get_bool(ID_is_type);
183 
184  if(is_type)
185  {
186  }
187  else
188  {
190  }
191 
192  // TODO: initializer
193  }
194 }
195 
197 {
198  other.push_back(type);
199  typet &t=other.back();
200  t.id(ID_code);
201 
202  // change subtype to return_type
203  typet &return_type=
204  static_cast<typet &>(t.add(ID_return_type));
205 
206  return_type.swap(t.subtype());
207  t.remove_subtype();
208 
209  if(return_type.is_not_nil())
210  cpp_convert_plain_type(return_type);
211 
212  // take care of parameter types
213  irept &parameters=t.add(ID_parameters);
214 
215  // see if we have an ellipsis
216  if(!parameters.get_sub().empty() &&
217  parameters.get_sub().back().id()==ID_ellipsis)
218  {
219  parameters.set(ID_ellipsis, true);
220  parameters.get_sub().erase(--parameters.get_sub().end());
221  }
222 
223  Forall_irep(it, parameters.get_sub())
224  {
225  exprt &parameter_expr=static_cast<exprt &>(*it);
226 
227  if(parameter_expr.id()==ID_cpp_declaration)
228  {
229  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
230  source_locationt type_location=declaration.type().source_location();
231 
232  cpp_convert_plain_type(declaration.type());
233 
234  // there should be only one declarator
235  assert(declaration.declarators().size()==1);
236 
237  cpp_declaratort &declarator=
238  declaration.declarators().front();
239 
240  // do we have a declarator?
241  if(declarator.is_nil())
242  {
243  parameter_expr=exprt(ID_parameter, declaration.type());
244  parameter_expr.add_source_location()=type_location;
245  }
246  else
247  {
248  const cpp_namet &cpp_name=declarator.name();
249  typet final_type=declarator.merge_type(declaration.type());
250 
251  // see if it's an array type
252  if(final_type.id()==ID_array)
253  {
254  // turn into pointer type
255  final_type=pointer_type(final_type.subtype());
256  }
257 
258  code_typet::parametert new_parameter(final_type);
259 
260  if(cpp_name.is_nil())
261  {
262  new_parameter.add_source_location()=type_location;
263  }
264  else if(cpp_name.is_simple_name())
265  {
266  irep_idt base_name=cpp_name.get_base_name();
267  assert(!base_name.empty());
268  new_parameter.set_identifier(base_name);
269  new_parameter.set_base_name(base_name);
270  new_parameter.add_source_location()=cpp_name.source_location();
271  }
272  else
273  {
274  throw "expected simple name as parameter";
275  }
276 
277  if(declarator.value().is_not_nil())
278  new_parameter.default_value().swap(declarator.value());
279 
280  parameter_expr.swap(new_parameter);
281  }
282  }
283  else if(parameter_expr.id()==ID_ellipsis)
284  {
285  throw "ellipsis only allowed as last parameter";
286  }
287  else
288  assert(false);
289  }
290 
291  // if we just have one parameter of type void, remove it
292  if(parameters.get_sub().size()==1 &&
293  parameters.get_sub().front().find(ID_type).id()==ID_empty)
294  parameters.get_sub().clear();
295 }
296 
298 {
299  type.clear();
300 
301  // first, do "other"
302 
303  if(!other.empty())
304  {
305  if(double_cnt || float_cnt || signed_cnt ||
309  int8_cnt || int16_cnt || int32_cnt ||
311  throw "type modifier not applicable";
312 
313  if(other.size()!=1)
314  throw "illegal combination of types";
315 
316  type.swap(other.front());
317  }
318  else if(double_cnt)
319  {
320  if(signed_cnt || unsigned_cnt || int_cnt ||
324  float_cnt ||
325  int8_cnt || int16_cnt || int32_cnt ||
326  int64_cnt || ptr32_cnt || ptr64_cnt ||
328  throw "illegal type modifier for double";
329 
330  if(long_cnt)
331  type=long_double_type();
332  else
333  type=double_type();
334  }
335  else if(float_cnt)
336  {
337  if(signed_cnt || unsigned_cnt || int_cnt ||
341  int8_cnt || int16_cnt || int32_cnt ||
343  throw "illegal type modifier for float";
344 
345  if(long_cnt)
346  throw "float can't be long";
347 
348  type=float_type();
349  }
350  else if(float128_cnt)
351  {
352  if(signed_cnt || unsigned_cnt || int_cnt ||
356  int8_cnt || int16_cnt || int32_cnt ||
358  throw "illegal type modifier for __float128";
359 
360  if(long_cnt)
361  throw "__float128 can't be long";
362 
363  // this isn't the same as long double
364  type=gcc_float128_type();
365  }
366  else if(cpp_bool_cnt)
367  {
371  int8_cnt || int16_cnt || int32_cnt ||
373  throw "illegal type modifier for C++ bool";
374 
375  type.id(ID_bool);
376  }
377  else if(proper_bool_cnt)
378  {
380  char_cnt || wchar_t_cnt ||
382  int8_cnt || int16_cnt || int32_cnt ||
384  throw "illegal type modifier for __CPROVER_bool";
385 
386  type.id(ID_bool);
387  }
388  else if(char_cnt)
389  {
390  if(int_cnt || short_cnt || wchar_t_cnt || long_cnt ||
392  int8_cnt || int16_cnt || int32_cnt ||
394  throw "illegal type modifier for char";
395 
396  // there are really three distinct char types in C++
397  if(unsigned_cnt)
398  type=unsigned_char_type();
399  else if(signed_cnt)
400  type=signed_char_type();
401  else
402  type=char_type();
403  }
404  else if(wchar_t_cnt)
405  {
406  // This is a distinct type, and can't be made signed/unsigned.
407  // This is tolerated by most compilers, however.
408 
409  if(int_cnt || short_cnt || char_cnt || long_cnt ||
411  int8_cnt || int16_cnt || int32_cnt ||
413  throw "illegal type modifier for wchar_t";
414 
415  type=wchar_t_type();
416  }
417  else if(char16_t_cnt)
418  {
419  // This is a distinct type, and can't be made signed/unsigned.
420  if(int_cnt || short_cnt || char_cnt || long_cnt ||
421  char32_t_cnt ||
422  int8_cnt || int16_cnt || int32_cnt ||
423  int64_cnt || ptr32_cnt || ptr64_cnt ||
425  throw "illegal type modifier for char16_t";
426 
427  type=char16_t_type();
428  }
429  else if(char32_t_cnt)
430  {
431  // This is a distinct type, and can't be made signed/unsigned.
432  if(int_cnt || short_cnt || char_cnt || long_cnt ||
433  int8_cnt || int16_cnt || int32_cnt ||
434  int64_cnt || ptr32_cnt || ptr64_cnt ||
436  throw "illegal type modifier for char32_t";
437 
438  type=char32_t_type();
439  }
440  else
441  {
442  // it must be integer -- signed or unsigned?
443 
444  if(signed_cnt && unsigned_cnt)
445  throw "integer cannot be both signed and unsigned";
446 
447  if(short_cnt)
448  {
449  if(long_cnt)
450  throw "cannot combine short and long";
451 
452  if(unsigned_cnt)
454  else
455  type=signed_short_int_type();
456  }
457  else if(int8_cnt)
458  {
459  if(long_cnt)
460  throw "illegal type modifier for __int8";
461 
462  // in terms of overloading, this behaves like "char"
463  if(unsigned_cnt)
464  type=unsigned_char_type();
465  else if(signed_cnt)
466  type=signed_char_type();
467  else
468  type=char_type(); // check?
469  }
470  else if(int16_cnt)
471  {
472  if(long_cnt)
473  throw "illegal type modifier for __int16";
474 
475  // in terms of overloading, this behaves like "short"
476  if(unsigned_cnt)
478  else
479  type=signed_short_int_type();
480  }
481  else if(int32_cnt)
482  {
483  if(long_cnt)
484  throw "illegal type modifier for __int32";
485 
486  // in terms of overloading, this behaves like "int"
487  if(unsigned_cnt)
488  type=unsigned_int_type();
489  else
490  type=signed_int_type();
491  }
492  else if(int64_cnt)
493  {
494  if(long_cnt)
495  throw "illegal type modifier for __int64";
496 
497  // in terms of overloading, this behaves like "long long"
498  if(unsigned_cnt)
500  else
502  }
503  else if(int128_cnt)
504  {
505  if(long_cnt)
506  throw "illegal type modifier for __int128";
507 
508  if(unsigned_cnt)
510  else
511  type=gcc_signed_int128_type();
512  }
513  else if(long_cnt==0)
514  {
515  if(unsigned_cnt)
516  type=unsigned_int_type();
517  else
518  type=signed_int_type();
519  }
520  else if(long_cnt==1)
521  {
522  if(unsigned_cnt)
523  type=unsigned_long_int_type();
524  else
525  type=signed_long_int_type();
526  }
527  else if(long_cnt==2)
528  {
529  if(unsigned_cnt)
531  else
533  }
534  else
535  throw "illegal combination of type modifiers";
536  }
537 
538  // is it constant?
539  if(const_cnt || constexpr_cnt)
540  type.set(ID_C_constant, true);
541 
542  // is it volatile?
543  if(volatile_cnt)
544  type.set(ID_C_volatile, true);
545 }
546 
548 {
549  if(type.id()==ID_cpp_name ||
550  type.id()==ID_struct ||
551  type.id()==ID_union ||
552  type.id()==ID_pointer ||
553  type.id()==ID_array ||
554  type.id()==ID_code ||
555  type.id()==ID_unsignedbv ||
556  type.id()==ID_signedbv ||
557  type.id()==ID_bool ||
558  type.id()==ID_floatbv ||
559  type.id()==ID_empty ||
560  type.id()==ID_symbol ||
561  type.id()==ID_constructor ||
562  type.id()==ID_destructor)
563  {
564  }
565  else if(type.id()==ID_c_enum)
566  {
567  // add width -- we use int, but the standard
568  // doesn't guarantee that
569  type.set(ID_width, config.ansi_c.int_width);
570  }
571  else
572  {
573  cpp_convert_typet cpp_convert_type(type);
574  cpp_convert_type.write(type);
575  }
576 }
The type of an expression.
Definition: type.h:20
#define forall_subtypes(it, type)
Definition: type.h:159
struct configt::ansi_ct ansi_c
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
unsigned int_width
Definition: config.h:30
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:43
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:174
bitvector_typet double_type()
Definition: c_types.cpp:203
typet & type()
Definition: expr.h:60
bool is_simple_name() const
Definition: cpp_name.h:88
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:21
cpp_convert_typet(const typet &type)
subt & get_sub()
Definition: irep.h:245
const irep_idt & id() const
Definition: irep.h:189
const source_locationt & source_location() const
Definition: cpp_name.h:72
const declaratorst & declarators() const
void remove_subtype()
Definition: type.h:84
bitvector_typet float_type()
Definition: c_types.cpp:184
std::list< typet > other
C++ Language Conversion.
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:79
void read(const typet &type)
Base class for tree-like data structures with sharing.
Definition: irep.h:87
#define Forall_irep(it, irep)
Definition: irep.h:66
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:164
bitvector_typet long_double_type()
Definition: c_types.cpp:222
const source_locationt & source_location() const
Definition: type.h:95
irep_idt get_base_name() const
Definition: cpp_name.cpp:17
void read_function_type(const typet &type)
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:36
C++ Language Type Checking.
void read_template(const typet &type)
bitvector_typet wchar_t_type()
Definition: c_types.cpp:148
cpp_declarationt & to_cpp_declaration(irept &irep)
API to type classes.
unsignedbv_typet gcc_unsigned_int128_type()
Definition: c_types.cpp:311
bitvector_typet gcc_float128_type()
Definition: c_types.cpp:260
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:50
Base class for all expressions.
Definition: expr.h:46
void clear()
Definition: irep.h:241
irept & add(const irep_namet &name)
Definition: irep.cpp:306
void cpp_convert_plain_type(typet &type)
void write(typet &type)
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:147
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:100
void read_rec(const typet &type)
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:134
const typet & subtype() const
Definition: type.h:31
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:93
signedbv_typet gcc_signed_int128_type()
Definition: c_types.cpp:318
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:86
bool empty() const
Definition: dstring.h:61
signedbv_typet signed_char_type()
Definition: c_types.cpp:141
bitvector_typet char_type()
Definition: c_types.cpp:113
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214