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/message.h>
17#include <util/std_types.h>
19
20#include "gcc_types.h"
21
23{
24 if(type.id()==ID_merged_type)
25 {
26 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
27 read_rec(subtype);
28 }
29 else if(type.id()==ID_signed)
30 signed_cnt++;
31 else if(type.id()==ID_unsigned)
33 else if(type.id()==ID_ptr32)
35 else if(type.id()==ID_ptr64)
37 else if(type.id()==ID_volatile)
39 else if(type.id()==ID_asm)
40 {
41 // These can have up to 5 subtypes; we only use the first one.
42 const auto &type_with_subtypes = to_type_with_subtypes(type);
43 if(
44 !type_with_subtypes.subtypes().empty() &&
45 type_with_subtypes.subtypes()[0].id() == ID_string_constant)
47 to_string_constant(type_with_subtypes.subtypes()[0]).get_value();
48 }
49 else if(
50 type.id() == ID_section && type.has_subtype() &&
51 to_type_with_subtype(type).subtype().id() == ID_string_constant)
52 {
54 to_string_constant(to_type_with_subtype(type).subtype()).get_value();
55 }
56 else if(type.id()==ID_const)
58 else if(type.id()==ID_restrict)
60 else if(type.id()==ID_atomic)
62 else if(type.id()==ID_atomic_type_specifier)
63 {
64 // this gets turned into the qualifier, uh
66 read_rec(to_type_with_subtype(type).subtype());
67 }
68 else if(type.id()==ID_char)
69 char_cnt++;
70 else if(type.id()==ID_int)
71 int_cnt++;
72 else if(type.id()==ID_int8)
73 int8_cnt++;
74 else if(type.id()==ID_int16)
75 int16_cnt++;
76 else if(type.id()==ID_int32)
77 int32_cnt++;
78 else if(type.id()==ID_int64)
79 int64_cnt++;
80 else if(type.id()==ID_gcc_float16)
82 else if(type.id()==ID_gcc_float32)
84 else if(type.id()==ID_gcc_float32x)
86 else if(type.id()==ID_gcc_float64)
88 else if(type.id()==ID_gcc_float64x)
90 else if(type.id()==ID_gcc_float128)
92 else if(type.id()==ID_gcc_float128x)
94 else if(type.id()==ID_gcc_int128)
96 else if(type.id()==ID_gcc_attribute_mode)
97 {
99 }
100 else if(type.id()==ID_msc_based)
101 {
102 const exprt &as_expr=
103 static_cast<const exprt &>(static_cast<const irept &>(type));
104 msc_based = to_unary_expr(as_expr).op();
105 }
106 else if(type.id()==ID_custom_bv)
107 {
108 bv_cnt++;
109 const exprt &size_expr=
110 static_cast<const exprt &>(type.find(ID_size));
111
113 }
114 else if(type.id()==ID_custom_floatbv)
115 {
116 floatbv_cnt++;
117
118 const exprt &size_expr=
119 static_cast<const exprt &>(type.find(ID_size));
120 const exprt &fsize_expr=
121 static_cast<const exprt &>(type.find(ID_f));
122
125 }
126 else if(type.id()==ID_custom_fixedbv)
127 {
128 fixedbv_cnt++;
129
130 const exprt &size_expr=
131 static_cast<const exprt &>(type.find(ID_size));
132 const exprt &fsize_expr=
133 static_cast<const exprt &>(type.find(ID_f));
134
137 }
138 else if(type.id()==ID_short)
139 short_cnt++;
140 else if(type.id()==ID_long)
141 long_cnt++;
142 else if(type.id()==ID_double)
143 double_cnt++;
144 else if(type.id()==ID_float)
145 float_cnt++;
146 else if(type.id()==ID_c_bool)
147 c_bool_cnt++;
148 else if(type.id()==ID_proper_bool)
150 else if(type.id()==ID_complex)
151 complex_cnt++;
152 else if(type.id()==ID_static)
154 else if(type.id()==ID_thread_local)
156 else if(type.id()==ID_inline)
158 else if(type.id()==ID_extern)
160 else if(type.id()==ID_typedef)
162 else if(type.id()==ID_register)
164 else if(type.id()==ID_weak)
166 else if(type.id() == ID_used)
167 c_storage_spec.is_used = true;
168 else if(type.id()==ID_auto)
169 {
170 // ignore
171 }
172 else if(type.id()==ID_packed)
173 packed=true;
174 else if(type.id()==ID_aligned)
175 {
176 aligned=true;
177
178 // may come with size or not
179 if(type.find(ID_size).is_nil())
181 else
182 alignment=static_cast<const exprt &>(type.find(ID_size));
183 }
184 else if(type.id()==ID_transparent_union)
185 {
187 }
188 else if(type.id() == ID_frontend_vector)
189 {
190 // note that this is not yet a vector_typet -- this is a size only
191 vector_size = static_cast<const constant_exprt &>(type.find(ID_size));
192 }
193 else if(type.id()==ID_void)
194 {
195 // we store 'void' as 'empty'
196 typet tmp=type;
197 tmp.id(ID_empty);
198 other.push_back(tmp);
199 }
200 else if(type.id()==ID_msc_declspec)
201 {
202 const exprt &as_expr=
203 static_cast<const exprt &>(static_cast<const irept &>(type));
204
205 for(const auto &op : as_expr.operands())
206 {
207 // these are symbols
208 const irep_idt &id = op.get(ID_identifier);
209
210 if(id==ID_thread)
212 else if(id=="align")
213 {
214 aligned=true;
215 alignment = to_unary_expr(op).op();
216 }
217 }
218 }
219 else if(type.id()==ID_noreturn)
221 else if(type.id()==ID_constructor)
222 constructor=true;
223 else if(type.id()==ID_destructor)
224 destructor=true;
225 else if(
226 type.id() == ID_alias && type.has_subtype() &&
227 to_type_with_subtype(type).subtype().id() == ID_string_constant)
228 {
230 to_string_constant(to_type_with_subtype(type).subtype()).get_value();
231 }
232 else if(type.id()==ID_frontend_pointer)
233 {
234 // We turn ID_frontend_pointer to ID_pointer
235 // Pointers have a width, much like integers,
236 // which is added here.
238 to_type_with_subtype(type).subtype(), config.ansi_c.pointer_width);
239 tmp.add_source_location()=type.source_location();
241 if(!typedef_identifier.empty())
243 other.push_back(tmp);
244 }
245 else if(type.id()==ID_pointer)
246 {
248 }
249 else if(type.id() == ID_C_spec_requires)
250 {
251 const exprt &as_expr =
252 static_cast<const exprt &>(static_cast<const irept &>(type));
253 c_requires.push_back(to_unary_expr(as_expr).op());
254 }
255 else if(type.id() == ID_C_spec_assigns)
256 {
257 const exprt &as_expr =
258 static_cast<const exprt &>(static_cast<const irept &>(type));
259
260 for(const exprt &target : to_unary_expr(as_expr).op().operands())
261 c_assigns.push_back(target);
262 }
263 else if(type.id() == ID_C_spec_frees)
264 {
265 const exprt &as_expr =
266 static_cast<const exprt &>(static_cast<const irept &>(type));
267
268 for(const exprt &target : to_unary_expr(as_expr).op().operands())
269 c_frees.push_back(target);
270 }
271 else if(type.id() == ID_C_spec_ensures)
272 {
273 const exprt &as_expr =
274 static_cast<const exprt &>(static_cast<const irept &>(type));
275 c_ensures.push_back(to_unary_expr(as_expr).op());
276 }
277 else
278 other.push_back(type);
279}
280
282{
284
285 type.clear();
286
287 // first, do "other"
288
289 if(!other.empty())
290 {
300 {
301 log.error().source_location = source_location;
302 log.error() << "illegal type modifier for defined type" << messaget::eom;
303 throw 0;
304 }
305
306 // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
307 if(other.size()==2)
308 {
309 if(other.front().id()==ID_asm && other.back().id()==ID_empty)
310 other.pop_front();
311 else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
312 other.pop_back();
313 }
314
315 if(other.size()!=1)
316 {
317 log.error().source_location = source_location;
318 log.error() << "illegal combination of defined types" << messaget::eom;
319 throw 0;
320 }
321
322 type.swap(other.front());
323
324 // the contract expressions are meant for function types only
325 if(!c_requires.empty())
326 to_code_with_contract_type(type).c_requires() = std::move(c_requires);
327
328 if(!c_assigns.empty())
329 to_code_with_contract_type(type).c_assigns() = std::move(c_assigns);
330
331 if(!c_frees.empty())
332 to_code_with_contract_type(type).c_frees() = std::move(c_frees);
333
334 if(!c_ensures.empty())
335 to_code_with_contract_type(type).c_ensures() = std::move(c_ensures);
336
338 {
340 {
341 log.error().source_location = source_location;
342 log.error() << "combining constructor and destructor not supported"
343 << messaget::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 {
353 log.error().source_location = source_location;
354 log.error() << "constructor and destructor required to be type void, "
355 << "found " << type_p->pretty() << messaget::eom;
356 throw 0;
357 }
358
360 }
361 }
362 else if(constructor || destructor)
363 {
364 log.error().source_location = source_location;
365 log.error() << "constructor and destructor required to be type void, "
366 << "found " << type.pretty() << messaget::eom;
367 throw 0;
368 }
369 else if(gcc_float16_cnt ||
373 {
378 {
379 log.error().source_location = source_location;
380 log.error() << "cannot combine integer type with floating-point type"
381 << messaget::eom;
382 throw 0;
383 }
384
390 {
391 log.error().source_location = source_location;
392 log.error() << "conflicting type modifiers" << messaget::eom;
393 throw 0;
394 }
395
396 // _not_ the same as float, double, long double
398 type=gcc_float16_type();
399 else if(gcc_float32_cnt)
400 type=gcc_float32_type();
401 else if(gcc_float32x_cnt)
402 type=gcc_float32x_type();
403 else if(gcc_float64_cnt)
404 type=gcc_float64_type();
405 else if(gcc_float64x_cnt)
406 type=gcc_float64x_type();
407 else if(gcc_float128_cnt)
408 type=gcc_float128_type();
409 else if(gcc_float128x_cnt)
410 type=gcc_float128x_type();
411 else
413 }
414 else if(double_cnt || float_cnt)
415 {
420 {
421 log.error().source_location = source_location;
422 log.error() << "cannot combine integer type with floating-point type"
423 << messaget::eom;
424 throw 0;
425 }
426
427 if(double_cnt && float_cnt)
428 {
429 log.error().source_location = source_location;
430 log.error() << "conflicting type modifiers" << messaget::eom;
431 throw 0;
432 }
433
434 if(long_cnt==0)
435 {
436 if(double_cnt!=0)
437 type=double_type();
438 else
439 type=float_type();
440 }
441 else if(long_cnt==1 || long_cnt==2)
442 {
443 if(double_cnt!=0)
444 type=long_double_type();
445 else
446 {
447 log.error().source_location = source_location;
448 log.error() << "conflicting type modifiers" << messaget::eom;
449 throw 0;
450 }
451 }
452 else
453 {
454 log.error().source_location = source_location;
455 log.error() << "illegal type modifier for float" << messaget::eom;
456 throw 0;
457 }
458 }
459 else if(c_bool_cnt)
460 {
465 {
466 log.error().source_location = source_location;
467 log.error() << "illegal type modifier for C boolean type"
468 << messaget::eom;
469 throw 0;
470 }
471
472 type=c_bool_type();
473 }
474 else if(proper_bool_cnt)
475 {
480 {
481 log.error().source_location = source_location;
482 log.error() << "illegal type modifier for proper boolean type"
483 << messaget::eom;
484 throw 0;
485 }
486
487 type.id(ID_bool);
488 }
489 else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
491 {
492 // the "default" for complex is double
493 type=double_type();
494 }
495 else if(char_cnt)
496 {
497 if(int_cnt || short_cnt || long_cnt ||
500 {
501 log.error().source_location = source_location;
502 log.error() << "illegal type modifier for char type" << messaget::eom;
503 throw 0;
504 }
505
507 {
508 log.error().source_location = source_location;
509 log.error() << "conflicting type modifiers" << messaget::eom;
510 throw 0;
511 }
512 else if(unsigned_cnt)
513 type=unsigned_char_type();
514 else if(signed_cnt)
515 type=signed_char_type();
516 else
517 type=char_type();
518 }
519 else
520 {
521 // it is integer -- signed or unsigned?
522
523 bool is_signed=true; // default
524
526 {
527 log.error().source_location = source_location;
528 log.error() << "conflicting type modifiers" << messaget::eom;
529 throw 0;
530 }
531 else if(unsigned_cnt)
532 is_signed=false;
533 else if(signed_cnt)
534 is_signed=true;
535
537 {
539 {
540 log.error().source_location = source_location;
541 log.error() << "conflicting type modifiers" << messaget::eom;
542 throw 0;
543 }
544
545 if(int8_cnt)
546 if(is_signed)
547 type=signed_char_type();
548 else
549 type=unsigned_char_type();
550 else if(int16_cnt)
551 if(is_signed)
553 else
555 else if(int32_cnt)
556 if(is_signed)
557 type=signed_int_type();
558 else
559 type=unsigned_int_type();
560 else if(int64_cnt) // Visual Studio: equivalent to long long int
561 if(is_signed)
563 else
565 else
567 }
568 else if(gcc_int128_cnt)
569 {
570 if(is_signed)
572 else
574 }
575 else if(bv_cnt)
576 {
577 // explicitly-given expression for width
579 type.set(ID_size, bv_width);
580 }
581 else if(floatbv_cnt)
582 {
583 type.id(ID_custom_floatbv);
584 type.set(ID_size, bv_width);
585 type.set(ID_f, fraction_width);
586 }
587 else if(fixedbv_cnt)
588 {
589 type.id(ID_custom_fixedbv);
590 type.set(ID_size, bv_width);
591 type.set(ID_f, fraction_width);
592 }
593 else if(short_cnt)
594 {
595 if(long_cnt || char_cnt)
596 {
597 log.error().source_location = source_location;
598 log.error() << "conflicting type modifiers" << messaget::eom;
599 throw 0;
600 }
601
602 if(is_signed)
604 else
606 }
607 else if(long_cnt==0)
608 {
609 if(is_signed)
610 type=signed_int_type();
611 else
612 type=unsigned_int_type();
613 }
614 else if(long_cnt==1)
615 {
616 if(is_signed)
618 else
620 }
621 else if(long_cnt==2)
622 {
623 if(is_signed)
625 else
627 }
628 else
629 {
630 log.error().source_location = source_location;
631 log.error() << "illegal type modifier for integer type" << messaget::eom;
632 throw 0;
633 }
634 }
635
637 set_attributes(type);
638}
639
642{
644 {
647 new_type.add_source_location()=vector_size.source_location();
648 type=new_type;
649 }
650
651 if(complex_cnt)
652 {
653 // These take more or less arbitrary subtypes.
655 new_type.add_source_location()=source_location;
656 type.swap(new_type);
657 }
658}
659
662{
664 {
666 new_type.add_subtype() = type;
667 type.swap(new_type);
668 }
669
670 c_qualifiers.write(type);
671
672 if(packed)
673 type.set(ID_C_packed, true);
674
675 if(aligned)
677}
ANSI-C Language Conversion.
configt config
Definition config.cpp:25
floatbv_typet float_type()
Definition c_types.cpp:182
signedbv_typet signed_long_int_type()
Definition c_types.cpp:77
signedbv_typet signed_char_type()
Definition c_types.cpp:139
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:98
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:91
signedbv_typet signed_int_type()
Definition c_types.cpp:27
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
bitvector_typet char_type()
Definition c_types.cpp:111
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:84
floatbv_typet long_double_type()
Definition c_types.cpp:198
typet c_bool_type()
Definition c_types.cpp:105
floatbv_typet double_type()
Definition c_types.cpp:190
signedbv_typet signed_short_int_type()
Definition c_types.cpp:34
unsignedbv_typet unsigned_short_int_type()
Definition c_types.cpp:48
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:467
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
virtual void read_rec(const typet &type)
c_storage_spect c_storage_spec
exprt::operandst c_ensures
virtual void write(typet &type)
message_handlert & message_handler
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
exprt::operandst c_requires
source_locationt source_location
exprt::operandst c_assigns
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
Complex numbers made of pair of given subtype.
Definition std_types.h:1077
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
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:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Type with a single subtype.
Definition type.h:147
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
bool has_subtype() const
Definition type.h:64
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:525
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
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:219
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45