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/c_types.h>
15 #include <util/config.h>
16 #include <util/std_code.h>
17 #include <util/std_types.h>
18 #include <util/string_constant.h>
19 
20 #include "gcc_types.h"
21 
23 {
24  clear();
26  read_rec(type);
27 }
28 
30 {
31  if(type.id()==ID_merged_type)
32  {
33  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
34  read_rec(subtype);
35  }
36  else if(type.id()==ID_signed)
37  signed_cnt++;
38  else if(type.id()==ID_unsigned)
39  unsigned_cnt++;
40  else if(type.id()==ID_ptr32)
42  else if(type.id()==ID_ptr64)
44  else if(type.id()==ID_volatile)
46  else if(type.id()==ID_asm)
47  {
48  // These can have up to 5 subtypes; we only use the first one.
49  const auto &type_with_subtypes = to_type_with_subtypes(type);
50  if(
51  !type_with_subtypes.subtypes().empty() &&
52  type_with_subtypes.subtypes()[0].id() == ID_string_constant)
54  to_string_constant(type_with_subtypes.subtypes()[0]).get_value();
55  }
56  else if(
57  type.id() == ID_section && type.has_subtype() &&
58  to_type_with_subtype(type).subtype().id() == ID_string_constant)
59  {
62  }
63  else if(type.id()==ID_const)
65  else if(type.id()==ID_restrict)
67  else if(type.id()==ID_atomic)
69  else if(type.id()==ID_atomic_type_specifier)
70  {
71  // this gets turned into the qualifier, uh
73  read_rec(to_type_with_subtype(type).subtype());
74  }
75  else if(type.id()==ID_char)
76  char_cnt++;
77  else if(type.id()==ID_int)
78  int_cnt++;
79  else if(type.id()==ID_int8)
80  int8_cnt++;
81  else if(type.id()==ID_int16)
82  int16_cnt++;
83  else if(type.id()==ID_int32)
84  int32_cnt++;
85  else if(type.id()==ID_int64)
86  int64_cnt++;
87  else if(type.id()==ID_gcc_float16)
89  else if(type.id()==ID_gcc_float32)
91  else if(type.id()==ID_gcc_float32x)
93  else if(type.id()==ID_gcc_float64)
95  else if(type.id()==ID_gcc_float64x)
97  else if(type.id()==ID_gcc_float128)
99  else if(type.id()==ID_gcc_float128x)
101  else if(type.id()==ID_gcc_int128)
102  gcc_int128_cnt++;
103  else if(type.id()==ID_gcc_attribute_mode)
104  {
105  gcc_attribute_mode=type;
106  }
107  else if(type.id()==ID_msc_based)
108  {
109  const exprt &as_expr=
110  static_cast<const exprt &>(static_cast<const irept &>(type));
111  msc_based = to_unary_expr(as_expr).op();
112  }
113  else if(type.id()==ID_custom_bv)
114  {
115  bv_cnt++;
116  const exprt &size_expr=
117  static_cast<const exprt &>(type.find(ID_size));
118 
119  bv_width=size_expr;
120  }
121  else if(type.id()==ID_custom_floatbv)
122  {
123  floatbv_cnt++;
124 
125  const exprt &size_expr=
126  static_cast<const exprt &>(type.find(ID_size));
127  const exprt &fsize_expr=
128  static_cast<const exprt &>(type.find(ID_f));
129 
130  bv_width=size_expr;
131  fraction_width=fsize_expr;
132  }
133  else if(type.id()==ID_custom_fixedbv)
134  {
135  fixedbv_cnt++;
136 
137  const exprt &size_expr=
138  static_cast<const exprt &>(type.find(ID_size));
139  const exprt &fsize_expr=
140  static_cast<const exprt &>(type.find(ID_f));
141 
142  bv_width=size_expr;
143  fraction_width=fsize_expr;
144  }
145  else if(type.id()==ID_short)
146  short_cnt++;
147  else if(type.id()==ID_long)
148  long_cnt++;
149  else if(type.id()==ID_double)
150  double_cnt++;
151  else if(type.id()==ID_float)
152  float_cnt++;
153  else if(type.id()==ID_c_bool)
154  c_bool_cnt++;
155  else if(type.id()==ID_proper_bool)
156  proper_bool_cnt++;
157  else if(type.id()==ID_complex)
158  complex_cnt++;
159  else if(type.id()==ID_static)
161  else if(type.id()==ID_thread_local)
163  else if(type.id()==ID_inline)
165  else if(type.id()==ID_extern)
167  else if(type.id()==ID_typedef)
169  else if(type.id()==ID_register)
171  else if(type.id()==ID_weak)
172  c_storage_spec.is_weak=true;
173  else if(type.id() == ID_used)
174  c_storage_spec.is_used = true;
175  else if(type.id()==ID_auto)
176  {
177  // ignore
178  }
179  else if(type.id()==ID_packed)
180  packed=true;
181  else if(type.id()==ID_aligned)
182  {
183  aligned=true;
184 
185  // may come with size or not
186  if(type.find(ID_size).is_nil())
187  alignment=exprt(ID_default);
188  else
189  alignment=static_cast<const exprt &>(type.find(ID_size));
190  }
191  else if(type.id()==ID_transparent_union)
192  {
194  }
195  else if(type.id() == ID_frontend_vector)
196  {
197  // note that this is not yet a vector_typet -- this is a size only
198  vector_size = static_cast<const constant_exprt &>(type.find(ID_size));
199  }
200  else if(type.id()==ID_void)
201  {
202  // we store 'void' as 'empty'
203  typet tmp=type;
204  tmp.id(ID_empty);
205  other.push_back(tmp);
206  }
207  else if(type.id()==ID_msc_declspec)
208  {
209  const exprt &as_expr=
210  static_cast<const exprt &>(static_cast<const irept &>(type));
211 
212  forall_operands(it, as_expr)
213  {
214  // these are symbols
215  const irep_idt &id=it->get(ID_identifier);
216 
217  if(id==ID_thread)
219  else if(id=="align")
220  {
221  aligned=true;
222  alignment = to_unary_expr(*it).op();
223  }
224  }
225  }
226  else if(type.id()==ID_noreturn)
228  else if(type.id()==ID_constructor)
229  constructor=true;
230  else if(type.id()==ID_destructor)
231  destructor=true;
232  else if(
233  type.id() == ID_alias && type.has_subtype() &&
234  to_type_with_subtype(type).subtype().id() == ID_string_constant)
235  {
238  }
239  else if(type.id()==ID_frontend_pointer)
240  {
241  // We turn ID_frontend_pointer to ID_pointer
242  // Pointers have a width, much like integers,
243  // which is added here.
244  pointer_typet tmp(
247  const irep_idt typedef_identifier=type.get(ID_C_typedef);
248  if(!typedef_identifier.empty())
249  tmp.set(ID_C_typedef, typedef_identifier);
250  other.push_back(tmp);
251  }
252  else if(type.id()==ID_pointer)
253  {
254  UNREACHABLE;
255  }
256  else if(type.id() == ID_C_spec_requires)
257  {
258  const exprt &as_expr =
259  static_cast<const exprt &>(static_cast<const irept &>(type));
260  requires.push_back(to_unary_expr(as_expr).op());
261  }
262  else if(type.id() == ID_C_spec_assigns)
263  {
264  const exprt &as_expr =
265  static_cast<const exprt &>(static_cast<const irept &>(type));
266 
267  for(const exprt &target : to_unary_expr(as_expr).op().operands())
268  assigns.push_back(target);
269  }
270  else if(type.id() == ID_C_spec_ensures)
271  {
272  const exprt &as_expr =
273  static_cast<const exprt &>(static_cast<const irept &>(type));
274  ensures.push_back(to_unary_expr(as_expr).op());
275  }
276  else
277  other.push_back(type);
278 }
279 
281 {
282  type.clear();
283 
284  // first, do "other"
285 
286  if(!other.empty())
287  {
288  if(double_cnt || float_cnt || signed_cnt ||
292  gcc_float16_cnt ||
297  {
299  error() << "illegal type modifier for defined type" << eom;
300  throw 0;
301  }
302 
303  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
304  if(other.size()==2)
305  {
306  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
307  other.pop_front();
308  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
309  other.pop_back();
310  }
311 
312  if(other.size()!=1)
313  {
315  error() << "illegal combination of defined types" << eom;
316  throw 0;
317  }
318 
319  type.swap(other.front());
320 
321  // the contract expressions are meant for function types only
322  if(!requires.empty())
323  to_code_with_contract_type(type).requires() = std::move(requires);
324 
325  if(!assigns.empty())
326  to_code_with_contract_type(type).assigns() = std::move(assigns);
327 
328  if(!ensures.empty())
329  to_code_with_contract_type(type).ensures() = std::move(ensures);
330 
331  if(constructor || destructor)
332  {
333  if(constructor && destructor)
334  {
336  error() << "combining constructor and destructor not supported"
337  << eom;
338  throw 0;
339  }
340 
341  typet *type_p=&type;
342  if(type.id()==ID_code)
343  type_p=&(to_code_type(type).return_type());
344 
345  else if(type_p->id()!=ID_empty)
346  {
348  error() << "constructor and destructor required to be type void, "
349  << "found " << type_p->pretty() << eom;
350  throw 0;
351  }
352 
353  type_p->id(constructor ? ID_constructor : ID_destructor);
354  }
355  }
356  else if(constructor || destructor)
357  {
359  error() << "constructor and destructor required to be type void, "
360  << "found " << type.pretty() << eom;
361  throw 0;
362  }
363  else if(gcc_float16_cnt ||
367  {
370  gcc_int128_cnt || bv_cnt ||
371  short_cnt || char_cnt)
372  {
374  error() << "cannot combine integer type with floating-point type" << eom;
375  throw 0;
376  }
377 
378  if(long_cnt+double_cnt+
383  {
385  error() << "conflicting type modifiers" << eom;
386  throw 0;
387  }
388 
389  // _not_ the same as float, double, long double
390  if(gcc_float16_cnt)
391  type=gcc_float16_type();
392  else if(gcc_float32_cnt)
393  type=gcc_float32_type();
394  else if(gcc_float32x_cnt)
395  type=gcc_float32x_type();
396  else if(gcc_float64_cnt)
397  type=gcc_float64_type();
398  else if(gcc_float64x_cnt)
399  type=gcc_float64x_type();
400  else if(gcc_float128_cnt)
401  type=gcc_float128_type();
402  else if(gcc_float128x_cnt)
403  type=gcc_float128x_type();
404  else
405  UNREACHABLE;
406  }
407  else if(double_cnt || float_cnt)
408  {
412  short_cnt || char_cnt)
413  {
415  error() << "cannot combine integer type with floating-point type" << eom;
416  throw 0;
417  }
418 
419  if(double_cnt && float_cnt)
420  {
422  error() << "conflicting type modifiers" << eom;
423  throw 0;
424  }
425 
426  if(long_cnt==0)
427  {
428  if(double_cnt!=0)
429  type=double_type();
430  else
431  type=float_type();
432  }
433  else if(long_cnt==1 || long_cnt==2)
434  {
435  if(double_cnt!=0)
436  type=long_double_type();
437  else
438  {
440  error() << "conflicting type modifiers" << eom;
441  throw 0;
442  }
443  }
444  else
445  {
447  error() << "illegal type modifier for float" << eom;
448  throw 0;
449  }
450  }
451  else if(c_bool_cnt)
452  {
456  char_cnt || long_cnt)
457  {
459  error() << "illegal type modifier for C boolean type" << eom;
460  throw 0;
461  }
462 
463  type=c_bool_type();
464  }
465  else if(proper_bool_cnt)
466  {
470  char_cnt || long_cnt)
471  {
473  error() << "illegal type modifier for proper boolean type" << eom;
474  throw 0;
475  }
476 
477  type.id(ID_bool);
478  }
479  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
481  {
482  // the "default" for complex is double
483  type=double_type();
484  }
485  else if(char_cnt)
486  {
487  if(int_cnt || short_cnt || long_cnt ||
490  {
492  error() << "illegal type modifier for char type" << eom;
493  throw 0;
494  }
495 
496  if(signed_cnt && unsigned_cnt)
497  {
499  error() << "conflicting type modifiers" << eom;
500  throw 0;
501  }
502  else if(unsigned_cnt)
503  type=unsigned_char_type();
504  else if(signed_cnt)
505  type=signed_char_type();
506  else
507  type=char_type();
508  }
509  else
510  {
511  // it is integer -- signed or unsigned?
512 
513  bool is_signed=true; // default
514 
515  if(signed_cnt && unsigned_cnt)
516  {
518  error() << "conflicting type modifiers" << eom;
519  throw 0;
520  }
521  else if(unsigned_cnt)
522  is_signed=false;
523  else if(signed_cnt)
524  is_signed=true;
525 
527  {
529  {
531  error() << "conflicting type modifiers" << eom;
532  throw 0;
533  }
534 
535  if(int8_cnt)
536  if(is_signed)
537  type=signed_char_type();
538  else
539  type=unsigned_char_type();
540  else if(int16_cnt)
541  if(is_signed)
542  type=signed_short_int_type();
543  else
545  else if(int32_cnt)
546  if(is_signed)
547  type=signed_int_type();
548  else
549  type=unsigned_int_type();
550  else if(int64_cnt) // Visual Studio: equivalent to long long int
551  if(is_signed)
553  else
555  else
556  UNREACHABLE;
557  }
558  else if(gcc_int128_cnt)
559  {
560  if(is_signed)
561  type=gcc_signed_int128_type();
562  else
564  }
565  else if(bv_cnt)
566  {
567  // explicitly-given expression for width
568  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
569  type.set(ID_size, bv_width);
570  }
571  else if(floatbv_cnt)
572  {
573  type.id(ID_custom_floatbv);
574  type.set(ID_size, bv_width);
575  type.set(ID_f, fraction_width);
576  }
577  else if(fixedbv_cnt)
578  {
579  type.id(ID_custom_fixedbv);
580  type.set(ID_size, bv_width);
581  type.set(ID_f, fraction_width);
582  }
583  else if(short_cnt)
584  {
585  if(long_cnt || char_cnt)
586  {
588  error() << "conflicting type modifiers" << eom;
589  throw 0;
590  }
591 
592  if(is_signed)
593  type=signed_short_int_type();
594  else
596  }
597  else if(long_cnt==0)
598  {
599  if(is_signed)
600  type=signed_int_type();
601  else
602  type=unsigned_int_type();
603  }
604  else if(long_cnt==1)
605  {
606  if(is_signed)
607  type=signed_long_int_type();
608  else
609  type=unsigned_long_int_type();
610  }
611  else if(long_cnt==2)
612  {
613  if(is_signed)
615  else
617  }
618  else
619  {
621  error() << "illegal type modifier for integer type" << eom;
622  throw 0;
623  }
624  }
625 
627  set_attributes(type);
628 }
629 
632 {
633  if(vector_size.is_not_nil())
634  {
635  type_with_subtypet new_type(ID_frontend_vector, type);
636  new_type.set(ID_size, vector_size);
638  type=new_type;
639  }
640 
641  if(complex_cnt)
642  {
643  // These take more or less arbitrary subtypes.
644  complex_typet new_type(type);
646  type.swap(new_type);
647  }
648 }
649 
652 {
654  {
655  typet new_type=gcc_attribute_mode;
656  new_type.subtype()=type;
657  type.swap(new_type);
658  }
659 
660  c_qualifiers.write(type);
661 
662  if(packed)
663  type.set(ID_C_packed, true);
664 
665  if(aligned)
666  type.set(ID_C_alignment, alignment);
667 }
ANSI-C Language Conversion.
floatbv_typet float_type()
Definition: c_types.cpp:195
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:90
signedbv_typet signed_char_type()
Definition: c_types.cpp:152
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:54
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:111
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:104
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:145
bitvector_typet char_type()
Definition: c_types.cpp:124
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:97
floatbv_typet long_double_type()
Definition: c_types.cpp:211
typet c_bool_type()
Definition: c_types.cpp:118
floatbv_typet double_type()
Definition: c_types.cpp:203
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:47
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:61
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition: c_types.h:418
exprt::operandst ensures
virtual void read_rec(const typet &type)
c_storage_spect c_storage_spec
virtual void read(const typet &type)
virtual void write(typet &type)
exprt::operandst requires
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
exprt::operandst assigns
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:92
virtual void write(typet &src) const override
bool is_transparent_union
Definition: c_qualifiers.h:98
irep_idt asm_label
const typet & return_type() const
Definition: std_types.h:645
const exprt::operandst & requires() const
Definition: c_types.h:379
const exprt::operandst & assigns() const
Definition: c_types.h:369
const exprt::operandst & ensures() const
Definition: c_types.h:389
Complex numbers made of pair of given subtype.
Definition: std_types.h:1057
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2807
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:230
operandst & operands()
Definition: expr.h:92
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void clear()
Definition: irep.h:452
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:376
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: pointer_expr.h:24
const irep_idt & get_value() const
Type with a single subtype.
Definition: type.h:149
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:74
const typet & subtype() const
Definition: type.h:48
bool has_subtype() const
Definition: type.h:66
source_locationt & add_source_location()
Definition: type.h:79
const exprt & op() const
Definition: std_expr.h:293
configt config
Definition: config.cpp:25
#define forall_operands(it, expr)
Definition: expr.h:18
floatbv_typet gcc_float32_type()
Definition: gcc_types.cpp:21
floatbv_typet gcc_float16_type()
Definition: gcc_types.cpp:13
floatbv_typet gcc_float64_type()
Definition: gcc_types.cpp:39
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:82
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:30
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:48
floatbv_typet gcc_float128x_type()
Definition: gcc_types.cpp:66
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:75
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:57
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const string_constantt & to_string_constant(const exprt &expr)
std::size_t pointer_width
Definition: config.h:115
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:221
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45