cprover
Loading...
Searching...
No Matches
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 <algorithm>
19
20#include <util/arith_tools.h>
21#include <util/c_types.h>
23#include <util/prefix.h>
24#include <util/simplify_expr.h>
25#include <util/std_expr.h>
27
29#include <ansi-c/merged_type.h>
30
31#include "cpp_convert_type.h"
32#include "cpp_type2name.h"
33#include "cpp_typecheck.h"
34#include "cpp_typecheck_fargs.h"
35#include "cpp_util.h"
36
42
46 resolve_identifierst &identifiers)
47{
48 for(const auto &id_ptr : id_set)
49 {
50 const cpp_idt &identifier = *id_ptr;
51 exprt e=convert_identifier(identifier, fargs);
52
53 if(e.is_not_nil())
54 {
55 CHECK_RETURN(e.id() != ID_type || e.type().is_not_nil());
56
57 identifiers.push_back(e);
58 }
59 }
60}
61
63 resolve_identifierst &identifiers,
66{
68 old_identifiers.swap(identifiers);
69
70 for(const auto &old_id : old_identifiers)
71 {
72 exprt e = old_id;
74
75 if(e.is_not_nil())
76 {
77 CHECK_RETURN(e.id() != ID_type || e.type().is_not_nil());
78
79 identifiers.push_back(e);
80 }
81 }
82}
83
86 resolve_identifierst &identifiers,
88{
90 old_identifiers.swap(identifiers);
91
92 for(const auto &old_id : old_identifiers)
93 {
95
96 if(e.is_not_nil())
97 {
98 CHECK_RETURN(e.id() != ID_type);
99 identifiers.push_back(e);
100 }
101 }
102
103 disambiguate_functions(identifiers, fargs);
104
105 // there should only be one left, or we have failed to disambiguate
106 if(identifiers.size()==1)
107 {
108 // instantiate that one
109 exprt e=*identifiers.begin();
111
114
117
118 // Let's build the instance.
119
120 const symbolt &new_symbol=
126
127 identifiers.clear();
128 identifiers.push_back(
129 symbol_exprt(new_symbol.name, new_symbol.type));
130 }
131}
132
134 resolve_identifierst &identifiers)
135{
137 old_identifiers.swap(identifiers);
138
139 for(const auto &old_id : old_identifiers)
140 {
141 if(!cpp_typecheck.follow(old_id.type()).get_bool(ID_is_template))
142 identifiers.push_back(old_id);
143 }
144}
145
147 resolve_identifierst &identifiers)
148{
150 old_identifiers.swap(identifiers);
151
152 std::set<irep_idt> ids;
153 std::set<exprt> other;
154
155 for(const auto &old_id : old_identifiers)
156 {
157 irep_idt id;
158
159 if(old_id.id() == ID_symbol)
160 id = to_symbol_expr(old_id).get_identifier();
161 else if(old_id.id() == ID_type && old_id.type().id() == ID_struct_tag)
162 id = to_struct_tag_type(old_id.type()).get_identifier();
163 else if(old_id.id() == ID_type && old_id.type().id() == ID_union_tag)
164 id = to_union_tag_type(old_id.type()).get_identifier();
165
166 if(id.empty())
167 {
168 if(other.insert(old_id).second)
169 identifiers.push_back(old_id);
170 }
171 else
172 {
173 if(ids.insert(id).second)
174 identifiers.push_back(old_id);
175 }
176 }
177}
178
180 const cpp_idt &identifier)
181{
182#ifdef DEBUG
183 std::cout << "RESOLVE MAP:\n";
185#endif
186
187 // look up the parameter in the template map
189
190 if(e.is_nil() ||
191 (e.id()==ID_type && e.type().is_nil()))
192 {
194 cpp_typecheck.error() << "internal error: template parameter "
195 << "without instance:\n"
196 << identifier << messaget::eom;
197 throw 0;
198 }
199
201
202 return e;
203}
204
206 const cpp_idt &identifier,
208{
210 return convert_template_parameter(identifier);
211
212 exprt e;
213
214 if(identifier.is_member &&
215 !identifier.is_constructor &&
216 !identifier.is_static_member)
217 {
218 // a regular struct or union member
219
222
224 compound_symbol.type.id() == ID_struct ||
225 compound_symbol.type.id() == ID_union);
226
229
230 const exprt &component =
231 struct_union_type.get_component(identifier.identifier);
232
233 const typet &type=component.type();
234 DATA_INVARIANT(type.is_not_nil(), "type must not be nil");
235
237 {
238 e=type_exprt(type);
239 }
240 else if(identifier.id_class==cpp_scopet::id_classt::SYMBOL)
241 {
242 // A non-static, non-type member.
243 // There has to be an object.
244 e=exprt(ID_member);
245 e.set(ID_component_name, identifier.identifier);
247
248 exprt object;
249 object.make_nil();
250
251 #if 0
252 std::cout << "I: " << identifier.class_identifier
253 << " "
255 this_class_identifier << '\n';
256 #endif
257
258 const exprt &this_expr=
260
261 if(fargs.has_object)
262 {
263 // the object is given to us in fargs
264 PRECONDITION(!fargs.operands.empty());
265 object=fargs.operands.front();
266 }
267 else if(this_expr.is_not_nil())
268 {
269 // use this->...
271 this_expr.type().id() == ID_pointer,
272 "this argument should be pointer");
273 object =
274 exprt(ID_dereference, to_pointer_type(this_expr.type()).base_type());
275 object.copy_to_operands(this_expr);
276 object.type().set(
278 to_pointer_type(this_expr.type())
279 .base_type()
280 .get_bool(ID_C_constant));
281 object.set(ID_C_lvalue, true);
282 object.add_source_location()=source_location;
283 }
284
285 // check if the member can be applied to the object
286 typet object_type=cpp_typecheck.follow(object.type());
287
288 if(object_type.id()==ID_struct ||
289 object_type.id()==ID_union)
290 {
292 to_struct_union_type(object_type),
293 identifier.identifier,
295 object.make_nil(); // failed!
296 }
297 else
298 object.make_nil();
299
300 if(object.is_not_nil())
301 {
302 // we got an object
303 e.add_to_operands(std::move(object));
304
309 }
310 else
311 {
312 // this has to be a method or form a pointer-to-member expression
313 if(identifier.is_method)
315 else
316 {
317 e.id(ID_ptrmember);
319 exprt("cpp-this", pointer_type(compound_symbol.type)));
320 e.type() = type;
321 }
322 }
323 }
324 }
325 else
326 {
327 const symbolt &symbol=
328 cpp_typecheck.lookup(identifier.identifier);
329
330 if(symbol.is_type)
331 {
332 e.make_nil();
333
334 if(symbol.is_macro) // includes typedefs
335 {
336 e = type_exprt(symbol.type);
337 PRECONDITION(symbol.type.is_not_nil());
338 }
339 else if(symbol.type.id()==ID_c_enum)
340 {
341 e = type_exprt(c_enum_tag_typet(symbol.name));
342 }
343 else if(symbol.type.id() == ID_struct)
344 {
345 e = type_exprt(struct_tag_typet(symbol.name));
346 }
347 else if(symbol.type.id() == ID_union)
348 {
349 e = type_exprt(union_tag_typet(symbol.name));
350 }
351 }
352 else if(symbol.is_macro)
353 {
354 e=symbol.value;
356 }
357 else
358 {
359 bool constant = symbol.type.get_bool(ID_C_constant);
360
361 if(
362 constant && symbol.value.is_not_nil() && is_number(symbol.type) &&
363 symbol.value.is_constant())
364 {
365 e=symbol.value;
366 }
367 else
368 {
369 e=cpp_symbol_expr(symbol);
370 }
371 }
372 }
373
375
376 return e;
377}
378
380 resolve_identifierst &identifiers,
381 const wantt want)
382{
384 old_identifiers.swap(identifiers);
385
386 for(const auto &old_id : old_identifiers)
387 {
388 bool match=false;
389
390 switch(want)
391 {
392 case wantt::TYPE:
393 match = (old_id.id() == ID_type);
394 break;
395
396 case wantt::VAR:
397 match = (old_id.id() != ID_type);
398 break;
399
400 case wantt::BOTH:
401 match=true;
402 break;
403
404 default:
406 }
407
408 if(match)
409 identifiers.push_back(old_id);
410 }
411}
412
414 resolve_identifierst &identifiers,
416{
417 if(!fargs.in_use)
418 return;
419
421 old_identifiers.swap(identifiers);
422
423 identifiers.clear();
424
425 // put in the ones that match precisely
426 for(const auto &old_id : old_identifiers)
427 {
428 unsigned distance;
429 if(disambiguate_functions(old_id, distance, fargs))
430 if(distance<=0)
431 identifiers.push_back(old_id);
432 }
433}
434
436 resolve_identifierst &identifiers,
438{
440 old_identifiers.swap(identifiers);
441
442 // sort according to distance
443 std::multimap<std::size_t, exprt> distance_map;
444
445 for(const auto &old_id : old_identifiers)
446 {
447 unsigned args_distance;
448
450 {
451 std::size_t template_distance=0;
452
453 if(!old_id.type().get(ID_C_template).empty())
456 .find(ID_arguments)
457 .get_sub()
458 .size();
459
460 // we give strong preference to functions that have
461 // fewer template arguments
462 std::size_t total_distance=
463 // NOLINTNEXTLINE(whitespace/operators)
465
467 }
468 }
469
471
472 // put in the top ones
473 if(!distance_map.empty())
474 {
475 auto range = distance_map.equal_range(distance_map.begin()->first);
476 for(auto it = range.first; it != range.second; ++it)
477 old_identifiers.push_back(it->second);
478 }
479
480 if(old_identifiers.size() > 1 && fargs.in_use)
481 {
482 // try to further disambiguate functions
483
484 for(resolve_identifierst::const_iterator old_it = old_identifiers.begin();
485 old_it != old_identifiers.end();
486 ++old_it)
487 {
488#if 0
489 std::cout << "I1: " << old_it->get(ID_identifier) << '\n';
490#endif
491
492 if(old_it->type().id() != ID_code)
493 {
494 identifiers.push_back(*old_it);
495 continue;
496 }
497
498 const code_typet &f1 = to_code_type(old_it->type());
499
500 for(resolve_identifierst::const_iterator resolve_it = old_it + 1;
502 ++resolve_it)
503 {
504 if(resolve_it->type().id() != ID_code)
505 continue;
506
507 const code_typet &f2 = to_code_type(resolve_it->type());
508
509 // TODO: may fail when using ellipsis
511 f1.parameters().size() == f2.parameters().size(),
512 "parameter numbers should match");
513
514 bool f1_better=true;
515 bool f2_better=true;
516
517 for(std::size_t i=0;
518 i<f1.parameters().size() && (f1_better || f2_better);
519 i++)
520 {
521 typet type1=f1.parameters()[i].type();
522 typet type2=f2.parameters()[i].type();
523
524 if(type1 == type2)
525 continue;
526
528 continue;
529
530 if(type1.id()==ID_pointer)
531 {
532 typet tmp = to_pointer_type(type1).base_type();
533 type1=tmp;
534 }
535
536 if(type2.id()==ID_pointer)
537 {
538 typet tmp = to_pointer_type(type2).base_type();
539 type2=tmp;
540 }
541
544
545 if(followed1.id() != ID_struct || followed2.id() != ID_struct)
546 continue;
547
550
552 {
553 f2_better=false;
554 }
556 {
557 f1_better=false;
558 }
559 }
560
561 if(!f1_better || f2_better)
562 identifiers.push_back(*resolve_it);
563 }
564 }
565 }
566 else
567 {
568 identifiers.swap(old_identifiers);
569 }
570
571 remove_duplicates(identifiers);
572}
573
575 resolve_identifierst &identifiers)
576{
578
579 for(const auto &identifier : identifiers)
580 {
581 if(identifier.id() != ID_type)
582 {
583 // already an expression
584 new_identifiers.push_back(identifier);
585 continue;
586 }
587
588 const typet &symbol_type = cpp_typecheck.follow(identifier.type());
589
590 // is it a POD?
591
593 {
594 // there are two pod constructors:
595
596 // 1. no arguments, default initialization
597 {
598 const code_typet t1({}, identifier.type());
601 }
602
603 // 2. one argument, copy/conversion
604 {
605 const code_typet t2(
606 {code_typet::parametert(identifier.type())}, identifier.type());
609 }
610
611 // enums, in addition, can also be constructed from int
612 if(symbol_type.id()==ID_c_enum_tag)
613 {
614 const code_typet t3(
615 {code_typet::parametert(signed_int_type())}, identifier.type());
618 }
619 }
620 else if(symbol_type.id()==ID_struct)
621 {
623
624 // go over components
625 for(const auto &component : struct_type.components())
626 {
627 const typet &type=component.type();
628
629 if(component.get_bool(ID_from_base))
630 continue;
631
632 if(
633 type.id() == ID_code &&
634 to_code_type(type).return_type().id() == ID_constructor)
635 {
636 const symbolt &symb =
637 cpp_typecheck.lookup(component.get_name());
639 e.type()=type;
640 new_identifiers.push_back(e);
641 }
642 }
643 }
644 }
645
646 identifiers.swap(new_identifiers);
647}
648
652{
653 if(argument.id() == ID_ambiguous) // could come from a template parameter
654 {
655 // this must be resolved in the template scope
658
660 }
661}
662
664 const irep_idt &base_name,
667{
668 exprt dest;
669
671 template_args.arguments();
672
673 if(base_name==ID_unsignedbv ||
674 base_name==ID_signedbv)
675 {
676 if(arguments.size()!=1)
677 {
680 << base_name << " expects one template argument, but got "
681 << arguments.size() << messaget::eom;
682 throw 0;
683 }
684
685 exprt argument=arguments.front(); // copy
686
687 if(argument.id()==ID_type)
688 {
691 << base_name << " expects one integer template argument, "
692 << "but got type" << messaget::eom;
693 throw 0;
694 }
695
697
698 const auto i = numeric_cast<mp_integer>(argument);
699 if(!i.has_value())
700 {
702 cpp_typecheck.error() << "template argument must be constant"
703 << messaget::eom;
704 throw 0;
705 }
706
707 if(*i < 1)
708 {
711 << "template argument must be greater than zero"
712 << messaget::eom;
713 throw 0;
714 }
715
716 dest=type_exprt(typet(base_name));
717 dest.type().set(ID_width, integer2string(*i));
718 }
719 else if(base_name==ID_fixedbv)
720 {
721 if(arguments.size()!=2)
722 {
725 << base_name << " expects two template arguments, but got "
726 << arguments.size() << messaget::eom;
727 throw 0;
728 }
729
730 exprt argument0=arguments[0];
732 exprt argument1=arguments[1];
734
735 if(argument0.id()==ID_type)
736 {
737 cpp_typecheck.error().source_location=argument0.find_source_location();
739 << base_name << " expects two integer template arguments, "
740 << "but got type" << messaget::eom;
741 throw 0;
742 }
743
744 if(argument1.id()==ID_type)
745 {
746 cpp_typecheck.error().source_location=argument1.find_source_location();
748 << base_name << " expects two integer template arguments, "
749 << "but got type" << messaget::eom;
750 throw 0;
751 }
752
753 const auto width = numeric_cast<mp_integer>(argument0);
754
755 if(!width.has_value())
756 {
757 cpp_typecheck.error().source_location=argument0.find_source_location();
758 cpp_typecheck.error() << "template argument must be constant"
759 << messaget::eom;
760 throw 0;
761 }
762
763 const auto integer_bits = numeric_cast<mp_integer>(argument1);
764
765 if(!integer_bits.has_value())
766 {
767 cpp_typecheck.error().source_location=argument1.find_source_location();
768 cpp_typecheck.error() << "template argument must be constant"
769 << messaget::eom;
770 throw 0;
771 }
772
773 if(*width < 1)
774 {
775 cpp_typecheck.error().source_location=argument0.find_source_location();
777 << "template argument must be greater than zero"
778 << messaget::eom;
779 throw 0;
780 }
781
782 if(*integer_bits < 0)
783 {
784 cpp_typecheck.error().source_location=argument1.find_source_location();
786 << "template argument must be greater or equal zero"
787 << messaget::eom;
788 throw 0;
789 }
790
791 if(*integer_bits > *width)
792 {
793 cpp_typecheck.error().source_location=argument1.find_source_location();
795 << "template argument must be smaller or equal width"
796 << messaget::eom;
797 throw 0;
798 }
799
800 dest=type_exprt(typet(base_name));
801 dest.type().set(ID_width, integer2string(*width));
802 dest.type().set(ID_integer_bits, integer2string(*integer_bits));
803 }
804 else if(base_name==ID_integer)
805 {
806 if(!arguments.empty())
807 {
810 << base_name << " expects no template arguments"
811 << messaget::eom;
812 throw 0;
813 }
814
815 dest=type_exprt(typet(base_name));
816 }
817 else if(has_prefix(id2string(base_name), "constant_infinity"))
818 {
819 // ok, but type missing
820 dest=exprt(ID_infinity, size_type());
821 }
822 else if(base_name=="dump_scopes")
823 {
825 cpp_typecheck.warning() << "Scopes in location "
829 }
830 else if(base_name=="current_scope")
831 {
833 cpp_typecheck.warning() << "Scope in location " << source_location
834 << ": " << original_scope->prefix
835 << messaget::eom;
836 }
837 else if(base_name == ID_size_t)
838 {
839 dest=type_exprt(size_type());
840 }
841 else if(base_name == ID_ssize_t)
842 {
844 }
845 else
846 {
848 cpp_typecheck.error() << "unknown built-in identifier: "
849 << base_name << messaget::eom;
850 throw 0;
851 }
852
853 return dest;
854}
855
860 const cpp_namet &cpp_name,
861 irep_idt &base_name,
863{
864 PRECONDITION(!cpp_name.get_sub().empty());
865
867 source_location=cpp_name.source_location();
868
869 irept::subt::const_iterator pos=cpp_name.get_sub().begin();
870
871 bool recursive=true;
872
873 // check if we need to go to the root scope
874 if(pos->id()=="::")
875 {
876 pos++;
878 recursive=false;
879 }
880
881 std::string final_base_name;
882 template_args.make_nil();
883
884 while(pos!=cpp_name.get_sub().end())
885 {
886 if(pos->id()==ID_name)
887 final_base_name+=pos->get_string(ID_identifier);
888 else if(pos->id()==ID_template_args)
890 else if(pos->id()=="::")
891 {
892 if(template_args.is_not_nil())
893 {
898
899#ifdef DEBUG
900 std::cout << "S: "
902 << '\n';
904 std::cout << "X: " << id_set.size() << '\n';
905#endif
908
909 instance.add_source_location()=source_location;
910
911 // the "::" triggers template elaboration
913
915 cpp_typecheck.cpp_scopes.get_scope(instance.get_identifier()));
916
917 template_args.make_nil();
918 }
919 else
920 {
924
926
927 if(id_set.empty())
928 {
932 << "scope '" << final_base_name << "' not found" << messaget::eom;
933 throw 0;
934 }
935 else if(id_set.size()>=2)
936 {
939 cpp_typecheck.error() << "scope '" << final_base_name
940 << "' is ambiguous" << messaget::eom;
941 throw 0;
942 }
943
944 CHECK_RETURN(id_set.size() == 1);
945
947
948 // the "::" triggers template elaboration
950 {
954 }
955 }
956
957 // we start from fresh
959 }
960 else if(pos->id()==ID_operator)
961 {
962 final_base_name+="operator";
963
964 irept::subt::const_iterator next=pos+1;
965 CHECK_RETURN(next != cpp_name.get_sub().end());
966
967 if(
968 next->id() == ID_cpp_name || next->id() == ID_pointer ||
969 next->id() == ID_int || next->id() == ID_char ||
970 next->id() == ID_c_bool || next->id() == ID_merged_type)
971 {
972 // it's a cast operator
973 irept next_ir=*next;
974 typet op_name;
975 op_name.swap(next_ir);
977 final_base_name+="("+cpp_type2name(op_name)+")";
978 pos++;
979 }
980 }
981 else
982 final_base_name+=pos->id_string();
983
984 pos++;
985 }
986
987 base_name=final_base_name;
988
990}
991
994 const irep_idt &base_name,
996 const cpp_template_args_non_tct &full_template_args)
997{
998 if(id_set.empty())
999 {
1002 cpp_typecheck.error() << "template scope '" << base_name << "' not found"
1003 << messaget::eom;
1004 throw 0;
1005 }
1006
1007 std::set<irep_idt> primary_templates;
1008
1009 for(const auto &id_ptr : id_set)
1010 {
1011 const irep_idt id = id_ptr->identifier;
1012 const symbolt &s=cpp_typecheck.lookup(id);
1014 continue;
1016 if(!cpp_declaration.is_class_template())
1017 continue;
1018 irep_idt specialization_of=cpp_declaration.get_specialization_of();
1019 if(!specialization_of.empty())
1021 else
1022 primary_templates.insert(id);
1023 }
1024
1026
1027 if(primary_templates.size()>=2)
1028 {
1031 cpp_typecheck.error() << "template scope '" << base_name << "' is ambiguous"
1032 << messaget::eom;
1033 throw 0;
1034 }
1035
1038
1039 // We typecheck the template arguments in the context
1040 // of the original scope!
1042
1043 {
1045
1047
1048 // use template type of 'primary template'
1053 full_template_args);
1054
1055 for(auto &arg : full_template_args_tc.arguments())
1056 {
1057 if(arg.id() == ID_type)
1058 continue;
1059 if(arg.id() == ID_symbol)
1060 {
1061 const symbol_exprt &s = to_symbol_expr(arg);
1062 const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier());
1063
1064 if(
1065 cpp_typecheck.cpp_is_pod(symbol.type) &&
1066 symbol.type.get_bool(ID_C_constant))
1067 {
1068 arg = symbol.value;
1069 }
1070 }
1071 simplify(arg, cpp_typecheck);
1072 }
1073
1074 // go back to where we used to be
1075 }
1076
1077 // find any matches
1078
1079 std::vector<matcht> matches;
1080
1081 // the baseline
1082 matches.push_back(
1085
1086 for(const auto &id_ptr : id_set)
1087 {
1088 const irep_idt id = id_ptr->identifier;
1089 const symbolt &s=cpp_typecheck.lookup(id);
1090
1091 if(s.type.get(ID_specialization_of).empty())
1092 continue;
1093
1096
1097 const cpp_template_args_non_tct &partial_specialization_args=
1098 cpp_declaration.partial_specialization_args();
1099
1100 // alright, set up template arguments as 'unassigned'
1101
1104
1106 cpp_declaration.template_type());
1107
1108 // iterate over template instance
1110 full_template_args_tc.arguments().size() ==
1111 partial_specialization_args.arguments().size(),
1112 "number of arguments should match");
1113
1114 // we need to do this in the right scope
1115
1117 static_cast<cpp_scopet *>(
1119
1120 if(template_scope==nullptr)
1121 {
1123 cpp_typecheck.error() << "template identifier: " << id << '\n'
1124 << "class template instantiation error"
1125 << messaget::eom;
1126 throw 0;
1127 }
1128
1129 // enter the scope of the template
1131
1132 for(std::size_t i=0; i<full_template_args_tc.arguments().size(); i++)
1133 {
1134 if(full_template_args_tc.arguments()[i].id()==ID_type)
1135 guess_template_args(partial_specialization_args.arguments()[i].type(),
1136 full_template_args_tc.arguments()[i].type());
1137 else
1138 guess_template_args(partial_specialization_args.arguments()[i],
1139 full_template_args_tc.arguments()[i]);
1140 }
1141
1142 // see if that has worked out
1143
1146 cpp_declaration.template_type());
1147
1148 if(!guessed_template_args.has_unassigned())
1149 {
1150 // check: we can now typecheck the partial_specialization_args
1151
1156 partial_specialization_args);
1157
1158 // if these match the arguments, we have a match
1159
1161 partial_specialization_args_tc.arguments().size() ==
1162 full_template_args_tc.arguments().size(),
1163 "argument numbers must match");
1164
1167 {
1168 matches.push_back(matcht(
1170 }
1171 }
1172 }
1173
1174 CHECK_RETURN(!matches.empty());
1175
1176 std::sort(matches.begin(), matches.end());
1177
1178 #if 0
1179 for(std::vector<matcht>::const_iterator
1180 m_it=matches.begin();
1181 m_it!=matches.end();
1182 m_it++)
1183 {
1184 std::cout << "M: " << m_it->cost
1185 << " " << m_it->id << '\n';
1186 }
1187
1188 std::cout << '\n';
1189 #endif
1190
1191 const matcht &match=*matches.begin();
1192
1193 const symbolt &choice=
1194 cpp_typecheck.lookup(match.id);
1195
1196 #if 0
1197 // build instance
1198 const symbolt &instance=
1201 choice,
1202 match.specialization_args,
1203 match.full_args);
1204
1205 if(instance.type.id()!=ID_struct)
1206 {
1208 cpp_typecheck.error() << "template '"
1209 << base_name << "' is not a class" << messaget::eom;
1210 throw 0;
1211 }
1212
1213 struct_tag_typet result(instance.name);
1215
1216 return result;
1217 #else
1218
1219 // build instance
1220 const symbolt &instance=
1223 choice,
1224 match.specialization_args,
1225 match.full_args);
1226
1227 struct_tag_typet result(instance.name);
1229
1230 return result;
1231 #endif
1232}
1233
1235 const cpp_namet &cpp_name)
1236{
1237 irep_idt base_name;
1239 template_args.make_nil();
1240
1243
1244 bool qualified=cpp_name.is_qualified();
1245
1248
1250
1251 if(id_set.empty())
1252 {
1254 cpp_typecheck.error() << "namespace '" << base_name << "' not found"
1255 << messaget::eom;
1256 throw 0;
1257 }
1258 else if(id_set.size()==1)
1259 {
1260 cpp_idt &id=**id_set.begin();
1261 return (cpp_scopet &)id;
1262 }
1263 else
1264 {
1266 cpp_typecheck.error() << "namespace '" << base_name << "' is ambiguous"
1267 << messaget::eom;
1268 throw 0;
1269 }
1270}
1271
1273 const irep_idt &base_name,
1274 const resolve_identifierst &identifiers,
1275 std::ostream &out)
1276{
1277 for(const auto &id_expr : identifiers)
1278 {
1279 out << " ";
1280
1281 if(id_expr.id()==ID_type)
1282 {
1283 out << "type " << cpp_typecheck.to_string(id_expr.type());
1284 }
1285 else
1286 {
1287 irep_idt id;
1288
1289 if(id_expr.type().get_bool(ID_is_template))
1290 out << "template ";
1291
1292 if(id_expr.id()==ID_member)
1293 {
1294 out << "member ";
1295 id="."+id2string(base_name);
1296 }
1297 else if(id_expr.id() == ID_pod_constructor)
1298 {
1299 out << "constructor ";
1300 id.clear();
1301 }
1303 {
1304 out << "symbol ";
1305 }
1306 else
1307 {
1308 out << "symbol ";
1310 }
1311
1312 if(id_expr.type().get_bool(ID_is_template))
1313 {
1314 }
1315 else if(id_expr.type().id()==ID_code)
1316 {
1318 const typet &return_type=code_type.return_type();
1319 const code_typet::parameterst &parameters=code_type.parameters();
1320 out << cpp_typecheck.to_string(return_type);
1321 out << " " << id << "(";
1322
1323 bool first = true;
1324
1325 for(const auto &parameter : parameters)
1326 {
1327 const typet &parameter_type = parameter.type();
1328
1329 if(first)
1330 first = false;
1331 else
1332 out << ", ";
1333
1335 }
1336
1337 if(code_type.has_ellipsis())
1338 {
1339 if(!parameters.empty())
1340 out << ", ";
1341 out << "...";
1342 }
1343
1344 out << ")";
1345 }
1346 else
1347 out << id << ": " << cpp_typecheck.to_string(id_expr.type());
1348
1349 if(id_expr.id()==ID_symbol)
1350 {
1352 out << " (" << symbol.location << ")";
1353 }
1355 {
1356 const symbolt &symbol=
1358 out << " (" << symbol.location << ")";
1359 }
1360 }
1361
1362 out << '\n';
1363 }
1364}
1365
1367 const cpp_namet &cpp_name,
1368 const wantt want,
1371{
1372 irep_idt base_name;
1374 template_args.make_nil();
1375
1378
1379 // this changes the scope
1381
1382#ifdef DEBUG
1383 std::cout << "base name: " << base_name << '\n';
1384 std::cout << "template args: " << template_args.pretty() << '\n';
1385 std::cout << "original-scope: " << original_scope->prefix << '\n';
1386 std::cout << "scope: " << cpp_typecheck.cpp_scopes.current_scope().prefix
1387 << '\n';
1388#endif
1389
1390 bool qualified=cpp_name.is_qualified();
1391
1392 // do __CPROVER scope
1393 if(qualified)
1394 {
1396 return do_builtin(base_name, fargs, template_args);
1397 }
1398 else
1399 {
1400 if(base_name=="__func__" ||
1401 base_name=="__FUNCTION__" ||
1402 base_name=="__PRETTY_FUNCTION__")
1403 {
1404 // __func__ is an ANSI-C standard compliant hack to get the function name
1405 // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
1408 return std::move(s);
1409 }
1410 }
1411
1413
1416
1417 if(template_args.is_nil())
1418 {
1419 id_set =
1421
1422 if(id_set.empty() && !cpp_typecheck.builtin_factory(base_name))
1423 {
1426 builtin_id.identifier = base_name;
1428
1429 id_set.insert(&builtin_id);
1430 }
1431 }
1432 else
1435
1436 // Argument-dependent name lookup
1437 #if 0
1438 // not clear what this is good for
1439 if(!qualified && !fargs.has_object)
1440 resolve_with_arguments(id_set, base_name, fargs);
1441 #endif
1442
1443 if(id_set.empty())
1444 {
1446 return nil_exprt();
1447
1450
1451 if(qualified)
1452 {
1453 cpp_typecheck.error() << "symbol '" << base_name << "' not found";
1454
1456 cpp_typecheck.error() << " in root scope";
1457 else
1459 << " in scope '" << cpp_typecheck.cpp_scopes.current_scope().prefix
1460 << "'";
1461 }
1462 else
1463 {
1464 cpp_typecheck.error() << "symbol '" << base_name << "' is unknown";
1465 }
1466
1468 // cpp_typecheck.cpp_scopes.get_root_scope().print(std::cout);
1469 // cpp_typecheck.cpp_scopes.current_scope().print(std::cout);
1470 throw 0;
1471 }
1472
1473 resolve_identifierst identifiers;
1474
1475 if(template_args.is_not_nil())
1476 {
1477 // first figure out if we are doing functions/methods or
1478 // classes
1479 bool have_classes=false, have_methods=false;
1480
1481 for(const auto &id_ptr : id_set)
1482 {
1483 const irep_idt id = id_ptr->identifier;
1484 const symbolt &s=cpp_typecheck.lookup(id);
1487 have_classes=true;
1488 else
1489 have_methods=true;
1490 }
1491
1493 {
1495 return nil_exprt();
1496
1499 cpp_typecheck.error() << "template symbol '" << base_name
1500 << "' is ambiguous" << messaget::eom;
1501 throw 0;
1502 }
1503
1505 {
1508
1510
1511 identifiers.push_back(exprt(ID_type, instance));
1512 }
1513 else
1514 {
1515 // methods and functions
1517 id_set, fargs, identifiers);
1518
1520 identifiers, template_args, fargs);
1521 }
1522 }
1523 else
1524 {
1526 id_set, fargs, identifiers);
1527 }
1528
1529 // change types into constructors if we want a constructor
1530 if(want==wantt::VAR)
1531 make_constructors(identifiers);
1532
1533 filter(identifiers, want);
1534
1535#ifdef DEBUG
1536 std::cout << "P0 " << base_name << " " << identifiers.size() << '\n';
1537 show_identifiers(base_name, identifiers, std::cout);
1538 std::cout << '\n';
1539#endif
1540
1541 exprt result;
1542
1543 // We disambiguate functions
1545
1547
1548#ifdef DEBUG
1549 std::cout << "P1 " << base_name << " " << new_identifiers.size() << '\n';
1550 show_identifiers(base_name, new_identifiers, std::cout);
1551 std::cout << '\n';
1552#endif
1553
1554 // we only want _exact_ matches, without templates!
1556
1557#ifdef DEBUG
1558 std::cout << "P2 " << base_name << " " << new_identifiers.size() << '\n';
1559 show_identifiers(base_name, new_identifiers, std::cout);
1560 std::cout << '\n';
1561#endif
1562
1563 // no exact matches? Try again with function template guessing.
1564 if(new_identifiers.empty())
1565 {
1566 new_identifiers=identifiers;
1567
1568 if(template_args.is_nil())
1569 {
1571
1572 if(new_identifiers.empty())
1573 new_identifiers=identifiers;
1574 }
1575
1577
1578#ifdef DEBUG
1579 std::cout << "P3 " << base_name << " " << new_identifiers.size() << '\n';
1580 show_identifiers(base_name, new_identifiers, std::cout);
1581 std::cout << '\n';
1582#endif
1583 }
1584 else
1586
1587#ifdef DEBUG
1588 std::cout << "P4 " << base_name << " " << new_identifiers.size() << '\n';
1589 show_identifiers(base_name, new_identifiers, std::cout);
1590 std::cout << '\n';
1591#endif
1592
1593 if(new_identifiers.size()==1)
1594 {
1595 result=*new_identifiers.begin();
1596 }
1597 else
1598 {
1599 // nothing or too many
1601 return nil_exprt();
1602
1603 if(new_identifiers.empty())
1604 {
1607 << "found no match for symbol '" << base_name << "', candidates are:\n";
1608 show_identifiers(base_name, identifiers, cpp_typecheck.error());
1609 }
1610 else
1611 {
1614 << "symbol '" << base_name << "' does not uniquely resolve:\n";
1616
1617#ifdef DEBUG
1618 exprt e1=*new_identifiers.begin();
1619 exprt e2=*(++new_identifiers.begin());
1620 cpp_typecheck.error() << "e1==e2: " << (e1 == e2) << '\n';
1622 << "e1.type==e2.type: " << (e1.type() == e2.type()) << '\n';
1624 << "e1.id()==e2.id(): " << (e1.id() == e2.id()) << '\n';
1626 << "e1.iden==e2.iden: "
1627 << (e1.get(ID_identifier) == e2.get(ID_identifier)) << '\n';
1628 cpp_typecheck.error() << "e1.iden:: " << e1.get(ID_identifier) << '\n';
1629 cpp_typecheck.error() << "e2.iden:: " << e2.get(ID_identifier) << '\n';
1630#endif
1631 }
1632
1633 if(fargs.in_use)
1634 {
1635 cpp_typecheck.error() << "\nargument types:\n";
1636
1637 for(const auto &op : fargs.operands)
1638 {
1640 << " " << cpp_typecheck.to_string(op.type()) << '\n';
1641 }
1642 }
1643
1645 {
1647 }
1648
1650 throw 0;
1651 }
1652
1653 // we do some checks before we return
1654 if(result.get_bool(ID_C_not_accessible))
1655 {
1656 #if 0
1658 return nil_exprt();
1659
1661 cpp_typecheck.str
1662 << "error: member '" << result.get(ID_component_name)
1663 << "' is not accessible";
1664 throw 0;
1665 #endif
1666 }
1667
1668 switch(want)
1669 {
1670 case wantt::VAR:
1671 if(result.id()==ID_type && !cpp_typecheck.cpp_is_pod(result.type()))
1672 {
1674 return nil_exprt();
1675
1677
1679 << "error: expected expression, but got type '"
1680 << cpp_typecheck.to_string(result.type()) << "'" << messaget::eom;
1681
1682 throw 0;
1683 }
1684 break;
1685
1686 case wantt::TYPE:
1687 if(result.id()!=ID_type)
1688 {
1690 return nil_exprt();
1691
1693
1695 << "error: expected type, but got expression '"
1696 << cpp_typecheck.to_string(result) << "'" << messaget::eom;
1697
1698 throw 0;
1699 }
1700 break;
1701
1702 case wantt::BOTH:
1703 break;
1704 }
1705
1706 return result;
1707}
1708
1710 const exprt &template_expr,
1711 const exprt &desired_expr)
1712{
1713 if(template_expr.id()==ID_cpp_name)
1714 {
1715 const cpp_namet &cpp_name=
1717
1718 if(!cpp_name.is_qualified())
1719 {
1721
1723 irep_idt base_name;
1725
1727 base_name, cpp_scopet::RECURSIVE);
1728
1729 // alright, rummage through these
1730 for(const auto &id_ptr : id_set)
1731 {
1732 const cpp_idt &id = *id_ptr;
1733 // template parameter?
1735 {
1736 // see if unassigned
1737 exprt &e=cpp_typecheck.template_map.expr_map[id.identifier];
1738 if(e.id()==ID_unassigned)
1739 {
1740 typet old_type=e.type();
1742 }
1743 }
1744 }
1745 }
1746 }
1747}
1748
1750 const typet &template_type,
1751 const typet &desired_type)
1752{
1753 // look at
1754 // http://publib.boulder.ibm.com/infocenter/comphelp/v8v101/topic/
1755 // com.ibm.xlcpp8a.doc/language/ref/template_argument_deduction.htm
1756
1757 // T
1758 // const T
1759 // volatile T
1760 // T&
1761 // T*
1762 // T[10]
1763 // A<T>
1764 // C(*)(T)
1765 // T(*)()
1766 // T(*)(U)
1767 // T C::*
1768 // C T::*
1769 // T U::*
1770 // T (C::*)()
1771 // C (T::*)()
1772 // D (C::*)(T)
1773 // C (T::*)(U)
1774 // T (C::*)(U)
1775 // T (U::*)()
1776 // T (U::*)(V)
1777 // E[10][i]
1778 // B<i>
1779 // TT<T>
1780 // TT<i>
1781 // TT<C>
1782
1783 #if 0
1784 std::cout << "TT: " << template_type.pretty() << '\n';
1785 std::cout << "DT: " << desired_type.pretty() << '\n';
1786 #endif
1787
1788 if(template_type.id()==ID_cpp_name)
1789 {
1790 // we only care about cpp_names that are template parameters!
1791 const cpp_namet &cpp_name=to_cpp_name(template_type);
1792
1794
1795 if(cpp_name.has_template_args())
1796 {
1797 // this could be something like my_template<T>, and we need
1798 // to match 'T'. Then 'desired_type' has to be a template instance.
1799
1800 // TODO
1801 }
1802 else
1803 {
1804 // template parameters aren't qualified
1805 if(!cpp_name.is_qualified())
1806 {
1807 irep_idt base_name;
1810
1812 base_name, cpp_scopet::RECURSIVE);
1813
1814 // alright, rummage through these
1815 for(const auto &id_ptr : id_set)
1816 {
1817 const cpp_idt &id = *id_ptr;
1818
1819 // template argument?
1821 {
1822 // see if unassigned
1823 typet &t=cpp_typecheck.template_map.type_map[id.identifier];
1824 if(t.id()==ID_unassigned)
1825 {
1826 t=desired_type;
1827
1828 // remove const, volatile (these can be added in the call)
1831 #if 0
1832 std::cout << "ASSIGN " << id.identifier << " := "
1834 #endif
1835 }
1836 }
1837 }
1838 }
1839 }
1840 }
1841 else if(template_type.id()==ID_merged_type)
1842 {
1843 // look at subtypes
1844 for(const auto &t : to_merged_type(template_type).subtypes())
1845 {
1847 }
1848 }
1849 else if(is_reference(template_type) ||
1850 is_rvalue_reference(template_type))
1851 {
1853 to_reference_type(template_type).base_type(), desired_type);
1854 }
1855 else if(template_type.id()==ID_pointer)
1856 {
1857 if(desired_type.id() == ID_pointer)
1859 to_pointer_type(template_type).base_type(),
1860 to_pointer_type(desired_type).base_type());
1861 }
1862 else if(template_type.id()==ID_array)
1863 {
1864 if(desired_type.id() == ID_array)
1865 {
1866 // look at subtype first
1868 to_array_type(template_type).element_type(),
1869 to_array_type(desired_type).element_type());
1870
1871 // size (e.g., buffer size guessing)
1873 to_array_type(template_type).size(),
1874 to_array_type(desired_type).size());
1875 }
1876 }
1877}
1878
1881 const exprt &expr,
1883{
1884 typet tmp = cpp_typecheck.follow(expr.type());
1885
1886 if(!tmp.get_bool(ID_is_template))
1887 return nil_exprt(); // not a template
1888
1889 PRECONDITION(expr.id() == ID_symbol);
1890
1891 // a template is always a declaration
1894
1895 // Class templates require explicit template arguments,
1896 // no guessing!
1897 if(cpp_declaration.is_class_template())
1898 return nil_exprt();
1899
1900 // we need function arguments for guessing
1901 if(fargs.operands.empty())
1902 return nil_exprt(); // give up
1903
1904 // We need to guess in the case of function templates!
1905
1907 to_symbol_expr(expr).get_identifier();
1908
1909 const symbolt &template_symbol=
1911
1912 // alright, set up template arguments as 'unassigned'
1913
1915
1917 cpp_declaration.template_type());
1918
1919 // there should be exactly one declarator
1920 PRECONDITION(cpp_declaration.declarators().size() == 1);
1921
1923 cpp_declaration.declarators().front();
1924
1925 // and that needs to have function type
1926 if(function_declarator.type().id()!=ID_function_type)
1927 {
1930 << "expected function type for function template"
1931 << messaget::eom;
1932 throw 0;
1933 }
1934
1936
1937 // we need the template scope
1939 static_cast<cpp_scopet *>(
1941
1942 if(template_scope==nullptr)
1943 {
1945 cpp_typecheck.error() << "template identifier: "
1946 << template_identifier << '\n'
1947 << "function template instantiation error"
1948 << messaget::eom;
1949 throw 0;
1950 }
1951
1952 // enter the scope of the template
1954
1955 // walk through the function parameters
1956 const irept::subt &parameters=
1957 function_declarator.type().find(ID_parameters).get_sub();
1958
1959 exprt::operandst::const_iterator it=fargs.operands.begin();
1960 for(const auto &parameter : parameters)
1961 {
1962 if(it==fargs.operands.end())
1963 break;
1964
1966 {
1969
1970 // again, there should be one declarator
1972 arg_declaration.declarators().size() == 1, "exactly one declarator");
1973
1974 // turn into type
1976 arg_declaration.declarators().front().
1977 merge_type(arg_declaration.type());
1978
1979 // We only convert the arg_type,
1980 // and don't typecheck it -- that could cause all
1981 // sorts of trouble.
1983
1984 guess_template_args(arg_type, it->type());
1985 }
1986
1987 ++it;
1988 }
1989
1990 // see if that has worked out
1991
1994 cpp_declaration.template_type());
1995
1996 if(template_args.has_unassigned())
1997 return nil_exprt(); // give up
1998
1999 // Build the type of the function.
2000
2001 typet function_type=
2002 function_declarator.merge_type(cpp_declaration.type());
2003
2004 cpp_typecheck.typecheck_type(function_type);
2005
2006 // Remember that this was a template
2007
2008 function_type.set(ID_C_template, template_symbol.name);
2010
2011 // Seems we got an instance for all parameters. Let's return that.
2012
2014 ID_template_function_instance, function_type);
2015
2017}
2018
2020 exprt &expr,
2023{
2024 if(expr.id()!=ID_symbol)
2025 return; // templates are always symbols
2026
2027 const symbolt &template_symbol =
2028 cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier());
2029
2030 if(!template_symbol.type.get_bool(ID_is_template))
2031 return;
2032
2033 #if 0
2034 if(template_args_non_tc.is_nil())
2035 {
2036 // no arguments, need to guess
2038 return;
2039 }
2040 #endif
2041
2042 // We typecheck the template arguments in the context
2043 // of the original scope!
2045
2046 {
2048
2050
2056 // go back to where we used to be
2057 }
2058
2059 // We never try 'unassigned' template arguments.
2060 if(template_args_tc.has_unassigned())
2062
2063 // a template is always a declaration
2066
2067 // is it a class template or function template?
2068 if(cpp_declaration.is_class_template())
2069 {
2070 const symbolt &new_symbol=
2076
2077 expr = type_exprt(struct_tag_typet(new_symbol.name));
2079 }
2080 else
2081 {
2082 // must be a function, maybe method
2083 const symbolt &new_symbol=
2089
2090 // check if it is a method
2091 const code_typet &code_type=to_code_type(new_symbol.type);
2092
2093 if(
2094 !code_type.parameters().empty() &&
2095 code_type.parameters().front().get_this())
2096 {
2097 // do we have an object?
2098 if(fargs.has_object)
2099 {
2100 const symbolt &type_symb=
2102 fargs.operands.begin()->type().get(ID_identifier));
2103
2104 CHECK_RETURN(type_symb.type.id() == ID_struct);
2105
2108
2109 DATA_INVARIANT(struct_type.has_component(new_symbol.name),
2110 "method should exist in struct");
2111
2112 member_exprt member(
2113 *fargs.operands.begin(),
2114 new_symbol.name,
2115 code_type);
2117 expr.swap(member);
2118 return;
2119 }
2120 }
2121
2122 expr=cpp_symbol_expr(new_symbol);
2124 }
2125}
2126
2128 const exprt &expr,
2129 unsigned &args_distance,
2131{
2132 args_distance=0;
2133
2134 if(expr.type().id()!=ID_code || !fargs.in_use)
2135 return true;
2136
2137 const code_typet &type=to_code_type(expr.type());
2138
2139 if(expr.id()==ID_member ||
2140 type.return_type().id() == ID_constructor)
2141 {
2142 // if it's a member, but does not have an object yet,
2143 // we add one
2144 if(!fargs.has_object)
2145 {
2146 const code_typet::parameterst &parameters=type.parameters();
2147 const code_typet::parametert &parameter=parameters.front();
2148
2149 INVARIANT(parameter.get_this(), "first parameter should be `this'");
2150
2151 if(type.return_type().id() == ID_constructor)
2152 {
2153 // it's a constructor
2154 const typet &object_type =
2155 to_pointer_type(parameter.type()).base_type();
2156 symbol_exprt object(irep_idt(), object_type);
2157 object.set(ID_C_lvalue, true);
2158
2160 new_fargs.add_object(object);
2161 return new_fargs.match(type, args_distance, cpp_typecheck);
2162 }
2163 else
2164 {
2165 if(
2166 expr.type().get_bool(ID_C_is_operator) &&
2167 fargs.operands.size() == parameters.size())
2168 {
2169 return fargs.match(type, args_distance, cpp_typecheck);
2170 }
2171
2173 new_fargs.add_object(to_member_expr(expr).compound());
2174
2175 return new_fargs.match(type, args_distance, cpp_typecheck);
2176 }
2177 }
2178 }
2179 else if(fargs.has_object)
2180 {
2181 // if it's not a member then we shall remove the object
2183 new_fargs.remove_object();
2184
2185 return new_fargs.match(type, args_distance, cpp_typecheck);
2186 }
2187
2188 return fargs.match(type, args_distance, cpp_typecheck);
2189}
2190
2193{
2195
2196 // std::cout << "FILTER\n";
2197
2198 // We only want scopes!
2199 for(const auto &id_ptr : id_set)
2200 {
2201 cpp_idt &id = *id_ptr;
2202
2203 if(id.is_class() || id.is_enum() || id.is_namespace())
2204 {
2205 // std::cout << "X1\n";
2206 DATA_INVARIANT(id.is_scope, "should be scope");
2207 new_set.insert(&id);
2208 }
2209 else if(id.is_typedef())
2210 {
2211 // std::cout << "X2\n";
2212 irep_idt identifier=id.identifier;
2213
2214 if(id.is_member)
2215 continue;
2216
2217 while(true)
2218 {
2219 const symbolt &symbol=cpp_typecheck.lookup(identifier);
2220 CHECK_RETURN(symbol.is_type);
2221
2222 // todo? maybe do enum here, too?
2223 if(symbol.type.id()==ID_struct)
2224 {
2225 // this is a scope, too!
2226 cpp_idt &class_id=
2227 cpp_typecheck.cpp_scopes.get_id(identifier);
2228
2229 DATA_INVARIANT(class_id.is_scope, "should be scope");
2230 new_set.insert(&class_id);
2231 break;
2232 }
2233 else
2234 break;
2235 }
2236 }
2237 else if(id.id_class==cpp_scopet::id_classt::TEMPLATE)
2238 {
2239 // std::cout << "X3\n";
2240 #if 0
2241 const symbolt &symbol=
2242 cpp_typecheck.lookup(id.identifier);
2243
2244 // Template struct? Really needs arguments to be a scope!
2245 if(symbol.type.id() == ID_struct)
2246 {
2247 id.print(std::cout);
2248 assert(id.is_scope);
2249 new_set.insert(&id);
2250 }
2251 #endif
2252 }
2253 else if(id.id_class==cpp_scopet::id_classt::TEMPLATE_PARAMETER)
2254 {
2255 // std::cout << "X4\n";
2256 // a template parameter may evaluate to be a scope: it could
2257 // be instantiated with a class/struct/union/enum
2258 exprt e=cpp_typecheck.template_map.lookup(id.identifier);
2259
2260 #if 0
2261 cpp_typecheck.template_map.print(std::cout);
2262 std::cout << "S: " << cpp_typecheck.cpp_scopes.current_scope().identifier
2263 << '\n';
2264 std::cout << "P: "
2266 << '\n';
2267 std::cout << "I: " << id.identifier << '\n';
2268 std::cout << "E: " << e.pretty() << '\n';
2269 #endif
2270
2271 if(e.id()!=ID_type)
2272 continue; // expressions are definitively not a scope
2273
2275 {
2276 auto type = to_template_parameter_symbol_type(e.type());
2277
2278 while(true)
2279 {
2280 irep_idt identifier=type.get_identifier();
2281
2282 const symbolt &symbol=cpp_typecheck.lookup(identifier);
2283 CHECK_RETURN(symbol.is_type);
2284
2287 else if(symbol.type.id()==ID_struct ||
2288 symbol.type.id()==ID_union ||
2289 symbol.type.id()==ID_c_enum)
2290 {
2291 // this is a scope, too!
2292 cpp_idt &class_id=
2293 cpp_typecheck.cpp_scopes.get_id(identifier);
2294
2295 DATA_INVARIANT(class_id.is_scope, "should be scope");
2296 new_set.insert(&class_id);
2297 break;
2298 }
2299 else // give up
2300 break;
2301 }
2302 }
2303 }
2304 }
2305
2306 id_set.swap(new_set);
2307}
2308
2311{
2312 // we only want namespaces
2313 for(cpp_scopest::id_sett::iterator
2314 it=id_set.begin();
2315 it!=id_set.end();
2316 ) // no it++
2317 {
2318 if((*it)->is_namespace())
2319 it++;
2320 else
2321 {
2322 cpp_scopest::id_sett::iterator old(it);
2323 it++;
2324 id_set.erase(old);
2325 }
2326 }
2327}
2328
2331 const irep_idt &base_name,
2333{
2334 // not clear what this is good for
2335 for(const auto &arg : fargs.operands)
2336 {
2337 const typet &final_type=cpp_typecheck.follow(arg.type());
2338
2339 if(final_type.id()!=ID_struct && final_type.id()!=ID_union)
2340 continue;
2341
2342 cpp_scopet &scope=
2344 const auto tmp_set = scope.lookup(base_name, cpp_scopet::SCOPE_ONLY);
2345 id_set.insert(tmp_set.begin(), tmp_set.end());
2346 }
2347}
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
unsignedbv_typet size_type()
Definition c_types.cpp:55
signedbv_typet signed_int_type()
Definition c_types.cpp:27
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet signed_size_type()
Definition c_types.cpp:71
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:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:539
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
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:39
bool empty() const
Definition dstring.h:90
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:155
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
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:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Extract member of struct or union.
Definition std_expr.h:2794
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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:3026
const irep_idt & get_function() const
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
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:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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
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:2906
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
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
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
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:47
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:77
API to expression classes.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
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:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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
dstringt irep_idt