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)
34 c_qualifiers.is_ptr32=true;
35 else if(type.id()==ID_ptr64)
36 c_qualifiers.is_ptr64=true;
37 else if(type.id()==ID_volatile)
38 c_qualifiers.is_volatile=true;
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)
46 c_storage_spec.asm_label =
47 to_string_constant(type_with_subtypes.subtypes()[0]).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 {
53 c_storage_spec.section =
55 }
56 else if(type.id()==ID_const)
57 c_qualifiers.is_constant=true;
58 else if(type.id()==ID_restrict)
59 c_qualifiers.is_restricted=true;
60 else if(type.id()==ID_atomic)
61 c_qualifiers.is_atomic=true;
62 else if(type.id()==ID_atomic_type_specifier)
63 {
64 // this gets turned into the qualifier, uh
65 c_qualifiers.is_atomic=true;
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_c_bitint)
81 {
82 bitint_cnt++;
83 const exprt &size_expr = static_cast<const exprt &>(type.find(ID_size));
84
85 bv_width = size_expr;
86 }
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
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)
157 else if(type.id()==ID_complex)
158 complex_cnt++;
159 else if(type.id()==ID_static)
160 c_storage_spec.is_static=true;
161 else if(type.id()==ID_thread_local)
162 c_storage_spec.is_thread_local=true;
163 else if(type.id()==ID_inline)
164 c_storage_spec.is_inline=true;
165 else if(type.id()==ID_extern)
166 c_storage_spec.is_extern=true;
167 else if(type.id()==ID_typedef)
168 c_storage_spec.is_typedef=true;
169 else if(type.id()==ID_register)
170 c_storage_spec.is_register=true;
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 {
193 c_qualifiers.is_transparent_union=true;
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 for(const auto &op : as_expr.operands())
213 {
214 // these are symbols
215 const irep_idt &id = op.get(ID_identifier);
216
217 if(id==ID_thread)
218 c_storage_spec.is_thread_local=true;
219 else if(id=="align")
220 {
221 aligned=true;
222 alignment = to_unary_expr(op).op();
223 }
224 }
225 }
226 else if(type.id() == ID_nodiscard)
227 c_qualifiers.is_nodiscard = true;
228 else if(type.id()==ID_noreturn)
229 c_qualifiers.is_noreturn=true;
230 else if(type.id()==ID_constructor)
231 constructor=true;
232 else if(type.id()==ID_destructor)
233 destructor=true;
234 else if(
235 type.id() == ID_alias && type.has_subtype() &&
236 to_type_with_subtype(type).subtype().id() == ID_string_constant)
237 {
238 c_storage_spec.alias =
240 }
241 else if(type.id()==ID_frontend_pointer)
242 {
243 // We turn ID_frontend_pointer to ID_pointer
244 // Pointers have a width, much like integers,
245 // which is added here.
246 pointer_typet tmp(
247 to_type_with_subtype(type).subtype(), config.ansi_c.pointer_width);
249 const irep_idt typedef_identifier=type.get(ID_C_typedef);
250 if(!typedef_identifier.empty())
251 tmp.set(ID_C_typedef, typedef_identifier);
252 other.push_back(tmp);
253 }
254 else if(type.id()==ID_pointer)
255 {
257 }
258 else if(type.id() == ID_C_spec_requires)
259 {
260 const exprt &as_expr =
261 static_cast<const exprt &>(static_cast<const irept &>(type));
262 c_requires.push_back(to_unary_expr(as_expr).op());
263 }
264 else if(type.id() == ID_C_spec_assigns)
265 {
266 const exprt &as_expr =
267 static_cast<const exprt &>(static_cast<const irept &>(type));
268
269 for(const exprt &target : to_unary_expr(as_expr).op().operands())
270 c_assigns.push_back(target);
271 }
272 else if(type.id() == ID_C_spec_frees)
273 {
274 const exprt &as_expr =
275 static_cast<const exprt &>(static_cast<const irept &>(type));
276
277 for(const exprt &target : to_unary_expr(as_expr).op().operands())
278 c_frees.push_back(target);
279 }
280 else if(type.id() == ID_C_spec_ensures)
281 {
282 const exprt &as_expr =
283 static_cast<const exprt &>(static_cast<const irept &>(type));
284 c_ensures.push_back(to_unary_expr(as_expr).op());
285 }
286 else
287 other.push_back(type);
288}
289
291{
293
294 type.clear();
295
296 // first, do "other"
297
298 if(!other.empty())
299 {
300 if(
307 {
309 log.error() << "illegal type modifier for defined type" << messaget::eom;
310 throw 0;
311 }
312
313 // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
314 if(other.size()==2)
315 {
316 if(other.front().id()==ID_asm && other.back().id()==ID_empty)
317 other.pop_front();
318 else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
319 other.pop_back();
320 }
321
322 if(other.size()!=1)
323 {
325 log.error() << "illegal combination of defined types" << messaget::eom;
326 throw 0;
327 }
328
329 type.swap(other.front());
330
331 // the contract expressions are meant for function types only
332 if(!c_requires.empty())
334
335 if(!c_assigns.empty())
337
338 if(!c_frees.empty())
339 to_code_with_contract_type(type).c_frees() = std::move(c_frees);
340
341 if(!c_ensures.empty())
343
345 {
347 {
349 log.error() << "combining constructor and destructor not supported"
350 << messaget::eom;
351 throw 0;
352 }
353
354 typet *type_p=&type;
355 if(type.id()==ID_code)
356 type_p=&(to_code_type(type).return_type());
357
358 else if(type_p->id()!=ID_empty)
359 {
361 log.error() << "constructor and destructor required to be type void, "
362 << "found " << type_p->pretty() << messaget::eom;
363 throw 0;
364 }
365
366 type_p->id(constructor ? ID_constructor : ID_destructor);
367 }
368 }
369 else if(constructor || destructor)
370 {
372 log.error() << "constructor and destructor required to be type void, "
373 << "found " << type.pretty() << messaget::eom;
374 throw 0;
375 }
376 else if(gcc_float16_cnt ||
380 {
381 if(
385 {
387 log.error() << "cannot combine integer type with floating-point type"
388 << messaget::eom;
389 throw 0;
390 }
391
397 {
399 log.error() << "conflicting type modifiers" << messaget::eom;
400 throw 0;
401 }
402
403 // _not_ the same as float, double, long double
405 type=gcc_float16_type();
406 else if(gcc_float32_cnt)
407 type=gcc_float32_type();
408 else if(gcc_float32x_cnt)
409 type=gcc_float32x_type();
410 else if(gcc_float64_cnt)
411 type=gcc_float64_type();
412 else if(gcc_float64x_cnt)
413 type=gcc_float64x_type();
414 else if(gcc_float128_cnt)
415 type=gcc_float128_type();
416 else if(gcc_float128x_cnt)
417 type=gcc_float128x_type();
418 else
420 }
421 else if(double_cnt || float_cnt)
422 {
423 if(
427 {
429 log.error() << "cannot combine integer type with floating-point type"
430 << messaget::eom;
431 throw 0;
432 }
433
434 if(double_cnt && float_cnt)
435 {
437 log.error() << "conflicting type modifiers" << messaget::eom;
438 throw 0;
439 }
440
441 if(long_cnt==0)
442 {
443 if(double_cnt!=0)
444 type=double_type();
445 else
446 type=float_type();
447 }
448 else if(long_cnt==1 || long_cnt==2)
449 {
450 if(double_cnt!=0)
451 type=long_double_type();
452 else
453 {
455 log.error() << "conflicting type modifiers" << messaget::eom;
456 throw 0;
457 }
458 }
459 else
460 {
462 log.error() << "illegal type modifier for float" << messaget::eom;
463 throw 0;
464 }
465 }
466 else if(c_bool_cnt)
467 {
468 if(
472 {
474 log.error() << "illegal type modifier for C boolean type"
475 << messaget::eom;
476 throw 0;
477 }
478
479 type=c_bool_type();
480 }
481 else if(proper_bool_cnt)
482 {
483 if(
487 {
489 log.error() << "illegal type modifier for proper boolean type"
490 << messaget::eom;
491 throw 0;
492 }
493
494 type.id(ID_bool);
495 }
496 else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
498 {
499 // the "default" for complex is double
500 type=double_type();
501 }
502 else if(char_cnt)
503 {
504 if(
507 {
509 log.error() << "illegal type modifier for char type" << messaget::eom;
510 throw 0;
511 }
512
514 {
516 log.error() << "conflicting type modifiers" << messaget::eom;
517 throw 0;
518 }
519 else if(unsigned_cnt)
520 type=unsigned_char_type();
521 else if(signed_cnt)
522 type=signed_char_type();
523 else
524 type=char_type();
525 }
526 else
527 {
528 // it is integer -- signed or unsigned?
529
530 bool is_signed=true; // default
531
533 {
535 log.error() << "conflicting type modifiers" << messaget::eom;
536 throw 0;
537 }
538 else if(unsigned_cnt)
539 is_signed=false;
540 else if(signed_cnt)
541 is_signed=true;
542
544 {
545 if(
547 bv_cnt)
548 {
550 log.error() << "conflicting type modifiers" << messaget::eom;
551 throw 0;
552 }
553
554 if(int8_cnt)
555 if(is_signed)
556 type=signed_char_type();
557 else
558 type=unsigned_char_type();
559 else if(int16_cnt)
560 if(is_signed)
562 else
564 else if(int32_cnt)
565 if(is_signed)
566 type=signed_int_type();
567 else
568 type=unsigned_int_type();
569 else if(int64_cnt) // Visual Studio: equivalent to long long int
570 if(is_signed)
572 else
574 else
576 }
577 else if(gcc_int128_cnt)
578 {
579 if(is_signed)
581 else
583 }
584 else if(bitint_cnt)
585 {
586 // explicitly-given expression for the number of value bits
587 type.id(is_signed ? ID_c_signed_bitint : ID_c_unsigned_bitint);
588 type.set(ID_width, bv_width);
589 }
590 else if(bv_cnt)
591 {
592 // explicitly-given expression for width
593 type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
594 type.set(ID_size, bv_width);
595 }
596 else if(floatbv_cnt)
597 {
598 type.id(ID_custom_floatbv);
599 type.set(ID_size, bv_width);
600 type.set(ID_f, fraction_width);
601 }
602 else if(fixedbv_cnt)
603 {
604 type.id(ID_custom_fixedbv);
605 type.set(ID_size, bv_width);
606 type.set(ID_f, fraction_width);
607 }
608 else if(short_cnt)
609 {
610 if(long_cnt || char_cnt)
611 {
613 log.error() << "conflicting type modifiers" << messaget::eom;
614 throw 0;
615 }
616
617 if(is_signed)
619 else
621 }
622 else if(long_cnt==0)
623 {
624 if(is_signed)
625 type=signed_int_type();
626 else
627 type=unsigned_int_type();
628 }
629 else if(long_cnt==1)
630 {
631 if(is_signed)
633 else
635 }
636 else if(long_cnt==2)
637 {
638 if(is_signed)
640 else
642 }
643 else
644 {
646 log.error() << "illegal type modifier for integer type" << messaget::eom;
647 throw 0;
648 }
649 }
650
652 set_attributes(type);
653}
654
657{
658 if(vector_size.is_not_nil())
659 {
660 type_with_subtypet new_type(ID_frontend_vector, type);
661 new_type.set(ID_size, vector_size);
662 new_type.add_source_location()=vector_size.source_location();
663 type=new_type;
664 }
665
666 if(complex_cnt)
667 {
668 // These take more or less arbitrary subtypes.
669 complex_typet new_type(type);
671 type.swap(new_type);
672 }
673}
674
677{
678 if(gcc_attribute_mode.is_not_nil())
679 {
680 typet new_type=gcc_attribute_mode;
681 new_type.add_subtype() = type;
682 type.swap(new_type);
683 }
684
685 c_qualifiers.write(type);
686
687 if(packed)
688 type.set(ID_C_packed, true);
689
690 if(aligned)
691 type.set(ID_C_alignment, alignment);
692}
ANSI-C Language Conversion.
configt config
Definition config.cpp:25
floatbv_typet float_type()
Definition c_types.cpp:177
signedbv_typet signed_long_int_type()
Definition c_types.cpp:72
signedbv_typet signed_char_type()
Definition c_types.cpp:134
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:93
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:86
signedbv_typet signed_int_type()
Definition c_types.cpp:22
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:127
bitvector_typet char_type()
Definition c_types.cpp:106
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:79
floatbv_typet long_double_type()
Definition c_types.cpp:193
typet c_bool_type()
Definition c_types.cpp:100
floatbv_typet double_type()
Definition c_types.cpp:185
signedbv_typet signed_short_int_type()
Definition c_types.cpp:29
unsignedbv_typet unsigned_short_int_type()
Definition c_types.cpp:43
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
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
const typet & return_type() const
Definition std_types.h:689
const exprt::operandst & c_frees() const
Definition c_types.h:418
const exprt::operandst & c_assigns() const
Definition c_types.h:408
const exprt::operandst & c_requires() const
Definition c_types.h:428
const exprt::operandst & c_ensures() const
Definition c_types.h:438
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
A constant literal expression.
Definition std_expr.h:3118
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
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:412
void clear()
Definition irep.h:444
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
source_locationt source_location
Definition message.h:239
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void value(const irep_idt &)
Type with a single subtype.
Definition type.h:180
The type of an expression, extends irept.
Definition type.h:29
source_locationt & add_source_location()
Definition type.h:77
const source_locationt & source_location() const
Definition type.h:72
bool has_subtype() const
Definition type.h:64
typet & add_subtype()
Definition type.h:53
const exprt & op() const
Definition std_expr.h:391
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:426
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const string_constantt & to_string_constant(const exprt &expr)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45
dstringt irep_idt