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 <cassert>
15 
16 #include <util/c_types.h>
17 #include <util/config.h>
18 #include <util/namespace.h>
19 #include <util/simplify_expr.h>
20 #include <util/arith_tools.h>
21 #include <util/std_types.h>
22 
23 #include "gcc_types.h"
24 
26 {
27  clear();
29  read_rec(type);
30 }
31 
33 {
34  if(type.id()==ID_merged_type)
35  {
36  forall_subtypes(it, type)
37  read_rec(*it);
38  }
39  else if(type.id()==ID_signed)
40  signed_cnt++;
41  else if(type.id()==ID_unsigned)
42  unsigned_cnt++;
43  else if(type.id()==ID_ptr32)
45  else if(type.id()==ID_ptr64)
47  else if(type.id()==ID_volatile)
49  else if(type.id()==ID_asm)
50  {
51  if(type.has_subtype() &&
52  type.subtype().id()==ID_string_constant)
53  c_storage_spec.asm_label=type.subtype().get(ID_value);
54  }
55  else if(type.id()==ID_section &&
56  type.has_subtype() &&
57  type.subtype().id()==ID_string_constant)
58  {
59  c_storage_spec.section=type.subtype().get(ID_value);
60  }
61  else if(type.id()==ID_const)
63  else if(type.id()==ID_restrict)
65  else if(type.id()==ID_atomic)
67  else if(type.id()==ID_atomic_type_specifier)
68  {
69  // this gets turned into the qualifier, uh
71  read_rec(type.subtype());
72  }
73  else if(type.id()==ID_char)
74  char_cnt++;
75  else if(type.id()==ID_int)
76  int_cnt++;
77  else if(type.id()==ID_int8)
78  int8_cnt++;
79  else if(type.id()==ID_int16)
80  int16_cnt++;
81  else if(type.id()==ID_int32)
82  int32_cnt++;
83  else if(type.id()==ID_int64)
84  int64_cnt++;
85  else if(type.id()==ID_gcc_float16)
87  else if(type.id()==ID_gcc_float32)
89  else if(type.id()==ID_gcc_float32x)
91  else if(type.id()==ID_gcc_float64)
93  else if(type.id()==ID_gcc_float64x)
95  else if(type.id()==ID_gcc_float128)
97  else if(type.id()==ID_gcc_float128x)
99  else if(type.id()==ID_gcc_int128)
100  gcc_int128_cnt++;
101  else if(type.id()==ID_gcc_attribute_mode)
102  {
103  gcc_attribute_mode=type;
104  }
105  else if(type.id()==ID_msc_based)
106  {
107  const exprt &as_expr=
108  static_cast<const exprt &>(static_cast<const irept &>(type));
109  assert(as_expr.operands().size()==1);
110  msc_based=as_expr.op0();
111  }
112  else if(type.id()==ID_custom_bv)
113  {
114  bv_cnt++;
115  const exprt &size_expr=
116  static_cast<const exprt &>(type.find(ID_size));
117 
118  bv_width=size_expr;
119  }
120  else if(type.id()==ID_custom_floatbv)
121  {
122  floatbv_cnt++;
123 
124  const exprt &size_expr=
125  static_cast<const exprt &>(type.find(ID_size));
126  const exprt &fsize_expr=
127  static_cast<const exprt &>(type.find(ID_f));
128 
129  bv_width=size_expr;
130  fraction_width=fsize_expr;
131  }
132  else if(type.id()==ID_custom_fixedbv)
133  {
134  fixedbv_cnt++;
135 
136  const exprt &size_expr=
137  static_cast<const exprt &>(type.find(ID_size));
138  const exprt &fsize_expr=
139  static_cast<const exprt &>(type.find(ID_f));
140 
141  bv_width=size_expr;
142  fraction_width=fsize_expr;
143  }
144  else if(type.id()==ID_short)
145  short_cnt++;
146  else if(type.id()==ID_long)
147  long_cnt++;
148  else if(type.id()==ID_double)
149  double_cnt++;
150  else if(type.id()==ID_float)
151  float_cnt++;
152  else if(type.id()==ID_c_bool)
153  c_bool_cnt++;
154  else if(type.id()==ID_proper_bool)
155  proper_bool_cnt++;
156  else if(type.id()==ID_complex)
157  complex_cnt++;
158  else if(type.id()==ID_static)
160  else if(type.id()==ID_thread_local)
162  else if(type.id()==ID_inline)
164  else if(type.id()==ID_extern)
166  else if(type.id()==ID_typedef)
168  else if(type.id()==ID_register)
170  else if(type.id()==ID_weak)
171  c_storage_spec.is_weak=true;
172  else if(type.id() == ID_used)
173  c_storage_spec.is_used = true;
174  else if(type.id() == ID_always_inline)
176  else if(type.id()==ID_auto)
177  {
178  // ignore
179  }
180  else if(type.id()==ID_packed)
181  packed=true;
182  else if(type.id()==ID_aligned)
183  {
184  aligned=true;
185 
186  // may come with size or not
187  if(type.find(ID_size).is_nil())
188  alignment=exprt(ID_default);
189  else
190  alignment=static_cast<const exprt &>(type.find(ID_size));
191  }
192  else if(type.id()==ID_transparent_union)
193  {
195  }
196  else if(type.id()==ID_vector)
198  else if(type.id()==ID_void)
199  {
200  // we store 'void' as 'empty'
201  typet tmp=type;
202  tmp.id(ID_empty);
203  other.push_back(tmp);
204  }
205  else if(type.id()==ID_msc_declspec)
206  {
207  const exprt &as_expr=
208  static_cast<const exprt &>(static_cast<const irept &>(type));
209 
210  forall_operands(it, as_expr)
211  {
212  // these are symbols
213  const irep_idt &id=it->get(ID_identifier);
214 
215  if(id==ID_thread)
217  else if(id=="align")
218  {
219  assert(it->operands().size()==1);
220  aligned=true;
221  alignment=it->op0();
222  }
223  }
224  }
225  else if(type.id()==ID_noreturn)
227  else if(type.id()==ID_constructor)
228  constructor=true;
229  else if(type.id()==ID_destructor)
230  destructor=true;
231  else if(type.id()==ID_alias &&
232  type.has_subtype() &&
233  type.subtype().id()==ID_string_constant)
234  {
235  c_storage_spec.alias=type.subtype().get(ID_value);
236  }
237  else if(type.id()==ID_frontend_pointer)
238  {
239  // We turn ID_frontend_pointer to ID_pointer
240  // Pointers have a width, much like integers,
241  // which is added here.
244  const irep_idt typedef_identifier=type.get(ID_C_typedef);
245  if(!typedef_identifier.empty())
246  tmp.set(ID_C_typedef, typedef_identifier);
247  other.push_back(tmp);
248  }
249  else if(type.id()==ID_pointer)
250  {
251  UNREACHABLE;
252  }
253  else
254  other.push_back(type);
255 }
256 
258 {
259  type.clear();
260 
261  // first, do "other"
262 
263  if(!other.empty())
264  {
265  if(double_cnt || float_cnt || signed_cnt ||
269  gcc_float16_cnt ||
274  {
276  error() << "illegal type modifier for defined type" << eom;
277  throw 0;
278  }
279 
280  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
281  if(other.size()==2)
282  {
283  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
284  other.pop_front();
285  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
286  other.pop_back();
287  }
288 
289  if(other.size()!=1)
290  {
292  error() << "illegal combination of defined types" << eom;
293  throw 0;
294  }
295 
296  type.swap(other.front());
297 
298  if(constructor || destructor)
299  {
300  if(constructor && destructor)
301  {
303  error() << "combining constructor and destructor not supported"
304  << eom;
305  throw 0;
306  }
307 
308  typet *type_p=&type;
309  if(type.id()==ID_code)
310  type_p=&(to_code_type(type).return_type());
311 
312  else if(type_p->id()!=ID_empty)
313  {
315  error() << "constructor and destructor required to be type void, "
316  << "found " << type_p->pretty() << eom;
317  throw 0;
318  }
319 
320  type_p->id(constructor ? ID_constructor : ID_destructor);
321  }
322  }
323  else if(constructor || destructor)
324  {
326  error() << "constructor and destructor required to be type void, "
327  << "found " << type.pretty() << eom;
328  throw 0;
329  }
330  else if(gcc_float16_cnt ||
334  {
337  gcc_int128_cnt || bv_cnt ||
338  short_cnt || char_cnt)
339  {
341  error() << "cannot combine integer type with floating-point type" << eom;
342  throw 0;
343  }
344 
345  if(long_cnt+double_cnt+
350  {
352  error() << "conflicting type modifiers" << eom;
353  throw 0;
354  }
355 
356  // _not_ the same as float, double, long double
357  if(gcc_float16_cnt)
358  type=gcc_float16_type();
359  else if(gcc_float32_cnt)
360  type=gcc_float32_type();
361  else if(gcc_float32x_cnt)
362  type=gcc_float32x_type();
363  else if(gcc_float64_cnt)
364  type=gcc_float64_type();
365  else if(gcc_float64x_cnt)
366  type=gcc_float64x_type();
367  else if(gcc_float128_cnt)
368  type=gcc_float128_type();
369  else if(gcc_float128x_cnt)
370  type=gcc_float128x_type();
371  else
372  UNREACHABLE;
373  }
374  else if(double_cnt || float_cnt)
375  {
379  short_cnt || char_cnt)
380  {
382  error() << "cannot combine integer type with floating-point type" << eom;
383  throw 0;
384  }
385 
386  if(double_cnt && float_cnt)
387  {
389  error() << "conflicting type modifiers" << eom;
390  throw 0;
391  }
392 
393  if(long_cnt==0)
394  {
395  if(double_cnt!=0)
396  type=double_type();
397  else
398  type=float_type();
399  }
400  else if(long_cnt==1 || long_cnt==2)
401  {
402  if(double_cnt!=0)
403  type=long_double_type();
404  else
405  {
407  error() << "conflicting type modifiers" << eom;
408  throw 0;
409  }
410  }
411  else
412  {
414  error() << "illegal type modifier for float" << eom;
415  throw 0;
416  }
417  }
418  else if(c_bool_cnt)
419  {
423  char_cnt || long_cnt)
424  {
426  error() << "illegal type modifier for C boolean type" << eom;
427  throw 0;
428  }
429 
430  type=c_bool_type();
431  }
432  else if(proper_bool_cnt)
433  {
437  char_cnt || long_cnt)
438  {
440  error() << "illegal type modifier for proper boolean type" << eom;
441  throw 0;
442  }
443 
444  type.id(ID_bool);
445  }
446  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
448  {
449  // the "default" for complex is double
450  type=double_type();
451  }
452  else if(char_cnt)
453  {
454  if(int_cnt || short_cnt || long_cnt ||
457  {
459  error() << "illegal type modifier for char type" << eom;
460  throw 0;
461  }
462 
463  if(signed_cnt && unsigned_cnt)
464  {
466  error() << "conflicting type modifiers" << eom;
467  throw 0;
468  }
469  else if(unsigned_cnt)
470  type=unsigned_char_type();
471  else if(signed_cnt)
472  type=signed_char_type();
473  else
474  type=char_type();
475  }
476  else
477  {
478  // it is integer -- signed or unsigned?
479 
480  bool is_signed=true; // default
481 
482  if(signed_cnt && unsigned_cnt)
483  {
485  error() << "conflicting type modifiers" << eom;
486  throw 0;
487  }
488  else if(unsigned_cnt)
489  is_signed=false;
490  else if(signed_cnt)
491  is_signed=true;
492 
494  {
496  {
498  error() << "conflicting type modifiers" << eom;
499  throw 0;
500  }
501 
502  if(int8_cnt)
503  if(is_signed)
504  type=signed_char_type();
505  else
506  type=unsigned_char_type();
507  else if(int16_cnt)
508  if(is_signed)
509  type=signed_short_int_type();
510  else
512  else if(int32_cnt)
513  if(is_signed)
514  type=signed_int_type();
515  else
516  type=unsigned_int_type();
517  else if(int64_cnt) // Visual Studio: equivalent to long long int
518  if(is_signed)
520  else
522  else
523  UNREACHABLE;
524  }
525  else if(gcc_int128_cnt)
526  {
527  if(is_signed)
528  type=gcc_signed_int128_type();
529  else
531  }
532  else if(bv_cnt)
533  {
534  // explicitly-given expression for width
535  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
536  type.set(ID_size, bv_width);
537  }
538  else if(floatbv_cnt)
539  {
540  type.id(ID_custom_floatbv);
541  type.set(ID_size, bv_width);
542  type.set(ID_f, fraction_width);
543  }
544  else if(fixedbv_cnt)
545  {
546  type.id(ID_custom_fixedbv);
547  type.set(ID_size, bv_width);
548  type.set(ID_f, fraction_width);
549  }
550  else if(short_cnt)
551  {
552  if(long_cnt || char_cnt)
553  {
555  error() << "conflicting type modifiers" << eom;
556  throw 0;
557  }
558 
559  if(is_signed)
560  type=signed_short_int_type();
561  else
563  }
564  else if(long_cnt==0)
565  {
566  if(is_signed)
567  type=signed_int_type();
568  else
569  type=unsigned_int_type();
570  }
571  else if(long_cnt==1)
572  {
573  if(is_signed)
574  type=signed_long_int_type();
575  else
576  type=unsigned_long_int_type();
577  }
578  else if(long_cnt==2)
579  {
580  if(is_signed)
582  else
584  }
585  else
586  {
588  error() << "illegal type modifier for integer type" << eom;
589  throw 0;
590  }
591  }
592 
593  if(vector_size.is_not_nil())
594  {
595  vector_typet new_type(type, vector_size);
597  type=new_type;
598  }
599 
600  if(complex_cnt)
601  {
602  // These take more or less arbitrary subtypes.
603  complex_typet new_type;
605  new_type.subtype()=type;
606  type.swap(new_type);
607  }
608 
610  {
611  typet new_type=gcc_attribute_mode;
612  new_type.subtype()=type;
613  type.swap(new_type);
614  }
615 
616  c_qualifiers.write(type);
617 
618  if(packed)
619  type.set(ID_C_packed, true);
620 
621  if(aligned)
622  type.set(ID_C_alignment, alignment);
623 }
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
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
#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
exprt & op0()
Definition: expr.h:72
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
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
bitvector_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
bitvector_typet double_type()
Definition: c_types.cpp:193
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
source_locationt source_location
bitvector_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
const irep_idt & id() const
Definition: irep.h:189
bitvector_typet float_type()
Definition: c_types.cpp:185
The pointer type.
Definition: std_types.h:1426
source_locationt source_location
Definition: message.h:214
A constant-size array type.
Definition: std_types.h:1629
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
const exprt & size() const
Definition: std_types.h:1639
bool is_transparent_union
Definition: c_qualifiers.h:97
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
Base class for tree-like data structures with sharing.
Definition: irep.h:86
#define forall_operands(it, expr)
Definition: expr.h:17
std::size_t pointer_width
Definition: config.h:36
ANSI-C Language Conversion.
bitvector_typet long_double_type()
Definition: c_types.cpp:201
const source_locationt & source_location() const
Definition: type.h:97
std::list< typet > other
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
Complex numbers made of pair of given subtype.
Definition: std_types.h:1677
c_storage_spect c_storage_spec
API to type classes.
void read(const typet &type)
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
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
void clear()
Definition: irep.h:241
void read_rec(const typet &type)
void swap(irept &irep)
Definition: irep.h:231
virtual void write(typet &src) const override
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
bool is_restricted
Definition: c_qualifiers.h:91
bitvector_typet gcc_float64_type()
Definition: gcc_types.cpp:40
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
bitvector_typet gcc_float16_type()
Definition: gcc_types.cpp:14
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
operandst & operands()
Definition: expr.h:66
typet c_bool_type()
Definition: c_types.cpp:108
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
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:895
bitvector_typet gcc_float128x_type()
Definition: gcc_types.cpp:67
bitvector_typet gcc_float32_type()
Definition: gcc_types.cpp:22
irep_idt asm_label
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214