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/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/invariant.h>
20 #include <util/std_types.h>
21 
22 #include <ansi-c/gcc_types.h>
23 
24 #include "cpp_declaration.h"
25 #include "cpp_name.h"
26 
28 {
29 public:
36 
37  void read(const typet &type);
38  void write(typet &type);
39 
40  std::list<typet> other;
41 
43  explicit cpp_convert_typet(const typet &type) { read(type); }
44 
45 protected:
46  void read_rec(const typet &type);
47  void read_function_type(const typet &type);
48  void read_template(const typet &type);
49 };
50 
51 void cpp_convert_typet::read(const typet &type)
52 {
59 
60  other.clear();
61 
62  #if 0
63  std::cout << "cpp_convert_typet::read: " << type.pretty() << '\n';
64  #endif
65 
66  read_rec(type);
67 }
68 
70 {
71  #if 0
72  std::cout << "cpp_convert_typet::read_rec: "
73  << type.pretty() << '\n';
74  #endif
75 
76  if(type.id()==ID_merged_type)
77  {
78  forall_subtypes(it, type)
79  read_rec(*it);
80  }
81  else if(type.id()==ID_signed)
82  signed_cnt++;
83  else if(type.id()==ID_unsigned)
84  unsigned_cnt++;
85  else if(type.id()==ID_volatile)
86  volatile_cnt++;
87  else if(type.id()==ID_char)
88  char_cnt++;
89  else if(type.id()==ID_int)
90  int_cnt++;
91  else if(type.id()==ID_short)
92  short_cnt++;
93  else if(type.id()==ID_long)
94  long_cnt++;
95  else if(type.id()==ID_double)
96  double_cnt++;
97  else if(type.id()==ID_float)
98  float_cnt++;
99  else if(type.id()==ID_gcc_float80)
100  float80_cnt++;
101  else if(type.id()==ID_gcc_float128)
102  float128_cnt++;
103  else if(type.id()==ID_gcc_int128)
104  int128_cnt++;
105  else if(type.id()==ID_complex)
106  complex_cnt++;
107  else if(type.id()==ID_bool)
108  cpp_bool_cnt++;
109  else if(type.id()==ID_proper_bool)
110  proper_bool_cnt++;
111  else if(type.id()==ID_wchar_t)
112  wchar_t_cnt++;
113  else if(type.id()==ID_char16_t)
114  char16_t_cnt++;
115  else if(type.id()==ID_char32_t)
116  char32_t_cnt++;
117  else if(type.id()==ID_int8)
118  int8_cnt++;
119  else if(type.id()==ID_int16)
120  int16_cnt++;
121  else if(type.id()==ID_int32)
122  int32_cnt++;
123  else if(type.id()==ID_int64)
124  int64_cnt++;
125  else if(type.id()==ID_ptr32)
126  ptr32_cnt++;
127  else if(type.id()==ID_ptr64)
128  ptr64_cnt++;
129  else if(type.id()==ID_const)
130  const_cnt++;
131  else if(type.id()==ID_restrict)
132  restrict_cnt++;
133  else if(type.id()==ID_constexpr)
134  constexpr_cnt++;
135  else if(type.id()==ID_extern)
136  extern_cnt++;
137  else if(type.id()==ID_noreturn)
138  {
139  noreturn_cnt++;
140  }
141  else if(type.id()==ID_function_type)
142  {
143  read_function_type(type);
144  }
145  else if(type.id()==ID_identifier)
146  {
147  // from parameters
148  }
149  else if(type.id()==ID_cpp_name)
150  {
151  // from typedefs
152  other.push_back(type);
153  }
154  else if(type.id()==ID_array)
155  {
156  other.push_back(type);
157  cpp_convert_plain_type(other.back().subtype());
158  }
159  else if(type.id()==ID_template)
160  {
161  read_template(type);
162  }
163  else if(type.id()==ID_void)
164  {
165  // we store 'void' as 'empty'
166  typet tmp=type;
167  tmp.id(ID_empty);
168  other.push_back(tmp);
169  }
170  else if(type.id()==ID_frontend_pointer)
171  {
172  // add width and turn into ID_pointer
175  if(type.get_bool(ID_C_reference))
176  tmp.set(ID_C_reference, true);
177  if(type.get_bool(ID_C_rvalue_reference))
178  tmp.set(ID_C_rvalue_reference, true);
179  other.push_back(tmp);
180  }
181  else if(type.id()==ID_pointer)
182  {
183  // ignore, we unfortunately convert multiple times
184  other.push_back(type);
185  }
186  else
187  {
188  other.push_back(type);
189  }
190 }
191 
193 {
194  other.push_back(type);
195  typet &t=other.back();
196 
198 
199  irept &arguments=t.add(ID_arguments);
200 
201  Forall_irep(it, arguments.get_sub())
202  {
203  exprt &decl=static_cast<exprt &>(*it);
204 
205  // may be type or expression
206  bool is_type=decl.get_bool(ID_is_type);
207 
208  if(is_type)
209  {
210  }
211  else
212  {
214  }
215 
216  // TODO: initializer
217  }
218 }
219 
221 {
222  other.push_back(type);
223  typet &t=other.back();
224  t.id(ID_code);
225 
226  // change subtype to return_type
227  typet &return_type=
228  static_cast<typet &>(t.add(ID_return_type));
229 
230  return_type.swap(t.subtype());
231  t.remove_subtype();
232 
233  if(return_type.is_not_nil())
234  cpp_convert_plain_type(return_type);
235 
236  // take care of parameter types
237  irept &parameters=t.add(ID_parameters);
238 
239  // see if we have an ellipsis
240  if(!parameters.get_sub().empty() &&
241  parameters.get_sub().back().id()==ID_ellipsis)
242  {
243  parameters.set(ID_ellipsis, true);
244  parameters.get_sub().erase(--parameters.get_sub().end());
245  }
246 
247  Forall_irep(it, parameters.get_sub())
248  {
249  exprt &parameter_expr=static_cast<exprt &>(*it);
250 
251  if(parameter_expr.id()==ID_cpp_declaration)
252  {
253  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
254  source_locationt type_location=declaration.type().source_location();
255 
256  cpp_convert_plain_type(declaration.type());
257 
258  // there should be only one declarator
259  assert(declaration.declarators().size()==1);
260 
261  cpp_declaratort &declarator=
262  declaration.declarators().front();
263 
264  // do we have a declarator?
265  if(declarator.is_nil())
266  {
267  parameter_expr=exprt(ID_parameter, declaration.type());
268  parameter_expr.add_source_location()=type_location;
269  }
270  else
271  {
272  const cpp_namet &cpp_name=declarator.name();
273  typet final_type=declarator.merge_type(declaration.type());
274 
275  // see if it's an array type
276  if(final_type.id()==ID_array)
277  {
278  // turn into pointer type
279  final_type=pointer_type(final_type.subtype());
280  }
281 
282  code_typet::parametert new_parameter(final_type);
283 
284  if(cpp_name.is_nil())
285  {
286  new_parameter.add_source_location()=type_location;
287  }
288  else if(cpp_name.is_simple_name())
289  {
290  irep_idt base_name=cpp_name.get_base_name();
291  assert(!base_name.empty());
292  new_parameter.set_identifier(base_name);
293  new_parameter.set_base_name(base_name);
294  new_parameter.add_source_location()=cpp_name.source_location();
295  }
296  else
297  {
298  throw "expected simple name as parameter";
299  }
300 
301  if(declarator.value().is_not_nil())
302  new_parameter.default_value().swap(declarator.value());
303 
304  parameter_expr.swap(new_parameter);
305  }
306  }
307  else if(parameter_expr.id()==ID_ellipsis)
308  {
309  throw "ellipsis only allowed as last parameter";
310  }
311  else
312  UNREACHABLE;
313  }
314 
315  // if we just have one parameter of type void, remove it
316  if(parameters.get_sub().size()==1 &&
317  parameters.get_sub().front().find(ID_type).id()==ID_empty)
318  parameters.get_sub().clear();
319 }
320 
322 {
323  type.clear();
324 
325  // first, do "other"
326 
327  if(!other.empty())
328  {
329  if(double_cnt || float_cnt || signed_cnt ||
333  int8_cnt || int16_cnt || int32_cnt ||
335  throw "type modifier not applicable";
336 
337  if(other.size()!=1)
338  throw "illegal combination of types";
339 
340  type.swap(other.front());
341  }
342  else if(double_cnt)
343  {
344  if(signed_cnt || unsigned_cnt || int_cnt ||
348  float_cnt ||
349  int8_cnt || int16_cnt || int32_cnt ||
350  int64_cnt || ptr32_cnt || ptr64_cnt ||
352  throw "illegal type modifier for double";
353 
354  if(long_cnt)
355  type=long_double_type();
356  else
357  type=double_type();
358  }
359  else if(float_cnt)
360  {
361  if(signed_cnt || unsigned_cnt || int_cnt ||
365  int8_cnt || int16_cnt || int32_cnt ||
366  int64_cnt || ptr32_cnt || ptr64_cnt ||
368  throw "illegal type modifier for float";
369 
370  if(long_cnt)
371  throw "float can't be long";
372 
373  type=float_type();
374  }
375  else if(float80_cnt)
376  {
377  if(signed_cnt || unsigned_cnt || int_cnt ||
381  int8_cnt || int16_cnt || int32_cnt ||
383  float128_cnt)
384  throw "illegal type modifier for __float80";
385 
386  if(long_cnt)
387  throw "__float80 can't be long";
388 
389  // this isn't the same as long double
390  type=gcc_float64x_type();
391  }
392  else if(float128_cnt)
393  {
394  if(signed_cnt || unsigned_cnt || int_cnt ||
398  int8_cnt || int16_cnt || int32_cnt ||
400  throw "illegal type modifier for __float128";
401 
402  if(long_cnt)
403  throw "__float128 can't be long";
404 
405  // this isn't the same as long double
406  type=gcc_float128_type();
407  }
408  else if(cpp_bool_cnt)
409  {
413  int8_cnt || int16_cnt || int32_cnt ||
415  throw "illegal type modifier for C++ bool";
416 
417  type.id(ID_bool);
418  }
419  else if(proper_bool_cnt)
420  {
422  char_cnt || wchar_t_cnt ||
424  int8_cnt || int16_cnt || int32_cnt ||
426  throw "illegal type modifier for __CPROVER_bool";
427 
428  type.id(ID_bool);
429  }
430  else if(char_cnt)
431  {
432  if(int_cnt || short_cnt || wchar_t_cnt || long_cnt ||
434  int8_cnt || int16_cnt || int32_cnt ||
436  throw "illegal type modifier for char";
437 
438  // there are really three distinct char types in C++
439  if(unsigned_cnt)
440  type=unsigned_char_type();
441  else if(signed_cnt)
442  type=signed_char_type();
443  else
444  type=char_type();
445  }
446  else if(wchar_t_cnt)
447  {
448  // This is a distinct type, and can't be made signed/unsigned.
449  // This is tolerated by most compilers, however.
450 
451  if(int_cnt || short_cnt || char_cnt || long_cnt ||
453  int8_cnt || int16_cnt || int32_cnt ||
455  throw "illegal type modifier for wchar_t";
456 
457  type=wchar_t_type();
458  }
459  else if(char16_t_cnt)
460  {
461  // This is a distinct type, and can't be made signed/unsigned.
462  if(int_cnt || short_cnt || char_cnt || long_cnt ||
463  char32_t_cnt ||
464  int8_cnt || int16_cnt || int32_cnt ||
465  int64_cnt || ptr32_cnt || ptr64_cnt ||
467  throw "illegal type modifier for char16_t";
468 
469  type=char16_t_type();
470  }
471  else if(char32_t_cnt)
472  {
473  // This is a distinct type, and can't be made signed/unsigned.
474  if(int_cnt || short_cnt || char_cnt || long_cnt ||
475  int8_cnt || int16_cnt || int32_cnt ||
476  int64_cnt || ptr32_cnt || ptr64_cnt ||
478  throw "illegal type modifier for char32_t";
479 
480  type=char32_t_type();
481  }
482  else
483  {
484  // it must be integer -- signed or unsigned?
485 
486  if(signed_cnt && unsigned_cnt)
487  throw "integer cannot be both signed and unsigned";
488 
489  if(short_cnt)
490  {
491  if(long_cnt)
492  throw "cannot combine short and long";
493 
494  if(unsigned_cnt)
496  else
497  type=signed_short_int_type();
498  }
499  else if(int8_cnt)
500  {
501  if(long_cnt)
502  throw "illegal type modifier for __int8";
503 
504  // in terms of overloading, this behaves like "char"
505  if(unsigned_cnt)
506  type=unsigned_char_type();
507  else if(signed_cnt)
508  type=signed_char_type();
509  else
510  type=char_type(); // check?
511  }
512  else if(int16_cnt)
513  {
514  if(long_cnt)
515  throw "illegal type modifier for __int16";
516 
517  // in terms of overloading, this behaves like "short"
518  if(unsigned_cnt)
520  else
521  type=signed_short_int_type();
522  }
523  else if(int32_cnt)
524  {
525  if(long_cnt)
526  throw "illegal type modifier for __int32";
527 
528  // in terms of overloading, this behaves like "int"
529  if(unsigned_cnt)
530  type=unsigned_int_type();
531  else
532  type=signed_int_type();
533  }
534  else if(int64_cnt)
535  {
536  if(long_cnt)
537  throw "illegal type modifier for __int64";
538 
539  // in terms of overloading, this behaves like "long long"
540  if(unsigned_cnt)
542  else
544  }
545  else if(int128_cnt)
546  {
547  if(long_cnt)
548  throw "illegal type modifier for __int128";
549 
550  if(unsigned_cnt)
552  else
553  type=gcc_signed_int128_type();
554  }
555  else if(long_cnt==0)
556  {
557  if(unsigned_cnt)
558  type=unsigned_int_type();
559  else
560  type=signed_int_type();
561  }
562  else if(long_cnt==1)
563  {
564  if(unsigned_cnt)
565  type=unsigned_long_int_type();
566  else
567  type=signed_long_int_type();
568  }
569  else if(long_cnt==2)
570  {
571  if(unsigned_cnt)
573  else
575  }
576  else
577  throw "illegal combination of type modifiers";
578  }
579 
580  // is it constant?
581  if(const_cnt || constexpr_cnt)
582  type.set(ID_C_constant, true);
583 
584  // is it volatile?
585  if(volatile_cnt)
586  type.set(ID_C_volatile, true);
587 }
588 
590 {
591  if(type.id()==ID_cpp_name ||
592  type.id()==ID_struct ||
593  type.id()==ID_union ||
594  type.id()==ID_array ||
595  type.id()==ID_code ||
596  type.id()==ID_unsignedbv ||
597  type.id()==ID_signedbv ||
598  type.id()==ID_bool ||
599  type.id()==ID_floatbv ||
600  type.id()==ID_empty ||
601  type.id()==ID_symbol ||
602  type.id()==ID_constructor ||
603  type.id()==ID_destructor)
604  {
605  }
606  else if(type.id()==ID_c_enum)
607  {
608  // add width -- we use int, but the standard
609  // doesn't guarantee that
610  type.set(ID_width, config.ansi_c.int_width);
611  }
612  else
613  {
614  cpp_convert_typet cpp_convert_type(type);
615  cpp_convert_type.write(type);
616  }
617 }
618 
619 void cpp_convert_auto(typet &dest, const typet &src)
620 {
621  if(dest.id() != ID_merged_type && dest.has_subtype())
622  {
623  cpp_convert_auto(dest.subtype(), src);
624  return;
625  }
626 
627  cpp_convert_typet cpp_convert_type(dest);
628  for(auto &t : cpp_convert_type.other)
629  if(t.id() == ID_auto)
630  t = src;
631 
632  cpp_convert_type.write(dest);
633 }
bitvector_typet gcc_float128_type()
Definition: gcc_types.cpp:58
The type of an expression.
Definition: type.h:22
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
#define forall_subtypes(it, type)
Definition: type.h:161
struct configt::ansi_ct ansi_c
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool has_subtype() const
Definition: type.h:79
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
bitvector_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
bitvector_typet double_type()
Definition: c_types.cpp:193
typet & type()
Definition: expr.h:56
bool is_simple_name() const
Definition: cpp_name.h:89
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:23
cpp_convert_typet(const typet &type)
subt & get_sub()
Definition: irep.h:317
void set_base_name(const irep_idt &name)
Definition: std_types.h:835
const irep_idt & id() const
Definition: irep.h:259
const source_locationt & source_location() const
Definition: cpp_name.h:73
const declaratorst & declarators() const
void remove_subtype()
Definition: type.h:86
bitvector_typet float_type()
Definition: c_types.cpp:185
void cpp_convert_auto(typet &dest, const typet &src)
The pointer type.
Definition: std_types.h:1435
std::list< typet > other
C++ Language Conversion.
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
void read(const typet &type)
std::size_t int_width
Definition: config.h:30
Base class for tree-like data structures with sharing.
Definition: irep.h:156
#define Forall_irep(it, irep)
Definition: irep.h:66
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::size_t pointer_width
Definition: config.h:36
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
bitvector_typet long_double_type()
Definition: c_types.cpp:201
const source_locationt & source_location() const
Definition: type.h:97
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:37
C++ Language Type Checking.
void read_template(const typet &type)
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
cpp_declarationt & to_cpp_declaration(irept &irep)
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:830
API to type classes.
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
Base class for all expressions.
Definition: expr.h:42
source_locationt & add_source_location()
Definition: type.h:102
#define UNREACHABLE
Definition: invariant.h:271
void clear()
Definition: irep.h:313
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:303
source_locationt & add_source_location()
Definition: expr.h:130
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
void read_rec(const typet &type)
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
const typet & subtype() const
Definition: type.h:33
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
bool empty() const
Definition: dstring.h:73
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
bitvector_typet char_type()
Definition: c_types.cpp:114
const exprt & default_value() const
Definition: std_types.h:812
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286