cprover
ansi_c_convert_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SpecC Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ansi_c_convert_type.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/config.h>
17 #include <util/namespace.h>
18 #include <util/simplify_expr.h>
19 #include <util/std_types.h>
20 #include <util/string_constant.h>
21 
22 #include "gcc_types.h"
23 
25 {
26  clear();
28  read_rec(type);
29 }
30 
32 {
33  if(type.id()==ID_merged_type)
34  {
35  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
36  read_rec(subtype);
37  }
38  else if(type.id()==ID_signed)
39  signed_cnt++;
40  else if(type.id()==ID_unsigned)
41  unsigned_cnt++;
42  else if(type.id()==ID_ptr32)
44  else if(type.id()==ID_ptr64)
46  else if(type.id()==ID_volatile)
48  else if(type.id()==ID_asm)
49  {
50  if(type.has_subtype() &&
51  type.subtype().id()==ID_string_constant)
53  }
54  else if(type.id()==ID_section &&
55  type.has_subtype() &&
56  type.subtype().id()==ID_string_constant)
57  {
59  }
60  else if(type.id()==ID_const)
62  else if(type.id()==ID_restrict)
64  else if(type.id()==ID_atomic)
66  else if(type.id()==ID_atomic_type_specifier)
67  {
68  // this gets turned into the qualifier, uh
70  read_rec(type.subtype());
71  }
72  else if(type.id()==ID_char)
73  char_cnt++;
74  else if(type.id()==ID_int)
75  int_cnt++;
76  else if(type.id()==ID_int8)
77  int8_cnt++;
78  else if(type.id()==ID_int16)
79  int16_cnt++;
80  else if(type.id()==ID_int32)
81  int32_cnt++;
82  else if(type.id()==ID_int64)
83  int64_cnt++;
84  else if(type.id()==ID_gcc_float16)
86  else if(type.id()==ID_gcc_float32)
88  else if(type.id()==ID_gcc_float32x)
90  else if(type.id()==ID_gcc_float64)
92  else if(type.id()==ID_gcc_float64x)
94  else if(type.id()==ID_gcc_float128)
96  else if(type.id()==ID_gcc_float128x)
98  else if(type.id()==ID_gcc_int128)
100  else if(type.id()==ID_gcc_attribute_mode)
101  {
102  gcc_attribute_mode=type;
103  }
104  else if(type.id()==ID_msc_based)
105  {
106  const exprt &as_expr=
107  static_cast<const exprt &>(static_cast<const irept &>(type));
108  msc_based = to_unary_expr(as_expr).op();
109  }
110  else if(type.id()==ID_custom_bv)
111  {
112  bv_cnt++;
113  const exprt &size_expr=
114  static_cast<const exprt &>(type.find(ID_size));
115 
116  bv_width=size_expr;
117  }
118  else if(type.id()==ID_custom_floatbv)
119  {
120  floatbv_cnt++;
121 
122  const exprt &size_expr=
123  static_cast<const exprt &>(type.find(ID_size));
124  const exprt &fsize_expr=
125  static_cast<const exprt &>(type.find(ID_f));
126 
127  bv_width=size_expr;
128  fraction_width=fsize_expr;
129  }
130  else if(type.id()==ID_custom_fixedbv)
131  {
132  fixedbv_cnt++;
133 
134  const exprt &size_expr=
135  static_cast<const exprt &>(type.find(ID_size));
136  const exprt &fsize_expr=
137  static_cast<const exprt &>(type.find(ID_f));
138 
139  bv_width=size_expr;
140  fraction_width=fsize_expr;
141  }
142  else if(type.id()==ID_short)
143  short_cnt++;
144  else if(type.id()==ID_long)
145  long_cnt++;
146  else if(type.id()==ID_double)
147  double_cnt++;
148  else if(type.id()==ID_float)
149  float_cnt++;
150  else if(type.id()==ID_c_bool)
151  c_bool_cnt++;
152  else if(type.id()==ID_proper_bool)
153  proper_bool_cnt++;
154  else if(type.id()==ID_complex)
155  complex_cnt++;
156  else if(type.id()==ID_static)
158  else if(type.id()==ID_thread_local)
160  else if(type.id()==ID_inline)
162  else if(type.id()==ID_extern)
164  else if(type.id()==ID_typedef)
166  else if(type.id()==ID_register)
168  else if(type.id()==ID_weak)
169  c_storage_spec.is_weak=true;
170  else if(type.id() == ID_used)
171  c_storage_spec.is_used = true;
172  else if(type.id()==ID_auto)
173  {
174  // ignore
175  }
176  else if(type.id()==ID_packed)
177  packed=true;
178  else if(type.id()==ID_aligned)
179  {
180  aligned=true;
181 
182  // may come with size or not
183  if(type.find(ID_size).is_nil())
184  alignment=exprt(ID_default);
185  else
186  alignment=static_cast<const exprt &>(type.find(ID_size));
187  }
188  else if(type.id()==ID_transparent_union)
189  {
191  }
192  else if(type.id()==ID_vector)
194  else if(type.id()==ID_void)
195  {
196  // we store 'void' as 'empty'
197  typet tmp=type;
198  tmp.id(ID_empty);
199  other.push_back(tmp);
200  }
201  else if(type.id()==ID_msc_declspec)
202  {
203  const exprt &as_expr=
204  static_cast<const exprt &>(static_cast<const irept &>(type));
205 
206  forall_operands(it, as_expr)
207  {
208  // these are symbols
209  const irep_idt &id=it->get(ID_identifier);
210 
211  if(id==ID_thread)
213  else if(id=="align")
214  {
215  aligned=true;
216  alignment = to_unary_expr(*it).op();
217  }
218  }
219  }
220  else if(type.id()==ID_noreturn)
222  else if(type.id()==ID_constructor)
223  constructor=true;
224  else if(type.id()==ID_destructor)
225  destructor=true;
226  else if(type.id()==ID_alias &&
227  type.has_subtype() &&
228  type.subtype().id()==ID_string_constant)
229  {
231  }
232  else if(type.id()==ID_frontend_pointer)
233  {
234  // We turn ID_frontend_pointer to ID_pointer
235  // Pointers have a width, much like integers,
236  // which is added here.
239  const irep_idt typedef_identifier=type.get(ID_C_typedef);
240  if(!typedef_identifier.empty())
241  tmp.set(ID_C_typedef, typedef_identifier);
242  other.push_back(tmp);
243  }
244  else if(type.id()==ID_pointer)
245  {
246  UNREACHABLE;
247  }
248  else
249  other.push_back(type);
250 }
251 
253 {
254  type.clear();
255 
256  // first, do "other"
257 
258  if(!other.empty())
259  {
260  if(double_cnt || float_cnt || signed_cnt ||
264  gcc_float16_cnt ||
269  {
271  error() << "illegal type modifier for defined type" << eom;
272  throw 0;
273  }
274 
275  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
276  if(other.size()==2)
277  {
278  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
279  other.pop_front();
280  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
281  other.pop_back();
282  }
283 
284  if(other.size()!=1)
285  {
287  error() << "illegal combination of defined types" << eom;
288  throw 0;
289  }
290 
291  type.swap(other.front());
292 
293  if(constructor || destructor)
294  {
295  if(constructor && destructor)
296  {
298  error() << "combining constructor and destructor not supported"
299  << eom;
300  throw 0;
301  }
302 
303  typet *type_p=&type;
304  if(type.id()==ID_code)
305  type_p=&(to_code_type(type).return_type());
306 
307  else if(type_p->id()!=ID_empty)
308  {
310  error() << "constructor and destructor required to be type void, "
311  << "found " << type_p->pretty() << eom;
312  throw 0;
313  }
314 
315  type_p->id(constructor ? ID_constructor : ID_destructor);
316  }
317  }
318  else if(constructor || destructor)
319  {
321  error() << "constructor and destructor required to be type void, "
322  << "found " << type.pretty() << eom;
323  throw 0;
324  }
325  else if(gcc_float16_cnt ||
329  {
332  gcc_int128_cnt || bv_cnt ||
333  short_cnt || char_cnt)
334  {
336  error() << "cannot combine integer type with floating-point type" << eom;
337  throw 0;
338  }
339 
340  if(long_cnt+double_cnt+
345  {
347  error() << "conflicting type modifiers" << eom;
348  throw 0;
349  }
350 
351  // _not_ the same as float, double, long double
352  if(gcc_float16_cnt)
353  type=gcc_float16_type();
354  else if(gcc_float32_cnt)
355  type=gcc_float32_type();
356  else if(gcc_float32x_cnt)
357  type=gcc_float32x_type();
358  else if(gcc_float64_cnt)
359  type=gcc_float64_type();
360  else if(gcc_float64x_cnt)
361  type=gcc_float64x_type();
362  else if(gcc_float128_cnt)
363  type=gcc_float128_type();
364  else if(gcc_float128x_cnt)
365  type=gcc_float128x_type();
366  else
367  UNREACHABLE;
368  }
369  else if(double_cnt || float_cnt)
370  {
374  short_cnt || char_cnt)
375  {
377  error() << "cannot combine integer type with floating-point type" << eom;
378  throw 0;
379  }
380 
381  if(double_cnt && float_cnt)
382  {
384  error() << "conflicting type modifiers" << eom;
385  throw 0;
386  }
387 
388  if(long_cnt==0)
389  {
390  if(double_cnt!=0)
391  type=double_type();
392  else
393  type=float_type();
394  }
395  else if(long_cnt==1 || long_cnt==2)
396  {
397  if(double_cnt!=0)
398  type=long_double_type();
399  else
400  {
402  error() << "conflicting type modifiers" << eom;
403  throw 0;
404  }
405  }
406  else
407  {
409  error() << "illegal type modifier for float" << eom;
410  throw 0;
411  }
412  }
413  else if(c_bool_cnt)
414  {
418  char_cnt || long_cnt)
419  {
421  error() << "illegal type modifier for C boolean type" << eom;
422  throw 0;
423  }
424 
425  type=c_bool_type();
426  }
427  else if(proper_bool_cnt)
428  {
432  char_cnt || long_cnt)
433  {
435  error() << "illegal type modifier for proper boolean type" << eom;
436  throw 0;
437  }
438 
439  type.id(ID_bool);
440  }
441  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
443  {
444  // the "default" for complex is double
445  type=double_type();
446  }
447  else if(char_cnt)
448  {
449  if(int_cnt || short_cnt || long_cnt ||
452  {
454  error() << "illegal type modifier for char type" << eom;
455  throw 0;
456  }
457 
458  if(signed_cnt && unsigned_cnt)
459  {
461  error() << "conflicting type modifiers" << eom;
462  throw 0;
463  }
464  else if(unsigned_cnt)
465  type=unsigned_char_type();
466  else if(signed_cnt)
467  type=signed_char_type();
468  else
469  type=char_type();
470  }
471  else
472  {
473  // it is integer -- signed or unsigned?
474 
475  bool is_signed=true; // default
476 
477  if(signed_cnt && unsigned_cnt)
478  {
480  error() << "conflicting type modifiers" << eom;
481  throw 0;
482  }
483  else if(unsigned_cnt)
484  is_signed=false;
485  else if(signed_cnt)
486  is_signed=true;
487 
489  {
491  {
493  error() << "conflicting type modifiers" << eom;
494  throw 0;
495  }
496 
497  if(int8_cnt)
498  if(is_signed)
499  type=signed_char_type();
500  else
501  type=unsigned_char_type();
502  else if(int16_cnt)
503  if(is_signed)
504  type=signed_short_int_type();
505  else
507  else if(int32_cnt)
508  if(is_signed)
509  type=signed_int_type();
510  else
511  type=unsigned_int_type();
512  else if(int64_cnt) // Visual Studio: equivalent to long long int
513  if(is_signed)
515  else
517  else
518  UNREACHABLE;
519  }
520  else if(gcc_int128_cnt)
521  {
522  if(is_signed)
523  type=gcc_signed_int128_type();
524  else
526  }
527  else if(bv_cnt)
528  {
529  // explicitly-given expression for width
530  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
531  type.set(ID_size, bv_width);
532  }
533  else if(floatbv_cnt)
534  {
535  type.id(ID_custom_floatbv);
536  type.set(ID_size, bv_width);
537  type.set(ID_f, fraction_width);
538  }
539  else if(fixedbv_cnt)
540  {
541  type.id(ID_custom_fixedbv);
542  type.set(ID_size, bv_width);
543  type.set(ID_f, fraction_width);
544  }
545  else if(short_cnt)
546  {
547  if(long_cnt || char_cnt)
548  {
550  error() << "conflicting type modifiers" << eom;
551  throw 0;
552  }
553 
554  if(is_signed)
555  type=signed_short_int_type();
556  else
558  }
559  else if(long_cnt==0)
560  {
561  if(is_signed)
562  type=signed_int_type();
563  else
564  type=unsigned_int_type();
565  }
566  else if(long_cnt==1)
567  {
568  if(is_signed)
569  type=signed_long_int_type();
570  else
571  type=unsigned_long_int_type();
572  }
573  else if(long_cnt==2)
574  {
575  if(is_signed)
577  else
579  }
580  else
581  {
583  error() << "illegal type modifier for integer type" << eom;
584  throw 0;
585  }
586  }
587 
589  set_attributes(type);
590 }
591 
594 {
595  if(vector_size.is_not_nil())
596  {
597  type_with_subtypet new_type(ID_frontend_vector, type);
598  new_type.set(ID_size, vector_size);
600  type=new_type;
601  }
602 
603  if(complex_cnt)
604  {
605  // These take more or less arbitrary subtypes.
606  complex_typet new_type(type);
608  type.swap(new_type);
609  }
610 }
611 
614 {
616  {
617  typet new_type=gcc_attribute_mode;
618  new_type.subtype()=type;
619  type.swap(new_type);
620  }
621 
622  c_qualifiers.write(type);
623 
624  if(packed)
625  type.set(ID_C_packed, true);
626 
627  if(aligned)
628  type.set(ID_C_alignment, alignment);
629 }
ANSI-C Language Conversion.
floatbv_typet float_type()
Definition: c_types.cpp:185
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
bitvector_typet char_type()
Definition: c_types.cpp:114
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
floatbv_typet long_double_type()
Definition: c_types.cpp:201
typet c_bool_type()
Definition: c_types.cpp:108
floatbv_typet double_type()
Definition: c_types.cpp:193
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
virtual void read_rec(const typet &type)
c_storage_spect c_storage_spec
virtual void read(const typet &type)
virtual void write(typet &type)
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
std::list< typet > other
bool is_restricted
Definition: c_qualifiers.h:91
virtual void write(typet &src) const override
bool is_transparent_union
Definition: c_qualifiers.h:97
irep_idt asm_label
const typet & return_type() const
Definition: std_types.h:850
Complex numbers made of pair of given subtype.
Definition: std_types.h:1804
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:234
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
void clear()
Definition: irep.h:462
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
const irep_idt & get_value() const
Type with a single subtype.
Definition: type.h:146
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
const typet & subtype() const
Definition: type.h:47
bool has_subtype() const
Definition: type.h:65
source_locationt & add_source_location()
Definition: type.h:76
const exprt & op() const
Definition: std_expr.h:294
const constant_exprt & size() const
Definition: std_types.cpp:282
configt config
Definition: config.cpp:24
#define forall_operands(it, expr)
Definition: expr.h:18
floatbv_typet gcc_float32_type()
Definition: gcc_types.cpp:22
floatbv_typet gcc_float16_type()
Definition: gcc_types.cpp:14
floatbv_typet gcc_float64_type()
Definition: gcc_types.cpp:40
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
floatbv_typet gcc_float128x_type()
Definition: gcc_types.cpp:67
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1789
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
const string_constantt & to_string_constant(const exprt &expr)
std::size_t pointer_width
Definition: config.h:117
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45