cprover
cpp_typecheck_template.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
12#include "cpp_typecheck.h"
13
15#include <util/simplify_expr.h>
16
17#include "cpp_type2name.h"
19#include "cpp_template_type.h"
20#include "cpp_convert_type.h"
21#include "cpp_template_args.h"
22
24 const template_typet &old_type,
25 template_typet &new_type)
26{
27 const template_typet::template_parameterst &old_parameters=
28 old_type.template_parameters();
30 new_type.template_parameters();
31
32 for(std::size_t i=0; i<new_parameters.size(); i++)
33 {
34 if(i<old_parameters.size() &&
35 old_parameters[i].has_default_argument() &&
36 !new_parameters[i].has_default_argument())
37 {
38 // TODO The default may depend on previous parameters!!
39 new_parameters[i].default_argument()=old_parameters[i].default_argument();
40 }
41 }
42}
43
45 cpp_declarationt &declaration)
46{
47 // Do template parameters. This also sets up the template scope.
48 cpp_scopet &template_scope=
50
51 typet &type=declaration.type();
52 template_typet &template_type=declaration.template_type();
53
54 bool has_body=type.find(ID_body).is_not_nil();
55
56 const cpp_namet &cpp_name=
57 static_cast<const cpp_namet &>(type.find(ID_tag));
58
59 if(cpp_name.is_nil())
60 {
62 error() << "class templates must not be anonymous" << eom;
63 throw 0;
64 }
65
66 if(!cpp_name.is_simple_name())
67 {
69 error() << "simple name expected as class template tag" << eom;
70 throw 0;
71 }
72
73 irep_idt base_name=cpp_name.get_base_name();
74
75 const cpp_template_args_non_tct &partial_specialization_args=
76 declaration.partial_specialization_args();
77
78 const irep_idt symbol_name=
80 base_name, template_type, partial_specialization_args);
81
82 #if 0
83 // Check if the name is already used by a different template
84 // in the same scope.
85 {
86 const auto id_set=
88 base_name,
90 cpp_scopet::TEMPLATE);
91
92 if(!id_set.empty())
93 {
94 const symbolt &previous=lookup((*id_set.begin())->identifier);
95 if(previous.name!=symbol_name || id_set.size()>1)
96 {
98 str << "template declaration of '" << base_name.c_str()
99 << " does not match previous declaration\n";
100 str << "location of previous definition: " << previous.location;
101 throw 0;
102 }
103 }
104 }
105 #endif
106
107 // check if we have it already
108
109 if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))
110 {
111 // there already
112 symbolt &previous_symbol=*maybe_symbol;
113 cpp_declarationt &previous_declaration=
114 to_cpp_declaration(previous_symbol.type);
115
116 bool previous_has_body=
117 previous_declaration.type().find(ID_body).is_not_nil();
118
119 // check if we have 2 bodies
120 if(has_body && previous_has_body)
121 {
123 error() << "template struct '" << base_name << "' defined previously\n"
124 << "location of previous definition: " << previous_symbol.location
125 << eom;
126 throw 0;
127 }
128
129 if(has_body)
130 {
131 // We replace the template!
132 // We have to retain any default parameters from the previous declaration.
134 previous_declaration.template_type(),
135 declaration.template_type());
136
137 previous_symbol.type.swap(declaration);
138
139 #if 0
140 std::cout << "*****\n";
141 std::cout << *cpp_scopes.id_map[symbol_name];
142 std::cout << "*****\n";
143 std::cout << "II: " << symbol_name << '\n';
144 #endif
145
146 // We also replace the template scope (the old one could be deleted).
147 cpp_scopes.id_map[symbol_name]=&template_scope;
148
149 // We also fix the parent scope in order to see the new
150 // template arguments
151 }
152 else
153 {
154 // just update any default arguments
156 declaration.template_type(),
157 previous_declaration.template_type());
158 }
159
160 INVARIANT(
161 cpp_scopes.id_map[symbol_name]->is_template_scope(),
162 "symbol should be in template scope");
163
164 return;
165 }
166
167 // it's not there yet
168
169 symbolt symbol;
170
171 symbol.name=symbol_name;
172 symbol.base_name=base_name;
173 symbol.location=cpp_name.source_location();
174 symbol.mode=ID_cpp;
175 symbol.module=module;
176 symbol.type.swap(declaration);
177 symbol.is_macro=false;
178 symbol.value = exprt(ID_template_decls);
179
180 symbol.pretty_name=
182
183 symbolt *new_symbol;
184 if(symbol_table.move(symbol, new_symbol))
185 {
187 error() << "cpp_typecheckt::typecheck_compound_type: "
188 << "symbol_table.move() failed"
189 << eom;
190 throw 0;
191 }
192
193 // put into current scope
194 cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
196 id.prefix=cpp_scopes.current_scope().prefix+
197 id2string(new_symbol->base_name);
198
199 // link the template symbol with the template scope
200 cpp_scopes.id_map[symbol_name]=&template_scope;
201
202 INVARIANT(
203 cpp_scopes.id_map[symbol_name]->is_template_scope(),
204 "symbol should be in template scope");
205}
206
209 cpp_declarationt &declaration)
210{
211 assert(declaration.declarators().size()==1);
212
213 cpp_declaratort &declarator=declaration.declarators()[0];
214 const cpp_namet &cpp_name = declarator.name();
215
216 // do template arguments
217 // this also sets up the template scope
218 cpp_scopet &template_scope=
220
221 if(!cpp_name.is_simple_name())
222 {
223 error().source_location=declaration.source_location();
224 error() << "function template must have simple name" << eom;
225 throw 0;
226 }
227
228 irep_idt base_name=cpp_name.get_base_name();
229
230 template_typet &template_type=declaration.template_type();
231
232 typet function_type=
233 declarator.merge_type(declaration.type());
234
236
237 irep_idt symbol_name=
239 base_name,
240 template_type,
241 function_type);
242
243 bool has_value=declarator.find(ID_value).is_not_nil();
244
245 // check if we have it already
246
247 symbol_tablet::symbolst::const_iterator previous_symbol=
248 symbol_table.symbols.find(symbol_name);
249
250 if(previous_symbol!=symbol_table.symbols.end())
251 {
252 bool previous_has_value =
253 to_cpp_declaration(previous_symbol->second.type).
254 declarators()[0].find(ID_value).is_not_nil();
255
256 if(has_value && previous_has_value)
257 {
259 error() << "function template symbol '" << base_name
260 << "' declared previously\n"
261 << "location of previous definition: "
262 << previous_symbol->second.location << eom;
263 throw 0;
264 }
265
266 if(has_value)
267 {
268 symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);
269 cpp_scopes.id_map[symbol_name]=&template_scope;
270 }
271
272 // todo: the old template scope now is useless,
273 // and thus, we could delete it
274 return;
275 }
276
277 symbolt symbol;
278 symbol.name=symbol_name;
279 symbol.base_name=base_name;
280 symbol.location=cpp_name.source_location();
281 symbol.mode=ID_cpp;
282 symbol.module=module;
283 symbol.value.make_nil();
284
285 symbol.type.swap(declaration);
286 symbol.pretty_name=
288
289 symbolt *new_symbol;
290 if(symbol_table.move(symbol, new_symbol))
291 {
293 error() << "cpp_typecheckt::typecheck_compound_type: "
294 << "symbol_table.move() failed"
295 << eom;
296 throw 0;
297 }
298
299 // put into scope
300 cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
302 id.prefix=cpp_scopes.current_scope().prefix+
303 id2string(new_symbol->base_name);
304
305 // link the template symbol with the template scope
306 cpp_scopes.id_map[symbol_name] = &template_scope;
307 INVARIANT(
308 template_scope.is_template_scope(), "symbol should be in template scope");
309}
310
313 cpp_declarationt &declaration)
314{
315 assert(declaration.declarators().size()==1);
316
317 cpp_declaratort &declarator=declaration.declarators()[0];
318 const cpp_namet &cpp_name = declarator.name();
319
320 assert(cpp_name.is_qualified() ||
321 cpp_name.has_template_args());
322
323 // must be of the form: name1<template_args>::name2
324 // or: name1<template_args>::operator X
325 if(cpp_name.get_sub().size()==4 &&
326 cpp_name.get_sub()[0].id()==ID_name &&
327 cpp_name.get_sub()[1].id()==ID_template_args &&
328 cpp_name.get_sub()[2].id()=="::" &&
329 cpp_name.get_sub()[3].id()==ID_name)
330 {
331 }
332 else if(cpp_name.get_sub().size()==5 &&
333 cpp_name.get_sub()[0].id()==ID_name &&
334 cpp_name.get_sub()[1].id()==ID_template_args &&
335 cpp_name.get_sub()[2].id()=="::" &&
336 cpp_name.get_sub()[3].id()==ID_operator)
337 {
338 }
339 else
340 {
341 return; // TODO
342
343#if 0
345 error() << "bad template name" << eom;
346 throw 0;
347#endif
348 }
349
350 // let's find the class template this function template belongs to.
351 const auto id_set = cpp_scopes.current_scope().lookup(
352 cpp_name.get_sub().front().get(ID_identifier),
353 cpp_scopet::SCOPE_ONLY, // look only in current scope
354 cpp_scopet::id_classt::TEMPLATE); // must be template
355
356 if(id_set.empty())
357 {
360 error() << "class template '"
361 << cpp_name.get_sub().front().get(ID_identifier) << "' not found"
362 << eom;
363 throw 0;
364 }
365 else if(id_set.size()>1)
366 {
368 error() << "class template '"
369 << cpp_name.get_sub().front().get(ID_identifier) << "' is ambiguous"
370 << eom;
371 throw 0;
372 }
373 else if((*(id_set.begin()))->id_class!=cpp_idt::id_classt::TEMPLATE)
374 {
375 // std::cerr << *(*id_set.begin()) << '\n';
377 error() << "class template '"
378 << cpp_name.get_sub().front().get(ID_identifier)
379 << "' is not a template" << eom;
380 throw 0;
381 }
382
383 const cpp_idt &cpp_id=**(id_set.begin());
384 symbolt &template_symbol = symbol_table.get_writeable_ref(cpp_id.identifier);
385
386 exprt &template_methods =
387 static_cast<exprt &>(template_symbol.value.add(ID_template_methods));
388
389 template_methods.copy_to_operands(declaration);
390
391 // save current scope
392 cpp_save_scopet cpp_saved_scope(cpp_scopes);
393
394 const irept &instantiated_with =
395 template_symbol.value.add(ID_instantiated_with);
396
397 for(std::size_t i=0; i<instantiated_with.get_sub().size(); i++)
398 {
399 const cpp_template_args_tct &tc_template_args=
400 static_cast<const cpp_template_args_tct &>(
401 instantiated_with.get_sub()[i]);
402
403 cpp_declarationt decl_tmp=declaration;
404
405 // do template arguments
406 // this also sets up the template scope of the method
407 cpp_scopet &method_scope=
409
410 cpp_scopes.go_to(method_scope);
411
412 // mapping from template arguments to values/types
413 template_map.build(decl_tmp.template_type(), tc_template_args);
414
415 decl_tmp.remove(ID_template_type);
416 decl_tmp.remove(ID_is_template);
417
418 convert(decl_tmp);
419 cpp_saved_scope.restore();
420 }
421}
422
424 const irep_idt &base_name,
425 const template_typet &template_type,
426 const cpp_template_args_non_tct &partial_specialization_args)
427{
428 std::string identifier=
430 "template."+id2string(base_name) + "<";
431
432 int counter=0;
433
434 // these are probably not needed -- templates
435 // should be unique in a namespace
436 for(template_typet::template_parameterst::const_iterator
437 it=template_type.template_parameters().begin();
438 it!=template_type.template_parameters().end();
439 it++)
440 {
441 if(counter!=0)
442 identifier+=',';
443
444 if(it->id()==ID_type)
445 identifier+="Type"+std::to_string(counter);
446 else
447 identifier+="Non_Type"+std::to_string(counter);
448
449 counter++;
450 }
451
452 identifier += ">";
453
454 if(!partial_specialization_args.arguments().empty())
455 {
456 identifier+="_specialized_to_<";
457
458 counter=0;
459 for(cpp_template_args_non_tct::argumentst::const_iterator
460 it=partial_specialization_args.arguments().begin();
461 it!=partial_specialization_args.arguments().end();
462 it++, counter++)
463 {
464 if(counter!=0)
465 identifier+=',';
466
467 // These are not yet typechecked, as they may depend
468 // on unassigned template parameters.
469
470 if(it->id() == ID_type || it->id() == ID_ambiguous)
471 identifier+=cpp_type2name(it->type());
472 else
473 identifier+=cpp_expr2name(*it);
474 }
475
476 identifier+='>';
477 }
478
479 return identifier;
480}
481
483 const irep_idt &base_name,
484 const template_typet &template_type,
485 const typet &function_type)
486{
487 // we first build something without function arguments
488 cpp_template_args_non_tct partial_specialization_args;
489 std::string identifier=
490 class_template_identifier(base_name, template_type,
491 partial_specialization_args);
492
493 // we must also add the signature of the function to the identifier
494 identifier+=cpp_type2name(function_type);
495
496 return identifier;
497}
498
500 cpp_declarationt &declaration)
501{
502 cpp_save_scopet saved_scope(cpp_scopes);
503
504 typet &type=declaration.type();
505
506 assert(type.id()==ID_struct);
507
508 cpp_namet &cpp_name=
509 static_cast<cpp_namet &>(type.add(ID_tag));
510
511 if(cpp_name.is_qualified())
512 {
514 error() << "qualifiers not expected here" << eom;
515 throw 0;
516 }
517
518 if(cpp_name.get_sub().size()!=2 ||
519 cpp_name.get_sub()[0].id()!=ID_name ||
520 cpp_name.get_sub()[1].id()!=ID_template_args)
521 {
522 // currently we are more restrictive
523 // than the standard
525 error() << "bad template-class-specialization name" << eom;
526 throw 0;
527 }
528
529 irep_idt base_name=
530 cpp_name.get_sub()[0].get(ID_identifier);
531
532 // copy the template arguments
533 const cpp_template_args_non_tct template_args_non_tc=
535
536 // Remove the template arguments from the name.
537 cpp_name.get_sub().pop_back();
538
539 // get the template symbol
540
541 auto id_set = cpp_scopes.current_scope().lookup(
543
544 // remove any specializations
545 for(cpp_scopest::id_sett::iterator
546 it=id_set.begin();
547 it!=id_set.end();
548 ) // no it++
549 {
550 cpp_scopest::id_sett::iterator next=it;
551 next++;
552
553 if(lookup((*it)->identifier).type.find(ID_specialization_of).is_not_nil())
554 id_set.erase(it);
555
556 it=next;
557 }
558
559 // only one should be left
560 if(id_set.empty())
561 {
563 error() << "class template '" << base_name << "' not found" << eom;
564 throw 0;
565 }
566 else if(id_set.size()>1)
567 {
569 error() << "class template '" << base_name << "' is ambiguous" << eom;
570 throw 0;
571 }
572
573 symbol_tablet::symbolst::const_iterator s_it=
574 symbol_table.symbols.find((*id_set.begin())->identifier);
575
576 assert(s_it!=symbol_table.symbols.end());
577
578 const symbolt &template_symbol=s_it->second;
579
580 if(!template_symbol.type.get_bool(ID_is_template))
581 {
583 error() << "expected a template" << eom;
584 }
585
586 #if 0
587 // is this partial specialization?
588 if(declaration.template_type().parameters().empty())
589 {
590 // typecheck arguments -- these are for the 'primary' template!
591 cpp_template_args_tct template_args_tc=
593 declaration.source_location(),
594 to_cpp_declaration(template_symbol.type).template_type(),
595 template_args_non_tc);
596
597 // Full specialization, i.e., template<>.
598 // We instantiate.
600 cpp_name.source_location(),
601 template_symbol,
602 template_args_tc,
603 type);
604 }
605 else // NOLINT(readability/braces)
606 #endif
607
608 {
609 // partial specialization -- we typecheck
610 declaration.partial_specialization_args()=template_args_non_tc;
611 declaration.set_specialization_of(template_symbol.name);
612
613 typecheck_class_template(declaration);
614 }
615}
616
618 cpp_declarationt &declaration)
619{
620 cpp_save_scopet saved_scope(cpp_scopes);
621
622 if(declaration.declarators().size()!=1 ||
623 declaration.declarators().front().type().id()!=ID_function_type)
624 {
625 error().source_location=declaration.type().source_location();
626 error() << "expected function template specialization" << eom;
627 throw 0;
628 }
629
630 assert(declaration.declarators().size()==1);
631 cpp_declaratort declarator=declaration.declarators().front();
632 cpp_namet &cpp_name=declarator.name();
633
634 // There is specialization (instantiation with template arguments)
635 // but also function overloading (no template arguments)
636
637 assert(!cpp_name.get_sub().empty());
638
639 if(cpp_name.get_sub().back().id()==ID_template_args)
640 {
641 // proper specialization with arguments
642 if(cpp_name.get_sub().size()!=2 ||
643 cpp_name.get_sub()[0].id()!=ID_name ||
644 cpp_name.get_sub()[1].id()!=ID_template_args)
645 {
646 // currently we are more restrictive
647 // than the standard
649 error() << "bad template-function-specialization name" << eom;
650 throw 0;
651 }
652
653 std::string base_name=
654 cpp_name.get_sub()[0].get(ID_identifier).c_str();
655
656 const auto id_set =
658
659 if(id_set.empty())
660 {
662 error() << "template function '" << base_name << "' not found" << eom;
663 throw 0;
664 }
665 else if(id_set.size()>1)
666 {
668 error() << "template function '" << base_name << "' is ambiguous" << eom;
669 throw 0;
670 }
671
672 const symbolt &template_symbol=
673 lookup((*id_set.begin())->identifier);
674
675 cpp_template_args_tct template_args=
677 declaration.source_location(),
678 template_symbol,
679 to_cpp_template_args_non_tc(cpp_name.get_sub()[1]));
680
681 cpp_name.get_sub().pop_back();
682
683 typet specialization;
684 specialization.swap(declarator);
685
687 cpp_name.source_location(),
688 template_symbol,
689 template_args,
690 template_args,
691 specialization);
692 }
693 else
694 {
695 // Just overloading, but this is still a template
696 // for disambiguation purposes!
697 // http://www.gotw.ca/publications/mill17.htm
698 cpp_declarationt new_declaration=declaration;
699
700 new_declaration.remove(ID_template_type);
701 new_declaration.remove(ID_is_template);
702 new_declaration.set(ID_C_template, ""); // todo, get identifier
703
704 convert_non_template_declaration(new_declaration);
705 }
706}
707
709 template_typet &type)
710{
711 cpp_save_scopet cpp_saved_scope(cpp_scopes);
712
713 assert(type.id()==ID_template);
714
715 std::string id_suffix="template::"+std::to_string(template_counter++);
716
717 // produce a new scope for the template parameters
718 cpp_scopet &template_scope = cpp_scopes.current_scope().new_scope(id_suffix);
720
721 cpp_scopes.go_to(template_scope);
722
723 // put template parameters into this scope
725 type.template_parameters();
726
727 unsigned anon_count=0;
728
729 for(template_typet::template_parameterst::iterator
730 it=parameters.begin();
731 it!=parameters.end();
732 it++)
733 {
734 exprt &parameter=*it;
735
736 cpp_declarationt declaration;
737 declaration.swap(static_cast<cpp_declarationt &>(parameter));
738
739 cpp_declarator_convertert cpp_declarator_converter(*this);
740
741 // there must be _one_ declarator
742 assert(declaration.declarators().size()==1);
743
744 cpp_declaratort &declarator=declaration.declarators().front();
745
746 // it may be anonymous
747 if(declarator.name().is_nil())
748 declarator.name() = cpp_namet("anon#" + std::to_string(++anon_count));
749
750 #if 1
751 // The declarator needs to be just a name
752 if(declarator.name().get_sub().size()!=1 ||
753 declarator.name().get_sub().front().id()!=ID_name)
754 {
755 error().source_location=declaration.source_location();
756 error() << "template parameter must be simple name" << eom;
757 throw 0;
758 }
759
761
762 irep_idt base_name=declarator.name().get_sub().front().get(ID_identifier);
763 irep_idt identifier=scope.prefix+id2string(base_name);
764
765 // add to scope
766 cpp_idt &id=scope.insert(base_name);
767 id.identifier=identifier;
769
770 // is it a type or not?
771 if(declaration.get_bool(ID_is_type))
772 {
773 parameter = type_exprt(template_parameter_symbol_typet(identifier));
774 parameter.type().add_source_location()=declaration.find_source_location();
775 }
776 else
777 {
778 // The type is not checked, as it might depend
779 // on earlier parameters.
780 parameter = symbol_exprt(identifier, declaration.type());
781 }
782
783 // There might be a default type or default value.
784 // We store it for later, as it can't be typechecked now
785 // because of possible dependencies on earlier parameters!
786 if(declarator.value().is_not_nil())
787 parameter.add(ID_C_default_value)=declarator.value();
788
789 #else
790 // is it a type or not?
791 cpp_declarator_converter.is_typedef=declaration.get_bool(ID_is_type);
792
793 // say it a template parameter
794 cpp_declarator_converter.is_template_parameter=true;
795
796 // There might be a default type or default value.
797 // We store it for later, as it can't be typechecked now
798 // because of possible dependencies on earlier parameters!
799 exprt default_value=declarator.value();
800 declarator.value().make_nil();
801
802 const symbolt &symbol=
803 cpp_declarator_converter.convert(declaration, declarator);
804
805 if(cpp_declarator_converter.is_typedef)
806 {
807 parameter = exprt(ID_type, struct_tag_typet(symbol.name));
808 parameter.type().add_source_location()=declaration.find_location();
809 }
810 else
811 parameter=symbol.symbol_expr();
812
813 // set (non-typechecked) default value
814 if(default_value.is_not_nil())
815 parameter.add(ID_C_default_value)=default_value;
816
817 parameter.add_source_location()=declaration.find_location();
818 #endif
819 }
820
821 return template_scope;
822}
823
827 const source_locationt &source_location,
828 const symbolt &template_symbol,
829 const cpp_template_args_non_tct &template_args)
830{
831 // old stuff
832 PRECONDITION(template_args.id() != ID_already_typechecked);
833
834 assert(template_symbol.type.get_bool(ID_is_template));
835
836 const template_typet &template_type=
837 to_cpp_declaration(template_symbol.type).template_type();
838
839 // bad re-cast, but better than copying the args one by one
841 (const cpp_template_args_tct &)(template_args);
842
844 result.arguments();
845
846 const template_typet::template_parameterst &parameters=
847 template_type.template_parameters();
848
849 if(parameters.size()<args.size())
850 {
851 error().source_location=source_location;
852 error() << "too many template arguments (expected "
853 << parameters.size() << ", but got "
854 << args.size() << ")" << eom;
855 throw 0;
856 }
857
858 // we will modify the template map
859 template_mapt old_template_map;
860 old_template_map=template_map;
861
862 // check for default arguments
863 for(std::size_t i=0; i<parameters.size(); i++)
864 {
865 const template_parametert &parameter=parameters[i];
866 cpp_save_scopet cpp_saved_scope(cpp_scopes);
867
868 if(i>=args.size())
869 {
870 // Check for default argument for the parameter.
871 // These may depend on previous arguments.
872 if(!parameter.has_default_argument())
873 {
874 error().source_location=source_location;
875 error() << "not enough template arguments (expected "
876 << parameters.size() << ", but got " << args.size()
877 << ")" << eom;
878 throw 0;
879 }
880
881 args.push_back(parameter.default_argument());
882
883 // these need to be typechecked in the scope of the template,
884 // not in the current scope!
885 cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
887 template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
888 cpp_scopes.go_to(*template_scope);
889 }
890
891 assert(i<args.size());
892
893 exprt &arg=args[i];
894
895 if(parameter.id()==ID_type)
896 {
897 if(arg.id()==ID_type)
898 {
899 typecheck_type(arg.type());
900 }
901 else if(arg.id() == ID_ambiguous)
902 {
903 typecheck_type(arg.type());
904 typet t=arg.type();
905 arg=exprt(ID_type, t);
906 }
907 else
908 {
910 error() << "expected type, but got expression" << eom;
911 throw 0;
912 }
913 }
914 else // expression
915 {
916 if(arg.id()==ID_type)
917 {
919 error() << "expected expression, but got type" << eom;
920 throw 0;
921 }
922 else if(arg.id() == ID_ambiguous)
923 {
924 exprt e;
925 e.swap(arg.type());
926 arg.swap(e);
927 }
928
929 typet type=parameter.type();
930
931 // First check the parameter type (might have earlier
932 // type parameters in it). Needs to be checked in scope
933 // of template.
934 {
935 cpp_save_scopet cpp_saved_scope_before_parameter_typecheck(cpp_scopes);
936 cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
938 template_scope!=nullptr,
940 "template_scope is null");
941 cpp_scopes.go_to(*template_scope);
942 typecheck_type(type);
943 }
944
945 // Now check the argument to match that.
946 typecheck_expr(arg);
947 simplify(arg, *this);
948 implicit_typecast(arg, type);
949 }
950
951 // Set right away -- this is for the benefit of default
952 // arguments and later parameters whose type might
953 // depend on an earlier parameter.
954
955 template_map.set(parameter, arg);
956 }
957
958 // restore template map
959 template_map.swap(old_template_map);
960
961 // now the numbers should match
962 assert(args.size()==parameters.size());
963
964 return result;
965}
966
968 cpp_declarationt &declaration)
969{
970 assert(declaration.is_template());
971
972 if(declaration.member_spec().is_virtual())
973 {
974 error().source_location=declaration.source_location();
975 error() << "invalid use of 'virtual' in template declaration"
976 << eom;
977 throw 0;
978 }
979
980 if(declaration.is_typedef())
981 {
982 error().source_location=declaration.source_location();
983 error() << "template declaration for typedef" << eom;
984 throw 0;
985 }
986
987 typet &type=declaration.type();
988
989 // there are
990 // 1) function templates
991 // 2) class templates
992 // 3) template members of class templates (static or methods)
993 // 4) variable templates (C++14)
994
995 if(declaration.is_class_template())
996 {
997 // there should not be declarators
998 if(!declaration.declarators().empty())
999 {
1000 error().source_location=declaration.source_location();
1001 error() << "class template not expected to have declarators"
1002 << eom;
1003 throw 0;
1004 }
1005
1006 // it needs to be a class template
1007 if(type.id()!=ID_struct)
1008 {
1009 error().source_location=declaration.source_location();
1010 error() << "expected class template" << eom;
1011 throw 0;
1012 }
1013
1014 // Is it class template specialization?
1015 // We can tell if there are template arguments in the class name,
1016 // like template<...> class tag<stuff> ...
1017 if((static_cast<const cpp_namet &>(
1018 type.find(ID_tag))).has_template_args())
1019 {
1021 return;
1022 }
1023
1024 typecheck_class_template(declaration);
1025 return;
1026 }
1027 // maybe function template, maybe class template member, maybe
1028 // template variable
1029 else
1030 {
1031 // there should be declarators in either case
1032 if(declaration.declarators().empty())
1033 {
1034 error().source_location=declaration.source_location();
1035 error() << "non-class template is expected to have a declarator"
1036 << eom;
1037 throw 0;
1038 }
1039
1040 // Is it function template specialization?
1041 // Only full specialization is allowed!
1042 if(declaration.template_type().template_parameters().empty())
1043 {
1045 return;
1046 }
1047
1048 // Explicit qualification is forbidden for function templates,
1049 // which we can use to distinguish them.
1050
1051 assert(declaration.declarators().size()>=1);
1052
1053 cpp_declaratort &declarator=declaration.declarators()[0];
1054 const cpp_namet &cpp_name = declarator.name();
1055
1056 if(cpp_name.is_qualified() ||
1057 cpp_name.has_template_args())
1058 return typecheck_class_template_member(declaration);
1059
1060 // must be function template
1061 typecheck_function_template(declaration);
1062 return;
1063 }
1064}
Generic exception types primarily designed for use with invariants.
symbol_tablet & symbol_table
const irep_idt module
const declaratorst & declarators() const
const cpp_member_spect & member_spec() const
void set_specialization_of(const irep_idt &id)
bool is_template() const
bool is_class_template() const
cpp_template_args_non_tct & partial_specialization_args()
template_typet & template_type()
bool is_typedef() const
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
typet merge_type(const typet &declaration_type) const
cpp_namet & name()
Definition: cpp_id.h:23
irep_idt identifier
Definition: cpp_id.h:72
std::string prefix
Definition: cpp_id.h:79
id_classt id_class
Definition: cpp_id.h:45
bool is_template_scope() const
Definition: cpp_id.h:67
bool is_virtual() const
bool is_qualified() const
Definition: cpp_name.h:109
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
bool has_template_args() const
Definition: cpp_name.h:124
bool is_simple_name() const
Definition: cpp_name.h:89
const source_locationt & source_location() const
Definition: cpp_name.h:73
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
id_mapt id_map
Definition: cpp_scopes.h:68
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:190
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
@ SCOPE_ONLY
Definition: cpp_scope.h:30
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition: cpp_scope.h:32
exprt::operandst argumentst
std::string class_template_identifier(const irep_idt &base_name, const template_typet &template_type, const cpp_template_args_non_tct &partial_specialization_args)
void typecheck_type(typet &) override
template_mapt template_map
std::string function_template_identifier(const irep_idt &base_name, const template_typet &template_type, const typet &function_type)
void convert_template_declaration(cpp_declarationt &declaration)
void implicit_typecast(exprt &expr, const typet &type) override
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
void convert_non_template_declaration(cpp_declarationt &declaration)
void typecheck_function_template(cpp_declarationt &declaration)
typecheck function templates
unsigned template_counter
void typecheck_class_template_member(cpp_declarationt &declaration)
typecheck class template members; these can be methods or static members
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 convert(cpp_linkage_spect &)
void typecheck_expr(exprt &) override
cpp_scopet & typecheck_template_parameters(template_typet &type)
void typecheck_class_template(cpp_declarationt &declaration)
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{})
cpp_scopest cpp_scopes
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
void convert_class_template_specialization(cpp_declarationt &declaration)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const char * c_str() const
Definition: dstring.h:99
size_t size() const
Definition: dstring.h:104
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
void remove(const irep_idt &name)
Definition: irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
subt & get_sub()
Definition: irep.h:456
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
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 & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Expression to hold a symbol (variable)
Definition: std_expr.h:80
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:90
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_macro
Definition: symbol.h:61
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void set(const template_parametert &parameter, const exprt &value)
void swap(template_mapt &template_map)
Definition: template_map.h:37
template_parameterst & template_parameters()
std::vector< template_parametert > template_parameterst
An expression denoting a type.
Definition: std_expr.h:2771
The type of an expression, extends irept.
Definition: type.h:29
source_locationt & add_source_location()
Definition: type.h:79
const source_locationt & source_location() const
Definition: type.h:74
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
C++ Language Type Checking.
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
std::string cpp_type2name(const typet &type)
std::string cpp_expr2name(const exprt &expr)
C++ Language Module.
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
bool simplify(exprt &expr, const namespacet &ns)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
a template parameter symbol that is a type