CBMC
cpp_instantiate_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 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <util/arith_tools.h>
19 #include <util/base_exceptions.h> // IWYU pragma: keep
20 #include <util/symbol_table_base.h>
21 
22 #include "cpp_type2name.h"
23 
25  const cpp_template_args_tct &template_args)
26 {
27  // quick hack
28  std::string result="<";
29  bool first=true;
30 
31  const cpp_template_args_tct::argumentst &arguments=
32  template_args.arguments();
33 
34  for(const auto &expr : arguments)
35  {
36  if(first)
37  first=false;
38  else
39  result+=',';
40 
42  expr.id() != ID_ambiguous, "template argument must not be ambiguous");
43 
44  if(expr.id()==ID_type)
45  {
46  const typet &type=expr.type();
47  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
48  result += id2string(to_tag_type(type).get_identifier());
49  else
50  result+=cpp_type2name(type);
51  }
52  else // expression
53  {
54  exprt e=expr;
55 
56  if(e.id() == ID_symbol)
57  {
58  const symbol_exprt &s = to_symbol_expr(e);
59  const symbolt &symbol = lookup(s.get_identifier());
60 
61  if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
62  e = symbol.value;
63  }
64 
65  make_constant(e);
66 
67  // this must be a constant, which includes true/false
68  mp_integer i;
69 
70  if(e.is_true())
71  i=1;
72  else if(e.is_false())
73  i=0;
74  else if(to_integer(to_constant_expr(e), i))
75  {
76  error().source_location = expr.find_source_location();
77  error() << "template argument expression expected to be "
78  << "scalar constant, but got '" << to_string(e) << "'" << eom;
79  throw 0;
80  }
81 
83  }
84  }
85 
86  result+='>';
87 
88  return result;
89 }
90 
92 {
93  for(const auto &e : instantiation_stack)
94  {
95  const symbolt &symbol = lookup(e.identifier);
96  out << "instantiating '" << symbol.pretty_name << "' with <";
97 
98  forall_expr(a_it, e.full_template_args.arguments())
99  {
100  if(a_it != e.full_template_args.arguments().begin())
101  out << ", ";
102 
103  if(a_it->id()==ID_type)
104  out << to_string(a_it->type());
105  else
106  out << to_string(*a_it);
107  }
108 
109  out << "> at " << e.source_location << '\n';
110  }
111 }
112 
115  cpp_scopet &template_scope,
116  const std::string &suffix)
117 {
118  cpp_scopet::id_sett id_set =
119  template_scope.lookup(suffix, cpp_scopet::SCOPE_ONLY);
120 
121  CHECK_RETURN(id_set.size() <= 1);
122 
123  if(id_set.size() == 1)
124  {
125  cpp_idt &cpp_id = **id_set.begin();
127 
128  return static_cast<cpp_scopet &>(cpp_id);
129  }
130  else
131  {
132  cpp_scopet &sub_scope = template_scope.new_scope(suffix);
134  sub_scope.prefix = template_scope.get_parent().prefix;
135  sub_scope.suffix = suffix;
136  sub_scope.add_using_scope(template_scope.get_parent());
137 
138  const std::string subscope_name =
139  id2string(template_scope.identifier) + suffix;
140  cpp_scopes.id_map.insert(
141  cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
142 
143  return sub_scope;
144  }
145 }
146 
148  const source_locationt &source_location,
149  const symbolt &template_symbol,
150  const cpp_template_args_tct &specialization_template_args,
151  const cpp_template_args_tct &full_template_args)
152 {
153  PRECONDITION(!full_template_args.has_unassigned());
154 
155  // do we have args?
156  if(full_template_args.arguments().empty())
157  {
158  error().source_location=source_location;
159  error() << "'" << template_symbol.base_name
160  << "' is a template; thus, expected template arguments" << eom;
161  throw 0;
162  }
163 
164  // produce new symbol name
165  std::string suffix=template_suffix(full_template_args);
166 
167  cpp_scopet *template_scope=
168  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
169 
171  template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
172 
173  irep_idt identifier = id2string(template_scope->get_parent().prefix) +
174  "tag-" + id2string(template_symbol.base_name) +
175  id2string(suffix);
176 
177  // already there?
178  symbol_table_baset::symbolst::const_iterator s_it =
179  symbol_table.symbols.find(identifier);
180  if(s_it!=symbol_table.symbols.end())
181  return s_it->second;
182 
183  // Create as incomplete struct, but mark as
184  // "template_class_instance", to be elaborated later.
185  type_symbolt new_symbol{identifier, struct_typet(), template_symbol.mode};
186  new_symbol.pretty_name=template_symbol.pretty_name;
187  new_symbol.location=template_symbol.location;
188  to_struct_type(new_symbol.type).make_incomplete();
189  new_symbol.type.set(ID_tag, template_symbol.type.find(ID_tag));
190  if(template_symbol.type.get_bool(ID_C_class))
191  new_symbol.type.set(ID_C_class, true);
192  new_symbol.type.set(ID_template_class_instance, true);
193  new_symbol.type.add_source_location()=template_symbol.location;
194  new_symbol.type.set(
195  ID_specialization_template_args, specialization_template_args);
196  new_symbol.type.set(ID_full_template_args, full_template_args);
197  new_symbol.type.set(ID_identifier, template_symbol.name);
198  new_symbol.base_name=template_symbol.base_name;
199 
200  symbolt *s_ptr;
201  symbol_table.move(new_symbol, s_ptr);
202 
203  // put into template scope
204  cpp_idt &id=cpp_scopes.put_into_scope(*s_ptr, *template_scope);
205 
207  id.is_scope=true;
208  id.prefix = template_scope->get_parent().prefix +
209  id2string(s_ptr->base_name) + id2string(suffix) + "::";
210  id.class_identifier=s_ptr->name;
211  id.id_class=cpp_idt::id_classt::CLASS;
212 
213  return *s_ptr;
214 }
215 
218  const typet &type)
219 {
220  if(type.id() != ID_struct_tag)
221  return;
222 
223  const symbolt &symbol = lookup(to_struct_tag_type(type));
224 
225  // Make a copy, as instantiate will destroy the symbol type!
226  const typet t_type=symbol.type;
227 
228  if(t_type.id() == ID_struct && t_type.get_bool(ID_template_class_instance))
229  {
231  type.source_location(),
232  lookup(t_type.get(ID_identifier)),
233  static_cast<const cpp_template_args_tct &>(
234  t_type.find(ID_specialization_template_args)),
235  static_cast<const cpp_template_args_tct &>(
236  t_type.find(ID_full_template_args)));
237  }
238 }
239 
244 #define MAX_DEPTH 50
245 
247  const source_locationt &source_location,
248  const symbolt &template_symbol,
249  const cpp_template_args_tct &specialization_template_args,
250  const cpp_template_args_tct &full_template_args,
251  const typet &specialization)
252 {
253 #ifdef DEBUG
254  std::cout << "instantiate_template: " << template_symbol.name << '\n';
255 #endif
256 
257  if(instantiation_stack.size()==MAX_DEPTH)
258  {
259  error().source_location=source_location;
260  error() << "reached maximum template recursion depth ("
261  << MAX_DEPTH << ")" << eom;
262  throw 0;
263  }
264 
266  instantiation_stack.back().source_location=source_location;
267  instantiation_stack.back().identifier=template_symbol.name;
268  instantiation_stack.back().full_template_args=full_template_args;
269 
270 #ifdef DEBUG
271  std::cout << "L: " << source_location << '\n';
272  std::cout << "I: " << template_symbol.name << '\n';
273 #endif
274 
276 
277  bool specialization_given=specialization.is_not_nil();
278 
279  // we should never get 'unassigned' here
281  !specialization_template_args.has_unassigned(),
282  "should never get 'unassigned' here");
284  !full_template_args.has_unassigned(), "should never get 'unassigned' here");
285 
286 #ifdef DEBUG
287  std::cout << "A: <";
288  forall_expr(it, specialization_template_args.arguments())
289  {
290  if(it!=specialization_template_args.arguments().begin())
291  std::cout << ", ";
292  if(it->id()==ID_type)
293  std::cout << to_string(it->type());
294  else
295  std::cout << to_string(*it);
296  }
297  std::cout << ">\n\n";
298 #endif
299 
300  // do we have arguments?
301  if(full_template_args.arguments().empty())
302  {
303  error().source_location=source_location;
304  error() << "'" << template_symbol.base_name
305  << "' is a template; thus, expected template arguments" << eom;
306  throw 0;
307  }
308 
309  // produce new symbol name
310  std::string suffix=template_suffix(full_template_args);
311 
312  // we need the template scope to see the template parameters
313  cpp_scopet *template_scope=
314  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
315 
316  if(template_scope==nullptr)
317  {
318  error().source_location=source_location;
319  error() << "identifier: " << template_symbol.name << '\n'
320  << "template instantiation error: scope not found" << eom;
321  throw 0;
322  }
323 
324  // produce new declaration
325  cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);
326 
327  // The new one is not a template any longer, but we remember the
328  // template type that was used.
329  template_typet template_type=new_decl.template_type();
330  new_decl.remove(ID_is_template);
331  new_decl.remove(ID_template_type);
332  new_decl.set(ID_C_template, template_symbol.name);
333  new_decl.set(ID_C_template_arguments, specialization_template_args);
334 
335  // save old scope
336  cpp_save_scopet saved_scope(cpp_scopes);
337 
338  // mapping from template parameters to values/types
339  template_map.build(template_type, specialization_template_args);
340 
341  // enter the template scope
342  cpp_scopes.go_to(*template_scope);
343 
344  // Is it a template method?
345  // It's in the scope of a class, and not a class itself.
346  bool is_template_method=
348  new_decl.type().id()!=ID_struct;
349 
350  irep_idt class_name;
351 
352  if(is_template_method)
354 
355  // sub-scope for fixing the prefix
356  cpp_scopet &sub_scope = sub_scope_for_instantiation(*template_scope, suffix);
357 
358  // let's see if we have the instance already
359  {
360  cpp_scopet::id_sett id_set =
361  sub_scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY);
362 
363  if(id_set.size()==1)
364  {
365  // It has already been instantiated!
366  const cpp_idt &cpp_id = **id_set.begin();
367 
371  "id must be class or symbol");
372 
373  const symbolt &symb=lookup(cpp_id.identifier);
374 
375  // continue if the type is incomplete only
376  if(cpp_id.id_class==cpp_idt::id_classt::CLASS &&
377  symb.type.id()==ID_struct)
378  return symb;
379  else if(symb.value.is_not_nil())
380  return symb;
381  }
382 
383  cpp_scopes.go_to(sub_scope);
384  }
385 
386  // store the information that the template has
387  // been instantiated using these arguments
388  {
389  // need non-const handle on template symbol
390  symbolt &s = symbol_table.get_writeable_ref(template_symbol.name);
391  irept &instantiated_with = s.value.add(ID_instantiated_with);
392  instantiated_with.get_sub().push_back(specialization_template_args);
393  }
394 
395  #ifdef DEBUG
396  std::cout << "CLASS MAP:\n";
397  template_map.print(std::cout);
398  #endif
399 
400  // fix the type
401  {
402  typet declaration_type=new_decl.type();
403 
404  // specialization?
405  if(specialization_given)
406  {
407  if(declaration_type.id()==ID_struct)
408  {
409  declaration_type=specialization;
410  declaration_type.add_source_location()=source_location;
411  }
412  else
413  {
414  irept tmp=specialization;
415  new_decl.declarators()[0].swap(tmp);
416  }
417  }
418 
419  template_map.apply(declaration_type);
420  new_decl.type().swap(declaration_type);
421  }
422 
423  if(new_decl.type().id()==ID_struct)
424  {
425  // a class template
427 
428  // also instantiate all the template methods
429  const exprt &template_methods = static_cast<const exprt &>(
430  template_symbol.value.find(ID_template_methods));
431 
432  for(auto &tm : template_methods.operands())
433  {
434  saved_scope.restore();
435 
436  cpp_declarationt method_decl=
437  static_cast<const cpp_declarationt &>(
438  static_cast<const irept &>(tm));
439 
440  // copy the type of the template method
441  template_typet method_type=
442  method_decl.template_type();
443 
444  // do template parameters
445  // this also sets up the template scope of the method
446  cpp_scopet &method_scope=
447  typecheck_template_parameters(method_type);
448 
449  cpp_scopes.go_to(method_scope);
450 
451  // mapping from template arguments to values/types
452  template_map.build(method_type, specialization_template_args);
453 #ifdef DEBUG
454  std::cout << "METHOD MAP:\n";
455  template_map.print(std::cout);
456 #endif
457 
458  method_decl.remove(ID_template_type);
459  method_decl.remove(ID_is_template);
460 
461  convert(method_decl);
462  }
463 
464  const irep_idt& new_symb_id = new_decl.type().get(ID_identifier);
465  symbolt &new_symb = symbol_table.get_writeable_ref(new_symb_id);
466 
467  // add template arguments to type in order to retrieve template map when
468  // typechecking function body
469  new_symb.type.set(ID_C_template, template_type);
470  new_symb.type.set(ID_C_template_arguments, specialization_template_args);
471 
472 #ifdef DEBUG
473  std::cout << "instance symbol: " << new_symb.name << "\n\n";
474  std::cout << "template type: " << template_type.pretty() << "\n\n";
475 #endif
476 
477  return new_symb;
478  }
479 
480  if(is_template_method)
481  {
482  symbolt &symb = symbol_table.get_writeable_ref(class_name);
483 
484  PRECONDITION(new_decl.declarators().size() == 1);
485 
486  if(new_decl.member_spec().is_virtual())
487  {
489  error() << "invalid use of `virtual' in template declaration"
490  << eom;
491  throw 0;
492  }
493 
494  if(new_decl.is_typedef())
495  {
497  error() << "template declaration for typedef" << eom;
498  throw 0;
499  }
500 
501  if(new_decl.storage_spec().is_extern() ||
502  new_decl.storage_spec().is_auto() ||
503  new_decl.storage_spec().is_register() ||
504  new_decl.storage_spec().is_mutable())
505  {
507  error() << "invalid storage class specified for template field"
508  << eom;
509  throw 0;
510  }
511 
512  bool is_static=new_decl.storage_spec().is_static();
513  irep_idt access = new_decl.get(ID_C_access);
514 
515  CHECK_RETURN(!access.empty());
516  PRECONDITION(symb.type.id() == ID_struct);
517 
519  symb,
520  new_decl,
521  new_decl.declarators()[0],
523  access,
524  is_static,
525  false,
526  false);
527 
528  return lookup(to_struct_type(symb.type).components().back().get_name());
529  }
530 
531  // not a class template, not a class template method,
532  // it must be a function template!
533 
534  PRECONDITION(new_decl.declarators().size() == 1);
535 
537 
538  const symbolt &symb=
539  lookup(new_decl.declarators()[0].get(ID_identifier));
540 
541  return symb;
542 }
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
Generic exception types primarily designed for use with invariants.
symbol_table_baset & symbol_table
virtual void make_constant(exprt &expr)
const declaratorst & declarators() const
const cpp_storage_spect & storage_spec() const
const cpp_member_spect & member_spec() const
template_typet & template_type()
bool is_typedef() const
Definition: cpp_id.h:23
irep_idt identifier
Definition: cpp_id.h:72
std::string prefix
Definition: cpp_id.h:79
id_classt id_class
Definition: cpp_id.h:45
bool is_template_scope() const
Definition: cpp_id.h:67
bool is_class() const
Definition: cpp_id.h:47
std::string suffix
Definition: cpp_id.h:79
bool is_virtual() const
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
id_mapt id_map
Definition: cpp_scopes.h:68
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:190
cpp_scopet & get_parent() const
Definition: cpp_scope.h:88
@ SCOPE_ONLY
Definition: cpp_scope.h:30
void add_using_scope(cpp_scopet &other)
Definition: cpp_scope.h:109
std::set< cpp_idt * > id_sett
Definition: cpp_scope.h:28
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition: cpp_scope.h:32
bool is_register() const
bool is_static() const
bool is_auto() const
bool is_mutable() const
bool is_extern() const
exprt::operandst argumentst
std::string template_suffix(const cpp_template_args_tct &template_args)
instantiation_stackt instantiation_stack
template_mapt template_map
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
void convert_non_template_declaration(cpp_declarationt &declaration)
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void show_instantiation_stack(std::ostream &)
void convert(cpp_linkage_spect &)
cpp_scopet & sub_scope_for_instantiation(cpp_scopet &template_scope, const std::string &suffix)
Set up a scope as subscope of the template scope.
void elaborate_class_template(const typet &type)
elaborate class template instances
cpp_scopet & typecheck_template_parameters(template_typet &type)
std::string to_string(const typet &) override
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
const source_locationt & source_location() const
Definition: expr.h:231
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:448
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void remove(const irep_idt &name)
Definition: irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
irept & add(const irep_idt &name)
Definition: irep.cpp:103
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
mstreamt & result() const
Definition: message.h:401
static eomt eom
Definition: message.h:289
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:191
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void print(std::ostream &out) const
void apply(exprt &dest) const
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:139
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
source_locationt & add_source_location()
Definition: type.h:77
cpp_declarationt & to_cpp_declaration(irept &irep)
#define MAX_DEPTH
std::string cpp_type2name(const typet &type)
C++ Language Module.
C++ Language Type Checking.
#define forall_expr(it, expr)
Definition: expr.h:32
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
BigInt mp_integer
Definition: smt_terms.h:17
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
Author: Diffblue Ltd.