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_types.h>
17 #include <util/string_constant.h>
18 
19 #include "gcc_types.h"
20 
22 {
23  clear();
25  read_rec(type);
26 }
27 
29 {
30  if(type.id()==ID_merged_type)
31  {
32  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
33  read_rec(subtype);
34  }
35  else if(type.id()==ID_signed)
36  signed_cnt++;
37  else if(type.id()==ID_unsigned)
38  unsigned_cnt++;
39  else if(type.id()==ID_ptr32)
41  else if(type.id()==ID_ptr64)
43  else if(type.id()==ID_volatile)
45  else if(type.id()==ID_asm)
46  {
47  if(type.has_subtype() &&
48  type.subtype().id()==ID_string_constant)
50  }
51  else if(type.id()==ID_section &&
52  type.has_subtype() &&
53  type.subtype().id()==ID_string_constant)
54  {
56  }
57  else if(type.id()==ID_const)
59  else if(type.id()==ID_restrict)
61  else if(type.id()==ID_atomic)
63  else if(type.id()==ID_atomic_type_specifier)
64  {
65  // this gets turned into the qualifier, uh
67  read_rec(type.subtype());
68  }
69  else if(type.id()==ID_char)
70  char_cnt++;
71  else if(type.id()==ID_int)
72  int_cnt++;
73  else if(type.id()==ID_int8)
74  int8_cnt++;
75  else if(type.id()==ID_int16)
76  int16_cnt++;
77  else if(type.id()==ID_int32)
78  int32_cnt++;
79  else if(type.id()==ID_int64)
80  int64_cnt++;
81  else if(type.id()==ID_gcc_float16)
83  else if(type.id()==ID_gcc_float32)
85  else if(type.id()==ID_gcc_float32x)
87  else if(type.id()==ID_gcc_float64)
89  else if(type.id()==ID_gcc_float64x)
91  else if(type.id()==ID_gcc_float128)
93  else if(type.id()==ID_gcc_float128x)
95  else if(type.id()==ID_gcc_int128)
97  else if(type.id()==ID_gcc_attribute_mode)
98  {
99  gcc_attribute_mode=type;
100  }
101  else if(type.id()==ID_msc_based)
102  {
103  const exprt &as_expr=
104  static_cast<const exprt &>(static_cast<const irept &>(type));
105  msc_based = to_unary_expr(as_expr).op();
106  }
107  else if(type.id()==ID_custom_bv)
108  {
109  bv_cnt++;
110  const exprt &size_expr=
111  static_cast<const exprt &>(type.find(ID_size));
112 
113  bv_width=size_expr;
114  }
115  else if(type.id()==ID_custom_floatbv)
116  {
117  floatbv_cnt++;
118 
119  const exprt &size_expr=
120  static_cast<const exprt &>(type.find(ID_size));
121  const exprt &fsize_expr=
122  static_cast<const exprt &>(type.find(ID_f));
123 
124  bv_width=size_expr;
125  fraction_width=fsize_expr;
126  }
127  else if(type.id()==ID_custom_fixedbv)
128  {
129  fixedbv_cnt++;
130 
131  const exprt &size_expr=
132  static_cast<const exprt &>(type.find(ID_size));
133  const exprt &fsize_expr=
134  static_cast<const exprt &>(type.find(ID_f));
135 
136  bv_width=size_expr;
137  fraction_width=fsize_expr;
138  }
139  else if(type.id()==ID_short)
140  short_cnt++;
141  else if(type.id()==ID_long)
142  long_cnt++;
143  else if(type.id()==ID_double)
144  double_cnt++;
145  else if(type.id()==ID_float)
146  float_cnt++;
147  else if(type.id()==ID_c_bool)
148  c_bool_cnt++;
149  else if(type.id()==ID_proper_bool)
150  proper_bool_cnt++;
151  else if(type.id()==ID_complex)
152  complex_cnt++;
153  else if(type.id()==ID_static)
155  else if(type.id()==ID_thread_local)
157  else if(type.id()==ID_inline)
159  else if(type.id()==ID_extern)
161  else if(type.id()==ID_typedef)
163  else if(type.id()==ID_register)
165  else if(type.id()==ID_weak)
166  c_storage_spec.is_weak=true;
167  else if(type.id() == ID_used)
168  c_storage_spec.is_used = true;
169  else if(type.id()==ID_auto)
170  {
171  // ignore
172  }
173  else if(type.id()==ID_packed)
174  packed=true;
175  else if(type.id()==ID_aligned)
176  {
177  aligned=true;
178 
179  // may come with size or not
180  if(type.find(ID_size).is_nil())
181  alignment=exprt(ID_default);
182  else
183  alignment=static_cast<const exprt &>(type.find(ID_size));
184  }
185  else if(type.id()==ID_transparent_union)
186  {
188  }
189  else if(type.id()==ID_vector)
191  else if(type.id()==ID_void)
192  {
193  // we store 'void' as 'empty'
194  typet tmp=type;
195  tmp.id(ID_empty);
196  other.push_back(tmp);
197  }
198  else if(type.id()==ID_msc_declspec)
199  {
200  const exprt &as_expr=
201  static_cast<const exprt &>(static_cast<const irept &>(type));
202 
203  forall_operands(it, as_expr)
204  {
205  // these are symbols
206  const irep_idt &id=it->get(ID_identifier);
207 
208  if(id==ID_thread)
210  else if(id=="align")
211  {
212  aligned=true;
213  alignment = to_unary_expr(*it).op();
214  }
215  }
216  }
217  else if(type.id()==ID_noreturn)
219  else if(type.id()==ID_constructor)
220  constructor=true;
221  else if(type.id()==ID_destructor)
222  destructor=true;
223  else if(type.id()==ID_alias &&
224  type.has_subtype() &&
225  type.subtype().id()==ID_string_constant)
226  {
228  }
229  else if(type.id()==ID_frontend_pointer)
230  {
231  // We turn ID_frontend_pointer to ID_pointer
232  // Pointers have a width, much like integers,
233  // which is added here.
236  const irep_idt typedef_identifier=type.get(ID_C_typedef);
237  if(!typedef_identifier.empty())
238  tmp.set(ID_C_typedef, typedef_identifier);
239  other.push_back(tmp);
240  }
241  else if(type.id()==ID_pointer)
242  {
243  UNREACHABLE;
244  }
245  else if(type.id() == ID_C_spec_requires)
246  {
247  const exprt &as_expr =
248  static_cast<const exprt &>(static_cast<const irept &>(type));
249  requires.push_back(to_unary_expr(as_expr).op());
250  }
251  else if(type.id() == ID_C_spec_assigns)
252  {
253  const exprt &as_expr =
254  static_cast<const exprt &>(static_cast<const irept &>(type));
255 
256  for(const exprt &operand : to_unary_expr(as_expr).op().operands())
257  {
258  if(
259  operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
260  operand.id() != ID_member && operand.id() != ID_dereference)
261  {
263  error() << "illegal target in assigns clause" << eom;
264  throw 0;
265  }
266  }
267 
268  if(assigns.is_nil())
269  assigns = to_unary_expr(as_expr).op();
270  else
271  {
272  for(auto &assignment : to_unary_expr(as_expr).op().operands())
273  assigns.add_to_operands(std::move(assignment));
274  }
275  }
276  else if(type.id() == ID_C_spec_ensures)
277  {
278  const exprt &as_expr =
279  static_cast<const exprt &>(static_cast<const irept &>(type));
280  ensures.push_back(to_unary_expr(as_expr).op());
281  }
282  else
283  other.push_back(type);
284 }
285 
287 {
288  type.clear();
289 
290  // first, do "other"
291 
292  if(!other.empty())
293  {
294  if(double_cnt || float_cnt || signed_cnt ||
298  gcc_float16_cnt ||
303  {
305  error() << "illegal type modifier for defined type" << eom;
306  throw 0;
307  }
308 
309  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
310  if(other.size()==2)
311  {
312  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
313  other.pop_front();
314  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
315  other.pop_back();
316  }
317 
318  if(other.size()!=1)
319  {
321  error() << "illegal combination of defined types" << eom;
322  throw 0;
323  }
324 
325  type.swap(other.front());
326 
327  // the contract expressions are meant for function types only
328  if(!requires.empty())
329  to_code_with_contract_type(type).requires() = std::move(requires);
330 
331  if(assigns.is_not_nil())
332  to_code_with_contract_type(type).assigns() = std::move(assigns);
333 
334  if(!ensures.empty())
335  to_code_with_contract_type(type).ensures() = std::move(ensures);
336 
337  if(constructor || destructor)
338  {
339  if(constructor && destructor)
340  {
342  error() << "combining constructor and destructor not supported"
343  << eom;
344  throw 0;
345  }
346 
347  typet *type_p=&type;
348  if(type.id()==ID_code)
349  type_p=&(to_code_type(type).return_type());
350 
351  else if(type_p->id()!=ID_empty)
352  {
354  error() << "constructor and destructor required to be type void, "
355  << "found " << type_p->pretty() << eom;
356  throw 0;
357  }
358 
359  type_p->id(constructor ? ID_constructor : ID_destructor);
360  }
361  }
362  else if(constructor || destructor)
363  {
365  error() << "constructor and destructor required to be type void, "
366  << "found " << type.pretty() << eom;
367  throw 0;
368  }
369  else if(gcc_float16_cnt ||
373  {
376  gcc_int128_cnt || bv_cnt ||
377  short_cnt || char_cnt)
378  {
380  error() << "cannot combine integer type with floating-point type" << eom;
381  throw 0;
382  }
383 
384  if(long_cnt+double_cnt+
389  {
391  error() << "conflicting type modifiers" << eom;
392  throw 0;
393  }
394 
395  // _not_ the same as float, double, long double
396  if(gcc_float16_cnt)
397  type=gcc_float16_type();
398  else if(gcc_float32_cnt)
399  type=gcc_float32_type();
400  else if(gcc_float32x_cnt)
401  type=gcc_float32x_type();
402  else if(gcc_float64_cnt)
403  type=gcc_float64_type();
404  else if(gcc_float64x_cnt)
405  type=gcc_float64x_type();
406  else if(gcc_float128_cnt)
407  type=gcc_float128_type();
408  else if(gcc_float128x_cnt)
409  type=gcc_float128x_type();
410  else
411  UNREACHABLE;
412  }
413  else if(double_cnt || float_cnt)
414  {
418  short_cnt || char_cnt)
419  {
421  error() << "cannot combine integer type with floating-point type" << eom;
422  throw 0;
423  }
424 
425  if(double_cnt && float_cnt)
426  {
428  error() << "conflicting type modifiers" << eom;
429  throw 0;
430  }
431 
432  if(long_cnt==0)
433  {
434  if(double_cnt!=0)
435  type=double_type();
436  else
437  type=float_type();
438  }
439  else if(long_cnt==1 || long_cnt==2)
440  {
441  if(double_cnt!=0)
442  type=long_double_type();
443  else
444  {
446  error() << "conflicting type modifiers" << eom;
447  throw 0;
448  }
449  }
450  else
451  {
453  error() << "illegal type modifier for float" << eom;
454  throw 0;
455  }
456  }
457  else if(c_bool_cnt)
458  {
462  char_cnt || long_cnt)
463  {
465  error() << "illegal type modifier for C boolean type" << eom;
466  throw 0;
467  }
468 
469  type=c_bool_type();
470  }
471  else if(proper_bool_cnt)
472  {
476  char_cnt || long_cnt)
477  {
479  error() << "illegal type modifier for proper boolean type" << eom;
480  throw 0;
481  }
482 
483  type.id(ID_bool);
484  }
485  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
487  {
488  // the "default" for complex is double
489  type=double_type();
490  }
491  else if(char_cnt)
492  {
493  if(int_cnt || short_cnt || long_cnt ||
496  {
498  error() << "illegal type modifier for char type" << eom;
499  throw 0;
500  }
501 
502  if(signed_cnt && unsigned_cnt)
503  {
505  error() << "conflicting type modifiers" << eom;
506  throw 0;
507  }
508  else if(unsigned_cnt)
509  type=unsigned_char_type();
510  else if(signed_cnt)
511  type=signed_char_type();
512  else
513  type=char_type();
514  }
515  else
516  {
517  // it is integer -- signed or unsigned?
518 
519  bool is_signed=true; // default
520 
521  if(signed_cnt && unsigned_cnt)
522  {
524  error() << "conflicting type modifiers" << eom;
525  throw 0;
526  }
527  else if(unsigned_cnt)
528  is_signed=false;
529  else if(signed_cnt)
530  is_signed=true;
531 
533  {
535  {
537  error() << "conflicting type modifiers" << eom;
538  throw 0;
539  }
540 
541  if(int8_cnt)
542  if(is_signed)
543  type=signed_char_type();
544  else
545  type=unsigned_char_type();
546  else if(int16_cnt)
547  if(is_signed)
548  type=signed_short_int_type();
549  else
551  else if(int32_cnt)
552  if(is_signed)
553  type=signed_int_type();
554  else
555  type=unsigned_int_type();
556  else if(int64_cnt) // Visual Studio: equivalent to long long int
557  if(is_signed)
559  else
561  else
562  UNREACHABLE;
563  }
564  else if(gcc_int128_cnt)
565  {
566  if(is_signed)
567  type=gcc_signed_int128_type();
568  else
570  }
571  else if(bv_cnt)
572  {
573  // explicitly-given expression for width
574  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
575  type.set(ID_size, bv_width);
576  }
577  else if(floatbv_cnt)
578  {
579  type.id(ID_custom_floatbv);
580  type.set(ID_size, bv_width);
581  type.set(ID_f, fraction_width);
582  }
583  else if(fixedbv_cnt)
584  {
585  type.id(ID_custom_fixedbv);
586  type.set(ID_size, bv_width);
587  type.set(ID_f, fraction_width);
588  }
589  else if(short_cnt)
590  {
591  if(long_cnt || char_cnt)
592  {
594  error() << "conflicting type modifiers" << eom;
595  throw 0;
596  }
597 
598  if(is_signed)
599  type=signed_short_int_type();
600  else
602  }
603  else if(long_cnt==0)
604  {
605  if(is_signed)
606  type=signed_int_type();
607  else
608  type=unsigned_int_type();
609  }
610  else if(long_cnt==1)
611  {
612  if(is_signed)
613  type=signed_long_int_type();
614  else
615  type=unsigned_long_int_type();
616  }
617  else if(long_cnt==2)
618  {
619  if(is_signed)
621  else
623  }
624  else
625  {
627  error() << "illegal type modifier for integer type" << eom;
628  throw 0;
629  }
630  }
631 
633  set_attributes(type);
634 }
635 
638 {
639  if(vector_size.is_not_nil())
640  {
641  type_with_subtypet new_type(ID_frontend_vector, type);
642  new_type.set(ID_size, vector_size);
644  type=new_type;
645  }
646 
647  if(complex_cnt)
648  {
649  // These take more or less arbitrary subtypes.
650  complex_typet new_type(type);
652  type.swap(new_type);
653  }
654 }
655 
658 {
660  {
661  typet new_type=gcc_attribute_mode;
662  new_type.subtype()=type;
663  type.swap(new_type);
664  }
665 
666  c_qualifiers.write(type);
667 
668  if(packed)
669  type.set(ID_C_packed, true);
670 
671  if(aligned)
672  type.set(ID_C_alignment, alignment);
673 }
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
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:399
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.
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:360
const exprt & assigns() const
Definition: c_types.h:347
const exprt::operandst & ensures() const
Definition: c_types.h:370
Complex numbers made of pair of given subtype.
Definition: std_types.h:1015
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:230
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
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:495
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:106
void clear()
Definition: irep.h:463
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:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
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: pointer_expr.h:24
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:293
const constant_exprt & size() const
Definition: std_types.cpp:239
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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
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:116
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