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/namespace.h>
18 #include <util/simplify_expr.h>
19 #include <util/config.h>
20 #include <util/arith_tools.h>
21 #include <util/std_types.h>
22 
24 {
25  clear();
27  read_rec(type);
28 }
29 
31 {
32  if(type.id()==ID_merged_type)
33  {
34  forall_subtypes(it, type)
35  read_rec(*it);
36  }
37  else if(type.id()==ID_signed)
38  signed_cnt++;
39  else if(type.id()==ID_unsigned)
40  unsigned_cnt++;
41  else if(type.id()==ID_ptr32)
43  else if(type.id()==ID_ptr64)
45  else if(type.id()==ID_volatile)
47  else if(type.id()==ID_asm)
48  {
49  if(type.has_subtype() &&
50  type.subtype().id()==ID_string_constant)
51  c_storage_spec.asm_label=type.subtype().get(ID_value);
52  }
53  else if(type.id()==ID_section &&
54  type.has_subtype() &&
55  type.subtype().id()==ID_string_constant)
56  {
57  c_storage_spec.section=type.subtype().get(ID_value);
58  }
59  else if(type.id()==ID_const)
61  else if(type.id()==ID_restrict)
63  else if(type.id()==ID_atomic)
65  else if(type.id()==ID_atomic_type_specifier)
66  {
67  // this gets turned into the qualifier, uh
69  read_rec(type.subtype());
70  }
71  else if(type.id()==ID_char)
72  char_cnt++;
73  else if(type.id()==ID_int)
74  int_cnt++;
75  else if(type.id()==ID_int8)
76  int8_cnt++;
77  else if(type.id()==ID_int16)
78  int16_cnt++;
79  else if(type.id()==ID_int32)
80  int32_cnt++;
81  else if(type.id()==ID_int64)
82  int64_cnt++;
83  else if(type.id()==ID_gcc_float128)
85  else if(type.id()==ID_gcc_int128)
87  else if(type.id()==ID_gcc_attribute_mode)
88  {
89  gcc_attribute_mode=type;
90  }
91  else if(type.id()==ID_msc_based)
92  {
93  const exprt &as_expr=
94  static_cast<const exprt &>(static_cast<const irept &>(type));
95  assert(as_expr.operands().size()==1);
96  msc_based=as_expr.op0();
97  }
98  else if(type.id()==ID_custom_bv)
99  {
100  bv_cnt++;
101  const exprt &size_expr=
102  static_cast<const exprt &>(type.find(ID_size));
103 
104  bv_width=size_expr;
105  }
106  else if(type.id()==ID_custom_floatbv)
107  {
108  floatbv_cnt++;
109 
110  const exprt &size_expr=
111  static_cast<const exprt &>(type.find(ID_size));
112  const exprt &fsize_expr=
113  static_cast<const exprt &>(type.find(ID_f));
114 
115  bv_width=size_expr;
116  fraction_width=fsize_expr;
117  }
118  else if(type.id()==ID_custom_fixedbv)
119  {
120  fixedbv_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_short)
131  short_cnt++;
132  else if(type.id()==ID_long)
133  long_cnt++;
134  else if(type.id()==ID_double)
135  double_cnt++;
136  else if(type.id()==ID_float)
137  float_cnt++;
138  else if(type.id()==ID_c_bool)
139  c_bool_cnt++;
140  else if(type.id()==ID_proper_bool)
141  proper_bool_cnt++;
142  else if(type.id()==ID_complex)
143  complex_cnt++;
144  else if(type.id()==ID_static)
146  else if(type.id()==ID_thread_local)
148  else if(type.id()==ID_inline)
150  else if(type.id()==ID_extern)
152  else if(type.id()==ID_typedef)
154  else if(type.id()==ID_register)
156  else if(type.id()==ID_weak)
157  c_storage_spec.is_weak=true;
158  else if(type.id()==ID_auto)
159  {
160  // ignore
161  }
162  else if(type.id()==ID_packed)
163  packed=true;
164  else if(type.id()==ID_aligned)
165  {
166  aligned=true;
167 
168  // may come with size or not
169  if(type.find(ID_size).is_nil())
170  alignment=exprt(ID_default);
171  else
172  alignment=static_cast<const exprt &>(type.find(ID_size));
173  }
174  else if(type.id()==ID_transparent_union)
175  {
177  }
178  else if(type.id()==ID_vector)
180  else if(type.id()==ID_void)
181  {
182  // we store 'void' as 'empty'
183  typet tmp=type;
184  tmp.id(ID_empty);
185  other.push_back(tmp);
186  }
187  else if(type.id()==ID_msc_declspec)
188  {
189  const exprt &as_expr=
190  static_cast<const exprt &>(static_cast<const irept &>(type));
191 
192  forall_operands(it, as_expr)
193  {
194  // these are symbols
195  const irep_idt &id=it->get(ID_identifier);
196 
197  if(id==ID_thread)
199  else if(id=="align")
200  {
201  assert(it->operands().size()==1);
202  aligned=true;
203  alignment=it->op0();
204  }
205  }
206  }
207  else if(type.id()==ID_noreturn)
209  else if(type.id()==ID_constructor)
210  constructor=true;
211  else if(type.id()==ID_destructor)
212  destructor=true;
213  else if(type.id()==ID_alias &&
214  type.has_subtype() &&
215  type.subtype().id()==ID_string_constant)
216  {
217  c_storage_spec.alias=type.subtype().get(ID_value);
218  }
219  else
220  other.push_back(type);
221 }
222 
224 {
225  type.clear();
226 
227  // first, do "other"
228 
229  if(!other.empty())
230  {
231  if(double_cnt || float_cnt || signed_cnt ||
236  {
238  error() << "illegal type modifier for defined type" << eom;
239  throw 0;
240  }
241 
242  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
243  if(other.size()==2)
244  {
245  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
246  other.pop_front();
247  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
248  other.pop_back();
249  }
250 
251  if(other.size()!=1)
252  {
254  error() << "illegal combination of defined types" << eom;
255  throw 0;
256  }
257 
258  type.swap(other.front());
259 
260  if(constructor || destructor)
261  {
262  if(constructor && destructor)
263  {
265  error() << "combining constructor and destructor not supported"
266  << eom;
267  throw 0;
268  }
269 
270  typet *type_p=&type;
271  if(type.id()==ID_code)
272  type_p=&(to_code_type(type).return_type());
273 
274  else if(type_p->id()!=ID_empty)
275  {
277  error() << "constructor and destructor required to be type void, "
278  << "found " << type_p->pretty() << eom;
279  throw 0;
280  }
281 
282  type_p->id(constructor ? ID_constructor : ID_destructor);
283  }
284  }
285  else if(constructor || destructor)
286  {
288  error() << "constructor and destructor required to be type void, "
289  << "found " << type.pretty() << eom;
290  throw 0;
291  }
292  else if(gcc_float128_cnt)
293  {
296  gcc_int128_cnt || bv_cnt ||
297  short_cnt || char_cnt)
298  {
300  error() << "cannot combine integer type with float" << eom;
301  throw 0;
302  }
303 
304  if(long_cnt || double_cnt || float_cnt)
305  {
307  error() << "conflicting type modifiers" << eom;
308  throw 0;
309  }
310 
311  // _not_ the same as long double
312  type=gcc_float128_type();
313  }
314  else if(double_cnt || float_cnt)
315  {
319  short_cnt || char_cnt)
320  {
322  error() << "cannot combine integer type with float" << eom;
323  throw 0;
324  }
325 
326  if(double_cnt && float_cnt)
327  {
329  error() << "conflicting type modifiers" << eom;
330  throw 0;
331  }
332 
333  if(long_cnt==0)
334  {
335  if(double_cnt!=0)
336  type=double_type();
337  else
338  type=float_type();
339  }
340  else if(long_cnt==1 || long_cnt==2)
341  {
342  if(double_cnt!=0)
343  type=long_double_type();
344  else
345  {
347  error() << "conflicting type modifiers" << eom;
348  throw 0;
349  }
350  }
351  else
352  {
354  error() << "illegal type modifier for float" << eom;
355  throw 0;
356  }
357  }
358  else if(c_bool_cnt)
359  {
363  char_cnt || long_cnt)
364  {
366  error() << "illegal type modifier for C boolean type" << eom;
367  throw 0;
368  }
369 
370  type=c_bool_type();
371  }
372  else if(proper_bool_cnt)
373  {
377  char_cnt || long_cnt)
378  {
380  error() << "illegal type modifier for proper boolean type" << eom;
381  throw 0;
382  }
383 
384  type.id(ID_bool);
385  }
386  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
388  {
389  // the "default" for complex is double
390  type=double_type();
391  }
392  else if(char_cnt)
393  {
394  if(int_cnt || short_cnt || long_cnt ||
397  {
399  error() << "illegal type modifier for char type" << eom;
400  throw 0;
401  }
402 
403  if(signed_cnt && unsigned_cnt)
404  {
406  error() << "conflicting type modifiers" << eom;
407  throw 0;
408  }
409  else if(unsigned_cnt)
410  type=unsigned_char_type();
411  else if(signed_cnt)
412  type=signed_char_type();
413  else
414  type=char_type();
415  }
416  else
417  {
418  // it is integer -- signed or unsigned?
419 
420  bool is_signed=true; // default
421 
422  if(signed_cnt && unsigned_cnt)
423  {
425  error() << "conflicting type modifiers" << eom;
426  throw 0;
427  }
428  else if(unsigned_cnt)
429  is_signed=false;
430  else if(signed_cnt)
431  is_signed=true;
432 
434  {
436  {
438  error() << "conflicting type modifiers" << eom;
439  throw 0;
440  }
441 
442  if(int8_cnt)
443  if(is_signed)
444  type=signed_char_type();
445  else
446  type=unsigned_char_type();
447  else if(int16_cnt)
448  if(is_signed)
449  type=signed_short_int_type();
450  else
452  else if(int32_cnt)
453  if(is_signed)
454  type=signed_int_type();
455  else
456  type=unsigned_int_type();
457  else if(int64_cnt) // Visual Studio: equivalent to long long int
458  if(is_signed)
460  else
462  else
463  assert(false);
464  }
465  else if(gcc_int128_cnt)
466  {
467  if(is_signed)
468  type=gcc_signed_int128_type();
469  else
471  }
472  else if(bv_cnt)
473  {
474  // explicitly-given expression for width
475  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
476  type.set(ID_size, bv_width);
477  }
478  else if(floatbv_cnt)
479  {
480  type.id(ID_custom_floatbv);
481  type.set(ID_size, bv_width);
482  type.set(ID_f, fraction_width);
483  }
484  else if(fixedbv_cnt)
485  {
486  type.id(ID_custom_fixedbv);
487  type.set(ID_size, bv_width);
488  type.set(ID_f, fraction_width);
489  }
490  else if(short_cnt)
491  {
492  if(long_cnt || char_cnt)
493  {
495  error() << "conflicting type modifiers" << eom;
496  throw 0;
497  }
498 
499  if(is_signed)
500  type=signed_short_int_type();
501  else
503  }
504  else if(long_cnt==0)
505  {
506  if(is_signed)
507  type=signed_int_type();
508  else
509  type=unsigned_int_type();
510  }
511  else if(long_cnt==1)
512  {
513  if(is_signed)
514  type=signed_long_int_type();
515  else
516  type=unsigned_long_int_type();
517  }
518  else if(long_cnt==2)
519  {
520  if(is_signed)
522  else
524  }
525  else
526  {
528  error() << "illegal type modifier for integer type" << eom;
529  throw 0;
530  }
531  }
532 
533  if(vector_size.is_not_nil())
534  {
535  vector_typet new_type;
536  new_type.size()=vector_size;
538  new_type.subtype().swap(type);
539  type=new_type;
540  }
541 
542  if(complex_cnt)
543  {
544  // These take more or less arbitrary subtypes.
545  complex_typet new_type;
547  new_type.subtype()=type;
548  type.swap(new_type);
549  }
550 
552  {
553  typet new_type=gcc_attribute_mode;
554  new_type.subtype()=type;
555  type.swap(new_type);
556  }
557 
558  c_qualifiers.write(type);
559 
560  if(packed)
561  type.set(ID_C_packed, true);
562 
563  if(aligned)
564  type.set(ID_C_alignment, alignment);
565 }
The type of an expression.
Definition: type.h:20
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
#define forall_subtypes(it, type)
Definition: type.h:159
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool has_subtype() const
Definition: type.h:77
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:43
bitvector_typet double_type()
Definition: c_types.cpp:203
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
source_locationt source_location
const irep_idt & id() const
Definition: irep.h:189
bitvector_typet float_type()
Definition: c_types.cpp:184
source_locationt source_location
Definition: message.h:175
A constant-size array type.
Definition: std_types.h:1554
void write(typet &src) const
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
const exprt & size() const
Definition: std_types.h:1568
bool is_transparent_union
Definition: c_qualifiers.h:49
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:79
Base class for tree-like data structures with sharing.
Definition: irep.h:87
#define forall_operands(it, expr)
Definition: expr.h:17
ANSI-C Language Conversion.
bitvector_typet long_double_type()
Definition: c_types.cpp:222
const source_locationt & source_location() const
Definition: type.h:95
std::list< typet > other
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:36
Complex numbers made of pair of given subtype.
Definition: std_types.h:1606
c_storage_spect c_storage_spec
API to type classes.
void read(const typet &type)
unsignedbv_typet gcc_unsigned_int128_type()
Definition: c_types.cpp:311
bitvector_typet gcc_float128_type()
Definition: c_types.cpp:260
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:50
Base class for all expressions.
Definition: expr.h:46
source_locationt & add_source_location()
Definition: type.h:100
const source_locationt & source_location() const
Definition: expr.h:142
void clear()
Definition: irep.h:241
void read_rec(const typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:100
bool is_restricted
Definition: c_qualifiers.h:43
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:134
const typet & subtype() const
Definition: type.h:31
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:93
signedbv_typet gcc_signed_int128_type()
Definition: c_types.cpp:318
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:86
operandst & operands()
Definition: expr.h:70
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
typet c_bool_type()
Definition: c_types.cpp:107
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
signedbv_typet signed_char_type()
Definition: c_types.cpp:141
bitvector_typet char_type()
Definition: c_types.cpp:113
const typet & return_type() const
Definition: std_types.h:831
irep_idt asm_label
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214