CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
template_map.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: 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
19#include "cpp_template_type.h"
20
21#include <ostream>
22
23void 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
73void 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
93exprt 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
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
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
136void 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,
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
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 {
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
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]=
253 }
254 else
255 {
256 template_args.arguments()[i]=
258 }
259 }
260
261 return template_args;
262}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
typet & type()
Return the type of the expression.
Definition expr.h:84
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
subt & get_sub()
Definition irep.h:448
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
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
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
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.
#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