cprover
boolbv_width.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv_width.h"
10 
11 #include <algorithm>
12 
13 #include <util/arith_tools.h>
14 #include <util/invariant.h>
15 #include <util/std_types.h>
16 
18 {
19 }
20 
22 {
23 }
24 
26 {
27  // check cache first
28 
29  std::pair<cachet::iterator, bool> cache_result=
30  cache.insert(std::pair<typet, entryt>(type, entryt()));
31 
32  entryt &entry=cache_result.first->second;
33 
34  if(!cache_result.second) // found!
35  return entry;
36 
37  entry.total_width=0;
38 
39  const irep_idt type_id=type.id();
40 
41  if(type_id==ID_struct)
42  {
43  const struct_typet::componentst &components=
44  to_struct_type(type).components();
45 
46  std::size_t offset=0;
47  entry.members.resize(components.size());
48 
49  for(std::size_t i=0; i<entry.members.size(); i++)
50  {
51  std::size_t sub_width=operator()(components[i].type());
52  entry.members[i].offset=offset;
53  entry.members[i].width=sub_width;
54  offset+=sub_width;
55  }
56 
57  entry.total_width=offset;
58  }
59  else if(type_id==ID_union)
60  {
61  const union_typet::componentst &components=
62  to_union_type(type).components();
63 
64  entry.members.resize(components.size());
65 
66  std::size_t max_width=0;
67 
68  for(std::size_t i=0; i<entry.members.size(); i++)
69  {
70  std::size_t sub_width=operator()(components[i].type());
71  entry.members[i].width=sub_width;
72  max_width=std::max(max_width, sub_width);
73  }
74 
75  entry.total_width=max_width;
76  }
77  else if(type_id==ID_bool)
78  entry.total_width=1;
79  else if(type_id==ID_c_bool)
80  {
81  entry.total_width=to_c_bool_type(type).get_width();
82  assert(entry.total_width!=0);
83  }
84  else if(type_id==ID_signedbv)
85  {
87  assert(entry.total_width!=0);
88  }
89  else if(type_id==ID_unsignedbv)
90  {
92  assert(entry.total_width!=0);
93  }
94  else if(type_id==ID_floatbv)
95  {
97  assert(entry.total_width!=0);
98  }
99  else if(type_id==ID_fixedbv)
100  {
101  entry.total_width=to_fixedbv_type(type).get_width();
102  assert(entry.total_width!=0);
103  }
104  else if(type_id==ID_bv)
105  {
106  entry.total_width=to_bv_type(type).get_width();
107  assert(entry.total_width!=0);
108  }
109  else if(type_id==ID_verilog_signedbv ||
110  type_id==ID_verilog_unsignedbv)
111  {
112  // we encode with two bits
113  entry.total_width = type.get_size_t(ID_width) * 2;
114  assert(entry.total_width!=0);
115  }
116  else if(type_id==ID_range)
117  {
118  mp_integer from=string2integer(type.get_string(ID_from)),
119  to=string2integer(type.get_string(ID_to));
120 
121  mp_integer size=to-from+1;
122 
123  if(size>=1)
124  {
125  entry.total_width = address_bits(size);
126  assert(entry.total_width!=0);
127  }
128  }
129  else if(type_id==ID_array)
130  {
131  const array_typet &array_type=to_array_type(type);
132  std::size_t sub_width=operator()(array_type.subtype());
133 
134  mp_integer array_size;
135 
136  if(to_integer(array_type.size(), array_size))
137  {
138  // we can still use the theory of arrays for this
139  entry.total_width=0;
140  }
141  else
142  {
143  mp_integer total=array_size*sub_width;
144  if(total>(1<<30)) // realistic limit
145  throw "array too large for flattening";
146 
147  entry.total_width=integer2unsigned(total);
148  }
149  }
150  else if(type_id==ID_vector)
151  {
152  const vector_typet &vector_type=to_vector_type(type);
153  std::size_t sub_width=operator()(vector_type.subtype());
154 
155  mp_integer vector_size;
156 
157  if(to_integer(vector_type.size(), vector_size))
158  {
159  // we can still use the theory of arrays for this
160  entry.total_width=0;
161  }
162  else
163  {
164  mp_integer total=vector_size*sub_width;
165  if(total>(1<<30)) // realistic limit
166  throw "vector too large for flattening";
167 
168  entry.total_width=integer2unsigned(vector_size*sub_width);
169  }
170  }
171  else if(type_id==ID_complex)
172  {
173  std::size_t sub_width=operator()(type.subtype());
174  entry.total_width=integer2unsigned(2*sub_width);
175  }
176  else if(type_id==ID_code)
177  {
178  }
179  else if(type_id==ID_enumeration)
180  {
181  // get number of necessary bits
182  std::size_t size=to_enumeration_type(type).elements().size();
183  entry.total_width = address_bits(size);
184  assert(entry.total_width!=0);
185  }
186  else if(type_id==ID_c_enum)
187  {
188  // these have a subtype
189  entry.total_width = type.subtype().get_size_t(ID_width);
190  assert(entry.total_width!=0);
191  }
192  else if(type_id==ID_incomplete_c_enum)
193  {
194  // no width
195  }
196  else if(type_id==ID_pointer)
197  entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
198  else if(type_id==ID_symbol)
199  entry=get_entry(ns.follow(type));
200  else if(type_id==ID_struct_tag)
202  else if(type_id==ID_union_tag)
204  else if(type_id==ID_c_enum_tag)
206  else if(type_id==ID_c_bit_field)
207  {
209  }
210  else if(type_id==ID_string)
211  entry.total_width=32;
212 
213  return entry;
214 }
215 
217  const struct_typet &type,
218  const irep_idt &member) const
219 {
220  std::size_t component_number=type.component_number(member);
221 
222  return get_entry(type).members[component_number];
223 }
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1296
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition: expr_cast.h:198
Structure type.
Definition: std_types.h:297
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1561
const irep_idt & id() const
Definition: irep.h:259
const membert & get_member(const struct_typet &type, const irep_idt &member) const
std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:22
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
Definition: std_types.h:649
The pointer type.
Definition: std_types.h:1435
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
A constant-size array type.
Definition: std_types.h:1638
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const exprt & size() const
Definition: std_types.h:1648
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1023
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const namespacet & ns
Definition: boolbv_width.h:37
boolbv_widtht(const namespacet &_ns)
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1212
std::vector< membert > members
Definition: boolbv_width.h:42
const irept::subt & elements() const
Definition: std_types.h:628
std::size_t get_width() const
Definition: std_types.h:1138
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:747
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1254
API to type classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
arrays with given size
Definition: std_types.h:1013
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1411
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
const typet & subtype() const
Definition: type.h:33
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
std::size_t total_width
Definition: boolbv_width.h:41
const entryt & get_entry(const typet &type) const