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 <cassert>
12 
13 #include <util/arith_tools.h>
14 #include <util/c_types.h>
15 #include <util/simplify_expr.h>
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 #include <util/threeval.h>
19 
20 #include "boolbv_type.h"
21 
22 exprt boolbvt::get(const exprt &expr) const
23 {
24  if(expr.id()==ID_symbol ||
25  expr.id()==ID_nondet_symbol)
26  {
27  const irep_idt &identifier=expr.get(ID_identifier);
28 
29  boolbv_mapt::mappingt::const_iterator it=
30  map.mapping.find(identifier);
31 
32  if(it!=map.mapping.end())
33  {
34  const boolbv_mapt::map_entryt &map_entry=it->second;
35  // an input expression must either be untyped (this is used for obtaining
36  // the value of clock symbols, which do not have a fixed type as the clock
37  // type is computed during symbolic execution) or match the type stored in
38  // the mapping
39  PRECONDITION(expr.type() == typet() || expr.type() == map_entry.type);
40 
41  std::vector<bool> unknown;
42  bvt bv;
43  std::size_t width=map_entry.width;
44 
45  bv.resize(width);
46  unknown.resize(width);
47 
48  for(std::size_t bit_nr=0; bit_nr<width; bit_nr++)
49  {
50  assert(bit_nr<map_entry.literal_map.size());
51 
52  if(map_entry.literal_map[bit_nr].is_set)
53  {
54  unknown[bit_nr]=false;
55  bv[bit_nr]=map_entry.literal_map[bit_nr].l;
56  }
57  else
58  {
59  unknown[bit_nr]=true;
60  bv[bit_nr].clear();
61  }
62  }
63 
64  return bv_get_rec(expr, bv, unknown, 0, map_entry.type);
65  }
66  }
67 
68  return SUB::get(expr);
69 }
70 
72  const exprt &expr,
73  const bvt &bv,
74  const std::vector<bool> &unknown,
75  std::size_t offset,
76  const typet &type) const
77 {
78  std::size_t width=boolbv_width(type);
79 
80  assert(bv.size()==unknown.size());
81  assert(bv.size()>=offset+width);
82 
83  if(type.id()==ID_bool)
84  {
85  if(!unknown[offset])
86  {
87  // clang-format off
88  switch(prop.l_get(bv[offset]).get_value())
89  {
90  case tvt::tv_enumt::TV_FALSE: return false_exprt();
91  case tvt::tv_enumt::TV_TRUE: return true_exprt();
92  case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
93  }
94  // clang-format on
95  }
96 
97  return false_exprt{}; // default
98  }
99 
100  bvtypet bvtype=get_bvtype(type);
101 
102  if(bvtype==bvtypet::IS_UNKNOWN)
103  {
104  if(type.id()==ID_array)
105  {
106  if(is_unbounded_array(type))
107  return bv_get_unbounded_array(expr);
108 
109  const typet &subtype=type.subtype();
110  std::size_t sub_width=boolbv_width(subtype);
111 
112  if(sub_width!=0)
113  {
114  exprt::operandst op;
115  op.reserve(width/sub_width);
116 
117  for(std::size_t new_offset=0;
118  new_offset<width;
119  new_offset+=sub_width)
120  {
121  const index_exprt index{
122  expr, from_integer(new_offset / sub_width, index_type())};
123  op.push_back(
124  bv_get_rec(index, bv, unknown, offset + new_offset, subtype));
125  }
126 
127  exprt dest=exprt(ID_array, type);
128  dest.operands().swap(op);
129  return dest;
130  }
131  }
132  else if(type.id()==ID_struct_tag)
133  {
134  exprt result = bv_get_rec(
135  expr, bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
136  result.type() = type;
137  return result;
138  }
139  else if(type.id()==ID_union_tag)
140  {
141  exprt result = bv_get_rec(
142  expr, bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
143  result.type() = type;
144  return result;
145  }
146  else if(type.id()==ID_struct)
147  {
148  const struct_typet &struct_type=to_struct_type(type);
149  const struct_typet::componentst &components=struct_type.components();
150  std::size_t new_offset=0;
151  exprt::operandst op;
152  op.reserve(components.size());
153 
154  for(const auto &c : components)
155  {
156  const typet &subtype = c.type();
157 
158  const member_exprt member{expr, c.get_name(), subtype};
159  op.push_back(
160  bv_get_rec(member, bv, unknown, offset + new_offset, subtype));
161 
162  std::size_t sub_width = boolbv_width(subtype);
163  if(sub_width!=0)
164  new_offset+=sub_width;
165  }
166 
167  return struct_exprt(std::move(op), type);
168  }
169  else if(type.id()==ID_union)
170  {
171  const union_typet &union_type=to_union_type(type);
172  const union_typet::componentst &components=union_type.components();
173 
174  assert(!components.empty());
175 
176  // Any idea that's better than just returning the first component?
177  std::size_t component_nr=0;
178 
179  const typet &subtype = components[component_nr].type();
180 
181  const member_exprt member{
182  expr, components[component_nr].get_name(), subtype};
183  return union_exprt(
184  components[component_nr].get_name(),
185  bv_get_rec(member, bv, unknown, offset, subtype),
186  union_type);
187  }
188  else if(type.id()==ID_vector)
189  {
190  const typet &subtype = type.subtype();
191  std::size_t sub_width=boolbv_width(subtype);
192 
193  if(sub_width!=0 && width%sub_width==0)
194  {
195  std::size_t size=width/sub_width;
196  vector_exprt value({}, to_vector_type(type));
197  value.reserve_operands(size);
198 
199  for(std::size_t i=0; i<size; i++)
200  {
201  const index_exprt index{expr, from_integer(i, index_type())};
202  value.operands().push_back(
203  bv_get_rec(index, bv, unknown, i * sub_width, subtype));
204  }
205 
206  return std::move(value);
207  }
208  }
209  else if(type.id()==ID_complex)
210  {
211  const typet &subtype = type.subtype();
212  std::size_t sub_width=boolbv_width(subtype);
213 
214  if(sub_width!=0 && width==sub_width*2)
215  {
216  const complex_exprt value(
217  bv_get_rec(
218  complex_real_exprt{expr}, bv, unknown, 0 * sub_width, subtype),
219  bv_get_rec(
220  complex_imag_exprt{expr}, bv, unknown, 1 * sub_width, subtype),
221  to_complex_type(type));
222 
223  return value;
224  }
225  }
226  }
227 
228  // most significant bit first
229  std::string value;
230 
231  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
232  {
233  char ch = '0';
234  if(!unknown[bit_nr])
235  {
236  switch(prop.l_get(bv[bit_nr]).get_value())
237  {
238  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
239  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
240  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
241  default: UNREACHABLE;
242  }
243  }
244 
245  value=ch+value;
246  }
247 
248  switch(bvtype)
249  {
250  case bvtypet::IS_UNKNOWN:
251  PRECONDITION(type.id() == ID_string || type.id() == ID_empty);
252  if(type.id()==ID_string)
253  {
254  mp_integer int_value=binary2integer(value, false);
255  irep_idt s;
256  if(int_value>=string_numbering.size())
257  s=irep_idt();
258  else
259  s = string_numbering[numeric_cast_v<std::size_t>(int_value)];
260 
261  return constant_exprt(s, type);
262  }
263  else if(type.id() == ID_empty)
264  {
265  return constant_exprt{irep_idt(), type};
266  }
267  break;
268 
269  case bvtypet::IS_RANGE:
270  {
271  mp_integer int_value = binary2integer(value, false);
272  mp_integer from = string2integer(type.get_string(ID_from));
273 
274  return constant_exprt(integer2string(int_value + from), type);
275  break;
276  }
277 
281  case bvtypet::IS_C_BOOL:
282  case bvtypet::IS_FIXED:
283  case bvtypet::IS_FLOAT:
285  case bvtypet::IS_SIGNED:
286  case bvtypet::IS_BV:
287  case bvtypet::IS_C_ENUM:
288  {
289  const irep_idt bvrep = make_bvrep(
290  width, [&value](size_t i) { return value[value.size() - i - 1] == '1'; });
291  return constant_exprt(bvrep, type);
292  }
293  }
294 
295  UNREACHABLE;
296 }
297 
298 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
299 {
300  std::vector<bool> unknown;
301  unknown.resize(bv.size(), false);
302  return bv_get_rec(nil_exprt{}, bv, unknown, 0, type);
303 }
304 
306 {
307  if(expr.type().id()==ID_bool) // boolean?
308  return get(expr);
309 
310  // look up literals in cache
311  bv_cachet::const_iterator it=bv_cache.find(expr);
312  CHECK_RETURN(it != bv_cache.end());
313 
314  return bv_get(it->second, expr.type());
315 }
316 
318 {
319  // first, try to get size
320 
321  const typet &type=expr.type();
322  const exprt &size_expr=to_array_type(type).size();
323  exprt size=simplify_expr(get(size_expr), ns);
324 
325  // get the numeric value, unless it's infinity
326  mp_integer size_mpint = 0;
327 
328  if(size.is_not_nil() && size.id() != ID_infinity)
329  {
330  const auto size_opt = numeric_cast<mp_integer>(size);
331  if(size_opt.has_value() && *size_opt >= 0)
332  size_mpint = *size_opt;
333  }
334 
335  // search array indices
336 
337  typedef std::map<mp_integer, exprt> valuest;
338  valuest values;
339 
340  const auto opt_num = arrays.get_number(expr);
341  if(opt_num.has_value())
342  {
343  // get root
344  const auto number = arrays.find_number(*opt_num);
345 
346  assert(number<index_map.size());
347  index_mapt::const_iterator it=index_map.find(number);
348  assert(it!=index_map.end());
349  const index_sett &index_set=it->second;
350 
351  for(index_sett::const_iterator it1=
352  index_set.begin();
353  it1!=index_set.end();
354  it1++)
355  {
356  index_exprt index(expr, *it1);
357 
358  exprt value=bv_get_cache(index);
359  exprt index_value=bv_get_cache(*it1);
360 
361  if(!index_value.is_nil())
362  {
363  const auto index_mpint = numeric_cast<mp_integer>(index_value);
364 
365  if(index_mpint.has_value())
366  {
367  if(value.is_nil())
368  values[*index_mpint] = exprt(ID_unknown, type.subtype());
369  else
370  values[*index_mpint] = value;
371  }
372  }
373  }
374  }
375 
376  exprt result;
377 
378  if(values.size() != size_mpint)
379  {
380  result = array_list_exprt({}, to_array_type(type));
381 
382  result.operands().reserve(values.size()*2);
383 
384  for(valuest::const_iterator it=values.begin();
385  it!=values.end();
386  it++)
387  {
388  exprt index=from_integer(it->first, size.type());
389  result.copy_to_operands(index, it->second);
390  }
391  }
392  else
393  {
394  // set the size
395  result=exprt(ID_array, type);
396 
397  // allocate operands
398  std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
399  result.operands().resize(size_int, exprt{ID_unknown});
400 
401  // search uninterpreted functions
402 
403  for(valuest::iterator it=values.begin();
404  it!=values.end();
405  it++)
406  if(it->first>=0 && it->first<size_mpint)
407  result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
408  it->second);
409  }
410 
411  return result;
412 }
413 
415  const bvt &bv,
416  std::size_t offset,
417  std::size_t width)
418 {
419  mp_integer value=0;
420  mp_integer weight=1;
421 
422  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
423  {
424  assert(bit_nr<bv.size());
425  switch(prop.l_get(bv[bit_nr]).get_value())
426  {
427  case tvt::tv_enumt::TV_FALSE: break;
428  case tvt::tv_enumt::TV_TRUE: value+=weight; break;
429  case tvt::tv_enumt::TV_UNKNOWN: break;
430  default: assert(false);
431  }
432 
433  weight*=2;
434  }
435 
436  return value;
437 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bvtypet::IS_SIGNED
@ IS_SIGNED
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
make_bvrep
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
Definition: arith_tools.cpp:305
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
arrayst::index_map
index_mapt index_map
Definition: arrays.h:78
bvtypet::IS_FIXED
@ IS_FIXED
union_find::find_number
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:202
bvtypet::IS_C_BIT_FIELD
@ IS_C_BIT_FIELD
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
boolbvt::bv_get_rec
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:71
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1740
boolbv_type.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1567
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition: boolbv_map.h:50
bvtypet::IS_VERILOG_SIGNED
@ IS_VERILOG_SIGNED
irep_idt
dstringt irep_idt
Definition: irep.h:32
bvtypet::IS_RANGE
@ IS_RANGE
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1531
bvtypet::IS_UNSIGNED
@ IS_UNSIGNED
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
bvtypet::IS_BV
@ IS_BV
boolbv_mapt::map_entryt::width
std::size_t width
Definition: boolbv_map.h:47
bvtypet
bvtypet
Definition: boolbv_type.h:17
bvtypet::IS_VERILOG_UNSIGNED
@ IS_VERILOG_UNSIGNED
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
array_typet::size
const exprt & size() const
Definition: std_types.h:973
boolbv_mapt::map_entryt
Definition: boolbv_map.h:41
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
bvtypet::IS_FLOAT
@ IS_FLOAT
tvt::tv_enumt::TV_TRUE
@ TV_TRUE
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:56
boolbvt::bv_cache
bv_cachet bv_cache
Definition: boolbv.h:121
boolbvt::string_numbering
numbering< irep_idt > string_numbering
Definition: boolbv.h:265
bvtypet::IS_C_BOOL
@ IS_C_BOOL
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
std_types.h
Pre-defined types.
prop_conv_solvert::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: prop_conv_solver.cpp:503
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
arrayst::index_sett
std::set< exprt > index_sett
Definition: arrays.h:74
boolbvt::bv_get_cache
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:305
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1672
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
union_typet
The union type.
Definition: std_types.h:393
boolbvt::get_value
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:83
boolbvt::bv_get_unbounded_array
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:317
boolbv_mapt::map_entryt::type
typet type
Definition: boolbv_map.h:49
simplify_expr.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:431
bvtypet::IS_C_ENUM
@ IS_C_ENUM
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
union_find::get_number
optionalt< number_type > get_number(const T &a) const
Definition: union_find.h:264
propt::l_get
virtual tvt l_get(literalt a) const =0
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
boolbvt::bv_get
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:298
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1785
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
boolbv.h
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1478
exprt::operands
operandst & operands()
Definition: expr.h:95
arrayst::arrays
union_find< exprt > arrays
Definition: arrays.h:71
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
index_exprt
Array index operator.
Definition: std_expr.h:1293
tvt::get_value
tv_enumt get_value() const
Definition: threeval.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:127
tvt::tv_enumt::TV_FALSE
@ TV_FALSE
std_expr.h
API to expression classes.
c_types.h
boolbvt::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:22
bvtypet::IS_UNKNOWN
@ IS_UNKNOWN
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106