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 #include <util/arith_tools.h>
15 #include <util/base_exceptions.h>
16 #include <util/simplify_expr.h>
17 
18 #include <util/c_types.h>
19 
20 #include "cpp_type2name.h"
21 
23  const cpp_template_args_tct &template_args)
24 {
25  // quick hack
26  std::string result="<";
27  bool first=true;
28 
29  const cpp_template_args_tct::argumentst &arguments=
30  template_args.arguments();
31 
32  for(cpp_template_args_tct::argumentst::const_iterator
33  it=arguments.begin();
34  it!=arguments.end();
35  it++)
36  {
37  if(first)
38  first=false;
39  else
40  result+=',';
41 
42  const exprt expr=*it;
43 
44  assert(expr.id()!="ambiguous");
45 
46  if(expr.id()==ID_type)
47  {
48  const typet &type=expr.type();
49  if(type.id()==ID_symbol)
50  result+=type.get_string(ID_identifier);
51  else
52  result+=cpp_type2name(type);
53  }
54  else // expression
55  {
56  exprt e=expr;
57  make_constant(e);
58 
59  // this must be a constant, which includes true/false
60  mp_integer i;
61 
62  if(e.is_true())
63  i=1;
64  else if(e.is_false())
65  i=0;
66  else if(to_integer(e, i))
67  {
68  error().source_location=it->find_source_location();
69  error() << "template argument expression expected to be "
70  << "scalar constant, but got `"
71  << to_string(e) << "'" << eom;
72  throw 0;
73  }
74 
76  }
77  }
78 
79  result+='>';
80 
81  return result;
82 }
83 
85 {
86  for(instantiation_stackt::const_iterator
87  s_it=instantiation_stack.begin();
88  s_it!=instantiation_stack.end();
89  s_it++)
90  {
91  const symbolt &symbol=lookup(s_it->identifier);
92  out << "instantiating `" << symbol.pretty_name << "' with <";
93 
94  forall_expr(a_it, s_it->full_template_args.arguments())
95  {
96  if(a_it!=s_it->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 " << s_it->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  "specialization_template_args", specialization_template_args);
162  new_symbol.type.set("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)
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("specialization_template_args")),
205  static_cast<const cpp_template_args_tct &>(
206  t_type.find("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  if(instantiation_stack.size()==MAX_DEPTH)
224  {
225  error().source_location=source_location;
226  error() << "reached maximum template recursion depth ("
227  << MAX_DEPTH << ")" << eom;
228  throw 0;
229  }
230 
232  instantiation_stack.back().source_location=source_location;
233  instantiation_stack.back().identifier=template_symbol.name;
234  instantiation_stack.back().full_template_args=full_template_args;
235 
236  #if 0
237  std::cout << "L: " << source_location << '\n';
238  std::cout << "I: " << template_symbol.name << '\n';
239  #endif
240 
242 
243  bool specialization_given=specialization.is_not_nil();
244 
245  // we should never get 'unassigned' here
246  assert(!specialization_template_args.has_unassigned());
247  assert(!full_template_args.has_unassigned());
248 
249  #if 0
250  std::cout << "A: <";
251  forall_expr(it, specialization_template_args.arguments())
252  {
253  if(it!=specialization_template_args.arguments().begin())
254  std::cout << ", ";
255  if(it->id()==ID_type)
256  std::cout << to_string(it->type());
257  else
258  std::cout << to_string(*it);
259  }
260  std::cout << ">\n";
261  #endif
262 
263  // do we have arguments?
264  if(full_template_args.arguments().empty())
265  {
266  error().source_location=source_location;
267  error() << "`" << template_symbol.base_name
268  << "' is a template; thus, expected template arguments"
269  << eom;
270  throw 0;
271  }
272 
273  // produce new symbol name
274  std::string suffix=template_suffix(full_template_args);
275 
276  // we need the template scope to see the template parameters
277  cpp_scopet *template_scope=
278  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
279 
280  if(template_scope==nullptr)
281  {
282  error().source_location=source_location;
283  error() << "identifier: " << template_symbol.name << '\n'
284  << "template instantiation error: scope not found" << eom;
285  throw 0;
286  }
287 
288  // produce new declaration
289  cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);
290 
291  // The new one is not a template any longer, but we remember the
292  // template type that was used.
293  template_typet template_type=new_decl.template_type();
294  new_decl.remove(ID_is_template);
295  new_decl.remove(ID_template_type);
296  new_decl.set(ID_C_template, template_symbol.name);
297  new_decl.set(ID_C_template_arguments, specialization_template_args);
298 
299  // save old scope
300  cpp_save_scopet saved_scope(cpp_scopes);
301 
302  // mapping from template parameters to values/types
303  template_map.build(template_type, specialization_template_args);
304 
305  // enter the template scope
306  cpp_scopes.go_to(*template_scope);
307 
308  // Is it a template method?
309  // It's in the scope of a class, and not a class itself.
310  bool is_template_method=
312  new_decl.type().id()!=ID_struct;
313 
314  irep_idt class_name;
315 
316  if(is_template_method)
318 
319  // sub-scope for fixing the prefix
320  std::string subscope_name=id2string(template_scope->identifier)+suffix;
321 
322  // let's see if we have the instance already
323  cpp_scopest::id_mapt::iterator scope_it=
324  cpp_scopes.id_map.find(subscope_name);
325 
326  if(scope_it!=cpp_scopes.id_map.end())
327  {
328  cpp_scopet &scope=cpp_scopes.get_scope(subscope_name);
329 
331  scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY, id_set);
332 
333  if(id_set.size()==1)
334  {
335  // It has already been instantiated!
336  const cpp_idt &cpp_id = **id_set.begin();
337 
338  assert(cpp_id.id_class == cpp_idt::id_classt::CLASS ||
340 
341  const symbolt &symb=lookup(cpp_id.identifier);
342 
343  // continue if the type is incomplete only
344  if(cpp_id.id_class==cpp_idt::id_classt::CLASS &&
345  symb.type.id()==ID_struct)
346  return symb;
347  else if(symb.value.is_not_nil())
348  return symb;
349  }
350 
351  cpp_scopes.go_to(scope);
352  }
353  else
354  {
355  // set up a scope as subscope of the template scope
356  cpp_scopet &sub_scope=
357  cpp_scopes.current_scope().new_scope(subscope_name);
359  sub_scope.prefix=template_scope->get_parent().prefix;
360  sub_scope.suffix=suffix;
361  sub_scope.add_using_scope(template_scope->get_parent());
362  cpp_scopes.go_to(sub_scope);
363  cpp_scopes.id_map.insert(
364  cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
365  }
366 
367  // store the information that the template has
368  // been instantiated using these arguments
369  {
370  // need non-const handle on template symbol
371  symbolt &s=*symbol_table.get_writeable(template_symbol.name);
372  irept &instantiated_with=s.value.add("instantiated_with");
373  instantiated_with.get_sub().push_back(specialization_template_args);
374  }
375 
376  #if 0
377  std::cout << "MAP:\n";
378  template_map.print(std::cout);
379  #endif
380 
381  // fix the type
382  {
383  typet declaration_type=new_decl.type();
384 
385  // specialization?
386  if(specialization_given)
387  {
388  if(declaration_type.id()==ID_struct)
389  {
390  declaration_type=specialization;
391  declaration_type.add_source_location()=source_location;
392  }
393  else
394  {
395  irept tmp=specialization;
396  new_decl.declarators()[0].swap(tmp);
397  }
398  }
399 
400  template_map.apply(declaration_type);
401  new_decl.type().swap(declaration_type);
402  }
403 
404  if(new_decl.type().id()==ID_struct)
405  {
406  // a class template
408 
409  // also instantiate all the template methods
410  const exprt &template_methods=
411  static_cast<const exprt &>(
412  template_symbol.value.find("template_methods"));
413 
414  for(auto &tm : template_methods.operands())
415  {
416  saved_scope.restore();
417 
418  cpp_declarationt method_decl=
419  static_cast<const cpp_declarationt &>(
420  static_cast<const irept &>(tm));
421 
422  // copy the type of the template method
423  template_typet method_type=
424  method_decl.template_type();
425 
426  // do template parameters
427  // this also sets up the template scope of the method
428  cpp_scopet &method_scope=
429  typecheck_template_parameters(method_type);
430 
431  cpp_scopes.go_to(method_scope);
432 
433  // mapping from template arguments to values/types
434  template_map.build(method_type, specialization_template_args);
435 
436  method_decl.remove(ID_template_type);
437  method_decl.remove(ID_is_template);
438 
439  convert(method_decl);
440  }
441 
442  const symbolt &new_symb = lookup(new_decl.type().get(ID_identifier));
443 
444  return new_symb;
445  }
446 
447  if(is_template_method)
448  {
449  symbolt &symb=*symbol_table.get_writeable(class_name);
450 
451  assert(new_decl.declarators().size() == 1);
452 
453  if(new_decl.member_spec().is_virtual())
454  {
456  error() << "invalid use of `virtual' in template declaration"
457  << eom;
458  throw 0;
459  }
460 
461  if(new_decl.is_typedef())
462  {
464  error() << "template declaration for typedef" << eom;
465  throw 0;
466  }
467 
468  if(new_decl.storage_spec().is_extern() ||
469  new_decl.storage_spec().is_auto() ||
470  new_decl.storage_spec().is_register() ||
471  new_decl.storage_spec().is_mutable())
472  {
474  error() << "invalid storage class specified for template field"
475  << eom;
476  throw 0;
477  }
478 
479  bool is_static=new_decl.storage_spec().is_static();
480  irep_idt access = new_decl.get(ID_C_access);
481 
482  assert(!access.empty());
483  assert(symb.type.id()==ID_struct);
484 
486  symb,
487  new_decl,
488  new_decl.declarators()[0],
490  access,
491  is_static,
492  false,
493  false);
494 
495  return lookup(to_struct_type(symb.type).components().back().get(ID_name));
496  }
497 
498  // not a class template, not a class template method,
499  // it must be a function template!
500 
501  assert(new_decl.declarators().size()==1);
502 
504 
505  const symbolt &symb=
506  lookup(new_decl.declarators()[0].get(ID_identifier));
507 
508  return symb;
509 }
bool is_typedef() const
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:213
void apply(exprt &dest) const
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
bool is_mutable() const
const cpp_storage_spect & storage_spec() const
void lookup(const irep_idt &base_name, lookup_kindt kind, id_sett &id_set)
Definition: cpp_scope.cpp:29
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
void convert_non_template_declaration(cpp_declarationt &declaration)
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
Definition: symbol.h:52
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:200
#define forall_expr(it, expr)
Definition: expr.h:28
bool is_auto() const
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
bool is_false() const
Definition: expr.cpp:131
cpp_scopet & get_parent() const
Definition: cpp_scope.h:89
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
void show_instantiation_stack(std::ostream &)
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
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
Definition: expr.cpp:124
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
bool is_register() const
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
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:245
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:87
std::string prefix
Definition: cpp_id.h:80
const irep_idt & id() const
Definition: irep.h:189
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:214
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:213
mstreamt & error() const
Definition: message.h:302
bool is_static() const
std::string cpp_type2name(const typet &type)
Base class for tree-like data structures with sharing.
Definition: irep.h:86
C++ Language Type Checking.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
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:97
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
cpp_declarationt & to_cpp_declaration(irept &irep)
mstreamt & result() const
Definition: message.h:312
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:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
source_locationt & add_source_location()
Definition: type.h:102
const source_locationt & source_location() const
Definition: expr.h:125
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual std::string to_string(const typet &type)
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
void swap(irept &irep)
Definition: irep.h:231
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:17
Definition: cpp_id.h:28
void remove(const irep_namet &name)
Definition: irep.cpp:270
operandst & operands()
Definition: expr.h:66
template_typet & template_type()
#define MAX_DEPTH
Generic exception types primarily designed for use with invariants.
bool empty() const
Definition: dstring.h:61
std::set< cpp_idt * > id_sett
Definition: cpp_scope.h:28
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void add_using_scope(cpp_scopet &other)
Definition: cpp_scope.h:110
bool is_virtual() const
void print(std::ostream &out) const
cpp_scopest cpp_scopes