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 
19 #include "cpp_template_parameter.h"
20 #include "cpp_template_type.h"
21 
22 void template_mapt::apply(typet &type) const
23 {
24  if(type.id()==ID_array)
25  {
26  apply(type.subtype());
27  apply(static_cast<exprt &>(type.add(ID_size)));
28  }
29  else if(type.id()==ID_pointer)
30  {
31  apply(type.subtype());
32  }
33  else if(type.id()==ID_struct ||
34  type.id()==ID_union)
35  {
36  for(auto &c : to_struct_union_type(type).components())
37  {
38  typet &subtype = c.type();
39  apply(subtype);
40  }
41  }
42  else if(type.id() == ID_template_parameter_symbol_type)
43  {
44  type_mapt::const_iterator m_it =
45  type_map.find(to_template_parameter_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(to_code_type(type).return_type());
56 
57  irept::subt &parameters=type.add(ID_parameters).get_sub();
58 
59  for(auto &parameter : parameters)
60  {
61  if(parameter.id() == ID_parameter)
62  apply(static_cast<typet &>(parameter.add(ID_type)));
63  }
64  }
65  else if(type.id()==ID_merged_type)
66  {
67  for(typet &subtype : to_type_with_subtypes(type).subtypes())
68  apply(subtype);
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(const auto &mapping : type_map)
138  out << mapping.first << " = " << mapping.second.pretty() << '\n';
139 
140  for(const auto &mapping : expr_map)
141  out << mapping.first << " = " << mapping.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
175  instance.size() == template_parameters.size(),
176  "template instantiation expected to match declaration");
177 
178  for(cpp_template_args_tct::argumentst::const_iterator
179  i_it=instance.begin();
180  i_it!=instance.end();
181  i_it++, t_it++)
182  {
183  set(*t_it, *i_it);
184  }
185 }
186 
188  const template_parametert &parameter,
189  const exprt &value)
190 {
191  if(parameter.id()==ID_type)
192  {
193  if(parameter.id()!=ID_type)
194  UNREACHABLE; // typechecked before!
195 
196  typet tmp=value.type();
197 
198  irep_idt identifier=parameter.type().get(ID_identifier);
199  type_map[identifier]=tmp;
200  }
201  else
202  {
203  // must be non-type
204 
205  if(value.id()==ID_type)
206  UNREACHABLE; // typechecked before!
207 
208  irep_idt identifier=parameter.get(ID_identifier);
209  expr_map[identifier]=value;
210  }
211 }
212 
214  const template_typet &template_type)
215 {
216  for(const auto &t : template_type.template_parameters())
217  {
218  if(t.id()==ID_type)
219  {
220  typet tmp(ID_unassigned);
221  tmp.set(ID_identifier, t.type().get(ID_identifier));
222  tmp.add_source_location()=t.source_location();
223  type_map[t.type().get(ID_identifier)]=tmp;
224  }
225  else
226  {
227  exprt tmp(ID_unassigned, t.type());
228  tmp.set(ID_identifier, t.get(ID_identifier));
229  tmp.add_source_location()=t.source_location();
230  expr_map[t.get(ID_identifier)]=tmp;
231  }
232  }
233 }
234 
236  const template_typet &template_type) const
237 {
238  const template_typet::template_parameterst &template_parameters=
239  template_type.template_parameters();
240 
241  cpp_template_args_tct template_args;
242  template_args.arguments().resize(template_parameters.size());
243 
244  for(std::size_t i=0; i<template_parameters.size(); i++)
245  {
246  const template_parametert &t=template_parameters[i];
247 
248  if(t.id()==ID_type)
249  {
250  template_args.arguments()[i]=
251  exprt(ID_type, lookup_type(t.type().get(ID_identifier)));
252  }
253  else
254  {
255  template_args.arguments()[i]=
256  lookup_expr(t.get(ID_identifier));
257  }
258  }
259 
260  return template_args;
261 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
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:213
template_parametert
Definition: cpp_template_parameter.h:20
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
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:214
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:116
invariant.h
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
exprt
Base class for all expressions.
Definition: expr.h:54
template_mapt::build_template_args
cpp_template_args_tct build_template_args(const template_typet &template_type) const
Definition: template_map.cpp:235
cpp_template_parameter.h
cpp_template_args_tct
Definition: cpp_template_args.h:65
template_map.h
C++ Language Type Checking.
template_mapt::expr_map
expr_mapt expr_map
Definition: template_map.h:32
template_mapt::apply
void apply(exprt &dest) const
Definition: template_map.cpp:72
template_mapt::lookup
exprt lookup(const irep_idt &identifier) const
Definition: template_map.cpp:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
template_mapt::lookup_type
typet lookup_type(const irep_idt &identifier) const
Definition: template_map.cpp:113
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:510
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:135
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
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:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:171
template_mapt::lookup_expr
exprt lookup_expr(const irep_idt &identifier) const
Definition: template_map.cpp:124
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:45
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
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:31
irept::get_sub
subt & get_sub()
Definition: irep.h:467
template_mapt::set
void set(const template_parametert &parameter, const exprt &value)
Definition: template_map.cpp:187
template_typet
Definition: cpp_template_type.h:19
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:20
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:144
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
std_expr.h
API to expression classes.
cpp_template_type.h