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)
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)
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((type1.id()==ID_symbol ||
163  type1.id()==ID_c_enum_tag ||
164  type1.id()==ID_struct_tag ||
165  type1.id()==ID_union_tag) &&
166  type2.id()==type1.id())
167  {
168  // already in same set?
170  type1.get(ID_identifier),
171  type2.get(ID_identifier)))
172  return true;
173  }
174 
175  if(type1.id()==ID_symbol ||
176  type1.id()==ID_c_enum_tag ||
177  type1.id()==ID_struct_tag ||
178  type1.id()==ID_union_tag)
179  {
180  const symbolt &symbol=
181  ns.lookup(type1.get(ID_identifier));
182 
183  if(!symbol.is_type)
184  return false;
185 
186  return base_type_eq_rec(symbol.type, type2);
187  }
188 
189  if(type2.id()==ID_symbol ||
190  type2.id()==ID_c_enum_tag ||
191  type2.id()==ID_struct_tag ||
192  type2.id()==ID_union_tag)
193  {
194  const symbolt &symbol=
195  ns.lookup(type2.get(ID_identifier));
196 
197  if(!symbol.is_type)
198  return false;
199 
200  return base_type_eq_rec(type1, symbol.type);
201  }
202 
203  if(type1.id()!=type2.id())
204  return false;
205 
206  if(type1.id()==ID_struct ||
207  type1.id()==ID_union)
208  {
209  const struct_union_typet::componentst &components1=
211 
212  const struct_union_typet::componentst &components2=
214 
215  if(components1.size()!=components2.size())
216  return false;
217 
218  for(std::size_t i=0; i<components1.size(); i++)
219  {
220  const typet &subtype1=components1[i].type();
221  const typet &subtype2=components2[i].type();
222  if(!base_type_eq_rec(subtype1, subtype2))
223  return false;
224  if(components1[i].get_name()!=components2[i].get_name())
225  return false;
226  }
227 
228  return true;
229  }
230  else if(type1.id()==ID_incomplete_struct)
231  {
232  return true;
233  }
234  else if(type1.id()==ID_incomplete_union)
235  {
236  return true;
237  }
238  else if(type1.id()==ID_code)
239  {
240  const code_typet::parameterst &parameters1=
241  to_code_type(type1).parameters();
242 
243  const code_typet::parameterst &parameters2=
244  to_code_type(type2).parameters();
245 
246  if(parameters1.size()!=parameters2.size())
247  return false;
248 
249  for(std::size_t i=0; i<parameters1.size(); i++)
250  {
251  const typet &subtype1=parameters1[i].type();
252  const typet &subtype2=parameters2[i].type();
253  if(!base_type_eq_rec(subtype1, subtype2))
254  return false;
255  }
256 
257  const typet &return_type1=to_code_type(type1).return_type();
258  const typet &return_type2=to_code_type(type2).return_type();
259 
260  if(!base_type_eq_rec(return_type1, return_type2))
261  return false;
262 
263  return true;
264  }
265  else if(type1.id()==ID_pointer)
266  {
267  return base_type_eq_rec(
268  to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype());
269  }
270  else if(type1.id()==ID_array)
271  {
272  if(!base_type_eq_rec(
273  to_array_type(type1).subtype(), to_array_type(type2).subtype()))
274  return false;
275 
276  if(to_array_type(type1).size()!=to_array_type(type2).size())
277  return false;
278 
279  return true;
280  }
281  else if(type1.id()==ID_incomplete_array)
282  {
283  return base_type_eq_rec(
284  to_incomplete_array_type(type1).subtype(),
285  to_incomplete_array_type(type2).subtype());
286  }
287 
288  // the below will go away
289  typet tmp1(type1), tmp2(type2);
290 
291  base_type(tmp1, ns);
292  base_type(tmp2, ns);
293 
294  return tmp1==tmp2;
295 }
296 
298  const exprt &expr1,
299  const exprt &expr2)
300 {
301  if(expr1.id()!=expr2.id())
302  return false;
303 
304  if(!base_type_eq(expr1.type(), expr2.type()))
305  return false;
306 
307  const exprt::operandst &expr1_op=expr1.operands();
308  const exprt::operandst &expr2_op=expr2.operands();
309  if(expr1_op.size()!=expr2_op.size())
310  return false;
311 
312  for(exprt::operandst::const_iterator
313  it1=expr1_op.begin(), it2=expr2_op.begin();
314  it1!=expr1_op.end() && it2!=expr2_op.end();
315  ++it1, ++it2)
316  if(!base_type_eq(*it1, *it2))
317  return false;
318 
319  if(expr1.id()==ID_constant)
320  if(expr1.get(ID_value)!=expr2.get(ID_value))
321  return false;
322 
323  return true;
324 }
325 
327  const typet &type1,
328  const typet &type2,
329  const namespacet &ns)
330 {
332  return base_type_eq.base_type_eq(type1, type2);
333 }
334 
336  const exprt &expr1,
337  const exprt &expr2,
338  const namespacet &ns)
339 {
341  return base_type_eq.base_type_eq(expr1, expr2);
342 }
The type of an expression.
Definition: type.h:22
const namespacet & ns
Definition: base_type.cpp:43
const irep_idt & get_identifier() const
Definition: std_types.h:509
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:641
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
const tag_typet & to_tag_type(const typet &type)
Cast a generic typet to a tag_typet.
Definition: std_types.h:525
std::vector< componentt > componentst
Definition: std_types.h:243
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
std::vector< parametert > parameterst
Definition: std_types.h:767
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const exprt & size() const
Definition: std_types.h:1023
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:33
identifierst identifiers
Definition: base_type.cpp:50
std::vector< exprt > operandst
Definition: expr.h:45
void clear()
Definition: union_find.h:244
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a generic typet to an incomplete_array_typet.
Definition: std_types.h:1094
base_type_eqt(const namespacet &_ns)
Definition: base_type.cpp:24
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
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:23
bool make_union(const T &a, const T &b)
Definition: union_find.h:150
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
bool is_type
Definition: symbol.h:63
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
virtual ~base_type_eqt()
Definition: base_type.cpp:40
operandst & operands()
Definition: expr.h:66
union_find< irep_idt > identifierst
Definition: base_type.cpp:49
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
const irep_idt & get_identifier() const
Definition: std_types.h:123