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  symbol_tablet::symbolst::iterator previous_symbol=
111  symbol_table.symbols.find(symbol_name);
112 
113  if(previous_symbol!=symbol_table.symbols.end())
114  {
115  // there already
116  cpp_declarationt &previous_declaration=
117  to_cpp_declaration(previous_symbol->second.type);
118 
119  bool previous_has_body=
120  previous_declaration.type().find(ID_body).is_not_nil();
121 
122  // check if we have 2 bodies
123  if(has_body && previous_has_body)
124  {
126  error() << "template struct `" << base_name
127  << "' defined previously\n"
128  << "location of previous definition: "
129  << previous_symbol->second.location << eom;
130  throw 0;
131  }
132 
133  if(has_body)
134  {
135  // We replace the template!
136  // We have to retain any default parameters from the previous declaration.
138  previous_declaration.template_type(),
139  declaration.template_type());
140 
141  previous_symbol->second.type.swap(declaration);
142 
143  #if 0
144  std::cout << "*****\n";
145  std::cout << *cpp_scopes.id_map[symbol_name];
146  std::cout << "*****\n";
147  std::cout << "II: " << symbol_name << '\n';
148  #endif
149 
150  // We also replace the template scope (the old one could be deleted).
151  cpp_scopes.id_map[symbol_name]=&template_scope;
152 
153  // We also fix the parent scope in order to see the new
154  // template arguments
155  }
156  else
157  {
158  // just update any default arguments
160  declaration.template_type(),
161  previous_declaration.template_type());
162  }
163 
164  assert(cpp_scopes.id_map[symbol_name]->id_class ==
166  return;
167  }
168 
169  // it's not there yet
170 
171  symbolt symbol;
172 
173  symbol.name=symbol_name;
174  symbol.base_name=base_name;
175  symbol.location=cpp_name.source_location();
176  symbol.mode=ID_cpp;
177  symbol.module=module;
178  symbol.type.swap(declaration);
179  symbol.is_macro=false;
180  symbol.value=exprt("template_decls");
181 
182  symbol.pretty_name=
184 
185  symbolt *new_symbol;
186  if(symbol_table.move(symbol, new_symbol))
187  {
188  error().source_location=symbol.location;
189  error() << "cpp_typecheckt::typecheck_compound_type: "
190  << "symbol_table.move() failed"
191  << eom;
192  throw 0;
193  }
194 
195  // put into current scope
196  cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
198  id.prefix=cpp_scopes.current_scope().prefix+
199  id2string(new_symbol->base_name);
200 
201  // link the template symbol with the template scope
202  cpp_scopes.id_map[symbol_name]=&template_scope;
203  assert(cpp_scopes.id_map[symbol_name]->id_class ==
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=to_cpp_name(declarator.add(ID_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 
235  cpp_convert_plain_type(function_type);
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::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  previous_symbol->second.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  {
292  error().source_location=symbol.location;
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  assert(template_scope.id_class==cpp_idt::id_classt::TEMPLATE_SCOPE);
307  cpp_scopes.id_map[symbol_name] = &template_scope;
308 }
309 
312  cpp_declarationt &declaration)
313 {
314  assert(declaration.declarators().size()==1);
315 
316  cpp_declaratort &declarator=declaration.declarators()[0];
317  const cpp_namet &cpp_name=to_cpp_name(declarator.add(ID_name));
318 
319  assert(cpp_name.is_qualified() ||
320  cpp_name.has_template_args());
321 
322  // must be of the form: name1<template_args>::name2
323  // or: name1<template_args>::operator X
324  if(cpp_name.get_sub().size()==4 &&
325  cpp_name.get_sub()[0].id()==ID_name &&
326  cpp_name.get_sub()[1].id()==ID_template_args &&
327  cpp_name.get_sub()[2].id()=="::" &&
328  cpp_name.get_sub()[3].id()==ID_name)
329  {
330  }
331  else if(cpp_name.get_sub().size()==5 &&
332  cpp_name.get_sub()[0].id()==ID_name &&
333  cpp_name.get_sub()[1].id()==ID_template_args &&
334  cpp_name.get_sub()[2].id()=="::" &&
335  cpp_name.get_sub()[3].id()==ID_operator)
336  {
337  }
338  else
339  {
340  return; // TODO
342  error() << "bad template name" << eom;
343  throw 0;
344  }
345 
346  // let's find the class template this function template belongs to.
348 
350  cpp_name.get_sub().front().get(ID_identifier),
351  cpp_scopet::SCOPE_ONLY, // look only in current scope
352  cpp_scopet::id_classt::TEMPLATE, // must be template
353  id_set);
354 
355  if(id_set.empty())
356  {
359  error() << "class template `"
360  << cpp_name.get_sub().front().get(ID_identifier)
361  << "' not found" << eom;
362  throw 0;
363  }
364  else if(id_set.size()>1)
365  {
367  error() << "class template `"
368  << cpp_name.get_sub().front().get(ID_identifier)
369  << "' is ambiguous" << eom;
370  throw 0;
371  }
372  else if((*(id_set.begin()))->id_class!=cpp_idt::id_classt::TEMPLATE)
373  {
374  // std::cerr << *(*id_set.begin()) << '\n';
376  error() << "class template `"
377  << cpp_name.get_sub().front().get(ID_identifier)
378  << "' is not a template" << eom;
379  throw 0;
380  }
381 
382  const cpp_idt &cpp_id=**(id_set.begin());
383  symbolt &template_symbol=
384  symbol_table.symbols.find(cpp_id.identifier)->second;
385 
386  exprt &template_methods=static_cast<exprt &>(
387  template_symbol.value.add("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("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()=="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  {
513  error().source_location=cpp_name.source_location();
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
524  error().source_location=cpp_name.source_location();
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=
534  to_cpp_template_args_non_tc(cpp_name.get_sub()[1]);
535 
536  // Remove the template arguments from the name.
537  cpp_name.get_sub().pop_back();
538 
539  // get the template symbol
540 
544 
545  // remove any specializations
546  for(cpp_scopest::id_sett::iterator
547  it=id_set.begin();
548  it!=id_set.end();
549  ) // no it++
550  {
551  cpp_scopest::id_sett::iterator next=it;
552  next++;
553 
554  if(lookup((*it)->identifier).type.
555  find("specialization_of").is_not_nil())
556  id_set.erase(it);
557 
558  it=next;
559  }
560 
561  // only one should be left
562  if(id_set.empty())
563  {
565  error() << "class template `" << base_name << "' not found" << eom;
566  throw 0;
567  }
568  else if(id_set.size()>1)
569  {
571  error() << "class template `" << base_name << "' is ambiguous"
572  << eom;
573  throw 0;
574  }
575 
576  symbol_tablet::symbolst::iterator s_it=
577  symbol_table.symbols.find((*id_set.begin())->identifier);
578 
579  assert(s_it!=symbol_table.symbols.end());
580 
581  symbolt &template_symbol=s_it->second;
582 
583  if(!template_symbol.type.get_bool(ID_is_template))
584  {
586  error() << "expected a template" << eom;
587  }
588 
589  #if 0
590  // is this partial specialization?
591  if(declaration.template_type().parameters().empty())
592  {
593  // typecheck arguments -- these are for the 'primary' template!
594  cpp_template_args_tct template_args_tc=
596  declaration.source_location(),
597  to_cpp_declaration(template_symbol.type).template_type(),
598  template_args_non_tc);
599 
600  // Full specialization, i.e., template<>.
601  // We instantiate.
603  cpp_name.source_location(),
604  template_symbol,
605  template_args_tc,
606  type);
607  }
608  else // NOLINT(readability/braces)
609  #endif
610 
611  {
612  // partial specialization -- we typecheck
613  declaration.partial_specialization_args()=template_args_non_tc;
614  declaration.set_specialization_of(template_symbol.name);
615 
616  typecheck_class_template(declaration);
617  }
618 }
619 
621  cpp_declarationt &declaration)
622 {
623  cpp_save_scopet saved_scope(cpp_scopes);
624 
625  if(declaration.declarators().size()!=1 ||
626  declaration.declarators().front().type().id()!=ID_function_type)
627  {
628  error().source_location=declaration.type().source_location();
629  error() << "expected function template specialization" << eom;
630  throw 0;
631  }
632 
633  assert(declaration.declarators().size()==1);
634  cpp_declaratort declarator=declaration.declarators().front();
635  cpp_namet &cpp_name=declarator.name();
636 
637  if(cpp_name.is_qualified())
638  {
640  error() << "qualifiers not expected here" << eom;
641  throw 0;
642  }
643 
644  // There is specialization (instantiation with template arguments)
645  // but also function overloading (no template arguments)
646 
647  assert(!cpp_name.get_sub().empty());
648 
649  if(cpp_name.get_sub().back().id()==ID_template_args)
650  {
651  // proper specialization with arguments
652  if(cpp_name.get_sub().size()!=2 ||
653  cpp_name.get_sub()[0].id()!=ID_name ||
654  cpp_name.get_sub()[1].id()!=ID_template_args)
655  {
656  // currently we are more restrictive
657  // than the standard
659  error() << "bad template-function-specialization name" << eom;
660  throw 0;
661  }
662 
663  std::string base_name=
664  cpp_name.get_sub()[0].get(ID_identifier).c_str();
665 
668  base_name, cpp_scopet::SCOPE_ONLY, id_set);
669 
670  if(id_set.empty())
671  {
673  error() << "template function `" << base_name << "' not found"
674  << eom;
675  throw 0;
676  }
677  else if(id_set.size()>1)
678  {
680  error() << "template function `" << base_name
681  << "' is ambiguous" << eom;
682  throw 0;
683  }
684 
685  const symbolt &template_symbol=
686  lookup((*id_set.begin())->identifier);
687 
688  cpp_template_args_tct template_args=
690  declaration.source_location(),
691  template_symbol,
692  to_cpp_template_args_non_tc(cpp_name.get_sub()[1]));
693 
694  cpp_name.get_sub().pop_back();
695 
696  typet specialization;
697  specialization.swap(declarator);
698 
700  cpp_name.source_location(),
701  template_symbol,
702  template_args,
703  template_args,
704  specialization);
705  }
706  else
707  {
708  // Just overloading, but this is still a template
709  // for disambiguation purposes!
710  // http://www.gotw.ca/publications/mill17.htm
711  cpp_declarationt new_declaration=declaration;
712 
713  new_declaration.remove(ID_template_type);
714  new_declaration.remove(ID_is_template);
715  new_declaration.set(ID_C_template, ""); // todo, get identifier
716 
717  convert_non_template_declaration(new_declaration);
718  }
719 }
720 
722  template_typet &type)
723 {
724  cpp_save_scopet cpp_saved_scope(cpp_scopes);
725 
726  assert(type.id()==ID_template);
727 
728  std::string id_suffix="template::"+std::to_string(template_counter++);
729 
730  // produce a new scope for the template parameters
731  cpp_scopet &template_scope=
733  cpp_scopes.current_scope().prefix+id_suffix);
734 
735  template_scope.prefix=template_scope.get_parent().prefix+id_suffix;
737 
738  cpp_scopes.go_to(template_scope);
739 
740  // put template parameters into this scope
742  type.template_parameters();
743 
744  unsigned anon_count=0;
745 
746  for(template_typet::template_parameterst::iterator
747  it=parameters.begin();
748  it!=parameters.end();
749  it++)
750  {
751  exprt &parameter=*it;
752 
753  cpp_declarationt declaration;
754  declaration.swap(static_cast<cpp_declarationt &>(parameter));
755 
756  cpp_declarator_convertert cpp_declarator_converter(*this);
757 
758  // there must be _one_ declarator
759  assert(declaration.declarators().size()==1);
760 
761  cpp_declaratort &declarator=declaration.declarators().front();
762 
763  // it may be anonymous
764  if(declarator.name().is_nil())
765  {
766  irept name(ID_name);
767  name.set(ID_identifier, "anon#"+std::to_string(++anon_count));
768  declarator.name()=cpp_namet();
769  declarator.name().get_sub().push_back(name);
770  }
771 
772  #if 1
773  // The declarator needs to be just a name
774  if(declarator.name().get_sub().size()!=1 ||
775  declarator.name().get_sub().front().id()!=ID_name)
776  {
777  error().source_location=declaration.source_location();
778  error() << "template parameter must be simple name" << eom;
779  throw 0;
780  }
781 
783 
784  irep_idt base_name=declarator.name().get_sub().front().get(ID_identifier);
785  irep_idt identifier=scope.prefix+id2string(base_name);
786 
787  // add to scope
788  cpp_idt &id=scope.insert(base_name);
789  id.identifier=identifier;
791 
792  // is it a type or not?
793  if(declaration.get_bool(ID_is_type))
794  {
795  parameter=exprt(ID_type, typet(ID_symbol));
796  parameter.type().set(ID_identifier, identifier);
797  parameter.type().add_source_location()=declaration.find_source_location();
798  }
799  else
800  {
801  // The type is not checked, as it might depend
802  // on earlier parameters.
803  typet type=declaration.type();
804  parameter=symbol_exprt(identifier, type);
805  }
806 
807  // There might be a default type or default value.
808  // We store it for later, as it can't be typechecked now
809  // because of possible dependencies on earlier parameters!
810  if(declarator.value().is_not_nil())
811  parameter.add(ID_C_default_value)=declarator.value();
812 
813  #else
814  // is it a type or not?
815  cpp_declarator_converter.is_typedef=declaration.get_bool(ID_is_type);
816 
817  // say it a template parameter
818  cpp_declarator_converter.is_template_parameter=true;
819 
820  // There might be a default type or default value.
821  // We store it for later, as it can't be typechecked now
822  // because of possible dependencies on earlier parameters!
823  exprt default_value=declarator.value();
824  declarator.value().make_nil();
825 
826  const symbolt &symbol=
827  cpp_declarator_converter.convert(declaration, declarator);
828 
829  if(cpp_declarator_converter.is_typedef)
830  {
831  parameter=exprt(ID_type, typet(ID_symbol));
832  parameter.type().set(ID_identifier, symbol.name);
833  parameter.type().add_source_location()=declaration.find_location();
834  }
835  else
836  parameter=symbol.symbol_expr();
837 
838  // set (non-typechecked) default value
839  if(default_value.is_not_nil())
840  parameter.add(ID_C_default_value)=default_value;
841 
842  parameter.add_source_location()=declaration.find_location();
843  #endif
844  }
845 
846  // continue without adding to the prefix
847  template_scope.prefix=template_scope.get_parent().prefix;
848 
849  return template_scope;
850 }
851 
855  const source_locationt &source_location,
856  const symbolt &template_symbol,
857  const cpp_template_args_non_tct &template_args)
858 {
859  // old stuff
860  assert(template_args.id()!=ID_already_typechecked);
861 
862  assert(template_symbol.type.get_bool(ID_is_template));
863 
864  const template_typet &template_type=
865  to_cpp_declaration(template_symbol.type).template_type();
866 
867  // bad re-cast, but better than copying the args one by one
869  (const cpp_template_args_tct &)(template_args);
870 
872  result.arguments();
873 
874  const template_typet::template_parameterst &parameters=
875  template_type.template_parameters();
876 
877  if(parameters.size()<args.size())
878  {
879  error().source_location=source_location;
880  error() << "too many template arguments (expected "
881  << parameters.size() << ", but got "
882  << args.size() << ")" << eom;
883  throw 0;
884  }
885 
886  // we will modify the template map
887  template_mapt old_template_map;
888  old_template_map=template_map;
889 
890  // check for default arguments
891  for(std::size_t i=0; i<parameters.size(); i++)
892  {
893  const template_parametert &parameter=parameters[i];
894  cpp_save_scopet cpp_saved_scope(cpp_scopes);
895 
896  if(i>=args.size())
897  {
898  // Check for default argument for the parameter.
899  // These may depend on previous arguments.
900  if(!parameter.has_default_argument())
901  {
902  error().source_location=source_location;
903  error() << "not enough template arguments (expected "
904  << parameters.size() << ", but got " << args.size()
905  << ")" << eom;
906  throw 0;
907  }
908 
909  args.push_back(parameter.default_argument());
910 
911  // these need to be typechecked in the scope of the template,
912  // not in the current scope!
913  cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
915  template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
916  cpp_scopes.go_to(*template_scope);
917  }
918 
919  assert(i<args.size());
920 
921  exprt &arg=args[i];
922 
923  if(parameter.id()==ID_type)
924  {
925  if(arg.id()==ID_type)
926  {
927  typecheck_type(arg.type());
928  }
929  else if(arg.id()=="ambiguous")
930  {
931  typecheck_type(arg.type());
932  typet t=arg.type();
933  arg=exprt(ID_type, t);
934  }
935  else
936  {
937  error().source_location=arg.source_location();
938  error() << "expected type, but got expression" << eom;
939  throw 0;
940  }
941  }
942  else // expression
943  {
944  if(arg.id()==ID_type)
945  {
946  error().source_location=arg.source_location();
947  error() << "expected expression, but got type" << eom;
948  throw 0;
949  }
950  else if(arg.id()=="ambiguous")
951  {
952  exprt e;
953  e.swap(arg.type());
954  arg.swap(e);
955  }
956 
957  typet type=parameter.type();
958 
959  // First check the parameter type (might have earlier
960  // type parameters in it). Needs to be checked in scope
961  // of template.
962  {
963  cpp_save_scopet cpp_saved_scope(cpp_scopes);
964  cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
966  template_scope!=nullptr,
968  "template_scope is null");
969  cpp_scopes.go_to(*template_scope);
970  typecheck_type(type);
971  }
972 
973  // Now check the argument to match that.
974  typecheck_expr(arg);
975  simplify(arg, *this);
976  implicit_typecast(arg, type);
977  }
978 
979  // Set right away -- this is for the benefit of default
980  // arguments and later parameters whose type might
981  // depend on an earlier parameter.
982 
983  template_map.set(parameter, arg);
984  }
985 
986  // restore template map
987  template_map.swap(old_template_map);
988 
989  // now the numbers should match
990  assert(args.size()==parameters.size());
991 
992  return result;
993 }
994 
996  cpp_declarationt &declaration)
997 {
998  assert(declaration.is_template());
999 
1000  if(declaration.member_spec().is_virtual())
1001  {
1002  error().source_location=declaration.source_location();
1003  error() << "invalid use of 'virtual' in template declaration"
1004  << eom;
1005  throw 0;
1006  }
1007 
1008  if(declaration.is_typedef())
1009  {
1010  error().source_location=declaration.source_location();
1011  error() << "template declaration for typedef" << eom;
1012  throw 0;
1013  }
1014 
1015  typet &type=declaration.type();
1016 
1017  // there are
1018  // 1) function templates
1019  // 2) class templates
1020  // 3) template members of class templates (static or methods)
1021  // 4) variable templates (C++14)
1022 
1023  if(declaration.is_class_template())
1024  {
1025  // there should not be declarators
1026  if(!declaration.declarators().empty())
1027  {
1028  error().source_location=declaration.source_location();
1029  error() << "class template not expected to have declarators"
1030  << eom;
1031  throw 0;
1032  }
1033 
1034  // it needs to be a class template
1035  if(type.id()!=ID_struct)
1036  {
1037  error().source_location=declaration.source_location();
1038  error() << "expected class template" << eom;
1039  throw 0;
1040  }
1041 
1042  // Is it class template specialization?
1043  // We can tell if there are template arguments in the class name,
1044  // like template<...> class tag<stuff> ...
1045  if((static_cast<const cpp_namet &>(
1046  type.find(ID_tag))).has_template_args())
1047  {
1049  return;
1050  }
1051 
1052  typecheck_class_template(declaration);
1053  return;
1054  }
1055  // maybe function template, maybe class template member, maybe
1056  // template variable
1057  else
1058  {
1059  // there should be declarators in either case
1060  if(declaration.declarators().empty())
1061  {
1062  error().source_location=declaration.source_location();
1063  error() << "non-class template is expected to have a declarator"
1064  << eom;
1065  throw 0;
1066  }
1067 
1068  // Is it function template specialization?
1069  // Only full specialization is allowed!
1070  if(declaration.template_type().template_parameters().empty())
1071  {
1073  return;
1074  }
1075 
1076  // Explicit qualification is forbidden for function templates,
1077  // which we can use to distinguish them.
1078 
1079  assert(declaration.declarators().size()>=1);
1080 
1081  cpp_declaratort &declarator=declaration.declarators()[0];
1082  const cpp_namet &cpp_name=to_cpp_name(declarator.add(ID_name));
1083 
1084  if(cpp_name.is_qualified() ||
1085  cpp_name.has_template_args())
1086  return typecheck_class_template_member(declaration);
1087 
1088  // must be function template
1089  typecheck_function_template(declaration);
1090  return;
1091  }
1092 }
bool is_typedef() const
C++ Language Type Checking.
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:209
mstreamt & result()
Definition: message.h:233
void set(const template_parametert &parameter, const exprt &value)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
void typecheck_type(typet &type)
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
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:55
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:61
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:143
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:40
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:49
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
bool is_simple_name() const
Definition: cpp_name.h:88
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:33
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
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:108
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
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:72
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
const declaratorst & declarators() const
symbolst symbols
Definition: symbol_table.h:57
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
const source_locationt & find_source_location() const
Definition: expr.cpp:466
C++ Language Module.
bool has_template_args() const
Definition: cpp_name.h:121
source_locationt source_location
Definition: message.h:175
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
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:87
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.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
id_mapt id_map
Definition: cpp_scopes.h:69
const source_locationt & source_location() const
Definition: type.h:95
irep_idt get_base_name() const
Definition: cpp_name.cpp:17
bool is_template() const
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
cpp_declarationt & to_cpp_declaration(irept &irep)
Base class for all expressions.
Definition: expr.h:46
void convert_class_template_specialization(cpp_declarationt &declaration)
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
unsigned template_counter
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:100
const source_locationt & source_location() const
Definition: expr.h:142
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
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
std::string cpp_expr2name(const exprt &expr)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:66
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