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/std_expr.h>
15 #include <util/threeval.h>
16 #include <util/std_types.h>
17 #include <util/simplify_expr.h>
18 
19 #include "boolbv_type.h"
20 
21 exprt 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  boolbv_mapt::mappingt::const_iterator it=
29  map.mapping.find(identifier);
30 
31  if(it!=map.mapping.end())
32  {
33  const boolbv_mapt::map_entryt &map_entry=it->second;
34 
35  if(is_unbounded_array(map_entry.type))
36  return bv_get_unbounded_array(expr);
37 
38  std::vector<bool> unknown;
39  bvt bv;
40  std::size_t width=map_entry.width;
41 
42  bv.resize(width);
43  unknown.resize(width);
44 
45  for(std::size_t bit_nr=0; bit_nr<width; bit_nr++)
46  {
47  assert(bit_nr<map_entry.literal_map.size());
48 
49  if(map_entry.literal_map[bit_nr].is_set)
50  {
51  unknown[bit_nr]=false;
52  bv[bit_nr]=map_entry.literal_map[bit_nr].l;
53  }
54  else
55  {
56  unknown[bit_nr]=true;
57  bv[bit_nr].clear();
58  }
59  }
60 
61  return bv_get_rec(bv, unknown, 0, map_entry.type);
62  }
63  }
64 
65  return SUB::get(expr);
66 }
67 
69  const bvt &bv,
70  const std::vector<bool> &unknown,
71  std::size_t offset,
72  const typet &type) const
73 {
74  if(type.id()==ID_symbol)
75  return bv_get_rec(bv, unknown, offset, ns.follow(type));
76 
77  std::size_t width=boolbv_width(type);
78 
79  assert(bv.size()==unknown.size());
80  assert(bv.size()>=offset+width);
81 
82  if(type.id()==ID_bool)
83  {
84  if(!unknown[offset])
85  {
86  switch(prop.l_get(bv[offset]).get_value())
87  {
88  case tvt::tv_enumt::TV_FALSE: return false_exprt();
89  case tvt::tv_enumt::TV_TRUE: return true_exprt();
90  default: return false_exprt(); // default
91  }
92  }
93 
94  return nil_exprt();
95  }
96 
97  bvtypet bvtype=get_bvtype(type);
98 
99  if(bvtype==bvtypet::IS_UNKNOWN)
100  {
101  if(type.id()==ID_array)
102  {
103  const typet &subtype=type.subtype();
104  std::size_t sub_width=boolbv_width(subtype);
105 
106  if(sub_width!=0)
107  {
108  exprt::operandst op;
109  op.reserve(width/sub_width);
110 
111  for(std::size_t new_offset=0;
112  new_offset<width;
113  new_offset+=sub_width)
114  {
115  op.push_back(
116  bv_get_rec(bv, unknown, offset+new_offset, subtype));
117  }
118 
119  exprt dest=exprt(ID_array, type);
120  dest.operands().swap(op);
121  return dest;
122  }
123  }
124  else if(type.id()==ID_struct_tag)
125  {
126  return
127  bv_get_rec(
128  bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
129  }
130  else if(type.id()==ID_union_tag)
131  {
132  return
133  bv_get_rec(
134  bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
135  }
136  else if(type.id()==ID_struct)
137  {
138  const struct_typet &struct_type=to_struct_type(type);
139  const struct_typet::componentst &components=struct_type.components();
140  std::size_t new_offset=0;
141  exprt::operandst op;
142  op.reserve(components.size());
143 
144  for(struct_typet::componentst::const_iterator
145  it=components.begin();
146  it!=components.end();
147  it++)
148  {
149  const typet &subtype=ns.follow(it->type());
150  op.push_back(nil_exprt());
151 
152  std::size_t sub_width=boolbv_width(subtype);
153 
154  if(sub_width!=0)
155  {
156  op.back()=bv_get_rec(bv, unknown, offset+new_offset, subtype);
157  new_offset+=sub_width;
158  }
159  }
160 
161  struct_exprt dest(type);
162  dest.operands().swap(op);
163  return dest;
164  }
165  else if(type.id()==ID_union)
166  {
167  const union_typet &union_type=to_union_type(type);
168  const union_typet::componentst &components=union_type.components();
169 
170  assert(!components.empty());
171 
172  // Any idea that's better than just returning the first component?
173  std::size_t component_nr=0;
174 
175  union_exprt value(union_type);
176 
177  value.set_component_name(
178  components[component_nr].get_name());
179 
180  const typet &subtype=components[component_nr].type();
181 
182  value.op()=bv_get_rec(bv, unknown, offset, subtype);
183 
184  return value;
185  }
186  else if(type.id()==ID_vector)
187  {
188  const typet &subtype=ns.follow(type.subtype());
189  std::size_t sub_width=boolbv_width(subtype);
190 
191  if(sub_width!=0 && width%sub_width==0)
192  {
193  std::size_t size=width/sub_width;
194  vector_exprt value(to_vector_type(type));
195  value.reserve_operands(size);
196 
197  for(std::size_t i=0; i<size; i++)
198  value.operands().push_back(
199  bv_get_rec(bv, unknown, i*sub_width, subtype));
200 
201  return value;
202  }
203  }
204  else if(type.id()==ID_complex)
205  {
206  const typet &subtype=ns.follow(type.subtype());
207  std::size_t sub_width=boolbv_width(subtype);
208 
209  if(sub_width!=0 && width==sub_width*2)
210  {
211  const complex_exprt value(
212  bv_get_rec(bv, unknown, 0 * sub_width, subtype),
213  bv_get_rec(bv, unknown, 1 * sub_width, subtype),
214  to_complex_type(type));
215 
216  return value;
217  }
218  }
219  }
220 
221  std::string value;
222 
223  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
224  {
225  char ch;
226  if(unknown[bit_nr])
227  ch='0';
228  else
229  {
230  switch(prop.l_get(bv[bit_nr]).get_value())
231  {
232  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
233  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
234  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
235  default: UNREACHABLE;
236  }
237  }
238 
239  value=ch+value;
240  }
241 
242  switch(bvtype)
243  {
244  case bvtypet::IS_UNKNOWN:
245  if(type.id()==ID_string)
246  {
247  mp_integer int_value=binary2integer(value, false);
248  irep_idt s;
249  if(int_value>=string_numbering.size())
250  s=irep_idt();
251  else
252  s=string_numbering[int_value.to_long()];
253 
254  return constant_exprt(s, type);
255  }
256  break;
257 
258  case bvtypet::IS_RANGE:
259  {
260  mp_integer int_value=binary2integer(value, false);
261  mp_integer from=string2integer(type.get_string(ID_from));
262 
263  constant_exprt value_expr(type);
264  value_expr.set_value(integer2string(int_value+from));
265  return value_expr;
266  }
267  break;
268 
269  default:
270  case bvtypet::IS_C_ENUM:
271  constant_exprt value_expr(type);
272  value_expr.set_value(value);
273  return value_expr;
274  }
275 
276  return nil_exprt();
277 }
278 
279 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
280 {
281  std::vector<bool> unknown;
282  unknown.resize(bv.size(), false);
283  return bv_get_rec(bv, unknown, 0, type);
284 }
285 
287 {
288  if(expr.type().id()==ID_bool) // boolean?
289  return get(expr);
290 
291  // look up literals in cache
292  bv_cachet::const_iterator it=bv_cache.find(expr);
293  if(it==bv_cache.end())
294  return nil_exprt();
295 
296  return bv_get(it->second, expr.type());
297 }
298 
300 {
301  // first, try to get size
302 
303  const typet &type=expr.type();
304  const exprt &size_expr=to_array_type(type).size();
305  exprt size=simplify_expr(get(size_expr), ns);
306 
307  // no size, give up
308  if(size.is_nil())
309  return nil_exprt();
310 
311  // get the numeric value, unless it's infinity
312  mp_integer size_mpint;
313 
314  if(size.id()!=ID_infinity)
315  {
316  if(to_integer(size, size_mpint))
317  return nil_exprt();
318 
319  // simple sanity check
320  if(size_mpint<0)
321  return nil_exprt();
322  }
323  else
324  size_mpint=0;
325 
326  // search array indices
327 
328  typedef std::map<mp_integer, exprt> valuest;
329  valuest values;
330 
331  {
332  const auto opt_num = arrays.get_number(expr);
333  if(!opt_num)
334  {
335  return nil_exprt();
336  }
337 
338  // get root
339  const auto number = arrays.find_number(*opt_num);
340 
341  assert(number<index_map.size());
342  index_mapt::const_iterator it=index_map.find(number);
343  assert(it!=index_map.end());
344  const index_sett &index_set=it->second;
345 
346  for(index_sett::const_iterator it1=
347  index_set.begin();
348  it1!=index_set.end();
349  it1++)
350  {
351  index_exprt index;
352  index.type()=type.subtype();
353  index.array()=expr;
354  index.index()=*it1;
355 
356  exprt value=bv_get_cache(index);
357  exprt index_value=bv_get_cache(*it1);
358 
359  if(!index_value.is_nil())
360  {
361  mp_integer index_mpint;
362 
363  if(!to_integer(index_value, index_mpint))
364  {
365  if(value.is_nil())
366  values[index_mpint]=exprt(ID_unknown, type.subtype());
367  else
368  values[index_mpint]=value;
369  }
370  }
371  }
372  }
373 
374  exprt result;
375 
376  if(size_mpint>100 || size.id()==ID_infinity)
377  {
379  result.type().set(ID_size, integer2string(size_mpint));
380 
381  result.operands().reserve(values.size()*2);
382 
383  for(valuest::const_iterator it=values.begin();
384  it!=values.end();
385  it++)
386  {
387  exprt index=from_integer(it->first, size.type());
388  result.copy_to_operands(index, it->second);
389  }
390  }
391  else
392  {
393  // set the size
394  result=exprt(ID_array, type);
395  result.type().set(ID_size, size);
396 
397  std::size_t size_int=integer2size_t(size_mpint);
398 
399  // allocate operands
400  result.operands().resize(size_int);
401 
402  for(std::size_t i=0; i<size_int; i++)
403  result.operands()[i]=exprt(ID_unknown);
404 
405  // search uninterpreted functions
406 
407  for(valuest::iterator it=values.begin();
408  it!=values.end();
409  it++)
410  if(it->first>=0 && it->first<size_mpint)
411  result.operands()[integer2size_t(it->first)].swap(it->second);
412  }
413 
414  return result;
415 }
416 
418  const bvt &bv,
419  std::size_t offset,
420  std::size_t width)
421 {
422  mp_integer value=0;
423  mp_integer weight=1;
424 
425  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
426  {
427  assert(bit_nr<bv.size());
428  switch(prop.l_get(bv[bit_nr]).get_value())
429  {
430  case tvt::tv_enumt::TV_FALSE: break;
431  case tvt::tv_enumt::TV_TRUE: value+=weight; break;
432  case tvt::tv_enumt::TV_UNKNOWN: break;
433  default: assert(false);
434  }
435 
436  weight*=2;
437  }
438 
439  return value;
440 }
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
literal_mapt literal_map
Definition: boolbv_map.h:53
bool is_nil() const
Definition: irep.h:102
union_find< exprt > arrays
Definition: arrays.h:64
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
index_mapt index_map
Definition: arrays.h:71
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:299
exprt get(const exprt &expr) const override
Definition: prop_conv.cpp:485
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:198
exprt simplify_expr(const exprt &src, const namespacet &ns)
const exprt & op() const
Definition: std_expr.h:340
std::set< exprt > index_sett
Definition: arrays.h:67
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
std::vector< componentt > componentst
Definition: std_types.h:243
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4424
Structure type.
Definition: std_types.h:297
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:74
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:4446
mappingt mapping
Definition: boolbv_map.h:59
The boolean constant true.
Definition: std_expr.h:4488
The NIL expression.
Definition: std_expr.h:4510
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
union constructor from single element
Definition: std_expr.h:1730
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
numbering< irep_idt > string_numbering
Definition: boolbv.h:256
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1014
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
vector constructor from list of elements
Definition: std_expr.h:1684
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
bvtypet
Definition: boolbv_type.h:16
The boolean constant false.
Definition: std_expr.h:4499
std::vector< exprt > operandst
Definition: expr.h:45
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:78
optionalt< number_type > get_number(const T &a) const
Definition: union_find.h:260
API to type classes.
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
mstreamt & result() const
Definition: message.h:312
exprt & index()
Definition: std_expr.h:1496
bv_cachet bv_cache
Definition: boolbv.h:116
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
The union type.
Definition: std_types.h:458
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:68
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
virtual tvt l_get(literalt a) const =0
#define UNREACHABLE
Definition: invariant.h:250
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1700
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1756
tv_enumt get_value() const
Definition: threeval.h:40
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
dstringt irep_idt
Definition: irep.h:31
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:279
boolbv_mapt map
Definition: boolbv.h:99
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:286
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815
exprt & array()
Definition: std_expr.h:1486
std::vector< literalt > bvt
Definition: literal.h:200
complex constructor from a pair of numbers
Definition: std_expr.h:1861
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1662
array index operator
Definition: std_expr.h:1462