cprover
base_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Base Type Computation
4 
5 Author: 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 "std_types.h"
18 #include "symbol.h"
19 #include "union_find.h"
20 
22 {
23 public:
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 
42 protected:
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(type.id() == ID_symbol_type)
57  {
58  const symbolt *symbol;
59 
60  if(
61  !ns.lookup(to_symbol_type(type).get_identifier(), symbol) &&
62  symbol->is_type && !symbol->type.is_nil())
63  {
64  type = symbol->type;
65  base_type_rec(type, ns, symb); // recursive call
66  return;
67  }
68  }
69  else if(
70  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
71  type.id() == ID_union_tag)
72  {
73  const symbolt *symbol;
74 
75  if(
76  !ns.lookup(to_tag_type(type).get_identifier(), symbol) &&
77  symbol->is_type && !symbol->type.is_nil())
78  {
79  type=symbol->type;
80  base_type_rec(type, ns, symb); // recursive call
81  return;
82  }
83  }
84  else if(type.id()==ID_array)
85  {
86  base_type_rec(to_array_type(type).subtype(), ns, symb);
87  }
88  else if(type.id()==ID_struct ||
89  type.id()==ID_union)
90  {
93 
94  for(auto &component : components)
95  base_type_rec(component.type(), ns, symb);
96  }
97  else if(type.id()==ID_pointer)
98  {
99  typet &subtype=to_pointer_type(type).subtype();
100 
101  // we need to avoid running into an infinite loop
102  if(subtype.id() == ID_symbol_type)
103  {
104  const irep_idt &id = to_symbol_type(subtype).get_identifier();
105 
106  if(symb.find(id) != symb.end())
107  return;
108 
109  symb.insert(id);
110 
111  base_type_rec(subtype, ns, symb);
112 
113  symb.erase(id);
114  }
115  else if(
116  subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
117  subtype.id() == ID_union_tag)
118  {
119  const irep_idt &id = to_tag_type(subtype).get_identifier();
120 
121  if(symb.find(id)!=symb.end())
122  return;
123 
124  symb.insert(id);
125 
126  base_type_rec(subtype, ns, symb);
127 
128  symb.erase(id);
129  }
130  else
131  base_type_rec(subtype, ns, symb);
132  }
133 }
134 
135 void base_type(typet &type, const namespacet &ns)
136 {
137  std::set<irep_idt> symb;
138  base_type_rec(type, ns, symb);
139 }
140 
141 void base_type(exprt &expr, const namespacet &ns)
142 {
143  base_type(expr.type(), ns);
144 
145  Forall_operands(it, expr)
146  base_type(*it, ns);
147 }
148 
150  const typet &type1,
151  const typet &type2)
152 {
153  if(type1==type2)
154  return true;
155 
156  #if 0
157  std::cout << "T1: " << type1.pretty() << '\n';
158  std::cout << "T2: " << type2.pretty() << '\n';
159  #endif
160 
161  // loop avoidance
162  if(
163  (type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
164  type1.id() == ID_struct_tag || type1.id() == ID_union_tag) &&
165  type2.id() == type1.id())
166  {
167  // already in same set?
169  type1.get(ID_identifier),
170  type2.get(ID_identifier)))
171  return true;
172  }
173 
174  if(
175  type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
176  type1.id() == ID_struct_tag || type1.id() == ID_union_tag)
177  {
178  const symbolt &symbol=
179  ns.lookup(type1.get(ID_identifier));
180 
181  if(!symbol.is_type)
182  return false;
183 
184  return base_type_eq_rec(symbol.type, type2);
185  }
186 
187  if(
188  type2.id() == ID_symbol_type || type2.id() == ID_c_enum_tag ||
189  type2.id() == ID_struct_tag || type2.id() == ID_union_tag)
190  {
191  const symbolt &symbol=
192  ns.lookup(type2.get(ID_identifier));
193 
194  if(!symbol.is_type)
195  return false;
196 
197  return base_type_eq_rec(type1, symbol.type);
198  }
199 
200  if(type1.id()!=type2.id())
201  return false;
202 
203  if(type1.id()==ID_struct ||
204  type1.id()==ID_union)
205  {
206  const struct_union_typet::componentst &components1=
208 
209  const struct_union_typet::componentst &components2=
211 
212  if(components1.size()!=components2.size())
213  return false;
214 
215  for(std::size_t i=0; i<components1.size(); i++)
216  {
217  const typet &subtype1=components1[i].type();
218  const typet &subtype2=components2[i].type();
219  if(!base_type_eq_rec(subtype1, subtype2))
220  return false;
221  if(components1[i].get_name()!=components2[i].get_name())
222  return false;
223  }
224 
225  return true;
226  }
227  else if(type1.id()==ID_incomplete_struct)
228  {
229  return true;
230  }
231  else if(type1.id()==ID_incomplete_union)
232  {
233  return true;
234  }
235  else if(type1.id()==ID_code)
236  {
237  const code_typet::parameterst &parameters1=
238  to_code_type(type1).parameters();
239 
240  const code_typet::parameterst &parameters2=
241  to_code_type(type2).parameters();
242 
243  if(parameters1.size()!=parameters2.size())
244  return false;
245 
246  for(std::size_t i=0; i<parameters1.size(); i++)
247  {
248  const typet &subtype1=parameters1[i].type();
249  const typet &subtype2=parameters2[i].type();
250  if(!base_type_eq_rec(subtype1, subtype2))
251  return false;
252  }
253 
254  const typet &return_type1=to_code_type(type1).return_type();
255  const typet &return_type2=to_code_type(type2).return_type();
256 
257  if(!base_type_eq_rec(return_type1, return_type2))
258  return false;
259 
260  return true;
261  }
262  else if(type1.id()==ID_pointer)
263  {
264  return base_type_eq_rec(
265  to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype());
266  }
267  else if(type1.id()==ID_array)
268  {
269  if(!base_type_eq_rec(
270  to_array_type(type1).subtype(), to_array_type(type2).subtype()))
271  return false;
272 
273  if(to_array_type(type1).size()!=to_array_type(type2).size())
274  return false;
275 
276  return true;
277  }
278  else if(type1.id()==ID_incomplete_array)
279  {
280  return base_type_eq_rec(
281  to_incomplete_array_type(type1).subtype(),
282  to_incomplete_array_type(type2).subtype());
283  }
284 
285  // the below will go away
286  typet tmp1(type1), tmp2(type2);
287 
288  base_type(tmp1, ns);
289  base_type(tmp2, ns);
290 
291  return tmp1==tmp2;
292 }
293 
295  const exprt &expr1,
296  const exprt &expr2)
297 {
298  if(expr1.id()!=expr2.id())
299  return false;
300 
301  if(!base_type_eq(expr1.type(), expr2.type()))
302  return false;
303 
304  const exprt::operandst &expr1_op=expr1.operands();
305  const exprt::operandst &expr2_op=expr2.operands();
306  if(expr1_op.size()!=expr2_op.size())
307  return false;
308 
309  for(exprt::operandst::const_iterator
310  it1=expr1_op.begin(), it2=expr2_op.begin();
311  it1!=expr1_op.end() && it2!=expr2_op.end();
312  ++it1, ++it2)
313  if(!base_type_eq(*it1, *it2))
314  return false;
315 
316  if(expr1.id()==ID_constant)
317  if(expr1.get(ID_value)!=expr2.get(ID_value))
318  return false;
319 
320  return true;
321 }
322 
333  const typet &type1,
334  const typet &type2,
335  const namespacet &ns)
336 {
338  return base_type_eq.base_type_eq(type1, type2);
339 }
340 
346  const exprt &expr1,
347  const exprt &expr2,
348  const namespacet &ns)
349 {
351  return base_type_eq.base_type_eq(expr1, expr2);
352 }
The type of an expression, extends irept.
Definition: type.h:27
const namespacet & ns
Definition: base_type.cpp:43
const irep_idt & get_identifier() const
Definition: std_types.h:479
bool is_nil() const
Definition: irep.h:172
Symbol table entry.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
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:332
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:503
std::vector< componentt > componentst
Definition: std_types.h:203
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
std::vector< parametert > parameterst
Definition: std_types.h:754
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
Symbol table entry.
Definition: symbol.h:27
const irep_idt & id() const
Definition: irep.h:259
virtual bool base_type_eq_rec(const typet &type1, const typet &type2)
Definition: base_type.cpp:149
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const exprt & size() const
Definition: std_types.h:1010
void base_type_rec(typet &type, const namespacet &ns, std::set< irep_idt > &symb)
Definition: base_type.cpp:53
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
identifierst identifiers
Definition: base_type.cpp:50
std::vector< exprt > operandst
Definition: expr.h:57
void clear()
Definition: union_find.h:248
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a typet to an incomplete_array_typet.
Definition: std_types.h:1087
base_type_eqt(const namespacet &_ns)
Definition: base_type.cpp:24
typet type
Type of symbol.
Definition: symbol.h:31
Pre-defined types.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
bool base_type_eq(const exprt &expr1, const exprt &expr2)
Definition: base_type.cpp:34
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:135
bool base_type_eq(const typet &type1, const typet &type2)
Definition: base_type.cpp:28
#define Forall_operands(it, expr)
Definition: expr.h:26
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
bool is_type
Definition: symbol.h:61
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
virtual ~base_type_eqt()
Definition: base_type.cpp:40
operandst & operands()
Definition: expr.h:78
union_find< irep_idt > identifierst
Definition: base_type.cpp:49
const typet & return_type() const
Definition: std_types.h:883
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
const irep_idt & get_identifier() const
Definition: std_types.h:75