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