CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_resolve.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
13
14#ifdef DEBUG
15#include <iostream>
16#endif
17
18#include <util/arith_tools.h>
19#include <util/c_types.h>
21#include <util/simplify_expr.h>
22#include <util/std_expr.h>
24
26#include <ansi-c/merged_type.h>
27
28#include "cpp_convert_type.h"
29#include "cpp_type2name.h"
30#include "cpp_typecheck.h"
31#include "cpp_typecheck_fargs.h"
32#include "cpp_util.h"
33
34#include <algorithm>
35
41
45 resolve_identifierst &identifiers)
46{
47 for(const auto &id_ptr : id_set)
48 {
49 const cpp_idt &identifier = *id_ptr;
50 exprt e=convert_identifier(identifier, fargs);
51
52 if(e.is_not_nil())
53 {
54 CHECK_RETURN(e.id() != ID_type || e.type().is_not_nil());
55
56 identifiers.push_back(e);
57 }
58 }
59}
60
62 resolve_identifierst &identifiers,
65{
67 old_identifiers.swap(identifiers);
68
69 for(const auto &old_id : old_identifiers)
70 {
71 exprt e = old_id;
73
74 if(e.is_not_nil())
75 {
76 CHECK_RETURN(e.id() != ID_type || e.type().is_not_nil());
77
78 identifiers.push_back(e);
79 }
80 }
81}
82
85 resolve_identifierst &identifiers,
87{
89 old_identifiers.swap(identifiers);
90
91 for(const auto &old_id : old_identifiers)
92 {
94
95 if(e.is_not_nil())
96 {
97 CHECK_RETURN(e.id() != ID_type);
98 identifiers.push_back(e);
99 }
100 }
101
102 disambiguate_functions(identifiers, fargs);
103
104 // there should only be one left, or we have failed to disambiguate
105 if(identifiers.size()==1)
106 {
107 // instantiate that one
108 exprt e=*identifiers.begin();
110
113
116
117 // Let's build the instance.
118
119 const symbolt &new_symbol=
125
126 identifiers.clear();
127 identifiers.push_back(
128 symbol_exprt(new_symbol.name, new_symbol.type));
129 }
130}
131
133 resolve_identifierst &identifiers)
134{
136 old_identifiers.swap(identifiers);
137
138 for(const auto &old_id : old_identifiers)
139 {
140 const typet &followed =
141 old_id.type().id() == ID_struct_tag
142 ? static_cast<const typet &>(
144 : old_id.type().id() == ID_union_tag
145 ? static_cast<const typet &>(
147 : old_id.type().id() == ID_c_enum_tag
148 ? static_cast<const typet &>(
150 : old_id.type();
151 if(!followed.get_bool(ID_is_template))
152 identifiers.push_back(old_id);
153 }
154}
155
157 resolve_identifierst &identifiers)
158{
160 old_identifiers.swap(identifiers);
161
162 std::set<irep_idt> ids;
163 std::set<exprt> other;
164
165 for(const auto &old_id : old_identifiers)
166 {
167 irep_idt id;
168
169 if(old_id.id() == ID_symbol)
170 id = to_symbol_expr(old_id).get_identifier();
171 else if(old_id.id() == ID_type && old_id.type().id() == ID_struct_tag)
172 id = to_struct_tag_type(old_id.type()).get_identifier();
173 else if(old_id.id() == ID_type && old_id.type().id() == ID_union_tag)
174 id = to_union_tag_type(old_id.type()).get_identifier();
175
176 if(id.empty())
177 {
178 if(other.insert(old_id).second)
179 identifiers.push_back(old_id);
180 }
181 else
182 {
183 if(ids.insert(id).second)
184 identifiers.push_back(old_id);
185 }
186 }
187}
188
190 const cpp_idt &identifier)
191{
192#ifdef DEBUG
193 std::cout << "RESOLVE MAP:\n";
195#endif
196
197 // look up the parameter in the template map
199
200 if(e.is_nil() ||
201 (e.id()==ID_type && e.type().is_nil()))
202 {
204 cpp_typecheck.error() << "internal error: template parameter "
205 << "without instance:\n"
206 << identifier << messaget::eom;
207 throw 0;
208 }
209
211
212 return e;
213}
214
216 const cpp_idt &identifier,
218{
220 return convert_template_parameter(identifier);
221
222 exprt e;
223
224 if(identifier.is_member &&
225 !identifier.is_constructor &&
226 !identifier.is_static_member)
227 {
228 // a regular struct or union member
229
232
234 compound_symbol.type.id() == ID_struct ||
235 compound_symbol.type.id() == ID_union);
236
239
240 const exprt &component =
241 struct_union_type.get_component(identifier.identifier);
242
243 const typet &type=component.type();
244 DATA_INVARIANT(type.is_not_nil(), "type must not be nil");
245
247 {
248 e=type_exprt(type);
249 }
250 else if(identifier.id_class==cpp_scopet::id_classt::SYMBOL)
251 {
252 // A non-static, non-type member.
253 // There has to be an object.
254 e=exprt(ID_member);
255 e.set(ID_component_name, identifier.identifier);
257
258 exprt object;
259 object.make_nil();
260
261 #if 0
262 std::cout << "I: " << identifier.class_identifier
263 << " "
265 this_class_identifier << '\n';
266 #endif
267
268 const exprt &this_expr=
270
271 if(fargs.has_object)
272 {
273 // the object is given to us in fargs
274 PRECONDITION(!fargs.operands.empty());
275 object=fargs.operands.front();
276 }
277 else if(this_expr.is_not_nil())
278 {
279 // use this->...
281 this_expr.type().id() == ID_pointer,
282 "this argument should be pointer");
283 object =
284 exprt(ID_dereference, to_pointer_type(this_expr.type()).base_type());
285 object.copy_to_operands(this_expr);
286 object.type().set(
288 to_pointer_type(this_expr.type())
289 .base_type()
290 .get_bool(ID_C_constant));
291 object.set(ID_C_lvalue, true);
292 object.add_source_location()=source_location;
293 }
294
295 // check if the member can be applied to the object
296 if(
297 (object.type().id() != ID_struct_tag &&
298 object.type().id() != ID_union_tag) ||
299 !has_component_rec(object.type(), identifier.identifier, cpp_typecheck))
300 {
301 // failed
302 object.make_nil();
303 }
304
305 if(object.is_not_nil())
306 {
307 // we got an object
308 e.add_to_operands(std::move(object));
309
314 }
315 else
316 {
317 // this has to be a method or form a pointer-to-member expression
318 if(identifier.is_method)
320 else
321 {
322 e.id(ID_ptrmember);
325 : ID_union_tag,
326 identifier.class_identifier};
328 e.type() = type;
329 }
330 }
331 }
332 }
333 else
334 {
335 const symbolt &symbol=
336 cpp_typecheck.lookup(identifier.identifier);
337
338 if(symbol.is_type)
339 {
340 e.make_nil();
341
342 if(symbol.is_macro) // includes typedefs
343 {
344 e = type_exprt(symbol.type);
345 PRECONDITION(symbol.type.is_not_nil());
346 }
347 else if(symbol.type.id()==ID_c_enum)
348 {
349 e = type_exprt(c_enum_tag_typet(symbol.name));
350 }
351 else if(symbol.type.id() == ID_struct)
352 {
353 e = type_exprt(struct_tag_typet(symbol.name));
354 }
355 else if(symbol.type.id() == ID_union)
356 {
357 e = type_exprt(union_tag_typet(symbol.name));
358 }
359 }
360 else if(symbol.is_macro)
361 {
362 e=symbol.value;
364 }
365 else
366 {
367 bool constant = symbol.type.get_bool(ID_C_constant);
368
369 if(
370 constant && symbol.value.is_not_nil() && is_number(symbol.type) &&
371 symbol.value.is_constant())
372 {
373 e=symbol.value;
374 }
375 else
376 {
377 e=cpp_symbol_expr(symbol);
378 }
379 }
380 }
381
383
384 return e;
385}
386
388 resolve_identifierst &identifiers,
389 const wantt want)
390{
392 old_identifiers.swap(identifiers);
393
394 for(const auto &old_id : old_identifiers)
395 {
396 bool match=false;
397
398 switch(want)
399 {
400 case wantt::TYPE:
401 match = (old_id.id() == ID_type);
402 break;
403
404 case wantt::VAR:
405 match = (old_id.id() != ID_type);
406 break;
407
408 case wantt::BOTH:
409 match=true;
410 break;
411
412 default:
414 }
415
416 if(match)
417 identifiers.push_back(old_id);
418 }
419}
420
422 resolve_identifierst &identifiers,
424{
425 if(!fargs.in_use)
426 return;
427
429 old_identifiers.swap(identifiers);
430
431 identifiers.clear();
432
433 // put in the ones that match precisely
434 for(const auto &old_id : old_identifiers)
435 {
436 unsigned distance;
437 if(disambiguate_functions(old_id, distance, fargs))
438 if(distance<=0)
439 identifiers.push_back(old_id);
440 }
441}
442
444 resolve_identifierst &identifiers,
446{
448 old_identifiers.swap(identifiers);
449
450 // sort according to distance
451 std::multimap<std::size_t, exprt> distance_map;
452
453 for(const auto &old_id : old_identifiers)
454 {
455 unsigned args_distance;
456
458 {
459 std::size_t template_distance=0;
460
461 if(!old_id.type().get(ID_C_template).empty())
464 .find(ID_arguments)
465 .get_sub()
466 .size();
467
468 // we give strong preference to functions that have
469 // fewer template arguments
470 std::size_t total_distance=
471 // NOLINTNEXTLINE(whitespace/operators)
473
475 }
476 }
477
479
480 // put in the top ones
481 if(!distance_map.empty())
482 {
483 auto range = distance_map.equal_range(distance_map.begin()->first);
484 for(auto it = range.first; it != range.second; ++it)
485 old_identifiers.push_back(it->second);
486 }
487
488 if(old_identifiers.size() > 1 && fargs.in_use)
489 {
490 // try to further disambiguate functions
491
492 for(resolve_identifierst::const_iterator old_it = old_identifiers.begin();
493 old_it != old_identifiers.end();
494 ++old_it)
495 {
496#if 0
497 std::cout << "I1: " << old_it->get(ID_identifier) << '\n';
498#endif
499
500 if(old_it->type().id() != ID_code)
501 {
502 identifiers.push_back(*old_it);
503 continue;
504 }
505
506 const code_typet &f1 = to_code_type(old_it->type());
507
508 for(resolve_identifierst::const_iterator resolve_it = old_it + 1;
510 ++resolve_it)
511 {
512 if(resolve_it->type().id() != ID_code)
513 continue;
514
515 const code_typet &f2 = to_code_type(resolve_it->type());
516
517 // TODO: may fail when using ellipsis
519 f1.parameters().size() == f2.parameters().size(),
520 "parameter numbers should match");
521
522 bool f1_better=true;
523 bool f2_better=true;
524
525 for(std::size_t i=0;
526 i<f1.parameters().size() && (f1_better || f2_better);
527 i++)
528 {
529 typet type1=f1.parameters()[i].type();
530 typet type2=f2.parameters()[i].type();
531
532 if(type1 == type2)
533 continue;
534
536 continue;
537
538 if(type1.id()==ID_pointer)
539 {
540 typet tmp = to_pointer_type(type1).base_type();
541 type1=tmp;
542 }
543
544 if(type2.id()==ID_pointer)
545 {
546 typet tmp = to_pointer_type(type2).base_type();
547 type2=tmp;
548 }
549
550 if(type1.id() != ID_struct_tag || type2.id() != ID_struct_tag)
551 continue;
552
553 if(
557 {
558 f2_better=false;
559 }
560 else if(
564 {
565 f1_better=false;
566 }
567 }
568
569 if(!f1_better || f2_better)
570 identifiers.push_back(*resolve_it);
571 }
572 }
573 }
574 else
575 {
576 identifiers.swap(old_identifiers);
577 }
578
579 remove_duplicates(identifiers);
580}
581
583 resolve_identifierst &identifiers)
584{
586
587 for(const auto &identifier : identifiers)
588 {
589 if(identifier.id() != ID_type)
590 {
591 // already an expression
592 new_identifiers.push_back(identifier);
593 continue;
594 }
595
596 // is it a POD?
597
598 if(cpp_typecheck.cpp_is_pod(identifier.type()))
599 {
600 // there are two pod constructors:
601
602 // 1. no arguments, default initialization
603 {
604 const code_typet t1({}, identifier.type());
607 }
608
609 // 2. one argument, copy/conversion
610 {
611 const code_typet t2(
612 {code_typet::parametert(identifier.type())}, identifier.type());
615 }
616
617 // enums, in addition, can also be constructed from int
618 if(identifier.type().id() == ID_c_enum_tag)
619 {
620 const code_typet t3(
621 {code_typet::parametert(signed_int_type())}, identifier.type());
624 }
625 }
626 else if(identifier.type().id() == ID_struct_tag)
627 {
629 cpp_typecheck.follow_tag(to_struct_tag_type(identifier.type()));
630
631 // go over components
632 for(const auto &component : struct_type.components())
633 {
634 const typet &type=component.type();
635
636 if(component.get_bool(ID_from_base))
637 continue;
638
639 if(
640 type.id() == ID_code &&
641 to_code_type(type).return_type().id() == ID_constructor)
642 {
643 const symbolt &symb =
644 cpp_typecheck.lookup(component.get_name());
646 e.type()=type;
647 new_identifiers.push_back(e);
648 }
649 }
650 }
651 }
652
653 identifiers.swap(new_identifiers);
654}
655
659{
660 if(argument.id() == ID_ambiguous) // could come from a template parameter
661 {
662 // this must be resolved in the template scope
665
667 }
668}
669
671 const irep_idt &base_name,
674{
675 exprt dest;
676
678 template_args.arguments();
679
680 if(base_name==ID_unsignedbv ||
681 base_name==ID_signedbv)
682 {
683 if(arguments.size()!=1)
684 {
687 << base_name << " expects one template argument, but got "
688 << arguments.size() << messaget::eom;
689 throw 0;
690 }
691
692 exprt argument=arguments.front(); // copy
693
694 if(argument.id()==ID_type)
695 {
698 << base_name << " expects one integer template argument, "
699 << "but got type" << messaget::eom;
700 throw 0;
701 }
702
704
705 const auto i = numeric_cast<mp_integer>(argument);
706 if(!i.has_value())
707 {
709 cpp_typecheck.error() << "template argument must be constant"
710 << messaget::eom;
711 throw 0;
712 }
713
714 if(*i < 1)
715 {
718 << "template argument must be greater than zero"
719 << messaget::eom;
720 throw 0;
721 }
722
723 dest=type_exprt(typet(base_name));
724 dest.type().set(ID_width, integer2string(*i));
725 }
726 else if(base_name==ID_fixedbv)
727 {
728 if(arguments.size()!=2)
729 {
732 << base_name << " expects two template arguments, but got "
733 << arguments.size() << messaget::eom;
734 throw 0;
735 }
736
737 exprt argument0=arguments[0];
739 exprt argument1=arguments[1];
741
742 if(argument0.id()==ID_type)
743 {
744 cpp_typecheck.error().source_location=argument0.find_source_location();
746 << base_name << " expects two integer template arguments, "
747 << "but got type" << messaget::eom;
748 throw 0;
749 }
750
751 if(argument1.id()==ID_type)
752 {
753 cpp_typecheck.error().source_location=argument1.find_source_location();
755 << base_name << " expects two integer template arguments, "
756 << "but got type" << messaget::eom;
757 throw 0;
758 }
759
760 const auto width = numeric_cast<mp_integer>(argument0);
761
762 if(!width.has_value())
763 {
764 cpp_typecheck.error().source_location=argument0.find_source_location();
765 cpp_typecheck.error() << "template argument must be constant"
766 << messaget::eom;
767 throw 0;
768 }
769
770 const auto integer_bits = numeric_cast<mp_integer>(argument1);
771
772 if(!integer_bits.has_value())
773 {
774 cpp_typecheck.error().source_location=argument1.find_source_location();
775 cpp_typecheck.error() << "template argument must be constant"
776 << messaget::eom;
777 throw 0;
778 }
779
780 if(*width < 1)
781 {
782 cpp_typecheck.error().source_location=argument0.find_source_location();
784 << "template argument must be greater than zero"
785 << messaget::eom;
786 throw 0;
787 }
788
789 if(*integer_bits < 0)
790 {
791 cpp_typecheck.error().source_location=argument1.find_source_location();
793 << "template argument must be greater or equal zero"
794 << messaget::eom;
795 throw 0;
796 }
797
798 if(*integer_bits > *width)
799 {
800 cpp_typecheck.error().source_location=argument1.find_source_location();
802 << "template argument must be smaller or equal width"
803 << messaget::eom;
804 throw 0;
805 }
806
807 dest=type_exprt(typet(base_name));
808 dest.type().set(ID_width, integer2string(*width));
809 dest.type().set(ID_integer_bits, integer2string(*integer_bits));
810 }
811 else if(base_name==ID_integer)
812 {
813 if(!arguments.empty())
814 {
817 << base_name << " expects no template arguments"
818 << messaget::eom;
819 throw 0;
820 }
821
822 dest=type_exprt(typet(base_name));
823 }
824 else if(base_name.starts_with("constant_infinity"))
825 {
826 // ok, but type missing
827 dest=exprt(ID_infinity, size_type());
828 }
829 else if(base_name=="dump_scopes")
830 {
832 cpp_typecheck.warning() << "Scopes in location "
836 }
837 else if(base_name=="current_scope")
838 {
840 cpp_typecheck.warning() << "Scope in location " << source_location
841 << ": " << original_scope->prefix
842 << messaget::eom;
843 }
844 else if(base_name == ID_size_t)
845 {
846 dest=type_exprt(size_type());
847 }
848 else if(base_name == ID_ssize_t)
849 {
851 }
852 else
853 {
855 cpp_typecheck.error() << "unknown built-in identifier: "
856 << base_name << messaget::eom;
857 throw 0;
858 }
859
860 return dest;
861}
862
867 const cpp_namet &cpp_name,
868 irep_idt &base_name,
870{
871 PRECONDITION(!cpp_name.get_sub().empty());
872
874 source_location=cpp_name.source_location();
875
876 irept::subt::const_iterator pos=cpp_name.get_sub().begin();
877
878 bool recursive=true;
879
880 // check if we need to go to the root scope
881 if(pos->id()=="::")
882 {
883 pos++;
885 recursive=false;
886 }
887
888 std::string final_base_name;
889 template_args.make_nil();
890
891 while(pos!=cpp_name.get_sub().end())
892 {
893 if(pos->id()==ID_name)
894 final_base_name+=pos->get_string(ID_identifier);
895 else if(pos->id()==ID_template_args)
897 else if(pos->id()=="::")
898 {
899 if(template_args.is_not_nil())
900 {
905
906#ifdef DEBUG
907 std::cout << "S: "
909 << '\n';
911 std::cout << "X: " << id_set.size() << '\n';
912#endif
915
916 instance.add_source_location()=source_location;
917
918 // the "::" triggers template elaboration
920
922 cpp_typecheck.cpp_scopes.get_scope(instance.get_identifier()));
923
924 template_args.make_nil();
925 }
926 else
927 {
931
933
934 if(id_set.empty())
935 {
939 << "scope '" << final_base_name << "' not found" << messaget::eom;
940 throw 0;
941 }
942 else if(id_set.size()>=2)
943 {
946 cpp_typecheck.error() << "scope '" << final_base_name
947 << "' is ambiguous" << messaget::eom;
948 throw 0;
949 }
950
951 CHECK_RETURN(id_set.size() == 1);
952
954
955 // the "::" triggers template elaboration
957 {
961 }
962 }
963
964 // we start from fresh
966 }
967 else if(pos->id()==ID_operator)
968 {
969 final_base_name+="operator";
970
971 irept::subt::const_iterator next=pos+1;
972 CHECK_RETURN(next != cpp_name.get_sub().end());
973
974 if(
975 next->id() == ID_cpp_name || next->id() == ID_pointer ||
976 next->id() == ID_int || next->id() == ID_char ||
977 next->id() == ID_c_bool || next->id() == ID_merged_type)
978 {
979 // it's a cast operator
980 irept next_ir=*next;
981 typet op_name;
982 op_name.swap(next_ir);
984 final_base_name+="("+cpp_type2name(op_name)+")";
985 pos++;
986 }
987 }
988 else
989 final_base_name+=pos->id_string();
990
991 pos++;
992 }
993
994 base_name=final_base_name;
995
997}
998
1001 const irep_idt &base_name,
1003 const cpp_template_args_non_tct &full_template_args)
1004{
1005 if(id_set.empty())
1006 {
1009 cpp_typecheck.error() << "template scope '" << base_name << "' not found"
1010 << messaget::eom;
1011 throw 0;
1012 }
1013
1014 std::set<irep_idt> primary_templates;
1015
1016 for(const auto &id_ptr : id_set)
1017 {
1018 const irep_idt id = id_ptr->identifier;
1019 const symbolt &s=cpp_typecheck.lookup(id);
1021 continue;
1023 if(!cpp_declaration.is_class_template())
1024 continue;
1025 irep_idt specialization_of=cpp_declaration.get_specialization_of();
1026 if(!specialization_of.empty())
1028 else
1029 primary_templates.insert(id);
1030 }
1031
1033
1034 if(primary_templates.size()>=2)
1035 {
1038 cpp_typecheck.error() << "template scope '" << base_name << "' is ambiguous"
1039 << messaget::eom;
1040 throw 0;
1041 }
1042
1045
1046 // We typecheck the template arguments in the context
1047 // of the original scope!
1049
1050 {
1052
1054
1055 // use template type of 'primary template'
1060 full_template_args);
1061
1062 for(auto &arg : full_template_args_tc.arguments())
1063 {
1064 if(arg.id() == ID_type)
1065 continue;
1066 if(arg.id() == ID_symbol)
1067 {
1068 const symbol_exprt &s = to_symbol_expr(arg);
1069 const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier());
1070
1071 if(
1072 cpp_typecheck.cpp_is_pod(symbol.type) &&
1073 symbol.type.get_bool(ID_C_constant))
1074 {
1075 arg = symbol.value;
1076 }
1077 }
1078 simplify(arg, cpp_typecheck);
1079 }
1080
1081 // go back to where we used to be
1082 }
1083
1084 // find any matches
1085
1086 std::vector<matcht> matches;
1087
1088 // the baseline
1089 matches.push_back(
1092
1093 for(const auto &id_ptr : id_set)
1094 {
1095 const irep_idt id = id_ptr->identifier;
1096 const symbolt &s=cpp_typecheck.lookup(id);
1097
1098 if(s.type.get(ID_specialization_of).empty())
1099 continue;
1100
1103
1104 const cpp_template_args_non_tct &partial_specialization_args=
1105 cpp_declaration.partial_specialization_args();
1106
1107 // alright, set up template arguments as 'unassigned'
1108
1111
1113 cpp_declaration.template_type());
1114
1115 // iterate over template instance
1117 full_template_args_tc.arguments().size() ==
1118 partial_specialization_args.arguments().size(),
1119 "number of arguments should match");
1120
1121 // we need to do this in the right scope
1122
1124 static_cast<cpp_scopet *>(
1126
1127 if(template_scope==nullptr)
1128 {
1130 cpp_typecheck.error() << "template identifier: " << id << '\n'
1131 << "class template instantiation error"
1132 << messaget::eom;
1133 throw 0;
1134 }
1135
1136 // enter the scope of the template
1138
1139 for(std::size_t i=0; i<full_template_args_tc.arguments().size(); i++)
1140 {
1141 if(full_template_args_tc.arguments()[i].id()==ID_type)
1142 guess_template_args(partial_specialization_args.arguments()[i].type(),
1143 full_template_args_tc.arguments()[i].type());
1144 else
1145 guess_template_args(partial_specialization_args.arguments()[i],
1146 full_template_args_tc.arguments()[i]);
1147 }
1148
1149 // see if that has worked out
1150
1153 cpp_declaration.template_type());
1154
1155 if(!guessed_template_args.has_unassigned())
1156 {
1157 // check: we can now typecheck the partial_specialization_args
1158
1163 partial_specialization_args);
1164
1165 // if these match the arguments, we have a match
1166
1168 partial_specialization_args_tc.arguments().size() ==
1169 full_template_args_tc.arguments().size(),
1170 "argument numbers must match");
1171
1174 {
1175 matches.push_back(matcht(
1177 }
1178 }
1179 }
1180
1181 CHECK_RETURN(!matches.empty());
1182
1183 std::sort(matches.begin(), matches.end());
1184
1185 #if 0
1186 for(std::vector<matcht>::const_iterator
1187 m_it=matches.begin();
1188 m_it!=matches.end();
1189 m_it++)
1190 {
1191 std::cout << "M: " << m_it->cost
1192 << " " << m_it->id << '\n';
1193 }
1194
1195 std::cout << '\n';
1196 #endif
1197
1198 const matcht &match=*matches.begin();
1199
1200 const symbolt &choice=
1201 cpp_typecheck.lookup(match.id);
1202
1203 #if 0
1204 // build instance
1205 const symbolt &instance=
1208 choice,
1209 match.specialization_args,
1210 match.full_args);
1211
1212 if(instance.type.id()!=ID_struct)
1213 {
1215 cpp_typecheck.error() << "template '"
1216 << base_name << "' is not a class" << messaget::eom;
1217 throw 0;
1218 }
1219
1220 struct_tag_typet result(instance.name);
1222
1223 return result;
1224 #else
1225
1226 // build instance
1227 const symbolt &instance=
1230 choice,
1231 match.specialization_args,
1232 match.full_args);
1233
1234 struct_tag_typet result(instance.name);
1236
1237 return result;
1238 #endif
1239}
1240
1242 const cpp_namet &cpp_name)
1243{
1244 irep_idt base_name;
1246 template_args.make_nil();
1247
1250
1251 bool qualified=cpp_name.is_qualified();
1252
1255
1257
1258 if(id_set.empty())
1259 {
1261 cpp_typecheck.error() << "namespace '" << base_name << "' not found"
1262 << messaget::eom;
1263 throw 0;
1264 }
1265 else if(id_set.size()==1)
1266 {
1267 cpp_idt &id=**id_set.begin();
1268 return (cpp_scopet &)id;
1269 }
1270 else
1271 {
1273 cpp_typecheck.error() << "namespace '" << base_name << "' is ambiguous"
1274 << messaget::eom;
1275 throw 0;
1276 }
1277}
1278
1280 const irep_idt &base_name,
1281 const resolve_identifierst &identifiers,
1282 std::ostream &out)
1283{
1284 for(const auto &id_expr : identifiers)
1285 {
1286 out << " ";
1287
1288 if(id_expr.id()==ID_type)
1289 {
1290 out << "type " << cpp_typecheck.to_string(id_expr.type());
1291 }
1292 else
1293 {
1294 irep_idt id;
1295
1296 if(id_expr.type().get_bool(ID_is_template))
1297 out << "template ";
1298
1299 if(id_expr.id()==ID_member)
1300 {
1301 out << "member ";
1302 id="."+id2string(base_name);
1303 }
1304 else if(id_expr.id() == ID_pod_constructor)
1305 {
1306 out << "constructor ";
1307 id.clear();
1308 }
1310 {
1311 out << "symbol ";
1312 }
1313 else
1314 {
1315 out << "symbol ";
1317 }
1318
1319 if(id_expr.type().get_bool(ID_is_template))
1320 {
1321 }
1322 else if(id_expr.type().id()==ID_code)
1323 {
1325 const typet &return_type=code_type.return_type();
1326 const code_typet::parameterst &parameters=code_type.parameters();
1327 out << cpp_typecheck.to_string(return_type);
1328 out << " " << id << "(";
1329
1330 bool first = true;
1331
1332 for(const auto &parameter : parameters)
1333 {
1334 const typet &parameter_type = parameter.type();
1335
1336 if(first)
1337 first = false;
1338 else
1339 out << ", ";
1340
1342 }
1343
1344 if(code_type.has_ellipsis())
1345 {
1346 if(!parameters.empty())
1347 out << ", ";
1348 out << "...";
1349 }
1350
1351 out << ")";
1352 }
1353 else
1354 out << id << ": " << cpp_typecheck.to_string(id_expr.type());
1355
1356 if(id_expr.id()==ID_symbol)
1357 {
1359 out << " (" << symbol.location << ")";
1360 }
1362 {
1363 const symbolt &symbol=
1365 out << " (" << symbol.location << ")";
1366 }
1367 }
1368
1369 out << '\n';
1370 }
1371}
1372
1374 const cpp_namet &cpp_name,
1375 const wantt want,
1378{
1379 irep_idt base_name;
1381 template_args.make_nil();
1382
1385
1386 // this changes the scope
1388
1389#ifdef DEBUG
1390 std::cout << "base name: " << base_name << '\n';
1391 std::cout << "template args: " << template_args.pretty() << '\n';
1392 std::cout << "original-scope: " << original_scope->prefix << '\n';
1393 std::cout << "scope: " << cpp_typecheck.cpp_scopes.current_scope().prefix
1394 << '\n';
1395#endif
1396
1397 bool qualified=cpp_name.is_qualified();
1398
1399 // do __CPROVER scope
1400 if(qualified)
1401 {
1403 return do_builtin(base_name, fargs, template_args);
1404 }
1405 else
1406 {
1407 if(base_name=="__func__" ||
1408 base_name=="__FUNCTION__" ||
1409 base_name=="__PRETTY_FUNCTION__")
1410 {
1411 // __func__ is an ANSI-C standard compliant hack to get the function name
1412 // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
1415 return std::move(s);
1416 }
1417 }
1418
1420
1423
1424 if(template_args.is_nil())
1425 {
1426 id_set =
1428
1429 if(id_set.empty() && !cpp_typecheck.builtin_factory(base_name))
1430 {
1433 builtin_id.identifier = base_name;
1435
1436 id_set.insert(&builtin_id);
1437 }
1438 }
1439 else
1442
1443 // Argument-dependent name lookup
1444 #if 0
1445 // not clear what this is good for
1446 if(!qualified && !fargs.has_object)
1447 resolve_with_arguments(id_set, base_name, fargs);
1448 #endif
1449
1450 if(id_set.empty())
1451 {
1453 return nil_exprt();
1454
1457
1458 if(qualified)
1459 {
1460 cpp_typecheck.error() << "symbol '" << base_name << "' not found";
1461
1463 cpp_typecheck.error() << " in root scope";
1464 else
1466 << " in scope '" << cpp_typecheck.cpp_scopes.current_scope().prefix
1467 << "'";
1468 }
1469 else
1470 {
1471 cpp_typecheck.error() << "symbol '" << base_name << "' is unknown";
1472 }
1473
1475 // cpp_typecheck.cpp_scopes.get_root_scope().print(std::cout);
1476 // cpp_typecheck.cpp_scopes.current_scope().print(std::cout);
1477 throw 0;
1478 }
1479
1480 resolve_identifierst identifiers;
1481
1482 if(template_args.is_not_nil())
1483 {
1484 // first figure out if we are doing functions/methods or
1485 // classes
1486 bool have_classes=false, have_methods=false;
1487
1488 for(const auto &id_ptr : id_set)
1489 {
1490 const irep_idt id = id_ptr->identifier;
1491 const symbolt &s=cpp_typecheck.lookup(id);
1494 have_classes=true;
1495 else
1496 have_methods=true;
1497 }
1498
1500 {
1502 return nil_exprt();
1503
1506 cpp_typecheck.error() << "template symbol '" << base_name
1507 << "' is ambiguous" << messaget::eom;
1508 throw 0;
1509 }
1510
1512 {
1515
1517
1518 identifiers.push_back(exprt(ID_type, instance));
1519 }
1520 else
1521 {
1522 // methods and functions
1524 id_set, fargs, identifiers);
1525
1527 identifiers, template_args, fargs);
1528 }
1529 }
1530 else
1531 {
1533 id_set, fargs, identifiers);
1534 }
1535
1536 // change types into constructors if we want a constructor
1537 if(want==wantt::VAR)
1538 make_constructors(identifiers);
1539
1540 filter(identifiers, want);
1541
1542#ifdef DEBUG
1543 std::cout << "P0 " << base_name << " " << identifiers.size() << '\n';
1544 show_identifiers(base_name, identifiers, std::cout);
1545 std::cout << '\n';
1546#endif
1547
1548 exprt result;
1549
1550 // We disambiguate functions
1552
1554
1555#ifdef DEBUG
1556 std::cout << "P1 " << base_name << " " << new_identifiers.size() << '\n';
1557 show_identifiers(base_name, new_identifiers, std::cout);
1558 std::cout << '\n';
1559#endif
1560
1561 // we only want _exact_ matches, without templates!
1563
1564#ifdef DEBUG
1565 std::cout << "P2 " << base_name << " " << new_identifiers.size() << '\n';
1566 show_identifiers(base_name, new_identifiers, std::cout);
1567 std::cout << '\n';
1568#endif
1569
1570 // no exact matches? Try again with function template guessing.
1571 if(new_identifiers.empty())
1572 {
1573 new_identifiers=identifiers;
1574
1575 if(template_args.is_nil())
1576 {
1578
1579 if(new_identifiers.empty())
1580 new_identifiers=identifiers;
1581 }
1582
1584
1585#ifdef DEBUG
1586 std::cout << "P3 " << base_name << " " << new_identifiers.size() << '\n';
1587 show_identifiers(base_name, new_identifiers, std::cout);
1588 std::cout << '\n';
1589#endif
1590 }
1591 else
1593
1594#ifdef DEBUG
1595 std::cout << "P4 " << base_name << " " << new_identifiers.size() << '\n';
1596 show_identifiers(base_name, new_identifiers, std::cout);
1597 std::cout << '\n';
1598#endif
1599
1600 if(new_identifiers.size()==1)
1601 {
1602 result=*new_identifiers.begin();
1603 }
1604 else
1605 {
1606 // nothing or too many
1608 return nil_exprt();
1609
1610 if(new_identifiers.empty())
1611 {
1614 << "found no match for symbol '" << base_name << "', candidates are:\n";
1615 show_identifiers(base_name, identifiers, cpp_typecheck.error());
1616 }
1617 else
1618 {
1621 << "symbol '" << base_name << "' does not uniquely resolve:\n";
1623
1624#ifdef DEBUG
1625 exprt e1=*new_identifiers.begin();
1626 exprt e2=*(++new_identifiers.begin());
1627 cpp_typecheck.error() << "e1==e2: " << (e1 == e2) << '\n';
1629 << "e1.type==e2.type: " << (e1.type() == e2.type()) << '\n';
1631 << "e1.id()==e2.id(): " << (e1.id() == e2.id()) << '\n';
1633 << "e1.iden==e2.iden: "
1634 << (e1.get(ID_identifier) == e2.get(ID_identifier)) << '\n';
1635 cpp_typecheck.error() << "e1.iden:: " << e1.get(ID_identifier) << '\n';
1636 cpp_typecheck.error() << "e2.iden:: " << e2.get(ID_identifier) << '\n';
1637#endif
1638 }
1639
1640 if(fargs.in_use)
1641 {
1642 cpp_typecheck.error() << "\nargument types:\n";
1643
1644 for(const auto &op : fargs.operands)
1645 {
1647 << " " << cpp_typecheck.to_string(op.type()) << '\n';
1648 }
1649 }
1650
1652 {
1654 }
1655
1657 throw 0;
1658 }
1659
1660 // we do some checks before we return
1661 if(result.get_bool(ID_C_not_accessible))
1662 {
1663 #if 0
1665 return nil_exprt();
1666
1668 cpp_typecheck.error() << "member '" << result.get(ID_component_name)
1669 << "' is not accessible" << messaget::eom;
1670 throw 0;
1671 #endif
1672 }
1673
1674 switch(want)
1675 {
1676 case wantt::VAR:
1677 if(result.id()==ID_type && !cpp_typecheck.cpp_is_pod(result.type()))
1678 {
1680 return nil_exprt();
1681
1683
1685 << "expected expression, but got type '"
1686 << cpp_typecheck.to_string(result.type()) << "'" << messaget::eom;
1687
1688 throw 0;
1689 }
1690 break;
1691
1692 case wantt::TYPE:
1693 if(result.id()!=ID_type)
1694 {
1696 return nil_exprt();
1697
1699
1701 << "expected type, but got expression '"
1702 << cpp_typecheck.to_string(result) << "'" << messaget::eom;
1703
1704 throw 0;
1705 }
1706 break;
1707
1708 case wantt::BOTH:
1709 break;
1710 }
1711
1712 return result;
1713}
1714
1716 const exprt &template_expr,
1717 const exprt &desired_expr)
1718{
1719 if(template_expr.id()==ID_cpp_name)
1720 {
1721 const cpp_namet &cpp_name=
1723
1724 if(!cpp_name.is_qualified())
1725 {
1727
1729 irep_idt base_name;
1731
1733 base_name, cpp_scopet::RECURSIVE);
1734
1735 // alright, rummage through these
1736 for(const auto &id_ptr : id_set)
1737 {
1738 const cpp_idt &id = *id_ptr;
1739 // template parameter?
1741 {
1742 // see if unassigned
1743 exprt &e=cpp_typecheck.template_map.expr_map[id.identifier];
1744 if(e.id()==ID_unassigned)
1745 {
1746 typet old_type=e.type();
1748 }
1749 }
1750 }
1751 }
1752 }
1753}
1754
1756 const typet &template_type,
1757 const typet &desired_type)
1758{
1759 // look at
1760 // http://publib.boulder.ibm.com/infocenter/comphelp/v8v101/topic/
1761 // com.ibm.xlcpp8a.doc/language/ref/template_argument_deduction.htm
1762
1763 // T
1764 // const T
1765 // volatile T
1766 // T&
1767 // T*
1768 // T[10]
1769 // A<T>
1770 // C(*)(T)
1771 // T(*)()
1772 // T(*)(U)
1773 // T C::*
1774 // C T::*
1775 // T U::*
1776 // T (C::*)()
1777 // C (T::*)()
1778 // D (C::*)(T)
1779 // C (T::*)(U)
1780 // T (C::*)(U)
1781 // T (U::*)()
1782 // T (U::*)(V)
1783 // E[10][i]
1784 // B<i>
1785 // TT<T>
1786 // TT<i>
1787 // TT<C>
1788
1789 #if 0
1790 std::cout << "TT: " << template_type.pretty() << '\n';
1791 std::cout << "DT: " << desired_type.pretty() << '\n';
1792 #endif
1793
1794 if(template_type.id()==ID_cpp_name)
1795 {
1796 // we only care about cpp_names that are template parameters!
1797 const cpp_namet &cpp_name=to_cpp_name(template_type);
1798
1800
1801 if(cpp_name.has_template_args())
1802 {
1803 // this could be something like my_template<T>, and we need
1804 // to match 'T'. Then 'desired_type' has to be a template instance.
1805
1806 // TODO
1807 }
1808 else
1809 {
1810 // template parameters aren't qualified
1811 if(!cpp_name.is_qualified())
1812 {
1813 irep_idt base_name;
1816
1818 base_name, cpp_scopet::RECURSIVE);
1819
1820 // alright, rummage through these
1821 for(const auto &id_ptr : id_set)
1822 {
1823 const cpp_idt &id = *id_ptr;
1824
1825 // template argument?
1827 {
1828 // see if unassigned
1829 typet &t=cpp_typecheck.template_map.type_map[id.identifier];
1830 if(t.id()==ID_unassigned)
1831 {
1832 t=desired_type;
1833
1834 // remove const, volatile (these can be added in the call)
1837 #if 0
1838 std::cout << "ASSIGN " << id.identifier << " := "
1840 #endif
1841 }
1842 }
1843 }
1844 }
1845 }
1846 }
1847 else if(template_type.id()==ID_merged_type)
1848 {
1849 // look at subtypes
1850 for(const auto &t : to_merged_type(template_type).subtypes())
1851 {
1853 }
1854 }
1855 else if(is_reference(template_type) ||
1856 is_rvalue_reference(template_type))
1857 {
1859 to_reference_type(template_type).base_type(), desired_type);
1860 }
1861 else if(template_type.id()==ID_pointer)
1862 {
1863 if(desired_type.id() == ID_pointer)
1865 to_pointer_type(template_type).base_type(),
1866 to_pointer_type(desired_type).base_type());
1867 }
1868 else if(template_type.id()==ID_array)
1869 {
1870 if(desired_type.id() == ID_array)
1871 {
1872 // look at subtype first
1874 to_array_type(template_type).element_type(),
1875 to_array_type(desired_type).element_type());
1876
1877 // size (e.g., buffer size guessing)
1879 to_array_type(template_type).size(),
1880 to_array_type(desired_type).size());
1881 }
1882 }
1883}
1884
1887 const exprt &expr,
1889{
1890 const typet &tmp =
1891 expr.type().id() == ID_struct_tag
1892 ? static_cast<const typet &>(
1894 : expr.type().id() == ID_union_tag
1895 ? static_cast<const typet &>(
1897 : expr.type().id() == ID_c_enum_tag
1898 ? static_cast<const typet &>(
1900 : expr.type();
1901
1902 if(!tmp.get_bool(ID_is_template))
1903 return nil_exprt(); // not a template
1904
1905 PRECONDITION(expr.id() == ID_symbol);
1906
1907 // a template is always a declaration
1910
1911 // Class templates require explicit template arguments,
1912 // no guessing!
1913 if(cpp_declaration.is_class_template())
1914 return nil_exprt();
1915
1916 // we need function arguments for guessing
1917 if(fargs.operands.empty())
1918 return nil_exprt(); // give up
1919
1920 // We need to guess in the case of function templates!
1921
1923 to_symbol_expr(expr).get_identifier();
1924
1925 const symbolt &template_symbol=
1927
1928 // alright, set up template arguments as 'unassigned'
1929
1931
1933 cpp_declaration.template_type());
1934
1935 // there should be exactly one declarator
1936 PRECONDITION(cpp_declaration.declarators().size() == 1);
1937
1939 cpp_declaration.declarators().front();
1940
1941 // and that needs to have function type
1942 if(function_declarator.type().id()!=ID_function_type)
1943 {
1946 << "expected function type for function template"
1947 << messaget::eom;
1948 throw 0;
1949 }
1950
1952
1953 // we need the template scope
1955 static_cast<cpp_scopet *>(
1957
1958 if(template_scope==nullptr)
1959 {
1961 cpp_typecheck.error() << "template identifier: "
1962 << template_identifier << '\n'
1963 << "function template instantiation error"
1964 << messaget::eom;
1965 throw 0;
1966 }
1967
1968 // enter the scope of the template
1970
1971 // walk through the function parameters
1972 const irept::subt &parameters=
1973 function_declarator.type().find(ID_parameters).get_sub();
1974
1975 exprt::operandst::const_iterator it=fargs.operands.begin();
1976 for(const auto &parameter : parameters)
1977 {
1978 if(it==fargs.operands.end())
1979 break;
1980
1982 {
1985
1986 // again, there should be one declarator
1988 arg_declaration.declarators().size() == 1, "exactly one declarator");
1989
1990 // turn into type
1992 arg_declaration.declarators().front().
1993 merge_type(arg_declaration.type());
1994
1995 // We only convert the arg_type,
1996 // and don't typecheck it -- that could cause all
1997 // sorts of trouble.
1999
2000 guess_template_args(arg_type, it->type());
2001 }
2002
2003 ++it;
2004 }
2005
2006 // see if that has worked out
2007
2010 cpp_declaration.template_type());
2011
2012 if(template_args.has_unassigned())
2013 return nil_exprt(); // give up
2014
2015 // Build the type of the function.
2016
2017 typet function_type=
2018 function_declarator.merge_type(cpp_declaration.type());
2019
2020 cpp_typecheck.typecheck_type(function_type);
2021
2022 // Remember that this was a template
2023
2024 function_type.set(ID_C_template, template_symbol.name);
2026
2027 // Seems we got an instance for all parameters. Let's return that.
2028
2030 ID_template_function_instance, function_type);
2031
2033}
2034
2036 exprt &expr,
2039{
2040 if(expr.id()!=ID_symbol)
2041 return; // templates are always symbols
2042
2043 const symbolt &template_symbol =
2044 cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier());
2045
2046 if(!template_symbol.type.get_bool(ID_is_template))
2047 return;
2048
2049 #if 0
2050 if(template_args_non_tc.is_nil())
2051 {
2052 // no arguments, need to guess
2054 return;
2055 }
2056 #endif
2057
2058 // We typecheck the template arguments in the context
2059 // of the original scope!
2061
2062 {
2064
2066
2072 // go back to where we used to be
2073 }
2074
2075 // We never try 'unassigned' template arguments.
2076 if(template_args_tc.has_unassigned())
2078
2079 // a template is always a declaration
2082
2083 // is it a class template or function template?
2084 if(cpp_declaration.is_class_template())
2085 {
2086 const symbolt &new_symbol=
2092
2093 expr = type_exprt(struct_tag_typet(new_symbol.name));
2095 }
2096 else
2097 {
2098 // must be a function, maybe method
2099 const symbolt &new_symbol=
2105
2106 // check if it is a method
2107 const code_typet &code_type=to_code_type(new_symbol.type);
2108
2109 if(
2110 !code_type.parameters().empty() &&
2111 code_type.parameters().front().get_this())
2112 {
2113 // do we have an object?
2114 if(fargs.has_object)
2115 {
2116 const symbolt &type_symb=
2118 fargs.operands.begin()->type().get(ID_identifier));
2119
2120 CHECK_RETURN(type_symb.type.id() == ID_struct);
2121
2124
2125 DATA_INVARIANT(struct_type.has_component(new_symbol.name),
2126 "method should exist in struct");
2127
2128 member_exprt member(
2129 *fargs.operands.begin(),
2130 new_symbol.name,
2131 code_type);
2133 expr.swap(member);
2134 return;
2135 }
2136 }
2137
2138 expr=cpp_symbol_expr(new_symbol);
2140 }
2141}
2142
2144 const exprt &expr,
2145 unsigned &args_distance,
2147{
2148 args_distance=0;
2149
2150 if(expr.type().id()!=ID_code || !fargs.in_use)
2151 return true;
2152
2153 const code_typet &type=to_code_type(expr.type());
2154
2155 if(expr.id()==ID_member ||
2156 type.return_type().id() == ID_constructor)
2157 {
2158 // if it's a member, but does not have an object yet,
2159 // we add one
2160 if(!fargs.has_object)
2161 {
2162 const code_typet::parameterst &parameters=type.parameters();
2163 const code_typet::parametert &parameter=parameters.front();
2164
2165 INVARIANT(parameter.get_this(), "first parameter should be `this'");
2166
2167 if(type.return_type().id() == ID_constructor)
2168 {
2169 // it's a constructor
2170 const typet &object_type =
2171 to_pointer_type(parameter.type()).base_type();
2172 symbol_exprt object(irep_idt(), object_type);
2173 object.set(ID_C_lvalue, true);
2174
2176 new_fargs.add_object(object);
2177 return new_fargs.match(type, args_distance, cpp_typecheck);
2178 }
2179 else
2180 {
2181 if(
2182 expr.type().get_bool(ID_C_is_operator) &&
2183 fargs.operands.size() == parameters.size())
2184 {
2185 return fargs.match(type, args_distance, cpp_typecheck);
2186 }
2187
2189 new_fargs.add_object(to_member_expr(expr).compound());
2190
2191 return new_fargs.match(type, args_distance, cpp_typecheck);
2192 }
2193 }
2194 }
2195 else if(fargs.has_object)
2196 {
2197 // if it's not a member then we shall remove the object
2199 new_fargs.remove_object();
2200
2201 return new_fargs.match(type, args_distance, cpp_typecheck);
2202 }
2203
2204 return fargs.match(type, args_distance, cpp_typecheck);
2205}
2206
2209{
2211
2212 // std::cout << "FILTER\n";
2213
2214 // We only want scopes!
2215 for(const auto &id_ptr : id_set)
2216 {
2217 cpp_idt &id = *id_ptr;
2218
2219 if(id.is_class() || id.is_enum() || id.is_namespace())
2220 {
2221 // std::cout << "X1\n";
2222 DATA_INVARIANT(id.is_scope, "should be scope");
2223 new_set.insert(&id);
2224 }
2225 else if(id.is_typedef())
2226 {
2227 // std::cout << "X2\n";
2228 irep_idt identifier=id.identifier;
2229
2230 if(id.is_member)
2231 continue;
2232
2233 while(true)
2234 {
2235 const symbolt &symbol=cpp_typecheck.lookup(identifier);
2236 CHECK_RETURN(symbol.is_type);
2237
2238 // todo? maybe do enum here, too?
2239 if(symbol.type.id()==ID_struct)
2240 {
2241 // this is a scope, too!
2242 cpp_idt &class_id=
2243 cpp_typecheck.cpp_scopes.get_id(identifier);
2244
2245 DATA_INVARIANT(class_id.is_scope, "should be scope");
2246 new_set.insert(&class_id);
2247 break;
2248 }
2249 else
2250 break;
2251 }
2252 }
2253 else if(id.id_class==cpp_scopet::id_classt::TEMPLATE)
2254 {
2255 // std::cout << "X3\n";
2256 #if 0
2257 const symbolt &symbol=
2258 cpp_typecheck.lookup(id.identifier);
2259
2260 // Template struct? Really needs arguments to be a scope!
2261 if(symbol.type.id() == ID_struct)
2262 {
2263 id.print(std::cout);
2264 assert(id.is_scope);
2265 new_set.insert(&id);
2266 }
2267 #endif
2268 }
2269 else if(id.id_class==cpp_scopet::id_classt::TEMPLATE_PARAMETER)
2270 {
2271 // std::cout << "X4\n";
2272 // a template parameter may evaluate to be a scope: it could
2273 // be instantiated with a class/struct/union/enum
2274 exprt e=cpp_typecheck.template_map.lookup(id.identifier);
2275
2276 #if 0
2277 cpp_typecheck.template_map.print(std::cout);
2278 std::cout << "S: " << cpp_typecheck.cpp_scopes.current_scope().identifier
2279 << '\n';
2280 std::cout << "P: "
2282 << '\n';
2283 std::cout << "I: " << id.identifier << '\n';
2284 std::cout << "E: " << e.pretty() << '\n';
2285 #endif
2286
2287 if(e.id()!=ID_type)
2288 continue; // expressions are definitively not a scope
2289
2291 {
2292 auto type = to_template_parameter_symbol_type(e.type());
2293
2294 while(true)
2295 {
2296 irep_idt identifier=type.get_identifier();
2297
2298 const symbolt &symbol=cpp_typecheck.lookup(identifier);
2299 CHECK_RETURN(symbol.is_type);
2300
2303 else if(symbol.type.id()==ID_struct ||
2304 symbol.type.id()==ID_union ||
2305 symbol.type.id()==ID_c_enum)
2306 {
2307 // this is a scope, too!
2308 cpp_idt &class_id=
2309 cpp_typecheck.cpp_scopes.get_id(identifier);
2310
2311 DATA_INVARIANT(class_id.is_scope, "should be scope");
2312 new_set.insert(&class_id);
2313 break;
2314 }
2315 else // give up
2316 break;
2317 }
2318 }
2319 }
2320 }
2321
2322 id_set.swap(new_set);
2323}
2324
2327{
2328 // we only want namespaces
2329 for(cpp_scopest::id_sett::iterator
2330 it=id_set.begin();
2331 it!=id_set.end();
2332 ) // no it++
2333 {
2334 if((*it)->is_namespace())
2335 it++;
2336 else
2337 {
2338 cpp_scopest::id_sett::iterator old(it);
2339 it++;
2340 id_set.erase(old);
2341 }
2342 }
2343}
2344
2347 const irep_idt &base_name,
2349{
2350 // not clear what this is good for
2351 for(const auto &arg : fargs.operands)
2352 {
2353 if(arg.type().id() != ID_struct_tag && arg.type().id() != ID_union_tag)
2354 continue;
2355
2356 const struct_union_typet &final_type =
2357 arg.type().id() == ID_struct_tag
2358 ? static_cast<const struct_union_typet &>(
2360 : static_cast<const struct_union_typet &>(
2362
2363 cpp_scopet &scope=
2365 const auto tmp_set = scope.lookup(base_name, cpp_scopet::SCOPE_ONLY);
2366 id_set.insert(tmp_set.begin(), tmp_set.end());
2367 }
2368}
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet signed_size_type()
Definition c_types.cpp:66
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:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
C enum tag type, i.e., c_enum_typet with an identifier.
Definition c_types.h:352
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
bool is_class_template() const
irep_idt identifier
Definition cpp_id.h:72
bool is_member
Definition cpp_id.h:42
exprt this_expr
Definition cpp_id.h:76
std::string prefix
Definition cpp_id.h:79
bool is_scope
Definition cpp_id.h:43
id_classt id_class
Definition cpp_id.h:45
void print(std::ostream &out, unsigned indent=0) const
Definition cpp_id.cpp:31
bool is_constructor
Definition cpp_id.h:43
bool is_method
Definition cpp_id.h:42
bool is_static_member
Definition cpp_id.h:42
irep_idt class_identifier
Definition cpp_id.h:75
void go_to_root_scope()
Definition cpp_scopes.h:98
void go_to(cpp_idt &id)
Definition cpp_scopes.h:103
cpp_idt & get_id(const irep_idt &identifier)
Definition cpp_scopes.h:72
std::set< cpp_idt * > id_sett
Definition cpp_scopes.h:30
id_mapt id_map
Definition cpp_scopes.h:68
cpp_scopet & get_scope(const irep_idt &identifier)
Definition cpp_scopes.h:80
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
cpp_scopet & get_root_scope()
Definition cpp_scopes.h:93
cpp_scopet & get_parent() const
Definition cpp_scope.h:88
cpp_idt & insert(const irep_idt &_base_name)
Definition cpp_scope.h:52
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition cpp_scope.h:32
bool is_root_scope() const
Definition cpp_scope.h:77
exprt::operandst argumentst
void remove_templates(resolve_identifierst &identifiers)
void filter(resolve_identifierst &identifiers, const wantt want)
exprt convert_template_parameter(const cpp_idt &id)
exprt convert_identifier(const cpp_idt &id, const cpp_typecheck_fargst &fargs)
cpp_scopet & resolve_namespace(const cpp_namet &cpp_name)
std::vector< exprt > resolve_identifierst
cpp_typecheck_resolvet(class cpp_typecheckt &_cpp_typecheck)
void remove_duplicates(resolve_identifierst &identifiers)
void filter_for_namespaces(cpp_scopest::id_sett &id_set)
exprt resolve(const cpp_namet &cpp_name, const wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
void resolve_argument(exprt &argument, const cpp_typecheck_fargst &fargs)
exprt do_builtin(const irep_idt &base_name, const cpp_typecheck_fargst &fargs, const cpp_template_args_non_tct &template_args)
void show_identifiers(const irep_idt &base_name, const resolve_identifierst &identifiers, std::ostream &out)
void filter_for_named_scopes(cpp_scopest::id_sett &id_set)
void make_constructors(resolve_identifierst &identifiers)
void guess_function_template_args(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
guess arguments of function templates
void convert_identifiers(const cpp_scopest::id_sett &id_set, const cpp_typecheck_fargst &fargs, resolve_identifierst &identifiers)
void disambiguate_functions(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
void apply_template_args(resolve_identifierst &identifiers, const cpp_template_args_non_tct &template_args, const cpp_typecheck_fargst &fargs)
void resolve_with_arguments(cpp_scopest::id_sett &id_set, const irep_idt &base_name, const cpp_typecheck_fargst &fargs)
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
struct_tag_typet disambiguate_template_classes(const irep_idt &base_name, const cpp_scopest::id_sett &id_set, const cpp_template_args_non_tct &template_args)
disambiguate partial specialization
void exact_match_functions(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
void guess_template_args(const typet &template_parameter, const typet &desired_type)
void typecheck_type(typet &) override
instantiation_stackt instantiation_stack
template_mapt template_map
bool cpp_is_pod(const typet &type) const
void show_instantiation_stack(std::ostream &)
cpp_template_args_tct typecheck_template_args(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_non_tct &template_args)
void elaborate_class_template(const typet &type)
elaborate class template instances
bool builtin_factory(const irep_idt &) override
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
std::string to_string(const typet &) override
bool disable_access_control
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
cpp_scopest cpp_scopes
void typecheck_expr_member(exprt &) override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
size_t size() const
Definition dstring.h:121
Base class for all expressions.
Definition expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:163
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
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
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
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
Extract member of struct or union.
Definition std_expr.h:2971
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
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 NIL expression.
Definition std_expr.h:3208
const irep_idt & get_function() const
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
Base type for structs and unions.
Definition std_types.h:62
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
bool is_macro
Definition symbol.h:62
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
A tag-based type, i.e., typet with an identifier.
Definition std_types.h:396
exprt lookup(const irep_idt &identifier) const
void build_unassigned(const template_typet &template_type)
void print(std::ostream &out) const
expr_mapt expr_map
type_mapt type_map
cpp_template_args_tct build_template_args(const template_typet &template_type) const
An expression denoting a type.
Definition std_expr.h:3081
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
source_locationt & add_source_location()
Definition type.h:77
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
cpp_declarationt & to_cpp_declaration(irept &irep)
cpp_namet & to_cpp_name(irept &cpp_name)
Definition cpp_name.h:148
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
cpp_template_args_tct & to_cpp_template_args_tc(irept &irep)
const template_parameter_symbol_typet & to_template_parameter_symbol_type(const typet &type)
Cast a typet to a template_parameter_symbol_typet.
std::string cpp_type2name(const typet &type)
C++ Language Module.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
C++ Language Type Checking.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition cpp_util.cpp:14
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
literalt pos(literalt a)
Definition literal.h:194
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition merged_type.h:29
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
bool is_reference(const typet &type)
Returns true if the type is a reference.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value 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.
bool simplify(exprt &expr, 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:97
API to expression classes.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
cpp_template_args_tct specialization_args
#define size_type
Definition unistd.c:186
dstringt irep_idt