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 "std_types.h"
19 #include "symbol.h"
20 #include "union_find.h"
21 
23 {
24 public:
25  explicit base_type_eqt(const namespacet &_ns):ns(_ns)
26  {
27  }
28 
29  bool base_type_eq(const typet &type1, const typet &type2)
30  {
32  return base_type_eq_rec(type1, type2);
33  }
34 
35  bool base_type_eq(const exprt &expr1, const exprt &expr2)
36  {
38  return base_type_eq_rec(expr1, expr2);
39  }
40 
41  virtual ~base_type_eqt() { }
42 
43 protected:
44  const namespacet &ns;
45 
46  virtual bool base_type_eq_rec(const typet &type1, const typet &type2);
47  virtual bool base_type_eq_rec(const exprt &expr1, const exprt &expr2);
48 
49  // for loop avoidance
52 };
53 
55  typet &type, const namespacet &ns, std::set<irep_idt> &symb)
56 {
57  if(
58  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
59  type.id() == ID_union_tag)
60  {
61  const symbolt *symbol;
62 
63  if(
64  !ns.lookup(to_tag_type(type).get_identifier(), symbol) &&
65  symbol->is_type && !symbol->type.is_nil())
66  {
67  type=symbol->type;
68  base_type_rec(type, ns, symb); // recursive call
69  return;
70  }
71  }
72  else if(type.id()==ID_array)
73  {
74  base_type_rec(to_array_type(type).subtype(), ns, symb);
75  }
76  else if(type.id()==ID_struct ||
77  type.id()==ID_union)
78  {
81 
82  for(auto &component : components)
83  base_type_rec(component.type(), ns, symb);
84  }
85  else if(type.id()==ID_pointer)
86  {
87  typet &subtype=to_pointer_type(type).subtype();
88 
89  // we need to avoid running into an infinite loop
90  if(
91  subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
92  subtype.id() == ID_union_tag)
93  {
94  const irep_idt &id = to_tag_type(subtype).get_identifier();
95 
96  if(symb.find(id)!=symb.end())
97  return;
98 
99  symb.insert(id);
100 
101  base_type_rec(subtype, ns, symb);
102 
103  symb.erase(id);
104  }
105  else
106  base_type_rec(subtype, ns, symb);
107  }
108 }
109 
110 void base_type(typet &type, const namespacet &ns)
111 {
112  std::set<irep_idt> symb;
113  base_type_rec(type, ns, symb);
114 }
115 
116 void base_type(exprt &expr, const namespacet &ns)
117 {
118  base_type(expr.type(), ns);
119 
120  Forall_operands(it, expr)
121  base_type(*it, ns);
122 }
123 
125  const typet &type1,
126  const typet &type2)
127 {
128  if(type1==type2)
129  return true;
130 
131  #if 0
132  std::cout << "T1: " << type1.pretty() << '\n';
133  std::cout << "T2: " << type2.pretty() << '\n';
134  #endif
135 
136  // loop avoidance
137  if(
138  (type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
139  type1.id() == ID_union_tag) &&
140  type2.id() == type1.id())
141  {
142  // already in same set?
144  type1.get(ID_identifier),
145  type2.get(ID_identifier)))
146  return true;
147  }
148 
149  if(
150  type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
151  type1.id() == ID_union_tag)
152  {
153  const symbolt &symbol=
154  ns.lookup(type1.get(ID_identifier));
155 
156  if(!symbol.is_type)
157  return false;
158 
159  return base_type_eq_rec(symbol.type, type2);
160  }
161 
162  if(
163  type2.id() == ID_c_enum_tag || type2.id() == ID_struct_tag ||
164  type2.id() == ID_union_tag)
165  {
166  const symbolt &symbol=
167  ns.lookup(type2.get(ID_identifier));
168 
169  if(!symbol.is_type)
170  return false;
171 
172  return base_type_eq_rec(type1, symbol.type);
173  }
174 
175  if(type1.id()!=type2.id())
176  return false;
177 
178  if(type1.id()==ID_struct ||
179  type1.id()==ID_union)
180  {
181  const struct_union_typet::componentst &components1=
183 
184  const struct_union_typet::componentst &components2=
186 
187  if(components1.size()!=components2.size())
188  return false;
189 
190  for(std::size_t i=0; i<components1.size(); i++)
191  {
192  const typet &subtype1=components1[i].type();
193  const typet &subtype2=components2[i].type();
194  if(!base_type_eq_rec(subtype1, subtype2))
195  return false;
196  if(components1[i].get_name()!=components2[i].get_name())
197  return false;
198  }
199 
200  return true;
201  }
202  else if(type1.id()==ID_code)
203  {
204  const code_typet::parameterst &parameters1=
205  to_code_type(type1).parameters();
206 
207  const code_typet::parameterst &parameters2=
208  to_code_type(type2).parameters();
209 
210  if(parameters1.size()!=parameters2.size())
211  return false;
212 
213  for(std::size_t i=0; i<parameters1.size(); i++)
214  {
215  const typet &subtype1=parameters1[i].type();
216  const typet &subtype2=parameters2[i].type();
217  if(!base_type_eq_rec(subtype1, subtype2))
218  return false;
219  }
220 
221  const typet &return_type1=to_code_type(type1).return_type();
222  const typet &return_type2=to_code_type(type2).return_type();
223 
224  if(!base_type_eq_rec(return_type1, return_type2))
225  return false;
226 
227  return true;
228  }
229  else if(type1.id()==ID_pointer)
230  {
231  return base_type_eq_rec(
232  to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype());
233  }
234  else if(type1.id()==ID_array)
235  {
236  if(!base_type_eq_rec(
237  to_array_type(type1).subtype(), to_array_type(type2).subtype()))
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 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:404
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
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:23
union_find.h
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
base_type_eqt::base_type_eq
bool base_type_eq(const exprt &expr1, const exprt &expr2)
Definition: base_type.cpp:35
base_type_eqt::ns
const namespacet & ns
Definition: base_type.cpp:44
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:208
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:535
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
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:54
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
base_type_eqt::identifierst
union_find< irep_idt > identifierst
Definition: base_type.cpp:50
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
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:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
union_find::clear
void clear()
Definition: union_find.h:247
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:428
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:155
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:110
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:291
base_type_eqt::base_type_eq_rec
virtual bool base_type_eq_rec(const typet &type1, const typet &type2)
Definition: base_type.cpp:124
base_type_eqt::base_type_eq
bool base_type_eq(const typet &type1, const typet &type2)
Definition: base_type.cpp:29
std_types.h
Pre-defined types.
pointer_expr.h
API to expression classes for Pointers.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
base_type_eqt::base_type_eqt
base_type_eqt(const namespacet &_ns)
Definition: base_type.cpp:25
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:41
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
exprt::operands
operandst & operands()
Definition: expr.h:96
base_type_eqt::identifiers
identifierst identifiers
Definition: base_type.cpp:51