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_type)
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(const auto &c : components)
145  {
146  const typet &subtype = ns.follow(c.type());
147  op.push_back(nil_exprt());
148 
149  std::size_t sub_width=boolbv_width(subtype);
150 
151  if(sub_width!=0)
152  {
153  op.back()=bv_get_rec(bv, unknown, offset+new_offset, subtype);
154  new_offset+=sub_width;
155  }
156  }
157 
158  struct_exprt dest(type);
159  dest.operands().swap(op);
160  return std::move(dest);
161  }
162  else if(type.id()==ID_union)
163  {
164  const union_typet &union_type=to_union_type(type);
165  const union_typet::componentst &components=union_type.components();
166 
167  assert(!components.empty());
168 
169  // Any idea that's better than just returning the first component?
170  std::size_t component_nr=0;
171 
172  union_exprt value(union_type);
173 
174  value.set_component_name(
175  components[component_nr].get_name());
176 
177  const typet &subtype=components[component_nr].type();
178 
179  value.op()=bv_get_rec(bv, unknown, offset, subtype);
180 
181  return std::move(value);
182  }
183  else if(type.id()==ID_vector)
184  {
185  const typet &subtype=ns.follow(type.subtype());
186  std::size_t sub_width=boolbv_width(subtype);
187 
188  if(sub_width!=0 && width%sub_width==0)
189  {
190  std::size_t size=width/sub_width;
191  vector_exprt value(to_vector_type(type));
192  value.reserve_operands(size);
193 
194  for(std::size_t i=0; i<size; i++)
195  value.operands().push_back(
196  bv_get_rec(bv, unknown, i*sub_width, subtype));
197 
198  return std::move(value);
199  }
200  }
201  else if(type.id()==ID_complex)
202  {
203  const typet &subtype=ns.follow(type.subtype());
204  std::size_t sub_width=boolbv_width(subtype);
205 
206  if(sub_width!=0 && width==sub_width*2)
207  {
208  const complex_exprt value(
209  bv_get_rec(bv, unknown, 0 * sub_width, subtype),
210  bv_get_rec(bv, unknown, 1 * sub_width, subtype),
211  to_complex_type(type));
212 
213  return value;
214  }
215  }
216  }
217 
218  // most significant bit first
219  std::string value;
220 
221  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
222  {
223  char ch = '0';
224  if(!unknown[bit_nr])
225  {
226  switch(prop.l_get(bv[bit_nr]).get_value())
227  {
228  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
229  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
230  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
231  default: UNREACHABLE;
232  }
233  }
234 
235  value=ch+value;
236  }
237 
238  switch(bvtype)
239  {
240  case bvtypet::IS_UNKNOWN:
241  if(type.id()==ID_string)
242  {
243  mp_integer int_value=binary2integer(value, false);
244  irep_idt s;
245  if(int_value>=string_numbering.size())
246  s=irep_idt();
247  else
248  s = string_numbering[numeric_cast_v<std::size_t>(int_value)];
249 
250  return constant_exprt(s, type);
251  }
252  break;
253 
254  case bvtypet::IS_RANGE:
255  {
256  mp_integer int_value=binary2integer(value, false);
257  mp_integer from=string2integer(type.get_string(ID_from));
258 
259  return constant_exprt(integer2string(int_value + from), type);
260  }
261  break;
262 
263  default:
264  case bvtypet::IS_C_ENUM:
265  {
266  const irep_idt bvrep = make_bvrep(
267  width, [&value](size_t i) { return value[value.size() - i - 1] == '1'; });
268  return constant_exprt(bvrep, type);
269  }
270  }
271 
272  return nil_exprt();
273 }
274 
275 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
276 {
277  std::vector<bool> unknown;
278  unknown.resize(bv.size(), false);
279  return bv_get_rec(bv, unknown, 0, type);
280 }
281 
283 {
284  if(expr.type().id()==ID_bool) // boolean?
285  return get(expr);
286 
287  // look up literals in cache
288  bv_cachet::const_iterator it=bv_cache.find(expr);
289  if(it==bv_cache.end())
290  return nil_exprt();
291 
292  return bv_get(it->second, expr.type());
293 }
294 
296 {
297  // first, try to get size
298 
299  const typet &type=expr.type();
300  const exprt &size_expr=to_array_type(type).size();
301  exprt size=simplify_expr(get(size_expr), ns);
302 
303  // no size, give up
304  if(size.is_nil())
305  return nil_exprt();
306 
307  // get the numeric value, unless it's infinity
308  mp_integer size_mpint;
309 
310  if(size.id()!=ID_infinity)
311  {
312  if(to_integer(size, size_mpint))
313  return nil_exprt();
314 
315  // simple sanity check
316  if(size_mpint<0)
317  return nil_exprt();
318  }
319  else
320  size_mpint=0;
321 
322  // search array indices
323 
324  typedef std::map<mp_integer, exprt> valuest;
325  valuest values;
326 
327  {
328  const auto opt_num = arrays.get_number(expr);
329  if(!opt_num)
330  {
331  return nil_exprt();
332  }
333 
334  // get root
335  const auto number = arrays.find_number(*opt_num);
336 
337  assert(number<index_map.size());
338  index_mapt::const_iterator it=index_map.find(number);
339  assert(it!=index_map.end());
340  const index_sett &index_set=it->second;
341 
342  for(index_sett::const_iterator it1=
343  index_set.begin();
344  it1!=index_set.end();
345  it1++)
346  {
347  index_exprt index;
348  index.type()=type.subtype();
349  index.array()=expr;
350  index.index()=*it1;
351 
352  exprt value=bv_get_cache(index);
353  exprt index_value=bv_get_cache(*it1);
354 
355  if(!index_value.is_nil())
356  {
357  mp_integer index_mpint;
358 
359  if(!to_integer(index_value, index_mpint))
360  {
361  if(value.is_nil())
362  values[index_mpint]=exprt(ID_unknown, type.subtype());
363  else
364  values[index_mpint]=value;
365  }
366  }
367  }
368  }
369 
370  exprt result;
371 
372  if(size_mpint>100 || size.id()==ID_infinity)
373  {
375  result.type().set(ID_size, integer2string(size_mpint));
376 
377  result.operands().reserve(values.size()*2);
378 
379  for(valuest::const_iterator it=values.begin();
380  it!=values.end();
381  it++)
382  {
383  exprt index=from_integer(it->first, size.type());
384  result.copy_to_operands(index, it->second);
385  }
386  }
387  else
388  {
389  // set the size
390  result=exprt(ID_array, type);
391  result.type().set(ID_size, size);
392 
393  std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
394 
395  // allocate operands
396  result.operands().resize(size_int);
397 
398  for(std::size_t i=0; i<size_int; i++)
399  result.operands()[i]=exprt(ID_unknown);
400 
401  // search uninterpreted functions
402 
403  for(valuest::iterator it=values.begin();
404  it!=values.end();
405  it++)
406  if(it->first>=0 && it->first<size_mpint)
407  result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
408  it->second);
409  }
410 
411  return result;
412 }
413 
415  const bvt &bv,
416  std::size_t offset,
417  std::size_t width)
418 {
419  mp_integer value=0;
420  mp_integer weight=1;
421 
422  for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
423  {
424  assert(bit_nr<bv.size());
425  switch(prop.l_get(bv[bit_nr]).get_value())
426  {
427  case tvt::tv_enumt::TV_FALSE: break;
428  case tvt::tv_enumt::TV_TRUE: value+=weight; break;
429  case tvt::tv_enumt::TV_UNKNOWN: break;
430  default: assert(false);
431  }
432 
433  weight*=2;
434  }
435 
436  return value;
437 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:101
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
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:329
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
typet
The type of an expression, extends irept.
Definition: type.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
threeval.h
arrayst::index_map
index_mapt index_map
Definition: arrays.h:71
union_find::find_number
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:202
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
boolbv_type.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
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:203
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition: boolbv_map.h:53
irep_idt
dstringt irep_idt
Definition: irep.h:32
bvtypet::IS_RANGE
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1800
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1838
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
union_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1868
boolbv_mapt::map_entryt::width
std::size_t width
Definition: boolbv_map.h:50
bvtypet
bvtypet
Definition: boolbv_type.h:16
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
array_typet::size
const exprt & size() const
Definition: std_types.h:1010
boolbv_mapt::map_entryt
Definition: boolbv_map.h:43
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
tvt::tv_enumt::TV_TRUE
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:59
messaget::result
mstreamt & result() const
Definition: message.h:396
boolbvt::bv_cache
bv_cachet bv_cache
Definition: boolbv.h:118
boolbvt::string_numbering
numbering< irep_idt > string_numbering
Definition: boolbv.h:256
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
std_types.h
prop_conv_solvert::get
exprt get(const exprt &expr) const override
Definition: prop_conv.cpp:485
arrayst::index_sett
std::set< exprt > index_sett
Definition: arrays.h:67
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
boolbvt::bv_get_cache
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:282
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1962
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
union_typet
The union type.
Definition: std_types.h:425
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
boolbvt::get_value
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:80
boolbvt::bv_get_unbounded_array
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:295
boolbv_mapt::map_entryt::type
typet type
Definition: boolbv_map.h:52
simplify_expr.h
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
bvtypet::IS_C_ENUM
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
union_find::get_number
optionalt< number_type > get_number(const T &a) const
Definition: union_find.h:264
propt::l_get
virtual tvt l_get(literalt a) const =0
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
boolbvt::bv_get
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:275
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
boolbvt::bv_get_rec
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
tvt::tv_enumt::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:1793
boolbv.h
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1779
exprt::operands
operandst & operands()
Definition: expr.h:78
arrayst::arrays
union_find< exprt > arrays
Definition: arrays.h:64
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
index_exprt
Array index operator.
Definition: std_expr.h:1595
tvt::get_value
tv_enumt get_value() const
Definition: threeval.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
tvt::tv_enumt::TV_FALSE
std_expr.h
boolbvt::get
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
bvtypet::IS_UNKNOWN
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106