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 = '0';
226  if(!unknown[bit_nr])
227  {
228  switch(prop.l_get(bv[bit_nr]).get_value())
229  {
230  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
231  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
232  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
233  default: UNREACHABLE;
234  }
235  }
236 
237  value=ch+value;
238  }
239 
240  switch(bvtype)
241  {
242  case bvtypet::IS_UNKNOWN:
243  if(type.id()==ID_string)
244  {
245  mp_integer int_value=binary2integer(value, false);
246  irep_idt s;
247  if(int_value>=string_numbering.size())
248  s=irep_idt();
249  else
250  s = string_numbering[numeric_cast_v<std::size_t>(int_value)];
251 
252  return constant_exprt(s, type);
253  }
254  break;
255 
256  case bvtypet::IS_RANGE:
257  {
258  mp_integer int_value=binary2integer(value, false);
259  mp_integer from=string2integer(type.get_string(ID_from));
260 
261  constant_exprt value_expr(type);
262  value_expr.set_value(integer2string(int_value+from));
263  return value_expr;
264  }
265  break;
266 
267  default:
268  case bvtypet::IS_C_ENUM:
269  constant_exprt value_expr(type);
270  value_expr.set_value(value);
271  return value_expr;
272  }
273 
274  return nil_exprt();
275 }
276 
277 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
278 {
279  std::vector<bool> unknown;
280  unknown.resize(bv.size(), false);
281  return bv_get_rec(bv, unknown, 0, type);
282 }
283 
285 {
286  if(expr.type().id()==ID_bool) // boolean?
287  return get(expr);
288 
289  // look up literals in cache
290  bv_cachet::const_iterator it=bv_cache.find(expr);
291  if(it==bv_cache.end())
292  return nil_exprt();
293 
294  return bv_get(it->second, expr.type());
295 }
296 
298 {
299  // first, try to get size
300 
301  const typet &type=expr.type();
302  const exprt &size_expr=to_array_type(type).size();
303  exprt size=simplify_expr(get(size_expr), ns);
304 
305  // no size, give up
306  if(size.is_nil())
307  return nil_exprt();
308 
309  // get the numeric value, unless it's infinity
310  mp_integer size_mpint;
311 
312  if(size.id()!=ID_infinity)
313  {
314  if(to_integer(size, size_mpint))
315  return nil_exprt();
316 
317  // simple sanity check
318  if(size_mpint<0)
319  return nil_exprt();
320  }
321  else
322  size_mpint=0;
323 
324  // search array indices
325 
326  typedef std::map<mp_integer, exprt> valuest;
327  valuest values;
328 
329  {
330  const auto opt_num = arrays.get_number(expr);
331  if(!opt_num)
332  {
333  return nil_exprt();
334  }
335 
336  // get root
337  const auto number = arrays.find_number(*opt_num);
338 
339  assert(number<index_map.size());
340  index_mapt::const_iterator it=index_map.find(number);
341  assert(it!=index_map.end());
342  const index_sett &index_set=it->second;
343 
344  for(index_sett::const_iterator it1=
345  index_set.begin();
346  it1!=index_set.end();
347  it1++)
348  {
349  index_exprt index;
350  index.type()=type.subtype();
351  index.array()=expr;
352  index.index()=*it1;
353 
354  exprt value=bv_get_cache(index);
355  exprt index_value=bv_get_cache(*it1);
356 
357  if(!index_value.is_nil())
358  {
359  mp_integer index_mpint;
360 
361  if(!to_integer(index_value, index_mpint))
362  {
363  if(value.is_nil())
364  values[index_mpint]=exprt(ID_unknown, type.subtype());
365  else
366  values[index_mpint]=value;
367  }
368  }
369  }
370  }
371 
372  exprt result;
373 
374  if(size_mpint>100 || size.id()==ID_infinity)
375  {
377  result.type().set(ID_size, integer2string(size_mpint));
378 
379  result.operands().reserve(values.size()*2);
380 
381  for(valuest::const_iterator it=values.begin();
382  it!=values.end();
383  it++)
384  {
385  exprt index=from_integer(it->first, size.type());
386  result.copy_to_operands(index, it->second);
387  }
388  }
389  else
390  {
391  // set the size
392  result=exprt(ID_array, type);
393  result.type().set(ID_size, size);
394 
395  std::size_t size_int=integer2size_t(size_mpint);
396 
397  // allocate operands
398  result.operands().resize(size_int);
399 
400  for(std::size_t i=0; i<size_int; i++)
401  result.operands()[i]=exprt(ID_unknown);
402 
403  // search uninterpreted functions
404 
405  for(valuest::iterator it=values.begin();
406  it!=values.end();
407  it++)
408  if(it->first>=0 && it->first<size_mpint)
409  result.operands()[integer2size_t(it->first)].swap(it->second);
410  }
411 
412  return result;
413 }
414 
416  const bvt &bv,
417  std::size_t offset,
418  std::size_t width)
419 {
420  mp_integer value=0;
421  mp_integer weight=1;
422 
423  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
424  {
425  assert(bit_nr<bv.size());
426  switch(prop.l_get(bv[bit_nr]).get_value())
427  {
428  case tvt::tv_enumt::TV_FALSE: break;
429  case tvt::tv_enumt::TV_TRUE: value+=weight; break;
430  case tvt::tv_enumt::TV_UNKNOWN: break;
431  default: assert(false);
432  }
433 
434  weight*=2;
435  }
436 
437  return value;
438 }
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:172
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:297
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:4422
Structure type.
Definition: std_types.h:297
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
const irep_idt & id() const
Definition: irep.h:259
void set_value(const irep_idt &value)
Definition: std_expr.h:4444
mappingt mapping
Definition: boolbv_map.h:59
The boolean constant true.
Definition: std_expr.h:4486
The NIL expression.
Definition: std_expr.h:4508
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:254
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1023
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:4497
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:1054
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:271
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1709
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
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:32
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:277
boolbv_mapt map
Definition: boolbv.h:99
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:284
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