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/c_types.h>
15 #include <util/exception_utils.h>
16 #include <util/invariant.h>
17 #include <util/namespace.h>
18 #include <util/pointer_expr.h>
19 #include <util/std_types.h>
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  }
83  else if(type_id==ID_signedbv)
84  {
86  }
87  else if(type_id==ID_unsignedbv)
88  {
90  }
91  else if(type_id==ID_floatbv)
92  {
94  }
95  else if(type_id==ID_fixedbv)
96  {
98  }
99  else if(type_id==ID_bv)
100  {
101  entry.total_width=to_bv_type(type).get_width();
102  }
103  else if(type_id==ID_verilog_signedbv ||
104  type_id==ID_verilog_unsignedbv)
105  {
106  // we encode with two bits
107  std::size_t size = to_bitvector_type(type).get_width();
109  size > 0, "verilog bitvector width shall be greater than zero");
110  entry.total_width = size * 2;
111  }
112  else if(type_id==ID_range)
113  {
114  mp_integer from=string2integer(type.get_string(ID_from)),
115  to=string2integer(type.get_string(ID_to));
116 
117  mp_integer size=to-from+1;
118 
119  if(size>=1)
120  {
121  entry.total_width = address_bits(size);
122  CHECK_RETURN(entry.total_width > 0);
123  }
124  }
125  else if(type_id==ID_array)
126  {
127  const array_typet &array_type=to_array_type(type);
128  std::size_t sub_width=operator()(array_type.subtype());
129 
130  const auto array_size = numeric_cast<mp_integer>(array_type.size());
131 
132  if(!array_size.has_value())
133  {
134  // we can still use the theory of arrays for this
135  entry.total_width=0;
136  }
137  else
138  {
139  mp_integer total = *array_size * sub_width;
140  if(total>(1<<30)) // realistic limit
141  throw analysis_exceptiont("array too large for flattening");
142 
143  if(total < 0)
144  entry.total_width = 0;
145  else
146  entry.total_width = numeric_cast_v<std::size_t>(total);
147  }
148  }
149  else if(type_id==ID_vector)
150  {
151  const vector_typet &vector_type=to_vector_type(type);
152  std::size_t sub_width=operator()(vector_type.subtype());
153 
154  const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
155 
156  mp_integer total = vector_size * sub_width;
157  if(total > (1 << 30)) // realistic limit
158  throw analysis_exceptiont("vector too large for flattening");
159 
160  entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
161  }
162  else if(type_id==ID_complex)
163  {
164  const mp_integer sub_width = operator()(type.subtype());
165  entry.total_width = numeric_cast_v<std::size_t>(2 * sub_width);
166  }
167  else if(type_id==ID_code)
168  {
169  }
170  else if(type_id==ID_enumeration)
171  {
172  // get number of necessary bits
173  std::size_t size=to_enumeration_type(type).elements().size();
174  entry.total_width = address_bits(size);
175  CHECK_RETURN(entry.total_width > 0);
176  }
177  else if(type_id==ID_c_enum)
178  {
179  // these have a subtype
181  CHECK_RETURN(entry.total_width > 0);
182  }
183  else if(type_id==ID_pointer)
184  entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
185  else if(type_id==ID_struct_tag)
187  else if(type_id==ID_union_tag)
189  else if(type_id==ID_c_enum_tag)
191  else if(type_id==ID_c_bit_field)
192  {
194  }
195  else if(type_id==ID_string)
196  entry.total_width=32;
197  else if(type_id != ID_empty)
199 
200  return entry;
201 }
202 
204  const struct_typet &type,
205  const irep_idt &member) const
206 {
207  std::size_t component_number=type.component_number(member);
208 
209  return get_entry(type).members[component_number];
210 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
to_enumeration_type
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:518
typet::subtype
const typet & subtype() const
Definition: type.h:47
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:93
boolbv_widtht::membert
Definition: boolbv_width.h:29
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
boolbv_widtht::get_entry
const entryt & get_entry(const typet &type) const
Definition: boolbv_width.cpp:25
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
invariant.h
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: bitvector_types.h:82
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
vector_typet
The vector type.
Definition: std_types.h:969
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
namespace.h
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:36
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
boolbv_widtht::entryt
Definition: boolbv_width.h:41
array_typet::size
const exprt & size() const
Definition: std_types.h:765
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:177
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
boolbv_widtht::operator()
virtual std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:23
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
std_types.h
Pre-defined types.
pointer_expr.h
API to expression classes for Pointers.
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
boolbv_widtht::ns
const namespacet & ns
Definition: boolbv_width.h:38
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:243
boolbv_widtht::boolbv_widtht
boolbv_widtht(const namespacet &_ns)
Definition: boolbv_width.cpp:21
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
boolbv_widtht::cache
cachet cache
Definition: boolbv_width.h:49
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:47
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
enumeration_typet::elements
const irept::subt & elements() const
Definition: std_types.h:490
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
array_typet
Arrays with given size.
Definition: std_types.h:757
boolbv_widtht::entryt::total_width
std::size_t total_width
Definition: boolbv_width.h:42
boolbv_width.h
boolbv_widtht::entryt::members
std::vector< membert > members
Definition: boolbv_width.h:43
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
boolbv_widtht::get_member
const membert & get_member(const struct_typet &type, const irep_idt &member) const
Definition: boolbv_width.cpp:203
c_types.h
analysis_exceptiont
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: exception_utils.h:157