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(
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).subtype(), 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  {
86  typet &subtype=to_pointer_type(type).subtype();
87 
88  // we need to avoid running into an infinite loop
89  if(
90  subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
91  subtype.id() == ID_union_tag)
92  {
93  const irep_idt &id = to_tag_type(subtype).get_identifier();
94 
95  if(symb.find(id)!=symb.end())
96  return;
97 
98  symb.insert(id);
99 
100  base_type_rec(subtype, ns, symb);
101 
102  symb.erase(id);
103  }
104  else
105  base_type_rec(subtype, 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(
231  to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype());
232  }
233  else if(type1.id()==ID_array)
234  {
235  if(!base_type_eq_rec(
236  to_array_type(type1).subtype(), to_array_type(type2).subtype()))
237  return false;
238 
239  if(to_array_type(type1).size()!=to_array_type(type2).size())
240  return false;
241 
242  return true;
243  }
244 
245  // the below will go away
246  typet tmp1(type1), tmp2(type2);
247 
248  base_type(tmp1, ns);
249  base_type(tmp2, ns);
250 
251  return tmp1==tmp2;
252 }
253 
255  const exprt &expr1,
256  const exprt &expr2)
257 {
258  if(expr1.id()!=expr2.id())
259  return false;
260 
261  if(!base_type_eq(expr1.type(), expr2.type()))
262  return false;
263 
264  const exprt::operandst &expr1_op=expr1.operands();
265  const exprt::operandst &expr2_op=expr2.operands();
266  if(expr1_op.size()!=expr2_op.size())
267  return false;
268 
269  for(exprt::operandst::const_iterator
270  it1=expr1_op.begin(), it2=expr2_op.begin();
271  it1!=expr1_op.end() && it2!=expr2_op.end();
272  ++it1, ++it2)
273  if(!base_type_eq(*it1, *it2))
274  return false;
275 
276  if(expr1.id()==ID_constant)
277  if(expr1.get(ID_value)!=expr2.get(ID_value))
278  return false;
279 
280  return true;
281 }
282 
291  const typet &type1,
292  const typet &type2,
293  const namespacet &ns)
294 {
296  return base_type_eq.base_type_eq(type1, type2);
297 }
298 
304  const exprt &expr1,
305  const exprt &expr2,
306  const namespacet &ns)
307 {
309  return base_type_eq.base_type_eq(expr1, expr2);
310 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
base_type_eqt
Definition: base_type.cpp:22
union_find.h
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
base_type_eqt::base_type_eq
bool base_type_eq(const exprt &expr1, const exprt &expr2)
Definition: base_type.cpp:34
base_type_eqt::ns
const namespacet & ns
Definition: base_type.cpp:43
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
base_type_rec
void base_type_rec(typet &type, const namespacet &ns, std::set< irep_idt > &symb)
Definition: base_type.cpp:53
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
base_type_eqt::identifierst
union_find< irep_idt > identifierst
Definition: base_type.cpp:49
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
union_find< irep_idt >
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:475
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
base_type.h
Base Type Computation.
base_type_eq
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:290
base_type_eqt::base_type_eq_rec
virtual bool base_type_eq_rec(const typet &type1, const typet &type2)
Definition: base_type.cpp:123
base_type_eqt::base_type_eq
bool base_type_eq(const typet &type1, const typet &type2)
Definition: base_type.cpp:28
std_types.h
Pre-defined types.
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
union_find::clear
void clear()
Definition: union_find.h:248
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
base_type_eqt::base_type_eqt
base_type_eqt(const namespacet &_ns)
Definition: base_type.cpp:24
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
base_type_eqt::~base_type_eqt
virtual ~base_type_eqt()
Definition: base_type.cpp:40
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
exprt::operands
operandst & operands()
Definition: expr.h:95
base_type_eqt::identifiers
identifierst identifiers
Definition: base_type.cpp:50