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_float128)
100  float128_cnt++;
101  else if(type.id()==ID_gcc_int128)
102  int128_cnt++;
103  else if(type.id()==ID_complex)
104  complex_cnt++;
105  else if(type.id()==ID_bool)
106  cpp_bool_cnt++;
107  else if(type.id()==ID_proper_bool)
108  proper_bool_cnt++;
109  else if(type.id()==ID_wchar_t)
110  wchar_t_cnt++;
111  else if(type.id()==ID_char16_t)
112  char16_t_cnt++;
113  else if(type.id()==ID_char32_t)
114  char32_t_cnt++;
115  else if(type.id()==ID_int8)
116  int8_cnt++;
117  else if(type.id()==ID_int16)
118  int16_cnt++;
119  else if(type.id()==ID_int32)
120  int32_cnt++;
121  else if(type.id()==ID_int64)
122  int64_cnt++;
123  else if(type.id()==ID_ptr32)
124  ptr32_cnt++;
125  else if(type.id()==ID_ptr64)
126  ptr64_cnt++;
127  else if(type.id()==ID_const)
128  const_cnt++;
129  else if(type.id()==ID_restrict)
130  restrict_cnt++;
131  else if(type.id()==ID_constexpr)
132  constexpr_cnt++;
133  else if(type.id()==ID_extern)
134  extern_cnt++;
135  else if(type.id()==ID_noreturn)
136  {
137  noreturn_cnt++;
138  }
139  else if(type.id()==ID_function_type)
140  {
141  read_function_type(type);
142  }
143  else if(type.id()==ID_identifier)
144  {
145  // from parameters
146  }
147  else if(type.id()==ID_cpp_name)
148  {
149  // from typedefs
150  other.push_back(type);
151  }
152  else if(type.id()==ID_array)
153  {
154  other.push_back(type);
155  cpp_convert_plain_type(other.back().subtype());
156  }
157  else if(type.id()==ID_template)
158  {
159  read_template(type);
160  }
161  else if(type.id()==ID_void)
162  {
163  // we store 'void' as 'empty'
164  typet tmp=type;
165  tmp.id(ID_empty);
166  other.push_back(tmp);
167  }
168  else if(type.id()==ID_frontend_pointer)
169  {
170  // add width and turn into ID_pointer
173  if(type.get_bool(ID_C_reference))
174  tmp.set(ID_C_reference, true);
175  if(type.get_bool(ID_C_rvalue_reference))
176  tmp.set(ID_C_rvalue_reference, true);
177  other.push_back(tmp);
178  }
179  else if(type.id()==ID_pointer)
180  {
181  // ignore, we unfortunately convert multiple times
182  other.push_back(type);
183  }
184  else
185  {
186  other.push_back(type);
187  }
188 }
189 
191 {
192  other.push_back(type);
193  typet &t=other.back();
194 
196 
197  irept &arguments=t.add(ID_arguments);
198 
199  Forall_irep(it, arguments.get_sub())
200  {
201  exprt &decl=static_cast<exprt &>(*it);
202 
203  // may be type or expression
204  bool is_type=decl.get_bool(ID_is_type);
205 
206  if(is_type)
207  {
208  }
209  else
210  {
212  }
213 
214  // TODO: initializer
215  }
216 }
217 
219 {
220  other.push_back(type);
221  typet &t=other.back();
222  t.id(ID_code);
223 
224  // change subtype to return_type
225  typet &return_type=
226  static_cast<typet &>(t.add(ID_return_type));
227 
228  return_type.swap(t.subtype());
229  t.remove_subtype();
230 
231  if(return_type.is_not_nil())
232  cpp_convert_plain_type(return_type);
233 
234  // take care of parameter types
235  irept &parameters=t.add(ID_parameters);
236 
237  // see if we have an ellipsis
238  if(!parameters.get_sub().empty() &&
239  parameters.get_sub().back().id()==ID_ellipsis)
240  {
241  parameters.set(ID_ellipsis, true);
242  parameters.get_sub().erase(--parameters.get_sub().end());
243  }
244 
245  Forall_irep(it, parameters.get_sub())
246  {
247  exprt &parameter_expr=static_cast<exprt &>(*it);
248 
249  if(parameter_expr.id()==ID_cpp_declaration)
250  {
251  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
252  source_locationt type_location=declaration.type().source_location();
253 
254  cpp_convert_plain_type(declaration.type());
255 
256  // there should be only one declarator
257  assert(declaration.declarators().size()==1);
258 
259  cpp_declaratort &declarator=
260  declaration.declarators().front();
261 
262  // do we have a declarator?
263  if(declarator.is_nil())
264  {
265  parameter_expr=exprt(ID_parameter, declaration.type());
266  parameter_expr.add_source_location()=type_location;
267  }
268  else
269  {
270  const cpp_namet &cpp_name=declarator.name();
271  typet final_type=declarator.merge_type(declaration.type());
272 
273  // see if it's an array type
274  if(final_type.id()==ID_array)
275  {
276  // turn into pointer type
277  final_type=pointer_type(final_type.subtype());
278  }
279 
280  code_typet::parametert new_parameter(final_type);
281 
282  if(cpp_name.is_nil())
283  {
284  new_parameter.add_source_location()=type_location;
285  }
286  else if(cpp_name.is_simple_name())
287  {
288  irep_idt base_name=cpp_name.get_base_name();
289  assert(!base_name.empty());
290  new_parameter.set_identifier(base_name);
291  new_parameter.set_base_name(base_name);
292  new_parameter.add_source_location()=cpp_name.source_location();
293  }
294  else
295  {
296  throw "expected simple name as parameter";
297  }
298 
299  if(declarator.value().is_not_nil())
300  new_parameter.default_value().swap(declarator.value());
301 
302  parameter_expr.swap(new_parameter);
303  }
304  }
305  else if(parameter_expr.id()==ID_ellipsis)
306  {
307  throw "ellipsis only allowed as last parameter";
308  }
309  else
310  UNREACHABLE;
311  }
312 
313  // if we just have one parameter of type void, remove it
314  if(parameters.get_sub().size()==1 &&
315  parameters.get_sub().front().find(ID_type).id()==ID_empty)
316  parameters.get_sub().clear();
317 }
318 
320 {
321  type.clear();
322 
323  // first, do "other"
324 
325  if(!other.empty())
326  {
327  if(double_cnt || float_cnt || signed_cnt ||
331  int8_cnt || int16_cnt || int32_cnt ||
333  throw "type modifier not applicable";
334 
335  if(other.size()!=1)
336  throw "illegal combination of types";
337 
338  type.swap(other.front());
339  }
340  else if(double_cnt)
341  {
342  if(signed_cnt || unsigned_cnt || int_cnt ||
346  float_cnt ||
347  int8_cnt || int16_cnt || int32_cnt ||
348  int64_cnt || ptr32_cnt || ptr64_cnt ||
350  throw "illegal type modifier for double";
351 
352  if(long_cnt)
353  type=long_double_type();
354  else
355  type=double_type();
356  }
357  else if(float_cnt)
358  {
359  if(signed_cnt || unsigned_cnt || int_cnt ||
363  int8_cnt || int16_cnt || int32_cnt ||
365  throw "illegal type modifier for float";
366 
367  if(long_cnt)
368  throw "float can't be long";
369 
370  type=float_type();
371  }
372  else if(float128_cnt)
373  {
374  if(signed_cnt || unsigned_cnt || int_cnt ||
378  int8_cnt || int16_cnt || int32_cnt ||
380  throw "illegal type modifier for __float128";
381 
382  if(long_cnt)
383  throw "__float128 can't be long";
384 
385  // this isn't the same as long double
386  type=gcc_float128_type();
387  }
388  else if(cpp_bool_cnt)
389  {
393  int8_cnt || int16_cnt || int32_cnt ||
395  throw "illegal type modifier for C++ bool";
396 
397  type.id(ID_bool);
398  }
399  else if(proper_bool_cnt)
400  {
402  char_cnt || wchar_t_cnt ||
404  int8_cnt || int16_cnt || int32_cnt ||
406  throw "illegal type modifier for __CPROVER_bool";
407 
408  type.id(ID_bool);
409  }
410  else if(char_cnt)
411  {
412  if(int_cnt || short_cnt || wchar_t_cnt || long_cnt ||
414  int8_cnt || int16_cnt || int32_cnt ||
416  throw "illegal type modifier for char";
417 
418  // there are really three distinct char types in C++
419  if(unsigned_cnt)
420  type=unsigned_char_type();
421  else if(signed_cnt)
422  type=signed_char_type();
423  else
424  type=char_type();
425  }
426  else if(wchar_t_cnt)
427  {
428  // This is a distinct type, and can't be made signed/unsigned.
429  // This is tolerated by most compilers, however.
430 
431  if(int_cnt || short_cnt || char_cnt || long_cnt ||
433  int8_cnt || int16_cnt || int32_cnt ||
435  throw "illegal type modifier for wchar_t";
436 
437  type=wchar_t_type();
438  }
439  else if(char16_t_cnt)
440  {
441  // This is a distinct type, and can't be made signed/unsigned.
442  if(int_cnt || short_cnt || char_cnt || long_cnt ||
443  char32_t_cnt ||
444  int8_cnt || int16_cnt || int32_cnt ||
445  int64_cnt || ptr32_cnt || ptr64_cnt ||
447  throw "illegal type modifier for char16_t";
448 
449  type=char16_t_type();
450  }
451  else if(char32_t_cnt)
452  {
453  // This is a distinct type, and can't be made signed/unsigned.
454  if(int_cnt || short_cnt || char_cnt || long_cnt ||
455  int8_cnt || int16_cnt || int32_cnt ||
456  int64_cnt || ptr32_cnt || ptr64_cnt ||
458  throw "illegal type modifier for char32_t";
459 
460  type=char32_t_type();
461  }
462  else
463  {
464  // it must be integer -- signed or unsigned?
465 
466  if(signed_cnt && unsigned_cnt)
467  throw "integer cannot be both signed and unsigned";
468 
469  if(short_cnt)
470  {
471  if(long_cnt)
472  throw "cannot combine short and long";
473 
474  if(unsigned_cnt)
476  else
477  type=signed_short_int_type();
478  }
479  else if(int8_cnt)
480  {
481  if(long_cnt)
482  throw "illegal type modifier for __int8";
483 
484  // in terms of overloading, this behaves like "char"
485  if(unsigned_cnt)
486  type=unsigned_char_type();
487  else if(signed_cnt)
488  type=signed_char_type();
489  else
490  type=char_type(); // check?
491  }
492  else if(int16_cnt)
493  {
494  if(long_cnt)
495  throw "illegal type modifier for __int16";
496 
497  // in terms of overloading, this behaves like "short"
498  if(unsigned_cnt)
500  else
501  type=signed_short_int_type();
502  }
503  else if(int32_cnt)
504  {
505  if(long_cnt)
506  throw "illegal type modifier for __int32";
507 
508  // in terms of overloading, this behaves like "int"
509  if(unsigned_cnt)
510  type=unsigned_int_type();
511  else
512  type=signed_int_type();
513  }
514  else if(int64_cnt)
515  {
516  if(long_cnt)
517  throw "illegal type modifier for __int64";
518 
519  // in terms of overloading, this behaves like "long long"
520  if(unsigned_cnt)
522  else
524  }
525  else if(int128_cnt)
526  {
527  if(long_cnt)
528  throw "illegal type modifier for __int128";
529 
530  if(unsigned_cnt)
532  else
533  type=gcc_signed_int128_type();
534  }
535  else if(long_cnt==0)
536  {
537  if(unsigned_cnt)
538  type=unsigned_int_type();
539  else
540  type=signed_int_type();
541  }
542  else if(long_cnt==1)
543  {
544  if(unsigned_cnt)
545  type=unsigned_long_int_type();
546  else
547  type=signed_long_int_type();
548  }
549  else if(long_cnt==2)
550  {
551  if(unsigned_cnt)
553  else
555  }
556  else
557  throw "illegal combination of type modifiers";
558  }
559 
560  // is it constant?
561  if(const_cnt || constexpr_cnt)
562  type.set(ID_C_constant, true);
563 
564  // is it volatile?
565  if(volatile_cnt)
566  type.set(ID_C_volatile, true);
567 }
568 
570 {
571  if(type.id()==ID_cpp_name ||
572  type.id()==ID_struct ||
573  type.id()==ID_union ||
574  type.id()==ID_array ||
575  type.id()==ID_code ||
576  type.id()==ID_unsignedbv ||
577  type.id()==ID_signedbv ||
578  type.id()==ID_bool ||
579  type.id()==ID_floatbv ||
580  type.id()==ID_empty ||
581  type.id()==ID_symbol ||
582  type.id()==ID_constructor ||
583  type.id()==ID_destructor)
584  {
585  }
586  else if(type.id()==ID_c_enum)
587  {
588  // add width -- we use int, but the standard
589  // doesn't guarantee that
590  type.set(ID_width, config.ansi_c.int_width);
591  }
592  else
593  {
594  cpp_convert_typet cpp_convert_type(type);
595  cpp_convert_type.write(type);
596  }
597 }
598 
599 void cpp_convert_auto(typet &dest, const typet &src)
600 {
601  if(dest.id() != ID_merged_type && dest.has_subtype())
602  {
603  cpp_convert_auto(dest.subtype(), src);
604  return;
605  }
606 
607  cpp_convert_typet cpp_convert_type(dest);
608  for(auto &t : cpp_convert_type.other)
609  if(t.id() == ID_auto)
610  t = src;
611 
612  cpp_convert_type.write(dest);
613 }
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:102
bool is_not_nil() const
Definition: irep.h:103
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
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:245
void set_base_name(const irep_idt &name)
Definition: std_types.h:835
const irep_idt & id() const
Definition: irep.h:189
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:1426
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:86
#define Forall_irep(it, irep)
Definition: irep.h:65
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:250
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: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:61
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:214