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 <cassert>
15 #include <set>
16 
17 #include "std_types.h"
18 #include "namespace.h"
19 #include "symbol.h"
20 
22  typet &type, const namespacet &ns, std::set<irep_idt> &symb)
23 {
24  if(type.id()==ID_symbol ||
25  type.id()==ID_c_enum_tag ||
26  type.id()==ID_struct_tag ||
27  type.id()==ID_union_tag)
28  {
29  const symbolt *symbol;
30 
31  if(!ns.lookup(type.get(ID_identifier), symbol) &&
32  symbol->is_type &&
33  !symbol->type.is_nil())
34  {
35  type=symbol->type;
36  base_type_rec(type, ns, symb); // recursive call
37  return;
38  }
39  }
40  else if(type.id()==ID_array)
41  {
42  base_type_rec(to_array_type(type).subtype(), ns, symb);
43  }
44  else if(type.id()==ID_struct ||
45  type.id()==ID_union)
46  {
49 
50  for(auto &component : components)
51  base_type_rec(component.type(), ns, symb);
52  }
53  else if(type.id()==ID_pointer)
54  {
55  typet &subtype=to_pointer_type(type).subtype();
56 
57  // we need to avoid running into an infinite loop
58  if(subtype.id()==ID_symbol ||
59  subtype.id()==ID_c_enum_tag ||
60  subtype.id()==ID_struct_tag ||
61  subtype.id()==ID_union_tag)
62  {
63  const irep_idt &id=subtype.get(ID_identifier);
64 
65  if(symb.find(id)!=symb.end())
66  return;
67 
68  symb.insert(id);
69 
70  base_type_rec(subtype, ns, symb);
71 
72  symb.erase(id);
73  }
74  else
75  base_type_rec(subtype, ns, symb);
76  }
77 }
78 
79 void base_type(typet &type, const namespacet &ns)
80 {
81  std::set<irep_idt> symb;
82  base_type_rec(type, ns, symb);
83 }
84 
85 void base_type(exprt &expr, const namespacet &ns)
86 {
87  base_type(expr.type(), ns);
88 
89  Forall_operands(it, expr)
90  base_type(*it, ns);
91 }
92 
94  const typet &type1,
95  const typet &type2)
96 {
97  if(type1==type2)
98  return true;
99 
100  #if 0
101  std::cout << "T1: " << type1.pretty() << '\n';
102  std::cout << "T2: " << type2.pretty() << '\n';
103  #endif
104 
105  // loop avoidance
106  if((type1.id()==ID_symbol ||
107  type1.id()==ID_c_enum_tag ||
108  type1.id()==ID_struct_tag ||
109  type1.id()==ID_union_tag) &&
110  type2.id()==type1.id())
111  {
112  // already in same set?
114  type1.get(ID_identifier),
115  type2.get(ID_identifier)))
116  return true;
117  }
118 
119  if(type1.id()==ID_symbol ||
120  type1.id()==ID_c_enum_tag ||
121  type1.id()==ID_struct_tag ||
122  type1.id()==ID_union_tag)
123  {
124  const symbolt &symbol=
125  ns.lookup(type1.get(ID_identifier));
126 
127  if(!symbol.is_type)
128  return false;
129 
130  return base_type_eq_rec(symbol.type, type2);
131  }
132 
133  if(type2.id()==ID_symbol ||
134  type2.id()==ID_c_enum_tag ||
135  type2.id()==ID_struct_tag ||
136  type2.id()==ID_union_tag)
137  {
138  const symbolt &symbol=
139  ns.lookup(type2.get(ID_identifier));
140 
141  if(!symbol.is_type)
142  return false;
143 
144  return base_type_eq_rec(type1, symbol.type);
145  }
146 
147  if(type1.id()!=type2.id())
148  return false;
149 
150  if(type1.id()==ID_struct ||
151  type1.id()==ID_union)
152  {
153  const struct_union_typet::componentst &components1=
155 
156  const struct_union_typet::componentst &components2=
158 
159  if(components1.size()!=components2.size())
160  return false;
161 
162  for(unsigned i=0; i<components1.size(); i++)
163  {
164  const typet &subtype1=components1[i].type();
165  const typet &subtype2=components2[i].type();
166  if(!base_type_eq_rec(subtype1, subtype2))
167  return false;
168  if(components1[i].get_name()!=components2[i].get_name())
169  return false;
170  }
171 
172  return true;
173  }
174  else if(type1.id()==ID_incomplete_struct)
175  {
176  return true;
177  }
178  else if(type1.id()==ID_incomplete_union)
179  {
180  return true;
181  }
182  else if(type1.id()==ID_code)
183  {
184  const code_typet::parameterst &parameters1=
185  to_code_type(type1).parameters();
186 
187  const code_typet::parameterst &parameters2=
188  to_code_type(type2).parameters();
189 
190  if(parameters1.size()!=parameters2.size())
191  return false;
192 
193  for(unsigned i=0; i<parameters1.size(); i++)
194  {
195  const typet &subtype1=parameters1[i].type();
196  const typet &subtype2=parameters2[i].type();
197  if(!base_type_eq_rec(subtype1, subtype2))
198  return false;
199  }
200 
201  const typet &return_type1=to_code_type(type1).return_type();
202  const typet &return_type2=to_code_type(type2).return_type();
203 
204  if(!base_type_eq_rec(return_type1, return_type2))
205  return false;
206 
207  return true;
208  }
209  else if(type1.id()==ID_pointer)
210  {
211  return base_type_eq_rec(
212  to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype());
213  }
214  else if(type1.id()==ID_array)
215  {
216  if(!base_type_eq_rec(
217  to_array_type(type1).subtype(), to_array_type(type2).subtype()))
218  return false;
219 
220  if(to_array_type(type1).size()!=to_array_type(type2).size())
221  return false;
222 
223  return true;
224  }
225  else if(type1.id()==ID_incomplete_array)
226  {
227  return base_type_eq_rec(
228  to_incomplete_array_type(type1).subtype(),
229  to_incomplete_array_type(type2).subtype());
230  }
231 
232  // the below will go away
233  typet tmp1(type1), tmp2(type2);
234 
235  base_type(tmp1, ns);
236  base_type(tmp2, ns);
237 
238  return tmp1==tmp2;
239 }
240 
242  const exprt &expr1,
243  const exprt &expr2)
244 {
245  if(expr1.id()!=expr2.id())
246  return false;
247 
248  if(!base_type_eq(expr1.type(), expr2.type()))
249  return false;
250 
251  const exprt::operandst &expr1_op=expr1.operands();
252  const exprt::operandst &expr2_op=expr2.operands();
253  if(expr1_op.size()!=expr2_op.size())
254  return false;
255 
256  for(exprt::operandst::const_iterator
257  it1=expr1_op.begin(), it2=expr2_op.begin();
258  it1!=expr1_op.end() && it2!=expr2_op.end();
259  ++it1, ++it2)
260  if(!base_type_eq(*it1, *it2))
261  return false;
262 
263  if(expr1.id()==ID_constant)
264  if(expr1.get(ID_value)!=expr2.get(ID_value))
265  return false;
266 
267  return true;
268 }
269 
271  const typet &type1,
272  const typet &type2,
273  const namespacet &ns)
274 {
276  return base_type_eq.base_type_eq(type1, type2);
277 }
278 
280  const exprt &expr1,
281  const exprt &expr2,
282  const namespacet &ns)
283 {
285  return base_type_eq.base_type_eq(expr1, expr2);
286 }
The type of an expression.
Definition: type.h:20
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const namespacet & ns
Definition: base_type.h:54
bool is_nil() const
Definition: irep.h:103
Symbol table entry.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::vector< componentt > componentst
Definition: std_types.h:240
std::vector< parametert > parameterst
Definition: std_types.h:829
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
virtual bool base_type_eq_rec(const typet &type1, const typet &type2)
Definition: base_type.cpp:93
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const exprt & size() const
Definition: std_types.h:915
void base_type_rec(typet &type, const namespacet &ns, std::set< irep_idt > &symb)
Definition: base_type.cpp:21
identifierst identifiers
Definition: base_type.h:61
std::vector< exprt > operandst
Definition: expr.h:49
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a generic typet to an incomplete_array_typet.
Definition: std_types.h:986
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:79
bool base_type_eq(const typet &type1, const typet &type2)
Definition: base_type.h:39
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
#define Forall_operands(it, expr)
Definition: expr.h:23
bool make_union(const T &a, const T &b)
Definition: union_find.h:140
bool is_type
Definition: symbol.h:66
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
const typet & return_type() const
Definition: std_types.h:831