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