CBMC
template_map.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 "template_map.h"
13 
14 #include <util/invariant.h>
15 #include <util/pointer_expr.h>
16 #include <util/std_expr.h>
17 
18 #include "cpp_template_parameter.h"
19 #include "cpp_template_type.h"
20 
21 #include <ostream>
22 
23 void template_mapt::apply(typet &type) const
24 {
25  if(type.id()==ID_array)
26  {
27  apply(to_array_type(type).element_type());
28  apply(to_array_type(type).size());
29  }
30  else if(type.id()==ID_pointer)
31  {
32  apply(to_pointer_type(type).base_type());
33  }
34  else if(type.id()==ID_struct ||
35  type.id()==ID_union)
36  {
37  for(auto &c : to_struct_union_type(type).components())
38  {
39  typet &subtype = c.type();
40  apply(subtype);
41  }
42  }
43  else if(type.id() == ID_template_parameter_symbol_type)
44  {
45  type_mapt::const_iterator m_it =
46  type_map.find(to_template_parameter_symbol_type(type).get_identifier());
47 
48  if(m_it!=type_map.end())
49  {
50  type=m_it->second;
51  return;
52  }
53  }
54  else if(type.id()==ID_code)
55  {
56  apply(to_code_type(type).return_type());
57 
58  irept::subt &parameters=type.add(ID_parameters).get_sub();
59 
60  for(auto &parameter : parameters)
61  {
62  if(parameter.id() == ID_parameter)
63  apply(static_cast<typet &>(parameter.add(ID_type)));
64  }
65  }
66  else if(type.id()==ID_merged_type)
67  {
68  for(typet &subtype : to_type_with_subtypes(type).subtypes())
69  apply(subtype);
70  }
71 }
72 
73 void template_mapt::apply(exprt &expr) const
74 {
75  apply(expr.type());
76 
77  if(expr.id()==ID_symbol)
78  {
79  expr_mapt::const_iterator m_it =
80  expr_map.find(to_symbol_expr(expr).get_identifier());
81 
82  if(m_it!=expr_map.end())
83  {
84  expr=m_it->second;
85  return;
86  }
87  }
88 
89  Forall_operands(it, expr)
90  apply(*it);
91 }
92 
93 exprt template_mapt::lookup(const irep_idt &identifier) const
94 {
95  type_mapt::const_iterator t_it=
96  type_map.find(identifier);
97 
98  if(t_it!=type_map.end())
99  {
100  exprt e(ID_type);
101  e.type()=t_it->second;
102  return e;
103  }
104 
105  expr_mapt::const_iterator e_it=
106  expr_map.find(identifier);
107 
108  if(e_it!=expr_map.end())
109  return e_it->second;
110 
111  return static_cast<const exprt &>(get_nil_irep());
112 }
113 
114 typet template_mapt::lookup_type(const irep_idt &identifier) const
115 {
116  type_mapt::const_iterator t_it=
117  type_map.find(identifier);
118 
119  if(t_it!=type_map.end())
120  return t_it->second;
121 
122  return static_cast<const typet &>(get_nil_irep());
123 }
124 
125 exprt template_mapt::lookup_expr(const irep_idt &identifier) const
126 {
127  expr_mapt::const_iterator e_it=
128  expr_map.find(identifier);
129 
130  if(e_it!=expr_map.end())
131  return e_it->second;
132 
133  return static_cast<const exprt &>(get_nil_irep());
134 }
135 
136 void template_mapt::print(std::ostream &out) const
137 {
138  for(const auto &mapping : type_map)
139  out << mapping.first << " = " << mapping.second.pretty() << '\n';
140 
141  for(const auto &mapping : expr_map)
142  out << mapping.first << " = " << mapping.second.pretty() << '\n';
143 }
144 
146  const template_typet &template_type,
147  const cpp_template_args_tct &template_args)
148 {
149  const template_typet::template_parameterst &template_parameters=
150  template_type.template_parameters();
151 
153  template_args.arguments();
154 
155  template_typet::template_parameterst::const_iterator t_it=
156  template_parameters.begin();
157 
158  if(instance.size()<template_parameters.size())
159  {
160  // check for default parameters
161  for(std::size_t i=instance.size();
162  i<template_parameters.size();
163  i++)
164  {
165  const template_parametert &param=template_parameters[i];
166 
167  if(param.has_default_argument())
168  instance.push_back(param.default_argument());
169  else
170  break;
171  }
172  }
173 
174  // these should have been typechecked before
176  instance.size() == template_parameters.size(),
177  "template instantiation expected to match declaration");
178 
179  for(cpp_template_args_tct::argumentst::const_iterator
180  i_it=instance.begin();
181  i_it!=instance.end();
182  i_it++, t_it++)
183  {
184  set(*t_it, *i_it);
185  }
186 }
187 
189  const template_parametert &parameter,
190  const exprt &value)
191 {
192  if(parameter.id()==ID_type)
193  {
194  if(parameter.id()!=ID_type)
195  UNREACHABLE; // typechecked before!
196 
197  typet tmp=value.type();
198 
199  irep_idt identifier=parameter.type().get(ID_identifier);
200  type_map[identifier]=tmp;
201  }
202  else
203  {
204  // must be non-type
205 
206  if(value.id()==ID_type)
207  UNREACHABLE; // typechecked before!
208 
209  irep_idt identifier=parameter.get(ID_identifier);
210  expr_map[identifier]=value;
211  }
212 }
213 
215  const template_typet &template_type)
216 {
217  for(const auto &t : template_type.template_parameters())
218  {
219  if(t.id()==ID_type)
220  {
221  typet tmp(ID_unassigned);
222  tmp.set(ID_identifier, t.type().get(ID_identifier));
223  tmp.add_source_location()=t.source_location();
224  type_map[t.type().get(ID_identifier)]=tmp;
225  }
226  else
227  {
228  exprt tmp(ID_unassigned, t.type());
229  tmp.set(ID_identifier, t.get(ID_identifier));
230  tmp.add_source_location()=t.source_location();
231  expr_map[t.get(ID_identifier)]=tmp;
232  }
233  }
234 }
235 
237  const template_typet &template_type) const
238 {
239  const template_typet::template_parameterst &template_parameters=
240  template_type.template_parameters();
241 
242  cpp_template_args_tct template_args;
243  template_args.arguments().resize(template_parameters.size());
244 
245  for(std::size_t i=0; i<template_parameters.size(); i++)
246  {
247  const template_parametert &t=template_parameters[i];
248 
249  if(t.id()==ID_type)
250  {
251  template_args.arguments()[i]=
252  exprt(ID_type, lookup_type(t.type().get(ID_identifier)));
253  }
254  else
255  {
256  template_args.arguments()[i]=
257  lookup_expr(t.get(ID_identifier));
258  }
259  }
260 
261  return template_args;
262 }
exprt::operandst argumentst
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
subt & get_sub()
Definition: irep.h:448
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
const irep_idt & id() const
Definition: irep.h:388
irept & add(const irep_idt &name)
Definition: irep.cpp:103
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
exprt lookup(const irep_idt &identifier) const
void build_unassigned(const template_typet &template_type)
void print(std::ostream &out) const
void apply(exprt &dest) const
expr_mapt expr_map
Definition: template_map.h:32
exprt lookup_expr(const irep_idt &identifier) const
void set(const template_parametert &parameter, const exprt &value)
typet lookup_type(const irep_idt &identifier) const
type_mapt type_map
Definition: template_map.h:31
cpp_template_args_tct build_template_args(const template_typet &template_type) const
template_parameterst & template_parameters()
std::vector< template_parametert > template_parameterst
The type of an expression, extends irept.
Definition: type.h:29
source_locationt & add_source_location()
Definition: type.h:77
const template_parameter_symbol_typet & to_template_parameter_symbol_type(const typet &type)
Cast a typet to a template_parameter_symbol_typet.
#define Forall_operands(it, expr)
Definition: expr.h:27
const irept & get_nil_irep()
Definition: irep.cpp:19
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
C++ Language Type Checking.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:252