cprover
Loading...
Searching...
No Matches
ansi_c_convert_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: SpecC Language Conversion
4
5Author: 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>
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)
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)
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)
103 else if(type.id()==ID_gcc_attribute_mode)
104 {
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
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
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
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)
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)
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())
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.
245 to_type_with_subtype(type).subtype(), config.ansi_c.pointer_width);
246 tmp.add_source_location()=type.source_location();
248 if(!typedef_identifier.empty())
250 other.push_back(tmp);
251 }
252 else if(type.id()==ID_pointer)
253 {
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 {
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
332 {
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)
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
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 {
372 {
374 error() << "cannot combine integer type with floating-point type" << eom;
375 throw 0;
376 }
377
383 {
385 error() << "conflicting type modifiers" << eom;
386 throw 0;
387 }
388
389 // _not_ the same as float, double, long double
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
406 }
407 else if(double_cnt || float_cnt)
408 {
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 {
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 {
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
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
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)
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
557 }
558 else if(gcc_int128_cnt)
559 {
560 if(is_signed)
562 else
564 }
565 else if(bv_cnt)
566 {
567 // explicitly-given expression for width
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)
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)
608 else
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{
634 {
637 new_type.add_source_location()=vector_size.source_location();
638 type=new_type;
639 }
640
641 if(complex_cnt)
642 {
643 // These take more or less arbitrary subtypes.
645 new_type.add_source_location()=source_location;
646 type.swap(new_type);
647 }
648}
649
652{
654 {
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)
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
virtual void read_rec(const typet &type)
exprt::operandst 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
virtual void write(typet &src) const override
bool is_transparent_union
const typet & return_type() const
Definition std_types.h:645
const exprt::operandst & assigns() const
Definition c_types.h:369
exprt::operandst &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
Base class for all expressions.
Definition expr.h:54
operandst & operands()
Definition expr.h:92
const source_locationt & source_location() const
Definition expr.h:230
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
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
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 ...
const irep_idt & get_value() const
subtypest & subtypes()
Definition type.h:206
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
bool has_subtype() const
Definition type.h:66
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)
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