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/std_types.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  if(is_unbounded_array(type))
74  return bv_get_unbounded_array(expr);
75 
76  const typet &subtype=type.subtype();
77  std::size_t sub_width=boolbv_width(subtype);
78 
79  if(sub_width!=0)
80  {
82  op.reserve(width/sub_width);
83 
84  for(std::size_t new_offset=0;
85  new_offset<width;
86  new_offset+=sub_width)
87  {
88  const index_exprt index{
89  expr, from_integer(new_offset / sub_width, index_type())};
90  op.push_back(bv_get_rec(index, bv, offset + new_offset, subtype));
91  }
92 
93  exprt dest=exprt(ID_array, type);
94  dest.operands().swap(op);
95  return dest;
96  }
97  else
98  {
99  return array_exprt{{}, to_array_type(type)};
100  }
101  }
102  else if(type.id()==ID_struct_tag)
103  {
104  exprt result =
105  bv_get_rec(expr, bv, offset, ns.follow_tag(to_struct_tag_type(type)));
106  result.type() = type;
107  return result;
108  }
109  else if(type.id()==ID_union_tag)
110  {
111  exprt result =
112  bv_get_rec(expr, bv, offset, ns.follow_tag(to_union_tag_type(type)));
113  result.type() = type;
114  return result;
115  }
116  else if(type.id()==ID_struct)
117  {
118  const struct_typet &struct_type=to_struct_type(type);
119  const struct_typet::componentst &components=struct_type.components();
120  std::size_t new_offset=0;
121  exprt::operandst op;
122  op.reserve(components.size());
123 
124  for(const auto &c : components)
125  {
126  const typet &subtype = c.type();
127 
128  const member_exprt member{expr, c.get_name(), subtype};
129  op.push_back(bv_get_rec(member, bv, offset + new_offset, subtype));
130 
131  std::size_t sub_width = boolbv_width(subtype);
132  if(sub_width!=0)
133  new_offset+=sub_width;
134  }
135 
136  return struct_exprt(std::move(op), type);
137  }
138  else if(type.id()==ID_union)
139  {
140  const union_typet &union_type=to_union_type(type);
141  const union_typet::componentst &components=union_type.components();
142 
143  assert(!components.empty());
144 
145  // Any idea that's better than just returning the first component?
146  std::size_t component_nr=0;
147 
148  const typet &subtype = components[component_nr].type();
149 
150  const member_exprt member{
151  expr, components[component_nr].get_name(), subtype};
152  return union_exprt(
153  components[component_nr].get_name(),
154  bv_get_rec(member, bv, offset, subtype),
155  union_type);
156  }
157  else if(type.id()==ID_vector)
158  {
159  const typet &subtype = type.subtype();
160  std::size_t sub_width=boolbv_width(subtype);
161 
162  if(sub_width!=0 && width%sub_width==0)
163  {
164  std::size_t size=width/sub_width;
165  vector_exprt value({}, to_vector_type(type));
166  value.reserve_operands(size);
167 
168  for(std::size_t i=0; i<size; i++)
169  {
170  const index_exprt index{expr, from_integer(i, index_type())};
171  value.operands().push_back(
172  bv_get_rec(index, bv, i * sub_width, subtype));
173  }
174 
175  return std::move(value);
176  }
177  }
178  else if(type.id()==ID_complex)
179  {
180  const typet &subtype = type.subtype();
181  std::size_t sub_width=boolbv_width(subtype);
182 
183  if(sub_width!=0 && width==sub_width*2)
184  {
185  const complex_exprt value(
186  bv_get_rec(complex_real_exprt{expr}, bv, 0 * sub_width, subtype),
187  bv_get_rec(complex_imag_exprt{expr}, bv, 1 * sub_width, subtype),
188  to_complex_type(type));
189 
190  return value;
191  }
192  }
193  }
194 
195  // most significant bit first
196  std::string value;
197 
198  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
199  {
200  char ch = '0';
201  // clang-format off
202  switch(prop.l_get(bv[bit_nr]).get_value())
203  {
204  case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
205  case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
206  case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
207  }
208  // clang-format on
209 
210  value=ch+value;
211  }
212 
213  switch(bvtype)
214  {
215  case bvtypet::IS_UNKNOWN:
216  PRECONDITION(type.id() == ID_string || type.id() == ID_empty);
217  if(type.id()==ID_string)
218  {
219  mp_integer int_value=binary2integer(value, false);
220  irep_idt s;
221  if(int_value>=string_numbering.size())
222  s=irep_idt();
223  else
224  s = string_numbering[numeric_cast_v<std::size_t>(int_value)];
225 
226  return constant_exprt(s, type);
227  }
228  else if(type.id() == ID_empty)
229  {
230  return constant_exprt{irep_idt(), type};
231  }
232  break;
233 
234  case bvtypet::IS_RANGE:
235  {
236  mp_integer int_value = binary2integer(value, false);
237  mp_integer from = string2integer(type.get_string(ID_from));
238 
239  return constant_exprt(integer2string(int_value + from), type);
240  break;
241  }
242 
244  case bvtypet::IS_VERILOG_UNSIGNED:
245  case bvtypet::IS_VERILOG_SIGNED:
246  case bvtypet::IS_C_BOOL:
247  case bvtypet::IS_FIXED:
248  case bvtypet::IS_FLOAT:
249  case bvtypet::IS_UNSIGNED:
250  case bvtypet::IS_SIGNED:
251  case bvtypet::IS_BV:
252  case bvtypet::IS_C_ENUM:
253  {
254  const irep_idt bvrep = make_bvrep(
255  width, [&value](size_t i) { return value[value.size() - i - 1] == '1'; });
256  return constant_exprt(bvrep, type);
257  }
258  }
259 
260  UNREACHABLE;
261 }
262 
263 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
264 {
265  return bv_get_rec(nil_exprt{}, bv, 0, type);
266 }
267 
269 {
270  if(expr.type().id()==ID_bool) // boolean?
271  return get(expr);
272 
273  // look up literals in cache
274  bv_cachet::const_iterator it=bv_cache.find(expr);
275  CHECK_RETURN(it != bv_cache.end());
276 
277  return bv_get(it->second, expr.type());
278 }
279 
281 {
282  // first, try to get size
283 
284  const typet &type=expr.type();
285  const exprt &size_expr=to_array_type(type).size();
286  exprt size=simplify_expr(get(size_expr), ns);
287 
288  // get the numeric value, unless it's infinity
289  mp_integer size_mpint = 0;
290 
291  if(size.is_not_nil() && size.id() != ID_infinity)
292  {
293  const auto size_opt = numeric_cast<mp_integer>(size);
294  if(size_opt.has_value() && *size_opt >= 0)
295  size_mpint = *size_opt;
296  }
297 
298  // search array indices
299 
300  typedef std::map<mp_integer, exprt> valuest;
301  valuest values;
302 
303  const auto opt_num = arrays.get_number(expr);
304  if(opt_num.has_value())
305  {
306  // get root
307  const auto number = arrays.find_number(*opt_num);
308 
309  assert(number<index_map.size());
310  index_mapt::const_iterator it=index_map.find(number);
311  assert(it!=index_map.end());
312  const index_sett &index_set=it->second;
313 
314  for(index_sett::const_iterator it1=
315  index_set.begin();
316  it1!=index_set.end();
317  it1++)
318  {
319  index_exprt index(expr, *it1);
320 
321  exprt value=bv_get_cache(index);
322  exprt index_value=bv_get_cache(*it1);
323 
324  if(!index_value.is_nil())
325  {
326  const auto index_mpint = numeric_cast<mp_integer>(index_value);
327 
328  if(index_mpint.has_value())
329  {
330  if(value.is_nil())
331  values[*index_mpint] = exprt(ID_unknown, type.subtype());
332  else
333  values[*index_mpint] = value;
334  }
335  }
336  }
337  }
338 
339  exprt result;
340 
341  if(values.size() != size_mpint)
342  {
343  result = array_list_exprt({}, to_array_type(type));
344 
345  result.operands().reserve(values.size()*2);
346 
347  for(valuest::const_iterator it=values.begin();
348  it!=values.end();
349  it++)
350  {
351  exprt index=from_integer(it->first, size.type());
352  result.copy_to_operands(index, it->second);
353  }
354  }
355  else
356  {
357  // set the size
358  result=exprt(ID_array, type);
359 
360  // allocate operands
361  std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
362  result.operands().resize(size_int, exprt{ID_unknown});
363 
364  // search uninterpreted functions
365 
366  for(valuest::iterator it=values.begin();
367  it!=values.end();
368  it++)
369  if(it->first>=0 && it->first<size_mpint)
370  result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
371  it->second);
372  }
373 
374  return result;
375 }
376 
378  const bvt &bv,
379  std::size_t offset,
380  std::size_t width)
381 {
382  mp_integer value=0;
383  mp_integer weight=1;
384 
385  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
386  {
387  assert(bit_nr<bv.size());
388  switch(prop.l_get(bv[bit_nr]).get_value())
389  {
390  case tvt::tv_enumt::TV_FALSE: break;
391  case tvt::tv_enumt::TV_TRUE: value+=weight; break;
392  case tvt::tv_enumt::TV_UNKNOWN: break;
393  default: assert(false);
394  }
395 
396  weight*=2;
397  }
398 
399  return value;
400 }
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:137
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:141
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:117
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:306
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:536
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
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
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
boolbv_mapt::map_entryt::literal_map
bvt literal_map
Definition: boolbv_map.h:31
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:45
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1689
boolbv_type.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1516
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
irep_idt
dstringt irep_idt
Definition: irep.h:37
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1480
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1034
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:1582
array_typet::size
const exprt & size() const
Definition: std_types.h:765
boolbv_mapt::map_entryt
Definition: boolbv_map.h:28
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:134
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
arrayst::ns
const namespacet & ns
Definition: arrays.h:54
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
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:497
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
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:268
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:468
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1621
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
union_typet
The union type.
Definition: c_types.h:112
boolbvt::get_value
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:84
boolbvt::bv_get_unbounded_array
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:280
boolbv_mapt::get_map_entry
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Definition: boolbv_map.h:55
boolbv_mapt::map_entryt::type
typet type
Definition: boolbv_map.h:30
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:2527
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:225
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:263
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
boolbvt::string_numbering
numberingt< irep_idt > string_numbering
Definition: boolbv.h:277
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:1734
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
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:994
boolbv.h
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1427
exprt::operands
operandst & operands()
Definition: expr.h:96
arrayst::arrays
union_find< exprt, irep_hash > arrays
Definition: arrays.h:76
index_exprt
Array index operator.
Definition: std_expr.h:1242
tvt::get_value
tv_enumt get_value() const
Definition: threeval.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:132
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:1381
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:20
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106