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  exprt value(ID_vector, 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  exprt value(ID_complex, type);
212  value.operands().resize(2);
213 
214  value.op0()=bv_get_rec(bv, unknown, 0*sub_width, subtype);
215  value.op1()=bv_get_rec(bv, unknown, 1*sub_width, subtype);
216 
217  return value;
218  }
219  }
220  }
221 
222  std::string value;
223 
224  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
225  {
226  char ch;
227  if(unknown[bit_nr])
228  ch='0';
229  else
230  {
231  switch(prop.l_get(bv[bit_nr]).get_value())
232  {
233  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
234  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
235  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
236  default: assert(false);
237  }
238  }
239 
240  value=ch+value;
241  }
242 
243  switch(bvtype)
244  {
245  case bvtypet::IS_UNKNOWN:
246  if(type.id()==ID_string)
247  {
248  mp_integer int_value=binary2integer(value, false);
249  irep_idt s;
250  if(int_value>=string_numbering.size())
251  s=irep_idt();
252  else
253  s=string_numbering[int_value.to_long()];
254 
255  return constant_exprt(s, type);
256  }
257  break;
258 
259  case bvtypet::IS_RANGE:
260  {
261  mp_integer int_value=binary2integer(value, false);
262  mp_integer from=string2integer(type.get_string(ID_from));
263 
264  constant_exprt value_expr(type);
265  value_expr.set_value(integer2string(int_value+from));
266  return value_expr;
267  }
268  break;
269 
270  default:
271  case bvtypet::IS_C_ENUM:
272  constant_exprt value_expr(type);
273  value_expr.set_value(value);
274  return value_expr;
275  }
276 
277  return nil_exprt();
278 }
279 
280 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
281 {
282  std::vector<bool> unknown;
283  unknown.resize(bv.size(), false);
284  return bv_get_rec(bv, unknown, 0, type);
285 }
286 
288 {
289  if(expr.type().id()==ID_bool) // boolean?
290  return get(expr);
291 
292  // look up literals in cache
293  bv_cachet::const_iterator it=bv_cache.find(expr);
294  if(it==bv_cache.end())
295  return nil_exprt();
296 
297  return bv_get(it->second, expr.type());
298 }
299 
301 {
302  // first, try to get size
303 
304  const typet &type=expr.type();
305  const exprt &size_expr=to_array_type(type).size();
306  exprt size=simplify_expr(get(size_expr), ns);
307 
308  // no size, give up
309  if(size.is_nil())
310  return nil_exprt();
311 
312  // get the numeric value, unless it's infinity
313  mp_integer size_mpint;
314 
315  if(size.id()!=ID_infinity)
316  {
317  if(to_integer(size, size_mpint))
318  return nil_exprt();
319 
320  // simple sanity check
321  if(size_mpint<0)
322  return nil_exprt();
323  }
324  else
325  size_mpint=0;
326 
327  // search array indices
328 
329  typedef std::map<mp_integer, exprt> valuest;
330  valuest values;
331 
332  {
333  std::size_t number;
334 
335  if(arrays.get_number(expr, number))
336  return nil_exprt();
337 
338  // get root
339  number=arrays.find_number(number);
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  {
378  result=exprt("array-list", type);
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:20
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
BigInt mp_integer
Definition: mp_arith.h:19
literal_mapt literal_map
Definition: boolbv_map.h:53
bool is_nil() const
Definition: irep.h:103
union_find< exprt > arrays
Definition: arrays.h:64
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
index_mapt index_map
Definition: arrays.h:71
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:300
exprt & op0()
Definition: expr.h:84
virtual exprt get(const exprt &expr) const override
Definition: prop_conv.cpp:505
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:191
exprt simplify_expr(const exprt &src, const namespacet &ns)
const exprt & op() const
Definition: std_expr.h:258
std::set< exprt > index_sett
Definition: arrays.h:67
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::vector< componentt > componentst
Definition: std_types.h:240
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:242
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
bool get_number(const T &a, number_type &n) const
Definition: numbering.h:48
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
mappingt mapping
Definition: boolbv_map.h:59
The boolean constant true.
Definition: std_expr.h:3742
The NIL expression.
Definition: std_expr.h:3764
union constructor from single element
Definition: std_expr.h:1389
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
numbering< irep_idt > string_numbering
Definition: boolbv.h:254
const exprt & size() const
Definition: std_types.h:915
const namespacet & ns
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:3753
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:78
API to type classes.
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:536
exprt & index()
Definition: std_expr.h:1208
bv_cachet bv_cache
Definition: boolbv.h:116
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:573
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
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
virtual tvt l_get(literalt a) const =0
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:1415
tv_enumt get_value() const
Definition: threeval.h:40
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
dstringt irep_idt
Definition: irep.h:32
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:280
boolbv_mapt map
Definition: boolbv.h:99
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:287
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1464
exprt & array()
Definition: std_expr.h:1198
std::vector< literalt > bvt
Definition: literal.h:197
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
array index operator
Definition: std_expr.h:1170