cprover
Loading...
Searching...
No Matches
boolbv_get.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/namespace.h>
14#include <util/simplify_expr.h>
15#include <util/std_expr.h>
16#include <util/threeval.h>
17
18#include "boolbv_type.h"
19
20exprt boolbvt::get(const exprt &expr) const
21{
22 if(expr.id()==ID_symbol ||
23 expr.id()==ID_nondet_symbol)
24 {
25 const irep_idt &identifier=expr.get(ID_identifier);
26
27 const auto map_entry_opt = map.get_map_entry(identifier);
28
29 if(map_entry_opt.has_value())
30 {
32 // an input expression must either be untyped (this is used for obtaining
33 // the value of clock symbols, which do not have a fixed type as the clock
34 // type is computed during symbolic execution) or match the type stored in
35 // the mapping
36 PRECONDITION(expr.type() == typet() || expr.type() == map_entry.type);
37
38 return bv_get_rec(expr, map_entry.literal_map, 0, map_entry.type);
39 }
40 }
41
42 return SUB::get(expr);
43}
44
46 const exprt &expr,
47 const bvt &bv,
48 std::size_t offset,
49 const typet &type) const
50{
51 std::size_t width=boolbv_width(type);
52
53 assert(bv.size()>=offset+width);
54
55 if(type.id()==ID_bool)
56 {
57 // clang-format off
58 switch(prop.l_get(bv[offset]).get_value())
59 {
62 case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
63 }
64 // clang-format on
65 }
66
68
70 {
71 if(type.id()==ID_array)
72 {
73 const auto &array_type = to_array_type(type);
74
75 if(is_unbounded_array(type))
76 return bv_get_unbounded_array(expr);
77
78 const typet &subtype = array_type.element_type();
79 std::size_t sub_width=boolbv_width(subtype);
80
81 if(sub_width!=0)
82 {
84 op.reserve(width/sub_width);
85
86 for(std::size_t new_offset=0;
87 new_offset<width;
89 {
90 const index_exprt index{
91 expr,
93 op.push_back(bv_get_rec(index, bv, offset + new_offset, subtype));
94 }
95
96 exprt dest=exprt(ID_array, type);
97 dest.operands().swap(op);
98 return dest;
99 }
100 else
101 {
102 return array_exprt{{}, array_type};
103 }
104 }
105 else if(type.id()==ID_struct_tag)
106 {
107 exprt result =
108 bv_get_rec(expr, bv, offset, ns.follow_tag(to_struct_tag_type(type)));
109 result.type() = type;
110 return result;
111 }
112 else if(type.id()==ID_union_tag)
113 {
114 exprt result =
115 bv_get_rec(expr, bv, offset, ns.follow_tag(to_union_tag_type(type)));
116 result.type() = type;
117 return result;
118 }
119 else if(type.id()==ID_struct)
120 {
122 const struct_typet::componentst &components=struct_type.components();
123 std::size_t new_offset=0;
125 op.reserve(components.size());
126
127 for(const auto &c : components)
128 {
129 const typet &subtype = c.type();
130
131 const member_exprt member{expr, c.get_name(), subtype};
132 op.push_back(bv_get_rec(member, bv, offset + new_offset, subtype));
133
134 std::size_t sub_width = boolbv_width(subtype);
135 if(sub_width!=0)
137 }
138
139 return struct_exprt(std::move(op), type);
140 }
141 else if(type.id()==ID_union)
142 {
144 const union_typet::componentst &components=union_type.components();
145
146 if(components.empty())
147 return empty_union_exprt(type);
148
149 // Any idea that's better than just returning the first component?
150 std::size_t component_nr=0;
151
152 const typet &subtype = components[component_nr].type();
153
154 const member_exprt member{
155 expr, components[component_nr].get_name(), subtype};
156 return union_exprt(
157 components[component_nr].get_name(),
158 bv_get_rec(member, bv, offset, subtype),
159 union_type);
160 }
161 else if(type.id()==ID_vector)
162 {
163 const auto &vector_type = to_vector_type(type);
164 const typet &element_type = vector_type.element_type();
165 std::size_t element_width = boolbv_width(element_type);
166
167 if(element_width != 0 && width % element_width == 0)
168 {
169 std::size_t size = width / element_width;
170 vector_exprt value({}, vector_type);
171 value.reserve_operands(size);
172
173 for(std::size_t i=0; i<size; i++)
174 {
175 const index_exprt index{expr,
176 from_integer(i, vector_type.index_type())};
177 value.operands().push_back(
178 bv_get_rec(index, bv, i * element_width, element_type));
179 }
180
181 return std::move(value);
182 }
183 }
184 else if(type.id()==ID_complex)
185 {
186 const typet &subtype = to_complex_type(type).subtype();
187 std::size_t sub_width=boolbv_width(subtype);
188
189 if(sub_width!=0 && width==sub_width*2)
190 {
191 const complex_exprt value(
192 bv_get_rec(complex_real_exprt{expr}, bv, 0 * sub_width, subtype),
193 bv_get_rec(complex_imag_exprt{expr}, bv, 1 * sub_width, subtype),
194 to_complex_type(type));
195
196 return value;
197 }
198 }
199 }
200
201 // most significant bit first
202 std::string value;
203
204 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
205 {
206 char ch = '0';
207 // clang-format off
208 switch(prop.l_get(bv[bit_nr]).get_value())
209 {
210 case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
211 case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
212 case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
213 }
214 // clang-format on
215
216 value=ch+value;
217 }
218
219 switch(bvtype)
220 {
222 PRECONDITION(type.id() == ID_string || type.id() == ID_empty);
223 if(type.id()==ID_string)
224 {
225 mp_integer int_value=binary2integer(value, false);
226 irep_idt s;
228 s=irep_idt();
229 else
231
232 return constant_exprt(s, type);
233 }
234 else if(type.id() == ID_empty)
235 {
236 return constant_exprt{irep_idt(), type};
237 }
238 break;
239
241 {
242 mp_integer int_value = binary2integer(value, false);
244
245 return constant_exprt(integer2string(int_value + from), type);
246 break;
247 }
248
257 case bvtypet::IS_BV:
259 {
260 const irep_idt bvrep = make_bvrep(
261 width, [&value](size_t i) { return value[value.size() - i - 1] == '1'; });
262 return constant_exprt(bvrep, type);
263 }
264 }
265
267}
268
269exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
270{
271 return bv_get_rec(nil_exprt{}, bv, 0, type);
272}
273
275{
276 if(expr.type().id()==ID_bool) // boolean?
277 return get(expr);
278
279 // look up literals in cache
280 bv_cachet::const_iterator it=bv_cache.find(expr);
281 CHECK_RETURN(it != bv_cache.end());
282
283 return bv_get(it->second, expr.type());
284}
285
287{
288 // first, try to get size
289
290 const typet &type=expr.type();
291 const exprt &size_expr=to_array_type(type).size();
293
294 // get the numeric value, unless it's infinity
296
297 if(size.is_not_nil() && size.id() != ID_infinity)
298 {
299 const auto size_opt = numeric_cast<mp_integer>(size);
300 if(size_opt.has_value() && *size_opt >= 0)
302 }
303
304 // search array indices
305
306 typedef std::map<mp_integer, exprt> valuest;
307 valuest values;
308
309 const auto opt_num = arrays.get_number(expr);
310 if(opt_num.has_value())
311 {
312 // get root
313 const auto number = arrays.find_number(*opt_num);
314
315 assert(number<index_map.size());
316 index_mapt::const_iterator it=index_map.find(number);
317 assert(it!=index_map.end());
318 const index_sett &index_set=it->second;
319
320 for(index_sett::const_iterator it1=
321 index_set.begin();
322 it1!=index_set.end();
323 it1++)
324 {
325 index_exprt index(expr, *it1);
326
327 exprt value=bv_get_cache(index);
329
330 if(!index_value.is_nil())
331 {
333
334 if(index_mpint.has_value())
335 {
336 if(value.is_nil())
337 values[*index_mpint] =
338 exprt(ID_unknown, to_array_type(type).subtype());
339 else
340 values[*index_mpint] = value;
341 }
342 }
343 }
344 }
345
346 exprt result;
347
348 if(values.size() != size_mpint)
349 {
350 result = array_list_exprt({}, to_array_type(type));
351
352 result.operands().reserve(values.size()*2);
353
354 for(valuest::const_iterator it=values.begin();
355 it!=values.end();
356 it++)
357 {
358 exprt index=from_integer(it->first, size.type());
359 result.copy_to_operands(index, it->second);
360 }
361 }
362 else
363 {
364 // set the size
365 result=exprt(ID_array, type);
366
367 // allocate operands
369 result.operands().resize(size_int, exprt{ID_unknown});
370
371 // search uninterpreted functions
372
373 for(valuest::iterator it=values.begin();
374 it!=values.end();
375 it++)
376 if(it->first>=0 && it->first<size_mpint)
377 result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
378 it->second);
379 }
380
381 return result;
382}
383
385 const bvt &bv,
386 std::size_t offset,
387 std::size_t width)
388{
389 mp_integer value=0;
391
392 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
393 {
394 assert(bit_nr<bv.size());
395 switch(prop.l_get(bv[bit_nr]).get_value())
396 {
397 case tvt::tv_enumt::TV_FALSE: break;
398 case tvt::tv_enumt::TV_TRUE: value+=weight; break;
399 case tvt::tv_enumt::TV_UNKNOWN: break;
400 default: assert(false);
401 }
402
403 weight*=2;
404 }
405
406 return value;
407}
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bvtypet get_bvtype(const typet &type)
bvtypet
Definition boolbv_type.h:17
@ IS_VERILOG_UNSIGNED
@ IS_VERILOG_SIGNED
@ IS_C_BIT_FIELD
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Array constructor from list of elements.
Definition std_expr.h:1476
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1522
const exprt & size() const
Definition std_types.h:790
index_mapt index_map
Definition arrays.h:85
const namespacet & ns
Definition arrays.h:56
union_find< exprt, irep_hash > arrays
Definition arrays.h:78
std::set< exprt > index_sett
Definition arrays.h:81
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Definition boolbv_map.h:56
bv_cachet bv_cache
Definition boolbv.h:132
bool is_unbounded_array(const typet &type) const override
Definition boolbv.cpp:547
exprt bv_get(const bvt &bv, const typet &type) const
numberingt< irep_idt > string_numbering
Definition boolbv.h:278
virtual exprt bv_get_unbounded_array(const exprt &) const
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
exprt bv_get_cache(const exprt &expr) const
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const
mp_integer get_value(const bvt &bv)
Definition boolbv.h:87
boolbv_mapt map
Definition boolbv.h:120
Complex constructor from a pair of numbers.
Definition std_expr.h:1761
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1874
Real part of the expression describing a complex number.
Definition std_expr.h:1829
A constant literal expression.
Definition std_expr.h:2807
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1677
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:129
void reserve_operands(operandst::size_type n)
Definition expr.h:124
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
The Boolean constant false.
Definition std_expr.h:2865
Array index operator.
Definition std_expr.h:1328
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
const std::string & get_string(const irep_idt &name) const
Definition irep.h:409
Extract member of struct or union.
Definition std_expr.h:2667
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
The NIL expression.
Definition std_expr.h:2874
size_type size() const
Definition numbering.h:66
virtual tvt l_get(literalt a) const =0
Struct constructor from list of elements.
Definition std_expr.h:1722
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
The Boolean constant true.
Definition std_expr.h:2856
const typet & subtype() const
Definition type.h:156
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1611
size_type find_number(const_iterator it) const
Definition union_find.h:201
optionalt< number_type > get_number(const T &a) const
Definition union_find.h:263
The union type.
Definition c_types.h:125
Vector constructor from list of elements.
Definition std_expr.h:1575
dstringt irep_idt
Definition irep.h:37
std::vector< literalt > bvt
Definition literal.h:201
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition mp_arith.cpp:117
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
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 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