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