cprover
Loading...
Searching...
No Matches
c_typecast.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_typecast.h"
10
11#include <algorithm>
12
13#include <util/arith_tools.h>
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/expr_util.h>
18#include <util/namespace.h>
19#include <util/pointer_expr.h>
20#include <util/simplify_expr.h>
21#include <util/std_expr.h>
22
23#include "c_qualifiers.h"
24
26 exprt &expr,
27 const typet &dest_type,
28 const namespacet &ns)
29{
31 c_typecast.implicit_typecast(expr, dest_type);
32 return !c_typecast.errors.empty();
33}
34
36 const typet &src_type,
37 const typet &dest_type,
38 const namespacet &ns)
39{
41 exprt tmp;
42 tmp.type()=src_type;
43 c_typecast.implicit_typecast(tmp, dest_type);
44 return !c_typecast.errors.empty();
45}
46
50 const namespacet &ns)
51{
53 c_typecast.implicit_typecast_arithmetic(expr1, expr2);
54 return !c_typecast.errors.empty();
55}
56
57bool has_a_void_pointer(const typet &type)
58{
59 if(type.id()==ID_pointer)
60 {
61 const auto &pointer_type = to_pointer_type(type);
62
64 return true;
65
67 }
68 else
69 return false;
70}
71
73 const typet &src_type,
74 const typet &dest_type)
75{
76 // check qualifiers
77
78 if(
79 src_type.id() == ID_pointer && dest_type.id() == ID_pointer &&
82 {
83 return true;
84 }
85
87 return false;
88
89 const irep_idt &src_type_id=src_type.id();
90
92 {
94 to_c_bit_field_type(src_type).underlying_type(), dest_type);
95 }
96
98 {
100 src_type, to_c_bit_field_type(dest_type).underlying_type());
101 }
102
104 {
105 if(dest_type.id()==ID_bool ||
106 dest_type.id()==ID_c_bool ||
107 dest_type.id()==ID_integer ||
108 dest_type.id()==ID_real ||
109 dest_type.id()==ID_complex ||
110 dest_type.id()==ID_unsignedbv ||
111 dest_type.id()==ID_signedbv ||
112 dest_type.id()==ID_floatbv ||
113 dest_type.id()==ID_complex)
114 return false;
115 }
116 else if(src_type_id==ID_integer)
117 {
118 if(dest_type.id()==ID_bool ||
119 dest_type.id()==ID_c_bool ||
120 dest_type.id()==ID_real ||
121 dest_type.id()==ID_complex ||
122 dest_type.id()==ID_unsignedbv ||
123 dest_type.id()==ID_signedbv ||
124 dest_type.id()==ID_floatbv ||
125 dest_type.id()==ID_fixedbv ||
126 dest_type.id()==ID_pointer ||
127 dest_type.id()==ID_complex)
128 return false;
129 }
130 else if(src_type_id==ID_real)
131 {
132 if(dest_type.id()==ID_bool ||
133 dest_type.id()==ID_c_bool ||
134 dest_type.id()==ID_complex ||
135 dest_type.id()==ID_floatbv ||
136 dest_type.id()==ID_fixedbv ||
137 dest_type.id()==ID_complex)
138 return false;
139 }
140 else if(src_type_id==ID_rational)
141 {
142 if(dest_type.id()==ID_bool ||
143 dest_type.id()==ID_c_bool ||
144 dest_type.id()==ID_complex ||
145 dest_type.id()==ID_floatbv ||
146 dest_type.id()==ID_fixedbv ||
147 dest_type.id()==ID_complex)
148 return false;
149 }
150 else if(src_type_id==ID_bool)
151 {
152 if(dest_type.id()==ID_c_bool ||
153 dest_type.id()==ID_integer ||
154 dest_type.id()==ID_real ||
155 dest_type.id()==ID_unsignedbv ||
156 dest_type.id()==ID_signedbv ||
157 dest_type.id()==ID_pointer ||
158 dest_type.id()==ID_floatbv ||
159 dest_type.id()==ID_fixedbv ||
160 dest_type.id()==ID_c_enum ||
161 dest_type.id()==ID_c_enum_tag ||
162 dest_type.id()==ID_complex)
163 return false;
164 }
165 else if(src_type_id==ID_unsignedbv ||
170 {
171 if(dest_type.id()==ID_unsignedbv ||
172 dest_type.id()==ID_bool ||
173 dest_type.id()==ID_c_bool ||
174 dest_type.id()==ID_integer ||
175 dest_type.id()==ID_real ||
176 dest_type.id()==ID_rational ||
177 dest_type.id()==ID_signedbv ||
178 dest_type.id()==ID_floatbv ||
179 dest_type.id()==ID_fixedbv ||
180 dest_type.id()==ID_pointer ||
181 dest_type.id()==ID_c_enum ||
182 dest_type.id()==ID_c_enum_tag ||
183 dest_type.id()==ID_complex)
184 return false;
185 }
186 else if(src_type_id==ID_floatbv ||
188 {
189 if(dest_type.id()==ID_bool ||
190 dest_type.id()==ID_c_bool ||
191 dest_type.id()==ID_integer ||
192 dest_type.id()==ID_real ||
193 dest_type.id()==ID_rational ||
194 dest_type.id()==ID_signedbv ||
195 dest_type.id()==ID_unsignedbv ||
196 dest_type.id()==ID_floatbv ||
197 dest_type.id()==ID_fixedbv ||
198 dest_type.id()==ID_complex)
199 return false;
200 }
201 else if(src_type_id==ID_complex)
202 {
203 if(dest_type.id()==ID_complex)
204 {
206 to_complex_type(src_type).subtype(),
207 to_complex_type(dest_type).subtype());
208 }
209 else
210 {
211 // 6.3.1.7, par 2:
212
213 // When a value of complex type is converted to a real type, the
214 // imaginary part of the complex value is discarded and the value of the
215 // real part is converted according to the conversion rules for the
216 // corresponding real type.
217
220 }
221 }
222 else if(src_type_id==ID_array ||
224 {
225 if(dest_type.id()==ID_pointer)
226 {
229
231 {
232 return false;
233 }
234 else if(
235 has_a_void_pointer(src_type) || // from void to anything
236 has_a_void_pointer(dest_type)) // to void from anything
237 {
238 return false;
239 }
240 }
241
242 if(
243 dest_type.id() == ID_array && to_type_with_subtype(src_type).subtype() ==
244 to_array_type(dest_type).element_type())
245 {
246 return false;
247 }
248
249 if(dest_type.id()==ID_bool ||
250 dest_type.id()==ID_c_bool ||
251 dest_type.id()==ID_unsignedbv ||
253 return false;
254 }
255 else if(src_type_id==ID_vector)
256 {
257 if(dest_type.id()==ID_vector)
258 return false;
259 }
260 else if(src_type_id==ID_complex)
261 {
262 if(dest_type.id()==ID_complex)
263 {
264 // We convert between complex types if we convert between
265 // their component types.
267 to_complex_type(src_type).subtype(),
268 to_complex_type(dest_type).subtype()))
269 {
270 return false;
271 }
272 }
273 }
274
275 return true;
276}
277
279{
280 if(
281 src_type.id() != ID_struct_tag &&
282 src_type.id() != ID_union_tag)
283 {
284 return src_type;
285 }
286
287 typet result_type=src_type;
288
289 // collect qualifiers
291
292 while(result_type.id() == ID_struct_tag || result_type.id() == ID_union_tag)
293 {
294 const typet &followed_type = ns.follow(result_type);
295 result_type = followed_type;
297 }
298
299 qualifiers.write(result_type);
300
301 return result_type;
302}
303
305 const typet &type) const
306{
307 if(type.id()==ID_signedbv)
308 {
309 const std::size_t width = to_bitvector_type(type).get_width();
310
311 if(width<=config.ansi_c.char_width)
312 return CHAR;
313 else if(width<=config.ansi_c.short_int_width)
314 return SHORT;
315 else if(width<=config.ansi_c.int_width)
316 return INT;
317 else if(width<=config.ansi_c.long_int_width)
318 return LONG;
319 else if(width<=config.ansi_c.long_long_int_width)
320 return LONGLONG;
321 else
322 return LARGE_SIGNED_INT;
323 }
324 else if(type.id()==ID_unsignedbv)
325 {
326 const std::size_t width = to_bitvector_type(type).get_width();
327
328 if(width<=config.ansi_c.char_width)
329 return UCHAR;
330 else if(width<=config.ansi_c.short_int_width)
331 return USHORT;
332 else if(width<=config.ansi_c.int_width)
333 return UINT;
334 else if(width<=config.ansi_c.long_int_width)
335 return ULONG;
336 else if(width<=config.ansi_c.long_long_int_width)
337 return ULONGLONG;
338 else
339 return LARGE_UNSIGNED_INT;
340 }
341 else if(type.id()==ID_bool)
342 return BOOL;
343 else if(type.id()==ID_c_bool)
344 return BOOL;
345 else if(type.id()==ID_floatbv)
346 {
347 const std::size_t width = to_bitvector_type(type).get_width();
348
349 if(width<=config.ansi_c.single_width)
350 return SINGLE;
351 else if(width<=config.ansi_c.double_width)
352 return DOUBLE;
353 else if(width<=config.ansi_c.long_double_width)
354 return LONGDOUBLE;
355 else if(width<=128)
356 return FLOAT128;
357 }
358 else if(type.id()==ID_fixedbv)
359 {
360 return FIXEDBV;
361 }
362 else if(type.id()==ID_pointer)
363 {
364 if(to_pointer_type(type).base_type().id() == ID_empty)
365 return VOIDPTR;
366 else
367 return PTR;
368 }
369 else if(type.id()==ID_array)
370 {
371 return PTR;
372 }
373 else if(type.id() == ID_c_enum || type.id() == ID_c_enum_tag)
374 {
375 return INT;
376 }
377 else if(type.id()==ID_rational)
378 return RATIONAL;
379 else if(type.id()==ID_real)
380 return REAL;
381 else if(type.id()==ID_complex)
382 return COMPLEX;
383 else if(type.id()==ID_c_bit_field)
384 {
385 const auto &bit_field_type = to_c_bit_field_type(type);
386
387 // We take the underlying type, and then apply the number
388 // of bits given
389 typet underlying_type;
390
391 if(bit_field_type.underlying_type().id() == ID_c_enum_tag)
392 {
393 const auto &followed =
395 if(followed.is_incomplete())
396 return INT;
397 else
398 underlying_type = followed.underlying_type();
399 }
400 else
401 underlying_type = bit_field_type.underlying_type();
402
404 underlying_type.id(), bit_field_type.get_width());
405
406 return get_c_type(new_type);
407 }
408 else if(type.id() == ID_integer)
409 return INTEGER;
410
411 return OTHER;
412}
413
415 exprt &expr,
417{
419
420 switch(c_type)
421 {
422 case PTR:
423 if(expr.type().id() == ID_array)
424 {
425 new_type = pointer_type(expr.type().subtype());
426 break;
427 }
428 return;
429
430 case BOOL: UNREACHABLE; // should always be promoted to int
431 case CHAR: UNREACHABLE; // should always be promoted to int
432 case UCHAR: UNREACHABLE; // should always be promoted to int
433 case SHORT: UNREACHABLE; // should always be promoted to int
434 case USHORT: UNREACHABLE; // should always be promoted to int
435 case INT: new_type=signed_int_type(); break;
436 case UINT: new_type=unsigned_int_type(); break;
437 case LONG: new_type=signed_long_int_type(); break;
441 case SINGLE: new_type=float_type(); break;
442 case DOUBLE: new_type=double_type(); break;
443 case LONGDOUBLE: new_type=long_double_type(); break;
444 // NOLINTNEXTLINE(whitespace/line_length)
446 case RATIONAL: new_type=rational_typet(); break;
447 case REAL: new_type=real_typet(); break;
448 case INTEGER: new_type=integer_typet(); break;
449 case COMPLEX:
450 case OTHER:
451 case VOIDPTR:
452 case FIXEDBV:
454 case LARGE_SIGNED_INT:
455 return; // do nothing
456 }
457
458 if(new_type != expr.type())
459 do_typecast(expr, new_type);
460}
461
463 const typet &type) const
464{
466
467 // 6.3.1.1, par 2
468
469 // "If an int can represent all values of the original type, the
470 // value is converted to an int; otherwise, it is converted to
471 // an unsigned int."
472
473 c_typet max_type=std::max(c_type, INT); // minimum promotion
474
475 // The second case can arise if we promote any unsigned type
476 // that is as large as unsigned int. In this case the promotion configuration
477 // via the enum is actually wrong, and we need to fix this up.
478 if(
479 config.ansi_c.short_int_width == config.ansi_c.int_width &&
480 c_type == USHORT)
482 else if(
483 config.ansi_c.char_width == config.ansi_c.int_width && c_type == UCHAR)
485
486 if(max_type==UINT &&
487 type.id()==ID_c_bit_field &&
488 to_c_bit_field_type(type).get_width()<config.ansi_c.int_width)
490
491 return max_type;
492}
493
499
513
515 exprt &expr,
516 const typet &src_type,
517 const typet &orig_dest_type,
518 const typet &dest_type)
519{
520 // do transparent union
521 if(dest_type.id()==ID_union &&
523 src_type.id()!=ID_union)
524 {
525 // The argument corresponding to a transparent union type can be of any
526 // type in the union; no explicit cast is required.
527
528 // GCC docs say:
529 // If the union member type is a pointer, qualifiers like const on the
530 // referenced type must be respected, just as with normal pointer
531 // conversions.
532 // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
534 if(
535 src_type.id() == ID_pointer &&
537 {
538 src_type_no_const.subtype().remove(ID_C_constant);
539 }
540
541 // Check union members.
542 for(const auto &comp : to_union_type(dest_type).components())
543 {
545 {
546 // build union constructor
547 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
548 if(!src_type.full_eq(src_type_no_const))
550 expr=union_expr;
551 return; // ok
552 }
553 }
554 }
555
556 if(dest_type.id()==ID_pointer)
557 {
558 // special case: 0 == NULL
559
560 if(simplify_expr(expr, ns).is_zero() && (
561 src_type.id()==ID_unsignedbv ||
562 src_type.id()==ID_signedbv ||
563 src_type.id()==ID_natural ||
564 src_type.id()==ID_integer))
565 {
567 return; // ok
568 }
569
570 if(src_type.id()==ID_pointer ||
571 src_type.id()==ID_array)
572 {
573 // we are quite generous about pointers
574
577
579 {
580 // from/to void is always good
581 }
582 else if(src_sub.id()==ID_code &&
583 dest_sub.id()==ID_code)
584 {
585 // very generous:
586 // between any two function pointers it's ok
587 }
588 else if(src_sub == dest_sub)
589 {
590 // ok
591 }
592 else if((is_number(src_sub) ||
593 src_sub.id()==ID_c_enum ||
594 src_sub.id()==ID_c_enum_tag) &&
596 dest_sub.id()==ID_c_enum ||
597 src_sub.id()==ID_c_enum_tag))
598 {
599 // Also generous: between any to scalar types it's ok.
600 // We should probably check the size.
601 }
602 else if(
603 src_sub.id() == ID_array && dest_sub.id() == ID_array &&
604 to_array_type(src_sub).element_type() ==
605 to_array_type(dest_sub).element_type())
606 {
607 // we ignore the size of the top-level array
608 // in the case of pointers to arrays
609 }
610 else
611 warnings.push_back("incompatible pointer types");
612
613 // check qualifiers
614
615 if(
616 to_type_with_subtype(src_type).subtype().get_bool(ID_C_volatile) &&
618 {
619 warnings.push_back("disregarding volatile");
620 }
621
623 {
624 expr.type()=src_type; // because of qualifiers
625 }
626 else
628
629 return; // ok
630 }
631 }
632
634 errors.push_back("implicit conversion not permitted");
635 else if(src_type!=dest_type)
637}
638
640 exprt &expr1,
641 exprt &expr2)
642{
643 const typet &type1 = expr1.type();
644 const typet &type2 = expr2.type();
645
648
649 c_typet max_type=std::max(c_type1, c_type2);
650
652 {
653 // get the biggest width of both
654 std::size_t width1 = to_bitvector_type(type1).get_width();
655 std::size_t width2 = to_bitvector_type(type2).get_width();
656
657 // produce type
658 typet result_type;
659
660 if(width1==width2)
661 {
663 result_type=signedbv_typet(width1);
664 else
665 result_type=unsignedbv_typet(width1);
666 }
667 else if(width1>width2)
668 result_type=type1;
669 else // width1<width2
670 result_type=type2;
671
672 do_typecast(expr1, result_type);
673 do_typecast(expr2, result_type);
674
675 return;
676 }
677 else if(max_type==FIXEDBV)
678 {
679 typet result_type;
680
682 {
683 // get bigger of both
684 std::size_t width1=to_fixedbv_type(type1).get_width();
685 std::size_t width2=to_fixedbv_type(type2).get_width();
686 if(width1>=width2)
687 result_type=type1;
688 else
689 result_type=type2;
690 }
691 else if(c_type1==FIXEDBV)
692 result_type=type1;
693 else
694 result_type=type2;
695
696 do_typecast(expr1, result_type);
697 do_typecast(expr2, result_type);
698
699 return;
700 }
701 else if(max_type==COMPLEX)
702 {
704 {
705 // promote to the one with bigger subtype
706 if(
707 get_c_type(to_complex_type(type1).subtype()) >
708 get_c_type(to_complex_type(type2).subtype()))
709 {
711 }
712 else
714 }
715 else if(c_type1==COMPLEX)
716 {
720 }
721 else
722 {
726 }
727
728 return;
729 }
730 else if(max_type==SINGLE || max_type==DOUBLE ||
732 {
733 // Special-case optimisation:
734 // If we have two non-standard sized floats, don't do implicit type
735 // promotion if we can possibly avoid it.
736 if(type1==type2)
737 return;
738 }
739 else if(max_type == OTHER)
740 {
741 errors.push_back("implicit arithmetic conversion not permitted");
742 return;
743 }
744
747}
748
750{
751 // special case: array -> pointer is actually
752 // something like address_of
753
754 const typet &src_type = expr.type();
755
756 if(src_type.id()==ID_array)
757 {
758 index_exprt index(expr, from_integer(0, c_index_type()));
760 return;
761 }
762
764 {
765 // C booleans are special; we produce the
766 // explicit comparison with zero.
767 // Note that this requires ieee_float_notequal
768 // in case of floating-point numbers.
769
771 {
772 expr = typecast_exprt(is_not_zero(expr, ns), dest_type);
773 }
774 else if(dest_type.id()==ID_bool)
775 {
776 expr=is_not_zero(expr, ns);
777 }
778 else
779 {
780 expr = typecast_exprt(expr, dest_type);
781 }
782 }
783}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void base_type(typet &type, const namespacet &ns)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
bool has_a_void_pointer(const typet &type)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
floatbv_typet float_type()
Definition c_types.cpp:195
signedbv_typet signed_long_int_type()
Definition c_types.cpp:90
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
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:97
floatbv_typet long_double_type()
Definition c_types.cpp:211
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:203
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:58
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class of fixed-width bit-vector types.
Definition std_types.h:853
std::size_t get_width() const
Definition std_types.h:864
@ LARGE_UNSIGNED_INT
Definition c_typecast.h:79
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
virtual void implicit_typecast(exprt &expr, const typet &type)
c_typet get_c_type(const typet &type) const
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< std::string > warnings
Definition c_typecast.h:66
const namespacet & ns
Definition c_typecast.h:69
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
Definition c_typecast.h:65
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
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
static ieee_float_spect quadruple_precision()
Definition ieee_float.h:83
Array index operator.
Definition std_expr.h:1328
Unbounded, signed integers (mathematical integers, not bitvectors)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The null pointer constant.
const typet & base_type() const
The type of the data what we point to.
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Fixed-width bit-vector with two's complement interpretation.
const componentst & components() const
Definition std_types.h:147
const typet & subtype() const
Definition type.h:156
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
Union constructor from single element.
Definition std_expr.h:1611
Fixed-width bit-vector with unsigned binary interpretation.
configt config
Definition config.cpp:25
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:97
Deprecated expression utility functions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
API to expression classes.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177