cprover
Loading...
Searching...
No Matches
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 <ostream>
15
16#include <util/invariant.h>
17#include <util/std_expr.h>
18
20#include "cpp_template_type.h"
21
22void template_mapt::apply(typet &type) const
23{
24 if(type.id()==ID_array)
25 {
26 apply(to_array_type(type).element_type());
27 apply(to_array_type(type).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 =
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
72void 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 =
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
92exprt 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
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
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
135void 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}
exprt::operandst argumentst
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
source_locationt & add_source_location()
Definition: expr.h:235
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
subt & get_sub()
Definition: irep.h:456
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
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
Definition: template_map.h:32
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
Definition: template_map.h:31
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 typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
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:25
const irept & get_nil_irep()
Definition: irep.cpp:20
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
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:221