cprover
boolbv_get.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.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 
20 exprt 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  {
31  const boolbv_mapt::map_entryt &map_entry = *map_entry_opt;
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  {
60  case tvt::tv_enumt::TV_FALSE: return false_exprt();
61  case tvt::tv_enumt::TV_TRUE: return true_exprt();
62  case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
63  }
64  // clang-format on
65  }
66 
67  bvtypet bvtype=get_bvtype(type);
68 
69  if(bvtype==bvtypet::IS_UNKNOWN)
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;
88  new_offset+=sub_width)
89  {
90  const index_exprt index{
91  expr,
92  from_integer(new_offset / sub_width, array_type.index_type())};
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  {
121  const struct_typet &struct_type=to_struct_type(type);
122  const struct_typet::componentst &components=struct_type.components();
123  std::size_t new_offset=0;
124  exprt::operandst op;
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)
136  new_offset+=sub_width;
137  }
138 
139  return struct_exprt(std::move(op), type);
140  }
141  else if(type.id()==ID_union)
142  {
143  const union_typet &union_type=to_union_type(type);
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  {
221  case bvtypet::IS_UNKNOWN:
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;
227  if(int_value>=string_numbering.size())
228  s=irep_idt();
229  else
230  s = string_numbering[numeric_cast_v<std::size_t>(int_value)];
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 
240  case bvtypet::IS_RANGE:
241  {
242  mp_integer int_value = binary2integer(value, false);
243  mp_integer from = string2integer(type.get_string(ID_from));
244 
245  return constant_exprt(integer2string(int_value + from), type);
246  break;
247  }
248 
252  case bvtypet::IS_C_BOOL:
253  case bvtypet::IS_FIXED:
254  case bvtypet::IS_FLOAT:
256  case bvtypet::IS_SIGNED:
257  case bvtypet::IS_BV:
258  case bvtypet::IS_C_ENUM:
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 
266  UNREACHABLE;
267 }
268 
269 exprt 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();
292  exprt size=simplify_expr(get(size_expr), ns);
293 
294  // get the numeric value, unless it's infinity
295  mp_integer size_mpint = 0;
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)
301  size_mpint = *size_opt;
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);
328  exprt index_value=bv_get_cache(*it1);
329 
330  if(!index_value.is_nil())
331  {
332  const auto index_mpint = numeric_cast<mp_integer>(index_value);
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
368  std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
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;
390  mp_integer weight=1;
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)
Definition: arith_tools.cpp:99
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:13
bvtypet
Definition: boolbv_type.h:17
@ IS_VERILOG_UNSIGNED
@ IS_VERILOG_SIGNED
@ IS_C_BIT_FIELD
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
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
Definition: boolbv_get.cpp:269
numberingt< irep_idt > string_numbering
Definition: boolbv.h:278
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:286
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:20
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:274
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
Definition: boolbv_get.cpp:45
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
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
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
bool is_nil() const
Definition: irep.h:376
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
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
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
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:2856
tv_enumt get_value() const
Definition: threeval.h:40
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
optionalt< number_type > get_number(const T &a) const
Definition: union_find.h:263
size_type find_number(const_iterator it) const
Definition: union_find.h:201
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)
BigInt mp_integer
Definition: smt_terms.h:12
#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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474