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/config.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_unsigned_int(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  {
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();
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_unsigned_int(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  type_id==ID_reference)
198  {
200  }
201  else if(type_id==ID_symbol)
202  entry=get_entry(ns.follow(type));
203  else if(type_id==ID_struct_tag)
205  else if(type_id==ID_union_tag)
207  else if(type_id==ID_c_enum_tag)
209  else if(type_id==ID_c_bit_field)
210  {
212  }
213  else if(type_id==ID_string)
214  entry.total_width=32;
215 
216  return entry;
217 }
218 
220  const struct_typet &type,
221  const irep_idt &member) const
222 {
223  std::size_t component_number=type.component_number(member);
224 
225  return get_entry(type).members[component_number];
226 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:19
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
mp_integer address_bits(const mp_integer &size)
ceil(log2(size))
Structure type.
Definition: std_types.h:296
configt config
Definition: config.cpp:21
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
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
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1473
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 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:717
A constant-size array type.
Definition: std_types.h:1554
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const exprt & size() const
Definition: std_types.h:1568
const exprt & size() const
Definition: std_types.h:915
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:1319
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
const namespacet & ns
Definition: boolbv_width.h:37
boolbv_widtht(const namespacet &_ns)
std::vector< membert > members
Definition: boolbv_width.h:42
const irept::subt & elements() const
Definition: std_types.h:598
std::size_t get_width() const
Definition: std_types.h:1030
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1108
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
API to type classes.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:536
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:573
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:250
arrays with given size
Definition: std_types.h:901
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const typet & subtype() const
Definition: type.h:31
unsigned pointer_width
Definition: config.h:36
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
std::size_t total_width
Definition: boolbv_width.h:41
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
Definition: std_types.h:619
const entryt & get_entry(const typet &type) const