cprover
base_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Base Type Computation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "base_type.h"
13
14#include <set>
15
16#include "namespace.h"
17#include "pointer_expr.h"
18#include "symbol.h"
19#include "union_find.h"
20
22{
23public:
24 explicit base_type_eqt(const namespacet &_ns):ns(_ns)
25 {
26 }
27
28 bool base_type_eq(const typet &type1, const typet &type2)
29 {
31 return base_type_eq_rec(type1, type2);
32 }
33
34 bool base_type_eq(const exprt &expr1, const exprt &expr2)
35 {
37 return base_type_eq_rec(expr1, expr2);
38 }
39
40 virtual ~base_type_eqt() { }
41
42protected:
43 const namespacet &ns;
44
45 virtual bool base_type_eq_rec(const typet &type1, const typet &type2);
46 virtual bool base_type_eq_rec(const exprt &expr1, const exprt &expr2);
47
48 // for loop avoidance
51};
52
54 typet &type, const namespacet &ns, std::set<irep_idt> &symb)
55{
56 if(
57 type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
58 type.id() == ID_union_tag)
59 {
60 const symbolt *symbol;
61
62 if(
63 !ns.lookup(to_tag_type(type).get_identifier(), symbol) &&
64 symbol->is_type && !symbol->type.is_nil())
65 {
66 type=symbol->type;
67 base_type_rec(type, ns, symb); // recursive call
68 return;
69 }
70 }
71 else if(type.id()==ID_array)
72 {
73 base_type_rec(to_array_type(type).element_type(), ns, symb);
74 }
75 else if(type.id()==ID_struct ||
76 type.id()==ID_union)
77 {
80
81 for(auto &component : components)
82 base_type_rec(component.type(), ns, symb);
83 }
84 else if(type.id()==ID_pointer)
85 {
87
88 // we need to avoid running into an infinite loop
89 if(
90 base_type.id() == ID_c_enum_tag || base_type.id() == ID_struct_tag ||
91 base_type.id() == ID_union_tag)
92 {
94
95 if(symb.find(id)!=symb.end())
96 return;
97
98 symb.insert(id);
99
100 base_type_rec(base_type, ns, symb);
101
102 symb.erase(id);
103 }
104 else
105 base_type_rec(base_type, ns, symb);
106 }
107}
108
109void base_type(typet &type, const namespacet &ns)
110{
111 std::set<irep_idt> symb;
112 base_type_rec(type, ns, symb);
113}
114
115void base_type(exprt &expr, const namespacet &ns)
116{
117 base_type(expr.type(), ns);
118
119 Forall_operands(it, expr)
120 base_type(*it, ns);
121}
122
124 const typet &type1,
125 const typet &type2)
126{
127 if(type1==type2)
128 return true;
129
130 #if 0
131 std::cout << "T1: " << type1.pretty() << '\n';
132 std::cout << "T2: " << type2.pretty() << '\n';
133 #endif
134
135 // loop avoidance
136 if(
137 (type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
138 type1.id() == ID_union_tag) &&
139 type2.id() == type1.id())
140 {
141 // already in same set?
143 type1.get(ID_identifier),
144 type2.get(ID_identifier)))
145 return true;
146 }
147
148 if(
149 type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
150 type1.id() == ID_union_tag)
151 {
152 const symbolt &symbol=
153 ns.lookup(type1.get(ID_identifier));
154
155 if(!symbol.is_type)
156 return false;
157
158 return base_type_eq_rec(symbol.type, type2);
159 }
160
161 if(
162 type2.id() == ID_c_enum_tag || type2.id() == ID_struct_tag ||
163 type2.id() == ID_union_tag)
164 {
165 const symbolt &symbol=
166 ns.lookup(type2.get(ID_identifier));
167
168 if(!symbol.is_type)
169 return false;
170
171 return base_type_eq_rec(type1, symbol.type);
172 }
173
174 if(type1.id()!=type2.id())
175 return false;
176
177 if(type1.id()==ID_struct ||
178 type1.id()==ID_union)
179 {
180 const struct_union_typet::componentst &components1=
182
183 const struct_union_typet::componentst &components2=
185
186 if(components1.size()!=components2.size())
187 return false;
188
189 for(std::size_t i=0; i<components1.size(); i++)
190 {
191 const typet &subtype1=components1[i].type();
192 const typet &subtype2=components2[i].type();
193 if(!base_type_eq_rec(subtype1, subtype2))
194 return false;
195 if(components1[i].get_name()!=components2[i].get_name())
196 return false;
197 }
198
199 return true;
200 }
201 else if(type1.id()==ID_code)
202 {
203 const code_typet::parameterst &parameters1=
204 to_code_type(type1).parameters();
205
206 const code_typet::parameterst &parameters2=
207 to_code_type(type2).parameters();
208
209 if(parameters1.size()!=parameters2.size())
210 return false;
211
212 for(std::size_t i=0; i<parameters1.size(); i++)
213 {
214 const typet &subtype1=parameters1[i].type();
215 const typet &subtype2=parameters2[i].type();
216 if(!base_type_eq_rec(subtype1, subtype2))
217 return false;
218 }
219
220 const typet &return_type1=to_code_type(type1).return_type();
221 const typet &return_type2=to_code_type(type2).return_type();
222
223 if(!base_type_eq_rec(return_type1, return_type2))
224 return false;
225
226 return true;
227 }
228 else if(type1.id()==ID_pointer)
229 {
230 return base_type_eq_rec(
232 }
233 else if(type1.id()==ID_array)
234 {
236 to_array_type(type1).element_type(),
237 to_array_type(type2).element_type()))
238 return false;
239
240 if(to_array_type(type1).size()!=to_array_type(type2).size())
241 return false;
242
243 return true;
244 }
245
246 // the below will go away
247 typet tmp1(type1), tmp2(type2);
248
249 base_type(tmp1, ns);
250 base_type(tmp2, ns);
251
252 return tmp1==tmp2;
253}
254
256 const exprt &expr1,
257 const exprt &expr2)
258{
259 if(expr1.id()!=expr2.id())
260 return false;
261
262 if(!base_type_eq(expr1.type(), expr2.type()))
263 return false;
264
265 const exprt::operandst &expr1_op=expr1.operands();
266 const exprt::operandst &expr2_op=expr2.operands();
267 if(expr1_op.size()!=expr2_op.size())
268 return false;
269
270 for(exprt::operandst::const_iterator
271 it1=expr1_op.begin(), it2=expr2_op.begin();
272 it1!=expr1_op.end() && it2!=expr2_op.end();
273 ++it1, ++it2)
274 if(!base_type_eq(*it1, *it2))
275 return false;
276
277 if(expr1.id()==ID_constant)
278 if(expr1.get(ID_value)!=expr2.get(ID_value))
279 return false;
280
281 return true;
282}
283
292 const typet &type1,
293 const typet &type2,
294 const namespacet &ns)
295{
297 return base_type_eq.base_type_eq(type1, type2);
298}
299
305 const exprt &expr1,
306 const exprt &expr2,
307 const namespacet &ns)
308{
310 return base_type_eq.base_type_eq(expr1, expr2);
311}
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
void base_type_rec(typet &type, const namespacet &ns, std::set< irep_idt > &symb)
Definition: base_type.cpp:53
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:291
Base Type Computation.
base_type_eqt(const namespacet &_ns)
Definition: base_type.cpp:24
virtual bool base_type_eq_rec(const typet &type1, const typet &type2)
Definition: base_type.cpp:123
bool base_type_eq(const typet &type1, const typet &type2)
Definition: base_type.cpp:28
identifierst identifiers
Definition: base_type.cpp:50
union_find< irep_idt > identifierst
Definition: base_type.cpp:49
const namespacet & ns
Definition: base_type.cpp:43
virtual ~base_type_eqt()
Definition: base_type.cpp:40
bool base_type_eq(const exprt &expr1, const exprt &expr2)
Definition: base_type.cpp:34
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
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
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Symbol table entry.
Definition: symbol.h:28
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
const irep_idt & get_identifier() const
Definition: std_types.h:410
The type of an expression, extends irept.
Definition: type.h:29
bool make_union(const T &a, const T &b)
Definition: union_find.h:155
void clear()
Definition: union_find.h:247
#define Forall_operands(it, expr)
Definition: expr.h:25
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
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
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
Symbol table entry.