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