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_c_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  other.back().id(ID_code);
224 
225  code_typet &t = to_code_type(other.back());
226 
227  // change subtype to return_type
228  typet &return_type = t.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  code_typet::parameterst &parameters = t.parameters();
238 
239  // see if we have an ellipsis
240  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
241  {
242  t.make_ellipsis();
243  parameters.pop_back();
244  }
245 
246  for(auto &parameter_expr : parameters)
247  {
248  if(parameter_expr.id()==ID_cpp_declaration)
249  {
250  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
251  source_locationt type_location=declaration.type().source_location();
252 
253  cpp_convert_plain_type(declaration.type());
254 
255  // there should be only one declarator
256  assert(declaration.declarators().size()==1);
257 
258  cpp_declaratort &declarator=
259  declaration.declarators().front();
260 
261  // do we have a declarator?
262  if(declarator.is_nil())
263  {
264  parameter_expr = code_typet::parametert(declaration.type());
265  parameter_expr.add_source_location()=type_location;
266  }
267  else
268  {
269  const cpp_namet &cpp_name=declarator.name();
270  typet final_type=declarator.merge_type(declaration.type());
271 
272  // see if it's an array type
273  if(final_type.id()==ID_array)
274  {
275  // turn into pointer type
276  final_type=pointer_type(final_type.subtype());
277  }
278 
279  code_typet::parametert new_parameter(final_type);
280 
281  if(cpp_name.is_nil())
282  {
283  new_parameter.add_source_location()=type_location;
284  }
285  else if(cpp_name.is_simple_name())
286  {
287  irep_idt base_name=cpp_name.get_base_name();
288  assert(!base_name.empty());
289  new_parameter.set_identifier(base_name);
290  new_parameter.set_base_name(base_name);
291  new_parameter.add_source_location()=cpp_name.source_location();
292  }
293  else
294  {
295  throw "expected simple name as parameter";
296  }
297 
298  if(declarator.value().is_not_nil())
299  new_parameter.default_value().swap(declarator.value());
300 
301  parameter_expr.swap(new_parameter);
302  }
303  }
304  else if(parameter_expr.id()==ID_ellipsis)
305  {
306  throw "ellipsis only allowed as last parameter";
307  }
308  else
309  UNREACHABLE;
310  }
311 
312  // if we just have one parameter of type void, remove it
313  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
314  parameters.clear();
315 }
316 
318 {
319  type.clear();
320 
321  // first, do "other"
322 
323  if(!other.empty())
324  {
325  if(double_cnt || float_cnt || signed_cnt ||
329  int8_cnt || int16_cnt || int32_cnt ||
331  throw "type modifier not applicable";
332 
333  if(other.size()!=1)
334  throw "illegal combination of types";
335 
336  type.swap(other.front());
337  }
338  else if(double_cnt)
339  {
340  if(signed_cnt || unsigned_cnt || int_cnt ||
344  float_cnt ||
345  int8_cnt || int16_cnt || int32_cnt ||
346  int64_cnt || ptr32_cnt || ptr64_cnt ||
348  throw "illegal type modifier for double";
349 
350  if(long_cnt)
351  type=long_double_type();
352  else
353  type=double_type();
354  }
355  else if(float_cnt)
356  {
357  if(signed_cnt || unsigned_cnt || int_cnt ||
361  int8_cnt || int16_cnt || int32_cnt ||
362  int64_cnt || ptr32_cnt || ptr64_cnt ||
364  throw "illegal type modifier for float";
365 
366  if(long_cnt)
367  throw "float can't be long";
368 
369  type=float_type();
370  }
371  else if(float80_cnt)
372  {
373  if(signed_cnt || unsigned_cnt || int_cnt ||
377  int8_cnt || int16_cnt || int32_cnt ||
379  float128_cnt)
380  throw "illegal type modifier for __float80";
381 
382  if(long_cnt)
383  throw "__float80 can't be long";
384 
385  // this isn't the same as long double
386  type=gcc_float64x_type();
387  }
388  else if(float128_cnt)
389  {
390  if(signed_cnt || unsigned_cnt || int_cnt ||
394  int8_cnt || int16_cnt || int32_cnt ||
396  throw "illegal type modifier for __float128";
397 
398  if(long_cnt)
399  throw "__float128 can't be long";
400 
401  // this isn't the same as long double
402  type=gcc_float128_type();
403  }
404  else if(cpp_bool_cnt)
405  {
409  int8_cnt || int16_cnt || int32_cnt ||
411  throw "illegal type modifier for C++ bool";
412 
413  type = c_bool_type();
414  }
415  else if(proper_bool_cnt)
416  {
418  char_cnt || wchar_t_cnt ||
420  int8_cnt || int16_cnt || int32_cnt ||
422  throw "illegal type modifier for " CPROVER_PREFIX "bool";
423 
424  type.id(ID_bool);
425  }
426  else if(char_cnt)
427  {
428  if(int_cnt || short_cnt || wchar_t_cnt || long_cnt ||
430  int8_cnt || int16_cnt || int32_cnt ||
432  throw "illegal type modifier for char";
433 
434  // there are really three distinct char types in C++
435  if(unsigned_cnt)
436  type=unsigned_char_type();
437  else if(signed_cnt)
438  type=signed_char_type();
439  else
440  type=char_type();
441  }
442  else if(wchar_t_cnt)
443  {
444  // This is a distinct type, and can't be made signed/unsigned.
445  // This is tolerated by most compilers, however.
446 
447  if(int_cnt || short_cnt || char_cnt || long_cnt ||
449  int8_cnt || int16_cnt || int32_cnt ||
451  throw "illegal type modifier for wchar_t";
452 
453  type=wchar_t_type();
454  }
455  else if(char16_t_cnt)
456  {
457  // This is a distinct type, and can't be made signed/unsigned.
458  if(int_cnt || short_cnt || char_cnt || long_cnt ||
459  char32_t_cnt ||
460  int8_cnt || int16_cnt || int32_cnt ||
461  int64_cnt || ptr32_cnt || ptr64_cnt ||
463  throw "illegal type modifier for char16_t";
464 
465  type=char16_t_type();
466  }
467  else if(char32_t_cnt)
468  {
469  // This is a distinct type, and can't be made signed/unsigned.
470  if(int_cnt || short_cnt || char_cnt || long_cnt ||
471  int8_cnt || int16_cnt || int32_cnt ||
472  int64_cnt || ptr32_cnt || ptr64_cnt ||
474  throw "illegal type modifier for char32_t";
475 
476  type=char32_t_type();
477  }
478  else
479  {
480  // it must be integer -- signed or unsigned?
481 
482  if(signed_cnt && unsigned_cnt)
483  throw "integer cannot be both signed and unsigned";
484 
485  if(short_cnt)
486  {
487  if(long_cnt)
488  throw "cannot combine short and long";
489 
490  if(unsigned_cnt)
492  else
493  type=signed_short_int_type();
494  }
495  else if(int8_cnt)
496  {
497  if(long_cnt)
498  throw "illegal type modifier for __int8";
499 
500  // in terms of overloading, this behaves like "char"
501  if(unsigned_cnt)
502  type=unsigned_char_type();
503  else if(signed_cnt)
504  type=signed_char_type();
505  else
506  type=char_type(); // check?
507  }
508  else if(int16_cnt)
509  {
510  if(long_cnt)
511  throw "illegal type modifier for __int16";
512 
513  // in terms of overloading, this behaves like "short"
514  if(unsigned_cnt)
516  else
517  type=signed_short_int_type();
518  }
519  else if(int32_cnt)
520  {
521  if(long_cnt)
522  throw "illegal type modifier for __int32";
523 
524  // in terms of overloading, this behaves like "int"
525  if(unsigned_cnt)
526  type=unsigned_int_type();
527  else
528  type=signed_int_type();
529  }
530  else if(int64_cnt)
531  {
532  if(long_cnt)
533  throw "illegal type modifier for __int64";
534 
535  // in terms of overloading, this behaves like "long long"
536  if(unsigned_cnt)
538  else
540  }
541  else if(int128_cnt)
542  {
543  if(long_cnt)
544  throw "illegal type modifier for __int128";
545 
546  if(unsigned_cnt)
548  else
549  type=gcc_signed_int128_type();
550  }
551  else if(long_cnt==0)
552  {
553  if(unsigned_cnt)
554  type=unsigned_int_type();
555  else
556  type=signed_int_type();
557  }
558  else if(long_cnt==1)
559  {
560  if(unsigned_cnt)
561  type=unsigned_long_int_type();
562  else
563  type=signed_long_int_type();
564  }
565  else if(long_cnt==2)
566  {
567  if(unsigned_cnt)
569  else
571  }
572  else
573  throw "illegal combination of type modifiers";
574  }
575 
576  // is it constant?
577  if(const_cnt || constexpr_cnt)
578  type.set(ID_C_constant, true);
579 
580  // is it volatile?
581  if(volatile_cnt)
582  type.set(ID_C_volatile, true);
583 }
584 
586 {
587  if(
588  type.id() == ID_cpp_name || type.id() == ID_struct ||
589  type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
590  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
591  type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
592  type.id() == ID_symbol_type || type.id() == ID_constructor ||
593  type.id() == ID_destructor)
594  {
595  }
596  else if(type.id()==ID_c_enum)
597  {
598  // add width -- we use int, but the standard
599  // doesn't guarantee that
600  type.set(ID_width, config.ansi_c.int_width);
601  }
602  else if(type.id() == ID_c_bool)
603  {
604  type.set(ID_width, config.ansi_c.bool_width);
605  }
606  else
607  {
608  cpp_convert_typet cpp_convert_type(type);
609  cpp_convert_type.write(type);
610  }
611 }
612 
613 void cpp_convert_auto(typet &dest, const typet &src)
614 {
615  if(dest.id() != ID_merged_type && dest.has_subtype())
616  {
617  cpp_convert_auto(dest.subtype(), src);
618  return;
619  }
620 
621  cpp_convert_typet cpp_convert_type(dest);
622  for(auto &t : cpp_convert_type.other)
623  if(t.id() == ID_auto)
624  t = src;
625 
626  cpp_convert_type.write(dest);
627 }
The type of an expression, extends irept.
Definition: type.h:27
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
#define forall_subtypes(it, type)
Definition: type.h:216
struct configt::ansi_ct ansi_c
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
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:640
#define CPROVER_PREFIX
bool has_subtype() const
Definition: type.h:56
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
std::vector< parametert > parameterst
Definition: std_types.h:754
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
typet & type()
Return the type of the expression.
Definition: expr.h:68
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:239
configt config
Definition: config.cpp:24
cpp_convert_typet(const typet &type)
void set_base_name(const irep_idt &name)
Definition: std_types.h:823
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:59
void cpp_convert_auto(typet &dest, const typet &src)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
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:35
std::size_t pointer_width
Definition: config.h:36
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
void make_ellipsis()
Definition: std_types.h:873
const source_locationt & source_location() const
Definition: type.h:62
irep_idt get_base_name() const
Definition: cpp_name.cpp:17
void read_function_type(const typet &type)
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
C++ Language Type Checking.
floatbv_typet long_double_type()
Definition: c_types.cpp:201
floatbv_typet float_type()
Definition: c_types.cpp:185
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:818
Pre-defined types.
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
Base class for all expressions.
Definition: expr.h:54
floatbv_typet double_type()
Definition: c_types.cpp:193
const parameterst & parameters() const
Definition: std_types.h:893
source_locationt & add_source_location()
Definition: type.h:67
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
void clear()
Definition: irep.h:313
irept & add(const irep_namet &name)
Definition: irep.cpp:305
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:233
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
void read_rec(const typet &type)
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
std::size_t bool_width
Definition: config.h:32
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:38
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
typet c_bool_type()
Definition: c_types.cpp:108
bool empty() const
Definition: dstring.h:75
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
bitvector_typet char_type()
Definition: c_types.cpp:114
const typet & return_type() const
Definition: std_types.h:883
const exprt & default_value() const
Definition: std_types.h:800
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286