cprover
boolbv_width.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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=
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=
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 {
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.element_type());
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.element_type());
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()(to_complex_type(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
179 entry.total_width =
180 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
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}
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
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:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:106
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
std::size_t get_width() const
Definition: std_types.h:864
boolbv_widtht(const namespacet &_ns)
const namespacet & ns
Definition: boolbv_width.h:39
const entryt & get_entry(const typet &type) const
virtual std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:24
const membert & get_member(const struct_typet &type, const irep_idt &member) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const irept::subt & elements() const
Definition: std_types.h:496
const irep_idt & id() const
Definition: irep.h:396
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
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:40
std::vector< componentt > componentst
Definition: std_types.h:140
The type of an expression, extends irept.
Definition: type.h:29
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define UNIMPLEMENTED
Definition: invariant.h:525
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:524
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
std::size_t total_width
Definition: boolbv_width.h:43
std::vector< membert > members
Definition: boolbv_width.h:44