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 <util/arith_tools.h>
10#include <util/c_types.h>
11#include <util/namespace.h>
12#include <util/simplify_expr.h>
13#include <util/std_expr.h>
14#include <util/threeval.h>
15
16#include "boolbv.h"
17#include "boolbv_type.h"
18
19#include <algorithm>
20
21exprt boolbvt::get(const exprt &expr) const
22{
23 if(expr.id()==ID_symbol ||
24 expr.id()==ID_nondet_symbol)
25 {
26 const irep_idt &identifier=expr.get(ID_identifier);
27
28 const auto map_entry_opt = map.get_map_entry(identifier);
29
30 if(map_entry_opt.has_value())
31 {
32 const boolbv_mapt::map_entryt &map_entry = *map_entry_opt;
33 // an input expression must either be untyped (this is used for obtaining
34 // the value of clock symbols, which do not have a fixed type as the clock
35 // type is computed during symbolic execution) or match the type stored in
36 // the mapping
37 if(expr.type() == map_entry.type)
38 return bv_get_rec(expr, map_entry.literal_map, 0);
39 else
40 {
41 PRECONDITION(expr.type() == typet{});
42 exprt skeleton = expr;
43 skeleton.type() = map_entry.type;
44 return bv_get_rec(skeleton, map_entry.literal_map, 0);
45 }
46 }
47 }
48
49 return SUB::get(expr);
50}
51
52exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
53 const
54{
55 const typet &type = expr.type();
56
57 if(type.id()==ID_bool)
58 {
59 PRECONDITION(bv.size() > offset);
60 // clang-format off
61 switch(prop.l_get(bv[offset]).get_value())
62 {
65 case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
66 }
67 // clang-format on
68 }
69
70 bvtypet bvtype=get_bvtype(type);
71
72 if(bvtype==bvtypet::IS_UNKNOWN)
73 {
74 if(type.id()==ID_array)
75 {
76 const auto &array_type = to_array_type(type);
77
78 if(is_unbounded_array(type))
79 return bv_get_unbounded_array(expr);
80
81 const typet &subtype = array_type.element_type();
82 const auto &sub_width_opt = bv_width.get_width_opt(subtype);
83
84 if(sub_width_opt.has_value() && *sub_width_opt > 0)
85 {
86 const std::size_t width = boolbv_width(type);
87
88 std::size_t sub_width = *sub_width_opt;
89
91 op.reserve(width/sub_width);
92
93 for(std::size_t new_offset=0;
94 new_offset<width;
95 new_offset+=sub_width)
96 {
97 const index_exprt index{
98 expr,
99 from_integer(new_offset / sub_width, array_type.index_type())};
100 op.push_back(bv_get_rec(index, bv, offset + new_offset));
101 }
102
103 exprt dest=exprt(ID_array, type);
104 dest.operands().swap(op);
105 return dest;
106 }
107 else
108 {
109 return array_exprt{{}, array_type};
110 }
111 }
112 else if(type.id() == ID_struct || type.id() == ID_struct_tag)
113 {
114 const struct_typet::componentst &components =
115 type.id() == ID_struct
116 ? to_struct_type(type).components()
117 : ns.follow_tag(to_struct_tag_type(type)).components();
118 std::size_t new_offset=0;
120 op.reserve(components.size());
121
122 for(const auto &c : components)
123 {
124 const typet &subtype = c.type();
125
126 const member_exprt member{expr, c.get_name(), subtype};
127 op.push_back(bv_get_rec(member, bv, offset + new_offset));
128
129 new_offset += boolbv_width(subtype);
130 }
131
132 return struct_exprt(std::move(op), type);
133 }
134 else if(type.id() == ID_union || type.id() == ID_union_tag)
135 {
136 const union_typet::componentst &components =
137 type.id() == ID_union
138 ? to_union_type(type).components()
139 : ns.follow_tag(to_union_tag_type(type)).components();
140
141 if(components.empty())
142 return empty_union_exprt(type);
143
144 // Any idea that's better than just returning the first component?
145 std::size_t component_nr=0;
146
147 const typet &subtype = components[component_nr].type();
148
149 const member_exprt member{
150 expr, components[component_nr].get_name(), subtype};
151 return union_exprt(
152 components[component_nr].get_name(),
153 bv_get_rec(member, bv, offset),
154 type);
155 }
156 else if(type.id()==ID_complex)
157 {
158 const std::size_t width = boolbv_width(type);
159
160 const typet &subtype = to_complex_type(type).subtype();
161 const std::size_t sub_width = boolbv_width(subtype);
162 CHECK_RETURN(sub_width > 0);
164 width == sub_width * 2,
165 "complex type has two elements of equal bit width");
166
167 return complex_exprt{
168 bv_get_rec(complex_real_exprt{expr}, bv, 0 * sub_width),
169 bv_get_rec(complex_imag_exprt{expr}, bv, 1 * sub_width),
170 to_complex_type(type)};
171 }
172 }
173
174 const std::size_t width = boolbv_width(type);
175 PRECONDITION(bv.size() >= offset + width);
176
177 std::string value;
178 value.reserve(width);
179
180 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
181 {
182 char ch = '0';
183 // clang-format off
184 switch(prop.l_get(bv[bit_nr]).get_value())
185 {
186 case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
187 case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
188 case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
189 }
190 // clang-format on
191
192 value += ch;
193 }
194
195 // The above collects bits starting with the least significant bit,
196 // but we need the most significant bit first.
197 std::reverse(value.begin(), value.end());
198
199 switch(bvtype)
200 {
202 PRECONDITION(type.id() == ID_string || type.id() == ID_empty);
203 if(type.id()==ID_string)
204 {
205 mp_integer int_value=binary2integer(value, false);
206 irep_idt s;
207 if(int_value>=string_numbering.size())
208 s=irep_idt();
209 else
211
212 return constant_exprt(s, type);
213 }
214 else if(type.id() == ID_empty)
215 {
216 return constant_exprt{irep_idt(), type};
217 }
218 break;
219
221 {
222 mp_integer int_value = binary2integer(value, false);
223 mp_integer from = string2integer(type.get_string(ID_from));
224
225 return constant_exprt(integer2string(int_value + from), type);
226 break;
227 }
228
237 case bvtypet::IS_BV:
239 {
240 const irep_idt bvrep = make_bvrep(
241 width, [&value](size_t i) { return value[value.size() - i - 1] == '1'; });
242 return constant_exprt(bvrep, type);
243 }
244 }
245
247}
248
249exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
250{
251 nil_exprt skeleton;
252 skeleton.type() = type;
253 return bv_get_rec(skeleton, bv, 0);
254}
255
257{
258 if(expr.is_boolean())
259 return get(expr);
260
261 // look up literals in cache
262 bv_cachet::const_iterator it=bv_cache.find(expr);
263 CHECK_RETURN(it != bv_cache.end());
264
265 return bv_get(it->second, expr.type());
266}
267
269{
270 // first, try to get size
271
272 const typet &type=expr.type();
273 const exprt &size_expr=to_array_type(type).size();
274 exprt size=simplify_expr(get(size_expr), ns);
275
276 // get the numeric value, unless it's infinity
277 const auto size_opt = numeric_cast<mp_integer>(size);
278
279 // search array indices, and only use those applicable to a particular model
280 // (array theory may have seen other indices, which might only be live under a
281 // different model)
282
283 typedef std::map<mp_integer, exprt> valuest;
284 valuest values;
285
286 const auto opt_num = arrays.get_number(expr);
287 if(opt_num.has_value())
288 {
289 // get root
290 const auto number = arrays.find_number(*opt_num);
291
292 CHECK_RETURN(number < index_map.size());
293 index_mapt::const_iterator it=index_map.find(number);
294 CHECK_RETURN(it != index_map.end());
295 const index_sett &index_set=it->second;
296
297 for(index_sett::const_iterator it1=
298 index_set.begin();
299 it1!=index_set.end();
300 it1++)
301 {
302 index_exprt index(expr, *it1);
303
304 exprt value=bv_get_cache(index);
305 exprt index_value=bv_get_cache(*it1);
306
307 if(!index_value.is_nil())
308 {
309 const auto index_mpint = numeric_cast<mp_integer>(index_value);
310
311 if(
312 index_mpint.has_value() && *index_mpint >= 0 &&
313 (!size_opt.has_value() || *index_mpint < *size_opt))
314 {
315 if(value.is_nil())
316 values[*index_mpint] =
317 exprt(ID_unknown, to_array_type(type).element_type());
318 else
319 values[*index_mpint] = value;
320 }
321 }
322 }
323 }
324
325 exprt result;
326
327 if(!size_opt.has_value() || values.size() != *size_opt)
328 {
329 result = array_list_exprt({}, to_array_type(type));
330
331 result.operands().reserve(values.size()*2);
332
333 for(valuest::const_iterator it=values.begin();
334 it!=values.end();
335 it++)
336 {
337 exprt index=from_integer(it->first, size.type());
338 result.add_to_operands(std::move(index), exprt{it->second});
339 }
340 }
341 else
342 {
343 // set the size
344 result=exprt(ID_array, type);
345
346 // allocate operands
347 std::size_t size_int = numeric_cast_v<std::size_t>(*size_opt);
348 result.operands().resize(size_int, exprt{ID_unknown});
349
350 // search uninterpreted functions
351
352 for(valuest::iterator it=values.begin();
353 it!=values.end();
354 it++)
355 {
356 result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
357 it->second);
358 }
359 }
360
361 return result;
362}
363
365 const bvt &bv,
366 std::size_t offset,
367 std::size_t width)
368{
369 PRECONDITION(offset + width <= bv.size());
370
371 mp_integer value=0;
372 mp_integer weight=1;
373
374 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
375 {
376 switch(prop.l_get(bv[bit_nr]).get_value())
377 {
378 case tvt::tv_enumt::TV_FALSE: break;
379 case tvt::tv_enumt::TV_TRUE: value+=weight; break;
380 case tvt::tv_enumt::TV_UNKNOWN: break;
381 default:
383 }
384
385 weight*=2;
386 }
387
388 return value;
389}
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)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
bvtypet get_bvtype(const typet &type)
bvtypet
Definition boolbv_type.h:17
@ IS_VERILOG_UNSIGNED
Definition boolbv_type.h:19
@ IS_VERILOG_SIGNED
Definition boolbv_type.h:19
@ IS_UNSIGNED
Definition boolbv_type.h:18
@ IS_C_BIT_FIELD
Definition boolbv_type.h:20
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Array constructor from list of elements.
Definition std_expr.h:1621
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition std_expr.h:1681
const exprt & size() const
Definition std_types.h:840
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
bv_cachet bv_cache
Definition boolbv.h:135
bool is_unbounded_array(const typet &type) const override
Definition boolbv.cpp:533
exprt bv_get(const bvt &bv, const typet &type) const
numberingt< irep_idt > string_numbering
Definition boolbv.h:280
virtual exprt bv_get_unbounded_array(const exprt &) const
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
boolbv_widtht bv_width
Definition boolbv.h:116
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:102
mp_integer get_value(const bvt &bv)
Definition boolbv.h:90
boolbv_mapt map
Definition boolbv.h:123
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
A constant literal expression.
Definition std_expr.h:2995
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1834
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
The Boolean constant false.
Definition std_expr.h:3077
Array index operator.
Definition std_expr.h:1470
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
Extract member of struct or union.
Definition std_expr.h:2849
The NIL expression.
Definition std_expr.h:3086
Struct constructor from list of elements.
Definition std_expr.h:1877
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The Boolean constant true.
Definition std_expr.h:3068
const typet & subtype() const
Definition type.h:187
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1770
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)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
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:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1155
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
dstringt irep_idt