CBMC
Loading...
Searching...
No Matches
cpp_typecheck_conversions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author:
6
7\*******************************************************************/
8
11
12#include "cpp_typecheck.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/config.h>
17#include <util/expr_util.h>
18#include <util/pointer_expr.h>
19#include <util/simplify_expr.h>
20#include <util/std_expr.h>
21
22#include <ansi-c/c_qualifiers.h>
23
24#include "cpp_util.h"
25
47 const exprt &expr,
48 exprt &new_expr) const
49{
51
52 if(expr.type().id() == ID_code)
53 return false;
54
55 if(
56 expr.type().id() == ID_struct &&
57 to_struct_type(expr.type()).is_incomplete())
58 return false;
59
60 if(expr.type().id() == ID_union && to_union_type(expr.type()).is_incomplete())
61 return false;
62
63 new_expr=expr;
64 new_expr.remove(ID_C_lvalue);
65
66 return true;
67}
68
78 const exprt &expr,
79 exprt &new_expr) const
80{
81 PRECONDITION(expr.type().id() == ID_array);
82
83 index_exprt index(expr, from_integer(0, c_index_type()));
84
85 index.set(ID_C_lvalue, true);
86
88
89 return true;
90}
91
100 const exprt &expr, exprt &new_expr) const
101{
102 if(!expr.get_bool(ID_C_lvalue))
103 return false;
104
106
107 return true;
108}
109
116 const exprt &expr,
117 const typet &type,
118 exprt &new_expr) const
119{
120 if(expr.type().id()!=ID_pointer ||
121 is_reference(expr.type()))
122 return false;
123
124 if(expr.get_bool(ID_C_lvalue))
125 return false;
126
127 if(expr.type()!=type)
128 return false;
129
130 typet sub_from = to_pointer_type(expr.type()).base_type();
131 typet sub_to = to_pointer_type(type).base_type();
132 bool const_to=true;
133
134 while(sub_from.id()==ID_pointer)
135 {
138
139 if(!qual_to.is_constant)
140 const_to=false;
141
142 if(qual_from.is_constant && !qual_to.is_constant)
143 return false;
144
145 if(qual_from!=qual_to && !const_to)
146 return false;
147
148 typet tmp1 = to_pointer_type(sub_from).base_type();
149 sub_from.swap(tmp1);
150
151 typet tmp2 = sub_to.add_subtype();
152 sub_to.swap(tmp2);
153 }
154
157
158 if(qual_from.is_subset_of(qual_to))
159 {
160 new_expr=expr;
161 new_expr.type()=type;
162 return true;
163 }
164
165 return false;
166}
167
194 const exprt &expr,
195 exprt &new_expr) const
196{
197 if(expr.get_bool(ID_C_lvalue))
198 return false;
199
201 qual_from.read(expr.type());
202
204 qual_from.write(int_type);
205
206 if(expr.type().id()==ID_signedbv)
207 {
208 std::size_t width=to_signedbv_type(expr.type()).get_width();
209 if(width >= config.ansi_c.int_width)
210 return false;
212 return true;
213 }
214
215 if(expr.type().id()==ID_unsignedbv)
216 {
217 std::size_t width=to_unsignedbv_type(expr.type()).get_width();
218 if(width >= config.ansi_c.int_width)
219 return false;
221 return true;
222 }
223
224 if(expr.is_boolean() || expr.type().id() == ID_c_bool)
225 {
227 return true;
228 }
229
230 if(expr.type().id()==ID_c_enum_tag)
231 {
233 return true;
234 }
235
236 return false;
237}
238
247 const exprt &expr,
248 exprt &new_expr) const
249{
250 if(expr.get_bool(ID_C_lvalue))
251 return false;
252
253 // we only do that with 'float',
254 // not with 'double' or 'long double'
255 if(expr.type()!=float_type())
256 return false;
257
258 std::size_t width=to_floatbv_type(expr.type()).get_width();
259
260 if(width!=config.ansi_c.single_width)
261 return false;
262
264 qual_from.read(expr.type());
265
267 qual_from.write(new_expr.type());
268
269 return true;
270}
271
301 const exprt &expr,
302 const typet &type,
303 exprt &new_expr) const
304{
305 if(type.id()!=ID_signedbv &&
306 type.id()!=ID_unsignedbv)
307 return false;
308
309 if(
310 expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
311 expr.type().id() != ID_c_bool && !expr.is_boolean() &&
312 expr.type().id() != ID_c_enum_tag)
313 {
314 return false;
315 }
316
317 if(expr.get_bool(ID_C_lvalue))
318 return false;
319
321 qual_from.read(expr.type());
323 qual_from.write(new_expr.type());
324
325 return true;
326}
327
348 const exprt &expr,
349 const typet &type,
350 exprt &new_expr) const
351{
352 if(expr.get_bool(ID_C_lvalue))
353 return false;
354
355 if(expr.type().id()==ID_floatbv ||
356 expr.type().id()==ID_fixedbv)
357 {
358 if(type.id()!=ID_signedbv &&
359 type.id()!=ID_unsignedbv)
360 return false;
361 }
362 else if(expr.type().id()==ID_signedbv ||
363 expr.type().id()==ID_unsignedbv ||
364 expr.type().id()==ID_c_enum_tag)
365 {
366 if(type.id()!=ID_fixedbv &&
367 type.id()!=ID_floatbv)
368 return false;
369 }
370 else
371 return false;
372
374 qual_from.read(expr.type());
376 qual_from.write(new_expr.type());
377
378 return true;
379}
380
381
399 const exprt &expr,
400 const typet &type,
401 exprt &new_expr) const
402{
403 if(expr.type().id()!=ID_floatbv &&
404 expr.type().id()!=ID_fixedbv)
405 return false;
406
407 if(type.id()!=ID_floatbv &&
408 type.id()!=ID_fixedbv)
409 return false;
410
411 if(expr.get_bool(ID_C_lvalue))
412 return false;
413
415
416 qual_from.read(expr.type());
418 qual_from.write(new_expr.type());
419
420 return true;
421}
422
456 const exprt &expr,
457 const typet &type,
459{
460 if(type.id()!=ID_pointer ||
461 is_reference(type))
462 return false;
463
464 if(expr.get_bool(ID_C_lvalue))
465 return false;
466
467 // integer 0 to NULL pointer conversion?
468 if(simplify_expr(expr, *this) == 0 && expr.type().id() != ID_pointer)
469 {
470 new_expr=expr;
472 new_expr.type()=type;
473 return true;
474 }
475
476 if(type.find(ID_to_member).is_not_nil())
477 return false;
478
479 if(
480 expr.type().id() != ID_pointer ||
481 expr.type().find(ID_to_member).is_not_nil())
482 {
483 return false;
484 }
485
487 const typet &sub_from = to_pointer_type(expr.type()).base_type();
489
490 // std::nullptr_t to _any_ pointer type
491 if(sub_from.id()==ID_nullptr)
492 return true;
493
494 // anything but function pointer to void *
495 if(sub_from.id()!=ID_code && sub_to.id()==ID_empty)
496 {
498 qual_from.read(to_pointer_type(expr.type()).base_type());
500 qual_from.write(to_pointer_type(new_expr.type()).base_type());
501 return true;
502 }
503
504 // struct * to struct *
505 if(sub_from.id() == ID_struct_tag && sub_to.id() == ID_struct_tag)
506 {
510 {
512 qual_from.read(to_pointer_type(expr.type()).base_type());
513 new_expr=expr;
515 qual_from.write(to_pointer_type(new_expr.type()).base_type());
516 return true;
517 }
518 }
519
520 return false;
521}
522
554 const exprt &expr,
555 const typet &type,
557{
558 if(
559 type.id() != ID_pointer || is_reference(type) ||
560 type.find(ID_to_member).is_nil())
561 {
562 return false;
563 }
564
565 if(expr.type().id() != ID_pointer || expr.type().find(ID_to_member).is_nil())
566 return false;
567
568 if(
569 to_pointer_type(type).base_type() !=
570 to_pointer_type(expr.type()).base_type())
571 {
572 // base types are different
573 if(
574 to_pointer_type(type).base_type().id() == ID_code &&
575 to_pointer_type(expr.type()).base_type().id() == ID_code)
576 {
577 code_typet code1 = to_code_type(to_pointer_type(expr.type()).base_type());
578 DATA_INVARIANT(!code1.parameters().empty(), "must have parameters");
579 code_typet::parametert this1=code1.parameters()[0];
580 INVARIANT(this1.get_this(), "first parameter should be `this'");
581 code1.parameters().erase(code1.parameters().begin());
582
583 code_typet code2 = to_code_type(to_pointer_type(type).base_type());
584 DATA_INVARIANT(!code2.parameters().empty(), "must have parameters");
585 code_typet::parametert this2=code2.parameters()[0];
586 INVARIANT(this2.get_this(), "first parameter should be `this'");
587 code2.parameters().erase(code2.parameters().begin());
588
589 if(
590 to_pointer_type(this2.type()).base_type().get_bool(ID_C_constant) &&
591 !to_pointer_type(this1.type()).base_type().get_bool(ID_C_constant))
592 return false;
593
594 // give a second chance ignoring `this'
595 if(code1!=code2)
596 return false;
597 }
598 else
599 return false;
600 }
601
602 if(expr.get_bool(ID_C_lvalue))
603 return false;
604
605 if(expr.is_constant() && to_constant_expr(expr).is_null_pointer())
606 {
608 return true;
609 }
610
612 static_cast<const typet &>(expr.type().find(ID_to_member))));
613
615 to_struct_tag_type(static_cast<const typet &>(type.find(ID_to_member))));
616
618 {
620 return true;
621 }
622
623 return false;
624}
625
636 const exprt &expr, exprt &new_expr) const
637{
638 if(expr.get_bool(ID_C_lvalue))
639 return false;
640
641 if(
642 expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
643 expr.type().id() != ID_pointer && !expr.is_boolean() &&
644 expr.type().id() != ID_c_enum_tag)
645 {
646 return false;
647 }
648
650 qual_from.read(expr.type());
651
653 qual_from.write(Bool);
654
656 return true;
657}
658
680 const exprt &expr,
681 const typet &type,
683 unsigned &rank)
684{
685 PRECONDITION(!is_reference(expr.type()) && !is_reference(type));
686
687 exprt curr_expr=expr;
688
689 // bit fields are converted like their underlying type
690 if(type.id()==ID_c_bit_field)
692 expr, to_c_bit_field_type(type).underlying_type(), new_expr, rank);
693
694 // we turn bit fields into their underlying type
695 if(curr_expr.type().id()==ID_c_bit_field)
697 curr_expr, to_c_bit_field_type(curr_expr.type()).underlying_type());
698
699 if(curr_expr.type().id()==ID_array)
700 {
701 if(type.id()==ID_pointer)
702 {
704 return false;
705 }
706 }
707 else if(curr_expr.type().id()==ID_code &&
708 type.id()==ID_pointer)
709 {
711 return false;
712 }
713 else if(curr_expr.get_bool(ID_C_lvalue))
714 {
716 return false;
717 }
718 else
720
721 curr_expr.swap(new_expr);
722
723 // two enums are the same if the tag is the same,
724 // even if the width differs (enum bit-fields!)
725 if(type.id() == ID_c_enum_tag && curr_expr.type().id() == ID_c_enum_tag)
726 {
727 if(
728 to_tag_type(type).get_identifier() ==
729 to_tag_type(curr_expr.type()).get_identifier())
730 {
731 return true;
732 }
733 else
734 {
735 // In contrast to C, we simply don't allow implicit conversions
736 // between enums.
737 return false;
738 }
739 }
740
741 // need to consider #c_type
742 if(
743 curr_expr.type() != type ||
744 curr_expr.type().get(ID_C_c_type) != type.get(ID_C_c_type))
745 {
746 if(
747 type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
748 type.id() == ID_c_enum_tag)
749 {
751 new_expr.type() != type)
752 {
754 {
756 curr_expr, type, new_expr))
757 return false;
758 }
759
760 rank+=3;
761 }
762 else
763 rank+=2;
764 }
765 else if(type.id()==ID_floatbv || type.id()==ID_fixedbv)
766 {
768 new_expr.type() != type)
769 {
771 curr_expr, type, new_expr) &&
773 curr_expr, type, new_expr))
774 return false;
775
776 rank += 3;
777 }
778 else
779 rank += 2;
780 }
781 else if(type.id()==ID_pointer)
782 {
783 if(
784 expr.type().id() == ID_pointer &&
785 to_pointer_type(expr.type()).base_type().id() == ID_nullptr)
786 {
787 // std::nullptr_t to _any_ pointer type is ok
789 }
791 {
793 return false;
794 }
795
796 rank += 3;
797 }
798 else if(type.id() == ID_c_bool)
799 {
801 return false;
802
803 rank += 3;
804 }
805 else if(type.id() == ID_bool)
806 {
808
809 rank += 3;
810 }
811 else
812 return false;
813 }
814 else
816
817 curr_expr.swap(new_expr);
818
819 if(curr_expr.type().id()==ID_pointer)
820 {
821 typet sub_from=curr_expr.type();
822 typet sub_to=type;
823
824 do
825 {
826 typet tmp_from = to_pointer_type(sub_from).base_type();
827 sub_from.swap(tmp_from);
828 typet tmp_to = sub_to.add_subtype();
829 sub_to.swap(tmp_to);
830
832 qual_from.read(sub_from);
833
835 qual_to.read(sub_to);
836
837 if(qual_from!=qual_to)
838 {
839 rank+=1;
840 break;
841 }
842 }
843 while(sub_from.id()==ID_pointer);
844
846 return false;
847 }
848 else
849 {
851 new_expr.type()=type;
852 }
853
854 return true;
855}
856
863 const exprt &expr,
864 const typet &to,
866 unsigned &rank)
867{
870
871 const typet &from = expr.type();
872
873 new_expr.make_nil();
874
875 // special case:
876 // A conversion from a type to the same type is given an exact
877 // match rank even though a user-defined conversion is used
878
879 if(from==to)
880 rank+=0;
881 else
882 rank+=4; // higher than all the standard conversions
883
884 if(to.id() == ID_struct_tag)
885 {
886 std::string err_msg;
887
888 if(cpp_is_pod(to))
889 {
890 if(from.id() == ID_struct_tag)
891 {
894
895 // potentially requires
896 // expr.get_bool(ID_C_lvalue) ??
897
899 {
900 exprt address=address_of_exprt(expr);
901
902 // simplify address
903 if(expr.id()==ID_dereference)
904 address = to_dereference_expr(expr).pointer();
905
908 qual_from.read(expr.type());
909 qual_from.write(ptr_sub.base_type());
910 make_ptr_typecast(address, ptr_sub);
911
912 const dereference_exprt deref(address);
913
914 // create temporary object
917 tmp_object_expr.copy_to_operands(deref);
918 tmp_object_expr.set(ID_C_lvalue, true);
920
922 return true;
923 }
924 }
925 }
926 else
927 {
928 bool found=false;
930
931 for(const auto &component : struct_type_to.components())
932 {
933 if(component.get_bool(ID_from_base))
934 continue;
935
936 if(component.get_bool(ID_is_explicit))
937 continue;
938
939 const typet &comp_type = component.type();
940
941 if(comp_type.id() !=ID_code)
942 continue;
943
944 if(to_code_type(comp_type).return_type().id() != ID_constructor)
945 continue;
946
947 // TODO: ellipsis
948
949 const auto &parameters = to_code_type(comp_type).parameters();
950
951 if(parameters.size() != 2)
952 continue;
953
954 exprt curr_arg1 = parameters[1];
956
958 {
959 typet tmp = to_reference_type(arg1_type).base_type();
960 arg1_type.swap(tmp);
961 }
962
963 unsigned tmp_rank=0;
964 if(arg1_type.id() != ID_struct_tag)
965 {
968 expr, arg1_type, tmp_expr, tmp_rank))
969 {
970 // check if it's ambiguous
971 if(found)
972 return false;
973 found=true;
974
975 if(expr.get_bool(ID_C_lvalue))
976 tmp_expr.set(ID_C_lvalue, true);
977
978 tmp_expr.add_source_location()=expr.source_location();
979
981 func_symb.type()=comp_type;
983
984 // create temporary object
986 std::move(func_symb),
987 {tmp_expr},
989 expr.source_location());
992
993 new_expr.swap(ctor_expr);
994
995 if(struct_type_to.get_bool(ID_C_constant))
996 new_expr.type().set(ID_C_constant, true);
997
998 rank += tmp_rank;
999 }
1000 }
1001 else if(from.id() == ID_struct_tag && arg1_type.id() == ID_struct_tag)
1002 {
1003 // try derived-to-base conversion
1006
1008 tmp_rank=0;
1011 {
1012 // check if it's ambiguous
1013 if(found)
1014 return false;
1015 found=true;
1016
1017 rank+=tmp_rank;
1018
1019 // create temporary object
1021 expr_deref.set(ID_C_lvalue, true);
1022 expr_deref.add_source_location()=expr.source_location();
1023
1025 new_object.set(ID_C_lvalue, true);
1026 new_object.type().set(ID_C_constant, false);
1027
1029 func_symb.type()=comp_type;
1031
1033 std::move(func_symb),
1034 {expr_deref},
1036 expr.source_location());
1038
1039 new_expr.swap(ctor_expr);
1040
1041 INVARIANT(
1043 "statement ID");
1044
1045 if(struct_type_to.get_bool(ID_C_constant))
1046 new_expr.type().set(ID_C_constant, true);
1047 }
1048 }
1049 }
1050 if(found)
1051 return true;
1052 }
1053 }
1054
1055 // conversion operators
1056 if(from.id() == ID_struct_tag)
1057 {
1058 bool found=false;
1059 for(const auto &component :
1060 follow_tag(to_struct_tag_type(from)).components())
1061 {
1062 if(component.get_bool(ID_from_base))
1063 continue;
1064
1065 if(!component.get_bool(ID_is_cast_operator))
1066 continue;
1067
1068 const code_typet &comp_type = to_code_type(component.type());
1070 comp_type.parameters().size() == 1, "expected exactly one parameter");
1071
1072 typet this_type = comp_type.parameters().front().type();
1073 this_type.set(ID_C_reference, true);
1074
1075 exprt this_expr(expr);
1076 this_type.set(ID_C_this, true);
1077
1078 unsigned tmp_rank=0;
1080
1082 this_expr, this_type, tmp_expr, tmp_rank))
1083 {
1084 // To take care of the possible virtual case,
1085 // we build the function as a member expression.
1086 const cpp_namet cpp_func_name(component.get_base_name());
1087
1090 member_func.copy_to_operands(already_typechecked_exprt{expr});
1091
1093 std::move(member_func),
1094 {},
1096 expr.source_location());
1098
1100 {
1101 // check if it's ambiguous
1102 if(found)
1103 return false;
1104 found=true;
1105
1106 rank+=tmp_rank;
1107 new_expr.swap(tmp_expr);
1108 }
1109 }
1110 }
1111 if(found)
1112 return true;
1113 }
1114
1115 return new_expr.is_not_nil();
1116}
1117
1123 const exprt &expr,
1124 const reference_typet &reference_type) const
1125{
1126 PRECONDITION(!is_reference(expr.type()));
1127
1128 const typet &from = expr.type();
1129 const typet &from_followed =
1130 from.id() == ID_struct_tag
1131 ? static_cast<const typet &>(follow_tag(to_struct_tag_type(from)))
1132 : from.id() == ID_union_tag
1133 ? static_cast<const typet &>(follow_tag(to_union_tag_type(from)))
1134 : from;
1135 const typet &to = reference_type.base_type();
1136 const typet &to_followed =
1137 to.id() == ID_struct_tag
1138 ? static_cast<const typet &>(follow_tag(to_struct_tag_type(to)))
1139 : to.id() == ID_union_tag
1140 ? static_cast<const typet &>(follow_tag(to_union_tag_type(to)))
1141 : to;
1142
1143 // need to check #c_type
1145 return false;
1146
1147 if(from==to)
1148 return true;
1149
1150 if(from.id() == ID_struct_tag && to.id() == ID_struct_tag)
1151 {
1152 return subtype_typecast(
1154 }
1155
1156 if(
1158 to.id() == ID_empty)
1159 {
1160 // virtual-call case
1161 return true;
1162 }
1163
1164 return false;
1165}
1166
1172 const exprt &expr,
1174 unsigned &rank) const
1175{
1176 PRECONDITION(!is_reference(expr.type()));
1177
1179 return false;
1180
1181 if(expr.type() != reference_type.base_type())
1182 rank+=3;
1183
1185 qual_from.read(expr.type());
1186
1189
1190 if(qual_from!=qual_to)
1191 rank+=1;
1192
1193 if(qual_from.is_subset_of(qual_to))
1194 return true;
1195
1196 return false;
1197}
1198
1234 exprt expr,
1236 exprt &new_expr,
1237 unsigned &rank)
1238{
1239 PRECONDITION(!is_reference(expr.type()));
1240
1241 unsigned backup_rank=rank;
1242
1244 {
1245 // `this' has to be an lvalue
1247 expr.set(ID_C_lvalue, true);
1248 else if(expr.get(ID_statement)==ID_function_call)
1249 expr.set(ID_C_lvalue, true);
1250 else if(expr.get_bool(ID_C_temporary_avoided))
1251 {
1254 new_temporary(expr.source_location(), expr.type(), expr, temporary);
1255 expr.swap(temporary);
1256 expr.set(ID_C_lvalue, true);
1257 }
1258 else
1259 return false;
1260 }
1261
1262 if(
1263 expr.get_bool(ID_C_lvalue) ||
1265 {
1267 {
1268 if(!expr.get_bool(ID_C_lvalue))
1269 {
1270 // create temporary object
1273 {std::move(expr)},
1275 expr.source_location()};
1276 tmp.set(ID_mode, ID_cpp);
1277 expr.swap(tmp);
1278 }
1279
1280 {
1282 tmp.add_source_location()=expr.source_location();
1283 new_expr.swap(tmp);
1284 }
1285
1286 if(expr.type() != reference_type.base_type())
1287 {
1289 qual_from.read(expr.type());
1291 qual_from.write(to_reference_type(new_expr.type()).base_type());
1292 }
1293
1294 return true;
1295 }
1296
1298 }
1299
1300 // conversion operators
1301 if(expr.type().id() == ID_struct_tag)
1302 {
1303 for(const auto &component :
1304 follow_tag(to_struct_tag_type(expr.type())).components())
1305 {
1306 if(component.get_bool(ID_from_base))
1307 continue;
1308
1309 if(!component.get_bool(ID_is_cast_operator))
1310 continue;
1311
1312 const code_typet &component_type = to_code_type(component.type());
1313
1314 // otherwise it cannot bind directly (not an lvalue)
1315 if(!is_reference(component_type.return_type()))
1316 continue;
1317
1319 component_type.parameters().size() == 1, "exactly one parameter");
1320
1322 component_type.parameters().front().type();
1323 this_type.set(ID_C_reference, true);
1324
1325 exprt this_expr(expr);
1326
1327 this_type.set(ID_C_this, true);
1328
1329 unsigned tmp_rank=0;
1330
1333 this_expr, this_type, tmp_expr, tmp_rank))
1334 {
1335 // To take care of the possible virtual case,
1336 // we build the function as a member expression.
1337 const cpp_namet cpp_func_name(component.get_base_name());
1338
1341 member_func.copy_to_operands(already_typechecked_exprt{expr});
1342
1344 std::move(member_func),
1345 {},
1347 expr.source_location());
1349
1350 // let's check if the returned value binds directly
1353
1354 if(
1355 returned_value.get_bool(ID_C_lvalue) &&
1357 {
1358 // returned values are lvalues in case of references only
1361 "the returned value must be pointer to reference");
1362
1364
1366 {
1368 qual_from.read(returned_value.type());
1370 qual_from.write(to_reference_type(new_expr.type()).base_type());
1371 }
1372 rank+=4+tmp_rank;
1373 return true;
1374 }
1375 }
1376 }
1377 }
1378
1379 // No temporary allowed for `this'
1381 return false;
1382
1383 if(
1384 !reference_type.base_type().get_bool(ID_C_constant) ||
1386 return false;
1387
1388 // TODO: handle the case for implicit parameters
1389 if(
1390 !reference_type.base_type().get_bool(ID_C_constant) &&
1391 !expr.get_bool(ID_C_lvalue))
1392 return false;
1393
1394 exprt arg_expr=expr;
1395
1396 if(arg_expr.type().id() == ID_struct_tag)
1397 {
1398 // required to initialize the temporary
1399 arg_expr.set(ID_C_lvalue, true);
1400 }
1401
1404 {
1406 tmp.add_source_location()=new_expr.source_location();
1407 new_expr.swap(tmp);
1408 return true;
1409 }
1410
1414 {
1415 {
1416 // create temporary object
1420 expr.source_location());
1421 tmp.set(ID_mode, ID_cpp);
1422 // tmp.set(ID_C_lvalue, true);
1423 tmp.add_to_operands(std::move(new_expr));
1424 new_expr.swap(tmp);
1425 }
1426
1428 tmp.type().set(ID_C_reference, true);
1429 tmp.add_source_location()=new_expr.source_location();
1430
1431 new_expr=tmp;
1432 return true;
1433 }
1434
1435 return false;
1436}
1437
1445 const exprt &expr,
1446 const typet &type,
1447 exprt &new_expr,
1448 unsigned &rank)
1449{
1450 unsigned backup_rank=rank;
1451
1452 exprt e=expr;
1454
1455 if(is_reference(type))
1456 {
1458 return false;
1459
1460 #if 0
1461 simplify_exprt simplify(*this);
1462 simplify.simplify(new_expr);
1463 new_expr.type().set(ID_C_reference, true);
1464 #endif
1465 }
1466 else if(!standard_conversion_sequence(e, type, new_expr, rank))
1467 {
1470 {
1471 if(
1472 type.id() == ID_integer &&
1473 (expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv))
1474 {
1475 // This is a nonstandard implicit conversion, from
1476 // bit-vectors to unbounded integers.
1477 rank = 0;
1478 new_expr = typecast_exprt(expr, type);
1479 return true;
1480 }
1481 else if(
1482 (type.id() == ID_signedbv || type.id() == ID_unsignedbv) &&
1483 expr.type().id() == ID_integer)
1484 {
1485 // This is a nonstandard implicit conversion, from
1486 // unbounded integers to bit-vectors.
1487 rank = 0;
1488 new_expr = typecast_exprt(expr, type);
1489 return true;
1490 }
1491
1492 // no conversion
1493 return false;
1494 }
1495
1496#if 0
1497 simplify_exprt simplify(*this);
1498 simplify.simplify(new_expr);
1499#endif
1500 }
1501
1502 return true;
1503}
1504
1511 const exprt &expr,
1512 const typet &type,
1513 exprt &new_expr)
1514{
1515 unsigned rank=0;
1516 return implicit_conversion_sequence(expr, type, new_expr, rank);
1517}
1518
1525 const exprt &expr,
1526 const typet &type,
1527 unsigned &rank)
1528{
1530 return implicit_conversion_sequence(expr, type, new_expr, rank);
1531}
1532
1534{
1535 exprt e=expr;
1536
1537 if(
1538 e.id() == ID_initializer_list && cpp_is_pod(type) &&
1539 e.operands().size() == 1)
1540 {
1541 e = to_unary_expr(expr).op();
1542 }
1543
1544 if(!implicit_conversion_sequence(e, type, expr))
1545 {
1548 error() << "invalid implicit conversion from '" << to_string(e.type())
1549 << "' to '" << to_string(type) << "'" << eom;
1550#if 0
1551 str << "\n " << e.type().pretty() << '\n';
1552 str << "\n " << type.pretty() << '\n';
1553#endif
1554 throw 0;
1555 }
1556}
1557
1601 exprt &expr,
1603{
1605
1606 unsigned rank=0;
1609 {
1610 expr.swap(new_expr);
1611 return;
1612 }
1613
1615 error() << "bad reference initializer" << eom;
1616 throw 0;
1617}
1618
1620 const typet &t1,
1621 const typet &t2) const
1622{
1623 PRECONDITION(t1.id() == ID_pointer && t2.id() == ID_pointer);
1624 typet nt1=t1;
1625 typet nt2=t2;
1626
1627 if(is_reference(nt1))
1628 nt1.remove(ID_C_reference);
1629 nt1.remove(ID_to_member);
1630
1631 if(is_reference(nt2))
1632 nt2.remove(ID_C_reference);
1633 nt2.remove(ID_to_member);
1634
1635 // substitute final subtypes
1636 std::vector<typet> snt1;
1637 snt1.push_back(nt1);
1638
1639 while(snt1.back().has_subtype())
1640 {
1641 snt1.reserve(snt1.size()+1);
1642 snt1.push_back(to_type_with_subtype(snt1.back()).subtype());
1643 }
1644
1646 q1.read(snt1.back());
1647
1649 q1.write(newnt1);
1650 snt1.back()=newnt1;
1651
1652 std::vector<typet> snt2;
1653 snt2.push_back(nt2);
1654 while(snt2.back().has_subtype())
1655 {
1656 snt2.reserve(snt2.size()+1);
1657 snt2.push_back(to_type_with_subtype(snt2.back()).subtype());
1658 }
1659
1661 q2.read(snt2.back());
1662
1664 q2.write(newnt2);
1665 snt2.back()=newnt2;
1666
1667 const std::size_t k=snt1.size() < snt2.size() ? snt1.size() : snt2.size();
1668
1669 for(std::size_t i=k; i > 1; i--)
1670 {
1671 to_type_with_subtype(snt1[snt1.size() - 2]).subtype() =
1672 snt1[snt1.size() - 1];
1673 snt1.pop_back();
1674
1675 to_type_with_subtype(snt2[snt2.size() - 2]).subtype() =
1676 snt2[snt2.size() - 1];
1677 snt2.pop_back();
1678 }
1679
1680 exprt e1("Dummy", snt1.back());
1681 exprt e2;
1682
1683 return !standard_conversion_qualification(e1, snt2.back(), e2);
1684}
1685
1687 const exprt &expr,
1688 const typet &type,
1689 exprt &new_expr)
1690{
1691 PRECONDITION(!is_reference(expr.type()));
1692
1693 exprt curr_expr=expr;
1694
1695 if(curr_expr.type().id()==ID_array)
1696 {
1697 if(type.id()==ID_pointer)
1698 {
1700 return false;
1701 }
1702 }
1703 else if(curr_expr.type().id()==ID_code &&
1704 type.id()==ID_pointer)
1705 {
1707 return false;
1708 }
1709 else if(curr_expr.get_bool(ID_C_lvalue))
1710 {
1712 return false;
1713 }
1714 else
1716
1717 if(is_reference(type))
1718 {
1719 if(!expr.get_bool(ID_C_lvalue))
1720 return false;
1721
1722 if(new_expr.type() != to_reference_type(type).base_type())
1723 return false;
1724
1728 return true;
1729 }
1730 else if(type.id()==ID_pointer)
1731 {
1732 if(type!=new_expr.type())
1733 return false;
1734
1735 // add proper typecast
1736 typecast_exprt typecast_expr(expr, type);
1737 new_expr.swap(typecast_expr);
1738 return true;
1739 }
1740
1741 return false;
1742}
1743
1745 const exprt &expr,
1746 const typet &type,
1747 exprt &new_expr)
1748{
1749 exprt e(expr);
1750
1751 if(type.id()==ID_pointer)
1752 {
1754 e = to_dereference_expr(expr).pointer();
1755
1756 if(e.type().id()==ID_pointer &&
1757 cast_away_constness(e.type(), type))
1758 return false;
1759 }
1760
1762
1763 if(is_reference(type))
1764 {
1765 if(to_reference_type(type).base_type().id() != ID_struct_tag)
1766 return false;
1767 }
1768 else if(type.id()==ID_pointer)
1769 {
1770 if(type.find(ID_to_member).is_not_nil())
1771 return false;
1772
1773 if(to_pointer_type(type).base_type().id() == ID_empty)
1774 {
1775 if(!e.get_bool(ID_C_lvalue))
1776 return false;
1777 UNREACHABLE; // currently not supported
1778 }
1779 else if(to_pointer_type(type).base_type().id() == ID_struct_tag)
1780 {
1781 if(e.get_bool(ID_C_lvalue))
1782 {
1783 exprt tmp(e);
1784
1786 return false;
1787 }
1788 }
1789 else return false;
1790 }
1791 else return false;
1792
1793 return static_typecast(e, type, new_expr);
1794}
1795
1797 const exprt &expr,
1798 const typet &type,
1799 exprt &new_expr,
1800 bool check_constantness)
1801{
1802 exprt e=expr;
1803
1804 if(check_constantness && type.id()==ID_pointer)
1805 {
1807 e = to_dereference_expr(expr).pointer();
1808
1809 if(e.type().id()==ID_pointer &&
1810 cast_away_constness(e.type(), type))
1811 return false;
1812 }
1813
1815
1816 if(!is_reference(type))
1817 {
1818 exprt tmp;
1819
1820 if(e.id()==ID_code)
1821 {
1823 e.swap(tmp);
1824 else
1825 return false;
1826 }
1827
1828 if(e.type().id()==ID_array)
1829 {
1831 e.swap(tmp);
1832 else
1833 return false;
1834 }
1835
1836 if(e.get_bool(ID_C_lvalue))
1837 {
1839 e.swap(tmp);
1840 else
1841 return false;
1842 }
1843 }
1844
1845 if(e.type().id()==ID_pointer &&
1846 (type.id()==ID_unsignedbv || type.id()==ID_signedbv))
1847 {
1848 // pointer to integer, always ok
1850 return true;
1851 }
1852
1853 if(
1854 (e.type().id() == ID_unsignedbv || e.type().id() == ID_signedbv ||
1855 e.type().id() == ID_c_bool || e.is_boolean()) &&
1856 type.id() == ID_pointer && !is_reference(type))
1857 {
1858 // integer to pointer
1859 if(simplify_expr(e, *this) == 0)
1860 {
1861 // NULL
1862 new_expr=e;
1864 new_expr.type()=type;
1865 }
1866 else
1867 {
1869 }
1870 return true;
1871 }
1872
1873 if(e.type().id()==ID_pointer &&
1874 type.id()==ID_pointer &&
1875 !is_reference(type))
1876 {
1877 // pointer to pointer: we ok it all.
1878 // This is more generous than the standard.
1880 return true;
1881 }
1882
1883 if(is_reference(type) && e.get_bool(ID_C_lvalue))
1884 {
1886 return true;
1887 }
1888
1889 return false;
1890}
1891
1893 const exprt &expr, // source expression
1894 const typet &type, // destination type
1895 exprt &new_expr,
1896 bool check_constantness)
1897{
1898 exprt e=expr;
1899
1900 if(check_constantness && type.id()==ID_pointer)
1901 {
1903 e = to_dereference_expr(expr).pointer();
1904
1905 if(e.type().id()==ID_pointer &&
1906 cast_away_constness(e.type(), type))
1907 return false;
1908 }
1909
1911
1912 if(type.get_bool(ID_C_reference))
1913 {
1915 unsigned rank=0;
1917 return true;
1918
1920 typet from = e.type();
1921
1922 if(subto.id() == ID_struct_tag && from.id() == ID_struct_tag)
1923 {
1924 if(!expr.get_bool(ID_C_lvalue))
1925 return false;
1926
1928 qual_from.read(e.type());
1929
1931 qual_to.read(subto);
1932
1933 if(!qual_to.is_subset_of(qual_from))
1934 return false;
1935
1938
1940 {
1941 if(e.id()==ID_dereference)
1942 {
1944 new_expr.swap(to_dereference_expr(e).pointer());
1945 return true;
1946 }
1947
1950 new_expr.swap(address_of);
1951 return true;
1952 }
1953 }
1954 return false;
1955 }
1956
1957 if(type.id()==ID_empty)
1958 {
1960 return true;
1961 }
1962
1963 // int/enum to enum
1964 if(type.id()==ID_c_enum_tag &&
1965 (e.type().id()==ID_signedbv ||
1966 e.type().id()==ID_unsignedbv ||
1967 e.type().id()==ID_c_enum_tag))
1968 {
1970 new_expr.remove(ID_C_lvalue);
1971 return true;
1972 }
1973
1975 {
1976 if(!cpp_is_pod(type))
1977 {
1980 e.source_location(),
1981 type,
1982 already_typechecked_exprt{new_expr},
1983 temporary);
1984 new_expr.swap(temporary);
1985 }
1986 else
1987 {
1988 // try to avoid temporary
1990 if(new_expr.get_bool(ID_C_lvalue))
1991 new_expr.remove(ID_C_lvalue);
1992 }
1993
1994 return true;
1995 }
1996
1997 if(type.id()==ID_pointer && e.type().id()==ID_pointer)
1998 {
2000 if(type.find(ID_to_member).is_nil() && e.type().find(ID_to_member).is_nil())
2001 {
2003 typet from = to_pointer_type(e.type()).base_type();
2004
2005 if(from.id()==ID_empty)
2006 {
2008 return true;
2009 }
2010
2011 if(to.id() == ID_struct_tag && from.id() == ID_struct_tag)
2012 {
2013 if(e.get_bool(ID_C_lvalue))
2014 {
2015 exprt tmp(e);
2017 return false;
2018 }
2019
2023 {
2025 new_expr.swap(e);
2026 return true;
2027 }
2028 }
2029
2030 return false;
2031 }
2032 else if(
2033 type.find(ID_to_member).is_not_nil() &&
2034 e.type().find(ID_to_member).is_not_nil())
2035 {
2036 if(pointer_type.base_type() != to_pointer_type(e.type()).base_type())
2037 return false;
2038
2040 static_cast<const typet &>(e.type().find(ID_to_member))));
2041
2043 static_cast<const typet &>(type.find(ID_to_member))));
2044
2046 {
2048 return true;
2049 }
2050 }
2051 else if(
2052 type.find(ID_to_member).is_nil() &&
2053 e.type().find(ID_to_member).is_not_nil())
2054 {
2055 if(pointer_type.base_type() != to_pointer_type(e.type()).base_type())
2056 {
2057 return false;
2058 }
2059
2061 static_cast<const typet &>(e.type().find(ID_to_member)));
2062
2063 new_expr = e;
2065
2066 return true;
2067 }
2068 else
2069 return false;
2070 }
2071
2072 return false;
2073}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
floatbv_typet float_type()
Definition c_types.cpp:177
reference_typet reference_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
typet c_bool_type()
Definition c_types.cpp:100
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:185
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:80
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
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:562
static void make_already_typechecked(exprt &expr)
The Boolean type.
Definition std_types.h:36
Base type of functions.
Definition std_types.h:583
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
struct configt::ansi_ct ansi_c
bool reference_compatible(const exprt &expr, const reference_typet &type, unsigned &rank) const
Reference-compatible.
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
bool standard_conversion_floating_point_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-point conversion.
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool standard_conversion_boolean(const exprt &expr, exprt &new_expr) const
Boolean conversion.
bool standard_conversion_pointer(const exprt &expr, const typet &type, exprt &new_expr)
Pointer conversion.
void implicit_typecast(exprt &expr, const typet &type) override
bool reference_related(const exprt &expr, const reference_typet &type) const
Reference-related.
bool standard_conversion_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Integral conversion.
bool standard_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
Standard Conversion Sequence.
bool standard_conversion_qualification(const exprt &expr, const typet &, exprt &new_expr) const
Qualification conversion.
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
bool standard_conversion_floating_point_promotion(const exprt &expr, exprt &new_expr) const
Floating-point-promotion conversion.
bool standard_conversion_floating_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-integral conversion.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void show_instantiation_stack(std::ostream &)
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
bool user_defined_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
User-defined conversion sequence.
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
bool cast_away_constness(const typet &t1, const typet &t2) const
void add_implicit_dereference(exprt &)
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
bool standard_conversion_integral_promotion(const exprt &expr, exprt &new_expr) const
Integral-promotion conversion.
std::string to_string(const typet &) override
bool standard_conversion_pointer_to_member(const exprt &expr, const typet &type, exprt &new_expr)
Pointer-to-member conversion.
void reference_initializer(exprt &expr, const reference_typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
bool reference_binding(exprt expr, const reference_typet &type, exprt &new_expr, unsigned &rank)
Reference binding.
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:57
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:68
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:229
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:213
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
const source_locationt & source_location() const
Definition expr.h:236
Array index operator.
Definition std_expr.h:1470
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
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 remove(const irep_idt &name)
Definition irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
The reference type.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
An expression containing a side effect.
Definition std_code.h:1450
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition cpp_util.cpp:14
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:69
Deprecated expression utility functions.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:291
API to expression classes.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition std_types.h:434
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208