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