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