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 "pointer_expr.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(
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 
109 void base_type(typet &type, const namespacet &ns)
110 {
111  std::set<irep_idt> symb;
112  base_type_rec(type, ns, symb);
113 }
114 
115 void 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  {
235  if(!base_type_eq_rec(
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:541
const typet & return_type() const
Definition: std_types.h:645
const parameterst & parameters() const
Definition: std_types.h:655
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.