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/invariant.h>
16 #include <util/namespace.h>
17 #include <util/std_types.h>
18 
20 {
21 }
22 
24 {
25  // check cache first
26 
27  std::pair<cachet::iterator, bool> cache_result=
28  cache.insert(std::pair<typet, entryt>(type, entryt()));
29 
30  entryt &entry=cache_result.first->second;
31 
32  if(!cache_result.second) // found!
33  return entry;
34 
35  entry.total_width=0;
36 
37  const irep_idt type_id=type.id();
38 
39  if(type_id==ID_struct)
40  {
41  const struct_typet::componentst &components=
42  to_struct_type(type).components();
43 
44  std::size_t offset=0;
45  entry.members.resize(components.size());
46 
47  for(std::size_t i=0; i<entry.members.size(); i++)
48  {
49  std::size_t sub_width=operator()(components[i].type());
50  entry.members[i].offset=offset;
51  entry.members[i].width=sub_width;
52  offset+=sub_width;
53  }
54 
55  entry.total_width=offset;
56  }
57  else if(type_id==ID_union)
58  {
59  const union_typet::componentst &components=
60  to_union_type(type).components();
61 
62  entry.members.resize(components.size());
63 
64  std::size_t max_width=0;
65 
66  for(std::size_t i=0; i<entry.members.size(); i++)
67  {
68  std::size_t sub_width=operator()(components[i].type());
69  entry.members[i].width=sub_width;
70  max_width=std::max(max_width, sub_width);
71  }
72 
73  entry.total_width=max_width;
74  }
75  else if(type_id==ID_bool)
76  entry.total_width=1;
77  else if(type_id==ID_c_bool)
78  {
79  entry.total_width=to_c_bool_type(type).get_width();
80  }
81  else if(type_id==ID_signedbv)
82  {
84  }
85  else if(type_id==ID_unsignedbv)
86  {
88  }
89  else if(type_id==ID_floatbv)
90  {
92  }
93  else if(type_id==ID_fixedbv)
94  {
96  }
97  else if(type_id==ID_bv)
98  {
99  entry.total_width=to_bv_type(type).get_width();
100  }
101  else if(type_id==ID_verilog_signedbv ||
102  type_id==ID_verilog_unsignedbv)
103  {
104  // we encode with two bits
105  std::size_t size = to_bitvector_type(type).get_width();
107  size > 0, "verilog bitvector width shall be greater than zero");
108  entry.total_width = size * 2;
109  }
110  else if(type_id==ID_range)
111  {
112  mp_integer from=string2integer(type.get_string(ID_from)),
113  to=string2integer(type.get_string(ID_to));
114 
115  mp_integer size=to-from+1;
116 
117  if(size>=1)
118  {
119  entry.total_width = address_bits(size);
120  CHECK_RETURN(entry.total_width > 0);
121  }
122  }
123  else if(type_id==ID_array)
124  {
125  const array_typet &array_type=to_array_type(type);
126  std::size_t sub_width=operator()(array_type.subtype());
127 
128  const auto array_size = numeric_cast<mp_integer>(array_type.size());
129 
130  if(!array_size.has_value())
131  {
132  // we can still use the theory of arrays for this
133  entry.total_width=0;
134  }
135  else
136  {
137  mp_integer total = *array_size * sub_width;
138  if(total>(1<<30)) // realistic limit
139  throw analysis_exceptiont("array too large for flattening");
140  if(total < 0)
141  entry.total_width = 0;
142  else
143  entry.total_width = numeric_cast_v<std::size_t>(total);
144  }
145  }
146  else if(type_id==ID_vector)
147  {
148  const vector_typet &vector_type=to_vector_type(type);
149  std::size_t sub_width=operator()(vector_type.subtype());
150 
151  const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
152 
153  mp_integer total = vector_size * sub_width;
154  if(total > (1 << 30)) // realistic limit
155  throw analysis_exceptiont("vector too large for flattening");
156  if(total < 0)
157  entry.total_width = 0;
158  else
159  entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
160  }
161  else if(type_id==ID_complex)
162  {
163  const mp_integer sub_width = operator()(type.subtype());
164  entry.total_width = numeric_cast_v<std::size_t>(2 * sub_width);
165  }
166  else if(type_id==ID_code)
167  {
168  }
169  else if(type_id==ID_enumeration)
170  {
171  // get number of necessary bits
172  std::size_t size=to_enumeration_type(type).elements().size();
173  entry.total_width = address_bits(size);
174  CHECK_RETURN(entry.total_width > 0);
175  }
176  else if(type_id==ID_c_enum)
177  {
178  // these have a subtype
180  CHECK_RETURN(entry.total_width > 0);
181  }
182  else if(type_id==ID_pointer)
183  entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
184  else if(type_id==ID_struct_tag)
186  else if(type_id==ID_union_tag)
188  else if(type_id==ID_c_enum_tag)
190  else if(type_id==ID_c_bit_field)
191  {
193  }
194  else if(type_id==ID_string)
195  entry.total_width=32;
196  else if(type_id != ID_empty)
198 
199  return entry;
200 }
201 
203  const struct_typet &type,
204  const irep_idt &member) const
205 {
206  std::size_t component_number=type.component_number(member);
207 
208  return get_entry(type).members[component_number];
209 }
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:147
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:524
typet::subtype
const typet & subtype() const
Definition: type.h:47
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:525
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:30
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
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:308
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
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:23
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
invariant.h
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
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:63
vector_typet
The vector type.
Definition: std_types.h:975
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:32
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:42
array_typet::size
const exprt & size() const
Definition: std_types.h:771
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:176
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
boolbv_widtht::operator()
virtual std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:24
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:510
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.
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:474
boolbv_widtht::ns
const namespacet & ns
Definition: boolbv_width.h:39
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:239
boolbv_widtht::boolbv_widtht
boolbv_widtht(const namespacet &_ns)
Definition: boolbv_width.cpp:19
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:843
boolbv_widtht::cache
cachet cache
Definition: boolbv_width.h:50
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:496
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
array_typet
Arrays with given size.
Definition: std_types.h:763
boolbv_widtht::entryt::total_width
std::size_t total_width
Definition: boolbv_width.h:43
boolbv_width.h
boolbv_widtht::entryt::members
std::vector< membert > members
Definition: boolbv_width.h:44
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
boolbv_widtht::get_member
const membert & get_member(const struct_typet &type, const irep_idt &member) const
Definition: boolbv_width.cpp:202
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