CBMC
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  {
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  {
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 
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  {
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  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=
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 
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 }
cpp_scopet::new_scope
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:190
cpp_typecheckt::convert
void convert(cpp_linkage_spect &)
Definition: cpp_typecheck_linkage_spec.cpp:14
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
cpp_typecheckt::convert_non_template_declaration
void convert_non_template_declaration(cpp_declarationt &declaration)
Definition: cpp_typecheck_declaration.cpp:99
dstringt::c_str
const char * c_str() const
Definition: dstring.h:115
cpp_declarationt::is_typedef
bool is_typedef() const
Definition: cpp_declaration.h:133
cpp_scopet
Definition: cpp_scope.h:20
template_parametert
Definition: cpp_template_parameter.h:19
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
cpp_typecheckt::salvage_default_arguments
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
Definition: cpp_typecheck_template.cpp:23
cpp_save_scopet
Definition: cpp_scopes.h:127
cpp_scopest::id_map
id_mapt id_map
Definition: cpp_scopes.h:68
cpp_idt::id_classt::TEMPLATE
@ TEMPLATE
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:104
cpp_scopet::lookup
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition: cpp_scope.h:32
irept::make_nil
void make_nil()
Definition: irep.h:454
typet
The type of an expression, extends irept.
Definition: type.h:28
to_cpp_template_args_non_tc
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
Definition: cpp_template_args.h:48
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:146
irept::find
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
cpp_typecheckt::typecheck_class_template
void typecheck_class_template(cpp_declarationt &declaration)
Definition: cpp_typecheck_template.cpp:44
cpp_typecheckt::typecheck_template_parameters
cpp_scopet & typecheck_template_parameters(template_typet &type)
Definition: cpp_typecheck_template.cpp:708
template_parameter_symbol_typet
a template parameter symbol that is a type
Definition: cpp_template_parameter.h:65
cpp_idt::identifier
irep_idt identifier
Definition: cpp_id.h:72
cpp_type2name.h
cpp_declaratort::name
cpp_namet & name()
Definition: cpp_declarator.h:36
cpp_declarator_convertert::convert
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
Definition: cpp_declarator_converter.cpp:35
exprt
Base class for all expressions.
Definition: expr.h:55
cpp_declarationt::partial_specialization_args
cpp_template_args_non_tct & partial_specialization_args()
Definition: cpp_declaration.h:106
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cpp_typecheckt::convert_class_template_specialization
void convert_class_template_specialization(cpp_declarationt &declaration)
Definition: cpp_typecheck_template.cpp:499
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:448
nullptr_exceptiont
Definition: base_exceptions.h:29
cpp_typecheckt::template_counter
unsigned template_counter
Definition: cpp_typecheck.h:220
cpp_scopet::SCOPE_ONLY
@ SCOPE_ONLY
Definition: cpp_scope.h:30
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
messaget::eom
static eomt eom
Definition: message.h:297
cpp_template_args.h
cpp_template_args_tct
Definition: cpp_template_args.h:64
cpp_declarationt::is_class_template
bool is_class_template() const
Definition: cpp_declaration.h:55
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
cpp_idt
Definition: cpp_id.h:22
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:62
cpp_declarationt::member_spec
const cpp_member_spect & member_spec() const
Definition: cpp_declaration.h:84
cpp_typecheckt::class_template_identifier
std::string class_template_identifier(const irep_idt &base_name, const template_typet &template_type, const cpp_template_args_non_tct &partial_specialization_args)
Definition: cpp_typecheck_template.cpp:423
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
base_exceptions.h
template_mapt::swap
void swap(template_mapt &template_map)
Definition: template_map.h:37
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
cpp_typecheckt::function_template_identifier
std::string function_template_identifier(const irep_idt &base_name, const template_typet &template_type, const typet &function_type)
Definition: cpp_typecheck_template.cpp:482
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:69
cpp_member_spect::is_virtual
bool is_virtual() const
Definition: cpp_member_spec.h:23
cpp_typecheckt::typecheck_class_template_member
void typecheck_class_template_member(cpp_declarationt &declaration)
typecheck class template members; these can be methods or static members
Definition: cpp_typecheck_template.cpp:312
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_typecheckt::typecheck_function_template
void typecheck_function_template(cpp_declarationt &declaration)
typecheck function templates
Definition: cpp_typecheck_template.cpp:208
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
cpp_idt::id_classt::TEMPLATE_PARAMETER
@ TEMPLATE_PARAMETER
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_template_args_baset::arguments
argumentst & arguments()
Definition: cpp_template_args.h:31
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
cpp_declarator_convertert
Definition: cpp_declarator_converter.h:24
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
template_typet::template_parameters
template_parameterst & template_parameters()
Definition: cpp_template_type.h:27
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
typet::source_location
const source_locationt & source_location() const
Definition: type.h:90
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
cpp_declarator_convertert::is_typedef
bool is_typedef
Definition: cpp_declarator_converter.h:30
template_typet::template_parameterst
std::vector< template_parametert > template_parameterst
Definition: cpp_template_type.h:25
cpp_namet::is_simple_name
bool is_simple_name() const
Definition: cpp_name.h:89
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2926
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:68
cpp_declarator_convertert::is_template_parameter
bool is_template_parameter
Definition: cpp_declarator_converter.h:32
cpp_declarationt::set_specialization_of
void set_specialization_of(const irep_idt &id)
Definition: cpp_declaration.h:118
irept::swap
void swap(irept &irep)
Definition: irep.h:442
cpp_convert_type.h
cpp_declarationt
Definition: cpp_declaration.h:21
irept::is_nil
bool is_nil() const
Definition: irep.h:376
irept::id
const irep_idt & id() const
Definition: irep.h:396
cpp_idt::id_classt::TEMPLATE_SCOPE
@ TEMPLATE_SCOPE
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_declarationt::is_template
bool is_template() const
Definition: cpp_declaration.h:50
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:95
cpp_typecheckt::convert_template_declaration
void convert_template_declaration(cpp_declarationt &declaration)
Definition: cpp_typecheck_template.cpp:967
cpp_typecheck.h
cpp_namet::is_qualified
bool is_qualified() const
Definition: cpp_name.h:109
cpp_template_args_non_tct
Definition: cpp_template_args.h:44
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:67
cpp_convert_plain_type
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
Definition: cpp_convert_type.cpp:328
source_locationt
Definition: source_location.h:18
simplify_expr.h
cpp_typecheckt::typecheck_template_args
cpp_template_args_tct typecheck_template_args(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_non_tct &template_args)
Definition: cpp_typecheck_template.cpp:826
symbol_tablet::get_writeable
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
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2263
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
type_exprt
An expression denoting a type.
Definition: std_expr.h:2905
template_parametert::has_default_argument
bool has_default_argument() const
Definition: cpp_template_parameter.h:58
cpp_namet::has_template_args
bool has_template_args() const
Definition: cpp_name.h:124
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
cpp_namet::source_location
const source_locationt & source_location() const
Definition: cpp_name.h:73
cpp_typecheckt::instantiate_template
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{})
Definition: cpp_instantiate_template.cpp:250
cpp_save_scopet::restore
void restore()
Definition: cpp_scopes.h:141
cpp_type2name
std::string cpp_type2name(const typet &type)
Definition: cpp_type2name.cpp:101
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
template_parametert::default_argument
exprt & default_argument()
Definition: cpp_template_parameter.h:48
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
cpp_idt::id_class
id_classt id_class
Definition: cpp_id.h:45
template_mapt
Definition: template_map.h:25
cpp_typecheckt::implicit_typecast
void implicit_typecast(exprt &expr, const typet &type) override
Definition: cpp_typecheck_conversions.cpp:1493
irept::get_sub
subt & get_sub()
Definition: irep.h:456
INVARIANT_STRUCTURED
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407
cpp_declaratort::value
exprt & value()
Definition: cpp_declarator.h:42
cpp_idt::prefix
std::string prefix
Definition: cpp_id.h:79
template_mapt::set
void set(const template_parametert &parameter, const exprt &value)
Definition: template_map.cpp:188
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
template_typet
Definition: cpp_template_type.h:18
cpp_template_args_baset::argumentst
exprt::operandst argumentst
Definition: cpp_template_args.h:29
cpp_typecheckt::convert_template_function_or_member_specialization
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
Definition: cpp_typecheck_template.cpp:617
template_mapt::build
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
Definition: template_map.cpp:145
cpp_expr2name
std::string cpp_expr2name(const exprt &expr)
Definition: cpp_type2name.cpp:183
irept::remove
void remove(const irep_idt &name)
Definition: irep.cpp:96
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:216
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
cpp_namet::get_base_name
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
cpp_typecheckt::template_map
template_mapt template_map
Definition: cpp_typecheck.h:223
cpp_idt::is_template_scope
bool is_template_scope() const
Definition: cpp_id.h:67
cpp_namet
Definition: cpp_name.h:16
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:211
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
cpp_declaratort
Definition: cpp_declarator.h:19
dstringt::size
size_t size() const
Definition: dstring.h:120
validation_modet::INVARIANT
@ INVARIANT
cpp_declarationt::template_type
template_typet & template_type()
Definition: cpp_declaration.h:96
cpp_template_type.h
cpp_scopet::insert
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
cpp_declarator_converter.h
cpp_declaratort::merge_type
typet merge_type(const typet &declaration_type) const
Definition: cpp_declarator.cpp:27