cprover
bv_pointers.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 "bv_pointers.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/byte_operators.h>
13 #include <util/c_types.h>
14 #include <util/config.h>
15 #include <util/exception_utils.h>
16 #include <util/namespace.h>
17 #include <util/pointer_expr.h>
20 
26 {
27 public:
29  const typet &type,
30  bool little_endian,
31  const namespacet &_ns,
32  const boolbv_widtht &_boolbv_width)
33  : endianness_mapt(_ns), boolbv_width(_boolbv_width)
34  {
35  build(type, little_endian);
36  }
37 
38 protected:
40 
41  void build_little_endian(const typet &type) override;
42  void build_big_endian(const typet &type) override;
43 };
44 
46 {
47  const std::size_t width = boolbv_width(src);
48 
49  if(width == 0)
50  return;
51 
52  const std::size_t new_size = map.size() + width;
53  map.reserve(new_size);
54 
55  for(std::size_t i = map.size(); i < new_size; ++i)
56  map.push_back(i);
57 }
58 
60 {
61  if(src.id() == ID_pointer)
63  else
65 }
66 
68 bv_pointerst::endianness_map(const typet &type, bool little_endian) const
69 {
70  return bv_endianness_mapt{type, little_endian, ns, bv_pointers_width};
71 }
72 
74 operator()(const typet &type) const
75 {
76  if(type.id() != ID_pointer)
77  return boolbv_widtht::operator()(type);
78 
79  // check or update the cache, just like boolbv_widtht does
80  std::pair<cachet::iterator, bool> cache_result =
81  cache.insert(std::pair<typet, entryt>(type, entryt()));
82 
83  if(cache_result.second)
84  {
85  std::size_t &total_width = cache_result.first->second.total_width;
86 
87  total_width = get_address_width(to_pointer_type(type));
88  DATA_INVARIANT(total_width > 0, "pointer width shall be greater than zero");
89  }
90 
91  return cache_result.first->second.total_width;
92 }
93 
95  const pointer_typet &type) const
96 {
97  // not actually type-dependent for now
98  (void)type;
100 }
101 
103  const pointer_typet &type) const
104 {
105  const std::size_t pointer_width = type.get_width();
106  const std::size_t object_width = get_object_width(type);
107  PRECONDITION(pointer_width >= object_width);
108  return pointer_width - object_width;
109 }
110 
112  const pointer_typet &type) const
113 {
114  return type.get_width();
115 }
116 
118 {
119  PRECONDITION(expr.type().id() == ID_bool);
120 
121  const exprt::operandst &operands=expr.operands();
122 
123  if(expr.id() == ID_is_invalid_pointer)
124  {
125  if(operands.size()==1 &&
126  operands[0].type().id()==ID_pointer)
127  {
128  const bvt &bv=convert_bv(operands[0]);
129 
130  if(!bv.empty())
131  {
132  const pointer_typet &type = to_pointer_type(operands[0].type());
133  bvt object_bv = object_literals(bv, type);
134 
135  bvt invalid_bv = object_literals(
136  encode(pointer_logic.get_invalid_object(), type), type);
137 
138  const std::size_t object_bits =
140 
141  bvt equal_invalid_bv;
142  equal_invalid_bv.reserve(object_bits);
143 
144  for(std::size_t i=0; i<object_bits; i++)
145  {
146  equal_invalid_bv.push_back(prop.lequal(object_bv[i], invalid_bv[i]));
147  }
148 
149  return prop.land(equal_invalid_bv);
150  }
151  }
152  }
153  else if(expr.id() == ID_is_dynamic_object)
154  {
155  if(operands.size()==1 &&
156  operands[0].type().id()==ID_pointer)
157  {
158  // we postpone
160 
161  postponed_list.emplace_back(bvt{1, l}, convert_bv(operands[0]), expr);
162 
163  return l;
164  }
165  }
166  else if(expr.id()==ID_lt || expr.id()==ID_le ||
167  expr.id()==ID_gt || expr.id()==ID_ge)
168  {
169  if(operands.size()==2 &&
170  operands[0].type().id()==ID_pointer &&
171  operands[1].type().id()==ID_pointer)
172  {
173  const bvt &bv0=convert_bv(operands[0]);
174  const bvt &bv1=convert_bv(operands[1]);
175 
176  const pointer_typet &type0 = to_pointer_type(operands[0].type());
177  bvt offset_bv0 = offset_literals(bv0, type0);
178 
179  const pointer_typet &type1 = to_pointer_type(operands[1].type());
180  bvt offset_bv1 = offset_literals(bv1, type1);
181 
182  // Comparison over pointers to distinct objects is undefined behavior in
183  // C; we choose to always produce "false" in such a case. Alternatively,
184  // we could do a comparison over the integer representation of a pointer
185 
186  // do the same-object-test via an expression as this may permit re-using
187  // already cached encodings of the equality test
188  const exprt same_object = ::same_object(operands[0], operands[1]);
189  const literalt same_object_lit = convert(same_object);
190  if(same_object_lit.is_false())
191  return same_object_lit;
192 
193  return prop.land(
194  same_object_lit,
195  bv_utils.rel(
196  offset_bv0,
197  expr.id(),
198  offset_bv1,
200  }
201  }
202 
203  return SUB::convert_rest(expr);
204 }
205 
207  const namespacet &_ns,
208  propt &_prop,
212  pointer_logic(_ns),
213  bv_pointers_width(_ns)
214 {
215 }
216 
218 {
219  if(expr.id()==ID_symbol)
220  {
221  return add_addr(expr);
222  }
223  else if(expr.id()==ID_label)
224  {
225  return add_addr(expr);
226  }
227  else if(expr.id() == ID_null_object)
228  {
229  pointer_typet pt = pointer_type(expr.type());
230  return encode(pointer_logic.get_null_object(), pt);
231  }
232  else if(expr.id()==ID_index)
233  {
234  const index_exprt &index_expr=to_index_expr(expr);
235  const exprt &array=index_expr.array();
236  const exprt &index=index_expr.index();
237  const auto &array_type = to_array_type(array.type());
238 
239  pointer_typet type = pointer_type(expr.type());
240  const std::size_t bits = boolbv_width(type);
241 
242  bvt bv;
243 
244  // recursive call
245  if(array_type.id()==ID_pointer)
246  {
247  // this should be gone
248  bv=convert_pointer_type(array);
249  CHECK_RETURN(bv.size()==bits);
250  }
251  else if(array_type.id()==ID_array ||
252  array_type.id()==ID_string_constant)
253  {
254  auto bv_opt = convert_address_of_rec(array);
255  if(!bv_opt.has_value())
256  return {};
257  bv = std::move(*bv_opt);
258  CHECK_RETURN(bv.size()==bits);
259  }
260  else
261  UNREACHABLE;
262 
263  // get size
264  auto size = pointer_offset_size(array_type.element_type(), ns);
265  CHECK_RETURN(size.has_value() && *size >= 0);
266 
267  bv = offset_arithmetic(type, bv, *size, index);
268  CHECK_RETURN(bv.size()==bits);
269 
270  return std::move(bv);
271  }
272  else if(expr.id()==ID_byte_extract_little_endian ||
273  expr.id()==ID_byte_extract_big_endian)
274  {
275  const auto &byte_extract_expr=to_byte_extract_expr(expr);
276 
277  // recursive call
278  auto bv_opt = convert_address_of_rec(byte_extract_expr.op());
279  if(!bv_opt.has_value())
280  return {};
281 
282  pointer_typet type = pointer_type(expr.type());
283  const std::size_t bits = boolbv_width(type);
284  CHECK_RETURN(bv_opt->size() == bits);
285 
286  bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
287  CHECK_RETURN(bv.size()==bits);
288  return std::move(bv);
289  }
290  else if(expr.id()==ID_member)
291  {
292  const member_exprt &member_expr=to_member_expr(expr);
293  const exprt &struct_op = member_expr.compound();
294  const typet &struct_op_type=ns.follow(struct_op.type());
295 
296  // recursive call
297  auto bv_opt = convert_address_of_rec(struct_op);
298  if(!bv_opt.has_value())
299  return {};
300 
301  bvt bv = std::move(*bv_opt);
302  if(struct_op_type.id()==ID_struct)
303  {
304  auto offset = member_offset(
305  to_struct_type(struct_op_type), member_expr.get_component_name(), ns);
306  CHECK_RETURN(offset.has_value());
307 
308  // add offset
309  pointer_typet type = pointer_type(expr.type());
310  bv = offset_arithmetic(type, bv, *offset);
311  }
312  else
313  {
314  INVARIANT(
315  struct_op_type.id() == ID_union,
316  "member expression should operate on struct or union");
317  // nothing to do, all members have offset 0
318  }
319 
320  return std::move(bv);
321  }
322  else if(expr.id()==ID_constant ||
323  expr.id()==ID_string_constant ||
324  expr.id()==ID_array)
325  { // constant
326  return add_addr(expr);
327  }
328  else if(expr.id()==ID_if)
329  {
330  const if_exprt &ifex=to_if_expr(expr);
331 
332  literalt cond=convert(ifex.cond());
333 
334  bvt bv1, bv2;
335 
336  auto bv1_opt = convert_address_of_rec(ifex.true_case());
337  if(!bv1_opt.has_value())
338  return {};
339 
340  auto bv2_opt = convert_address_of_rec(ifex.false_case());
341  if(!bv2_opt.has_value())
342  return {};
343 
344  return bv_utils.select(cond, *bv1_opt, *bv2_opt);
345  }
346 
347  return {};
348 }
349 
351 {
352  const pointer_typet &type = to_pointer_type(expr.type());
353 
354  const std::size_t bits = boolbv_width(expr.type());
355 
356  if(expr.id()==ID_symbol)
357  {
358  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
359 
360  return map.get_literals(identifier, type, bits);
361  }
362  else if(expr.id()==ID_nondet_symbol)
363  {
364  return prop.new_variables(bits);
365  }
366  else if(expr.id()==ID_typecast)
367  {
368  const typecast_exprt &typecast_expr = to_typecast_expr(expr);
369 
370  const exprt &op = typecast_expr.op();
371  const typet &op_type = op.type();
372 
373  if(op_type.id()==ID_pointer)
374  return convert_bv(op);
375  else if(
376  can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_bool ||
377  op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
378  {
379  // Cast from a bitvector type to pointer.
380  // We just do a zero extension.
381 
382  const bvt &op_bv=convert_bv(op);
383 
384  return bv_utils.zero_extension(op_bv, bits);
385  }
386  }
387  else if(expr.id()==ID_if)
388  {
389  return SUB::convert_if(to_if_expr(expr));
390  }
391  else if(expr.id()==ID_index)
392  {
393  return SUB::convert_index(to_index_expr(expr));
394  }
395  else if(expr.id()==ID_member)
396  {
397  return SUB::convert_member(to_member_expr(expr));
398  }
399  else if(expr.id()==ID_address_of)
400  {
401  const address_of_exprt &address_of_expr = to_address_of_expr(expr);
402 
403  auto bv_opt = convert_address_of_rec(address_of_expr.op());
404  if(!bv_opt.has_value())
405  return conversion_failed(address_of_expr);
406 
407  CHECK_RETURN(bv_opt->size() == bits);
408  return *bv_opt;
409  }
410  else if(expr.id()==ID_constant)
411  {
412  irep_idt value=to_constant_expr(expr).get_value();
413 
414  if(value==ID_NULL)
415  return encode(pointer_logic.get_null_object(), type);
416  else
417  {
418  mp_integer i = bvrep2integer(value, bits, false);
419  return bv_utils.build_constant(i, bits);
420  }
421  }
422  else if(expr.id()==ID_plus)
423  {
424  // this has to be pointer plus integer
425 
426  const plus_exprt &plus_expr = to_plus_expr(expr);
427 
428  bvt bv;
429 
430  mp_integer size=0;
431  std::size_t count=0;
432 
433  forall_operands(it, plus_expr)
434  {
435  if(it->type().id()==ID_pointer)
436  {
437  count++;
438  bv=convert_bv(*it);
439  CHECK_RETURN(bv.size()==bits);
440 
441  typet pointer_base_type = to_pointer_type(it->type()).base_type();
442 
443  if(pointer_base_type.id() == ID_empty)
444  {
445  // This is a gcc extension.
446  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
447  size = 1;
448  }
449  else
450  {
451  auto size_opt = pointer_offset_size(pointer_base_type, ns);
452  CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
453  size = *size_opt;
454  }
455  }
456  }
457 
458  INVARIANT(
459  count == 1,
460  "there should be exactly one pointer-type operand in a pointer-type sum");
461 
462  const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
463  bvt sum = bv_utils.build_constant(0, offset_bits);
464 
465  forall_operands(it, plus_expr)
466  {
467  if(it->type().id()==ID_pointer)
468  continue;
469 
470  if(it->type().id()!=ID_unsignedbv &&
471  it->type().id()!=ID_signedbv)
472  {
473  return conversion_failed(plus_expr);
474  }
475 
477  it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
479 
480  bvt op=convert_bv(*it);
481  CHECK_RETURN(!op.empty());
482 
483  op = bv_utils.extension(op, offset_bits, rep);
484 
485  sum=bv_utils.add(sum, op);
486  }
487 
488  return offset_arithmetic(type, bv, size, sum);
489  }
490  else if(expr.id()==ID_minus)
491  {
492  // this is pointer-integer
493 
494  const minus_exprt &minus_expr = to_minus_expr(expr);
495 
496  INVARIANT(
497  minus_expr.lhs().type().id() == ID_pointer,
498  "first operand should be of pointer type");
499 
500  if(
501  minus_expr.rhs().type().id() != ID_unsignedbv &&
502  minus_expr.rhs().type().id() != ID_signedbv)
503  {
504  return conversion_failed(minus_expr);
505  }
506 
507  const unary_minus_exprt neg_op1(minus_expr.rhs());
508 
509  const bvt &bv = convert_bv(minus_expr.lhs());
510 
511  typet pointer_base_type =
512  to_pointer_type(minus_expr.lhs().type()).base_type();
513  mp_integer element_size;
514 
515  if(pointer_base_type.id() == ID_empty)
516  {
517  // This is a gcc extension.
518  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
519  element_size = 1;
520  }
521  else
522  {
523  auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
524  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
525  element_size = *element_size_opt;
526  }
527 
528  return offset_arithmetic(type, bv, element_size, neg_op1);
529  }
530  else if(expr.id()==ID_byte_extract_little_endian ||
531  expr.id()==ID_byte_extract_big_endian)
532  {
534  }
535  else if(
536  expr.id() == ID_byte_update_little_endian ||
537  expr.id() == ID_byte_update_big_endian)
538  {
540  }
541 
542  return conversion_failed(expr);
543 }
544 
545 static bool is_pointer_subtraction(const exprt &expr)
546 {
547  if(expr.id() != ID_minus)
548  return false;
549 
550  const auto &minus_expr = to_minus_expr(expr);
551 
552  return minus_expr.lhs().type().id() == ID_pointer &&
553  minus_expr.rhs().type().id() == ID_pointer;
554 }
555 
557 {
558  if(expr.type().id()==ID_pointer)
559  return convert_pointer_type(expr);
560 
561  if(is_pointer_subtraction(expr))
562  {
563  std::size_t width=boolbv_width(expr.type());
564 
565  if(width==0)
566  return conversion_failed(expr);
567 
568  // pointer minus pointer is subtraction over the offset divided by element
569  // size, iff the pointers point to the same object
570  const auto &minus_expr = to_minus_expr(expr);
571 
572  // do the same-object-test via an expression as this may permit re-using
573  // already cached encodings of the equality test
574  const exprt same_object = ::same_object(minus_expr.lhs(), minus_expr.rhs());
575  const literalt same_object_lit = convert(same_object);
576 
577  // compute the object size (again, possibly using cached results)
578  const exprt object_size = ::object_size(minus_expr.lhs());
579  const bvt object_size_bv =
581 
582  bvt bv = prop.new_variables(width);
583 
584  if(!same_object_lit.is_false())
585  {
586  const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type());
587  const bvt &lhs = convert_bv(minus_expr.lhs());
588  const bvt lhs_offset =
589  bv_utils.sign_extension(offset_literals(lhs, lhs_pt), width);
590 
591  const literalt lhs_in_bounds = prop.land(
592  !bv_utils.sign_bit(lhs_offset),
593  bv_utils.rel(
594  lhs_offset,
595  ID_le,
596  object_size_bv,
598 
599  const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type());
600  const bvt &rhs = convert_bv(minus_expr.rhs());
601  const bvt rhs_offset =
602  bv_utils.sign_extension(offset_literals(rhs, rhs_pt), width);
603 
604  const literalt rhs_in_bounds = prop.land(
605  !bv_utils.sign_bit(rhs_offset),
606  bv_utils.rel(
607  rhs_offset,
608  ID_le,
609  object_size_bv,
611 
612  bvt difference = bv_utils.sub(lhs_offset, rhs_offset);
613 
614  // Support for void* is a gcc extension, with the size treated as 1 byte
615  // (no division required below).
616  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
617  if(lhs_pt.base_type().id() != ID_empty)
618  {
619  auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
620  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
621 
622  if(*element_size_opt != 1)
623  {
624  bvt element_size_bv =
625  bv_utils.build_constant(*element_size_opt, width);
626  difference = bv_utils.divider(
627  difference, element_size_bv, bv_utilst::representationt::SIGNED);
628  }
629  }
630 
632  prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
633  bv_utils.equal(difference, bv)));
634  }
635 
636  return bv;
637  }
638  else if(
639  expr.id() == ID_pointer_offset &&
640  to_unary_expr(expr).op().type().id() == ID_pointer)
641  {
642  std::size_t width=boolbv_width(expr.type());
643 
644  if(width==0)
645  return conversion_failed(expr);
646 
647  const exprt &op0 = to_unary_expr(expr).op();
648  const bvt &op0_bv = convert_bv(op0);
649 
650  bvt offset_bv = offset_literals(op0_bv, to_pointer_type(op0.type()));
651 
652  // we do a sign extension to permit negative offsets
653  return bv_utils.sign_extension(offset_bv, width);
654  }
655  else if(
656  expr.id() == ID_object_size &&
657  to_unary_expr(expr).op().type().id() == ID_pointer)
658  {
659  // we postpone until we know the objects
660  std::size_t width=boolbv_width(expr.type());
661 
662  postponed_list.emplace_back(
663  prop.new_variables(width), convert_bv(to_unary_expr(expr).op()), expr);
664 
665  return postponed_list.back().bv;
666  }
667  else if(
668  expr.id() == ID_pointer_object &&
669  to_unary_expr(expr).op().type().id() == ID_pointer)
670  {
671  std::size_t width=boolbv_width(expr.type());
672 
673  if(width==0)
674  return conversion_failed(expr);
675 
676  const exprt &op0 = to_unary_expr(expr).op();
677  const bvt &op0_bv = convert_bv(op0);
678 
679  bvt object_bv = object_literals(op0_bv, to_pointer_type(op0.type()));
680 
681  return bv_utils.zero_extension(object_bv, width);
682  }
683  else if(
684  expr.id() == ID_typecast &&
685  to_typecast_expr(expr).op().type().id() == ID_pointer)
686  {
687  // pointer to int
688  bvt op0 = convert_pointer_type(to_typecast_expr(expr).op());
689 
690  // squeeze it in!
691 
692  std::size_t width=boolbv_width(expr.type());
693 
694  if(width==0)
695  return conversion_failed(expr);
696 
697  return bv_utils.zero_extension(op0, width);
698  }
699  else if(expr.id() == ID_object_address)
700  {
701  const auto &object_address_expr = to_object_address_expr(expr);
702  return add_addr(object_address_expr.object_expr());
703  }
704  else if(expr.id() == ID_field_address)
705  {
706  const auto &field_address_expr = to_field_address_expr(expr);
707  const typet &compound_type = ns.follow(field_address_expr.compound_type());
708 
709  // recursive call
710  auto bv = convert_bitvector(field_address_expr.base());
711 
712  if(compound_type.id() == ID_struct)
713  {
714  auto offset = member_offset(
715  to_struct_type(compound_type), field_address_expr.component_name(), ns);
716  CHECK_RETURN(offset.has_value());
717 
718  // add offset
719  bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
720  }
721  else if(compound_type.id() == ID_union)
722  {
723  // nothing to do, all fields have offset 0
724  }
725  else
726  {
727  INVARIANT(false, "field address expressions operate on struct or union");
728  }
729 
730  return bv;
731  }
732  else if(expr.id() == ID_element_address)
733  {
734  const auto &element_address_expr = to_element_address_expr(expr);
735 
736  // recursive call
737  auto bv = convert_bitvector(element_address_expr.base());
738 
739  // get element size
740  auto size = pointer_offset_size(element_address_expr.element_type(), ns);
741  CHECK_RETURN(size.has_value() && *size >= 0);
742 
743  // add offset
744  bv = offset_arithmetic(
745  element_address_expr.type(), bv, *size, element_address_expr.index());
746 
747  return bv;
748  }
749 
750  return SUB::convert_bitvector(expr);
751 }
752 
753 static std::string bits_to_string(const propt &prop, const bvt &bv)
754 {
755  std::string result;
756 
757  for(const auto &literal : bv)
758  {
759  char ch=0;
760 
761  // clang-format off
762  switch(prop.l_get(literal).get_value())
763  {
764  case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
765  case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
766  case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
767  }
768  // clang-format on
769 
770  result = ch + result;
771  }
772 
773  return result;
774 }
775 
777  const exprt &expr,
778  const bvt &bv,
779  std::size_t offset,
780  const typet &type) const
781 {
782  if(type.id() != ID_pointer)
783  return SUB::bv_get_rec(expr, bv, offset, type);
784 
785  const pointer_typet &pt = to_pointer_type(type);
786  const std::size_t bits = boolbv_width(pt);
787  bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
788 
789  std::string value = bits_to_string(prop, value_bv);
790  std::string value_addr = bits_to_string(prop, object_literals(value_bv, pt));
791  std::string value_offset =
792  bits_to_string(prop, offset_literals(value_bv, pt));
793 
794  // we treat these like bit-vector constants, but with
795  // some additional annotation
796 
797  const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
798  return value[value.size() - 1 - i] == '1';
799  });
800 
801  constant_exprt result(bvrep, type);
802 
803  pointer_logict::pointert pointer;
804  pointer.object =
805  numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
806  pointer.offset=binary2integer(value_offset, true);
807 
808  // we add the elaborated expression as operand
809  result.copy_to_operands(pointer_logic.pointer_expr(pointer, pt));
810 
811  return std::move(result);
812 }
813 
814 bvt bv_pointerst::encode(std::size_t addr, const pointer_typet &type) const
815 {
816  const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
817  const std::size_t object_bits = bv_pointers_width.get_object_width(type);
818 
819  bvt zero_offset(offset_bits, const_literal(false));
820 
821  // set variable part
822  bvt object;
823  object.reserve(object_bits);
824  for(std::size_t i=0; i<object_bits; i++)
825  object.push_back(const_literal((addr & (std::size_t(1) << i)) != 0));
826 
827  return object_offset_encoding(object, zero_offset);
828 }
829 
831  const pointer_typet &type,
832  const bvt &bv,
833  const mp_integer &x)
834 {
835  const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
836 
837  return offset_arithmetic(
838  type, bv, 1, bv_utils.build_constant(x, offset_bits));
839 }
840 
842  const pointer_typet &type,
843  const bvt &bv,
844  const mp_integer &factor,
845  const exprt &index)
846 {
847  bvt bv_index=convert_bv(index);
848 
850  index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
852 
853  const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
854  bv_index=bv_utils.extension(bv_index, offset_bits, rep);
855 
856  return offset_arithmetic(type, bv, factor, bv_index);
857 }
858 
860  const pointer_typet &type,
861  const bvt &bv,
862  const mp_integer &factor,
863  const bvt &index)
864 {
865  bvt bv_index;
866 
867  if(factor==1)
868  bv_index=index;
869  else
870  {
871  bvt bv_factor=bv_utils.build_constant(factor, index.size());
872  bv_index = bv_utils.signed_multiplier(index, bv_factor);
873  }
874 
875  const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
876  bv_index = bv_utils.sign_extension(bv_index, offset_bits);
877 
878  bvt offset_bv = offset_literals(bv, type);
879 
880  bvt bv_tmp = bv_utils.add(offset_bv, bv_index);
881 
882  return object_offset_encoding(object_literals(bv, type), bv_tmp);
883 }
884 
886 {
887  std::size_t a=pointer_logic.add_object(expr);
888 
889  const pointer_typet type = pointer_type(expr.type());
890  const std::size_t object_bits = bv_pointers_width.get_object_width(type);
891  const std::size_t max_objects=std::size_t(1)<<object_bits;
892 
893  if(a==max_objects)
894  throw analysis_exceptiont(
895  "too many addressed objects: maximum number of objects is set to 2^n=" +
896  std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
897  "); " +
898  "use the `--object-bits n` option to increase the maximum number");
899 
900  return encode(a, type);
901 }
902 
904  const postponedt &postponed)
905 {
906  if(postponed.expr.id() == ID_is_dynamic_object)
907  {
908  const auto &type =
909  to_pointer_type(to_unary_expr(postponed.expr).op().type());
910  const auto &objects = pointer_logic.objects;
911  std::size_t number=0;
912 
913  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
914  {
915  const exprt &expr=*it;
916 
917  bool is_dynamic=pointer_logic.is_dynamic_object(expr);
918 
919  // only compare object part
920  pointer_typet pt = pointer_type(expr.type());
921  bvt bv = object_literals(encode(number, pt), type);
922 
923  bvt saved_bv = object_literals(postponed.op, type);
924 
925  POSTCONDITION(bv.size()==saved_bv.size());
926  PRECONDITION(postponed.bv.size()==1);
927 
928  literalt l1=bv_utils.equal(bv, saved_bv);
929  literalt l2=postponed.bv.front();
930 
931  if(!is_dynamic)
932  l2=!l2;
933 
934  prop.l_set_to_true(prop.limplies(l1, l2));
935  }
936  }
937  else if(postponed.expr.id()==ID_object_size)
938  {
939  const auto &type =
940  to_pointer_type(to_unary_expr(postponed.expr).op().type());
941  const auto &objects = pointer_logic.objects;
942  std::size_t number=0;
943 
944  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
945  {
946  const exprt &expr=*it;
947 
948  if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
949  continue;
950 
951  const auto size_expr = size_of_expr(expr.type(), ns);
952 
953  if(!size_expr.has_value())
954  continue;
955 
957  size_expr.value(), postponed.expr.type());
958 
959  // only compare object part
960  pointer_typet pt = pointer_type(expr.type());
961  bvt bv = object_literals(encode(number, pt), type);
962 
963  bvt saved_bv = object_literals(postponed.op, type);
964 
965  bvt size_bv = convert_bv(object_size);
966 
967  POSTCONDITION(bv.size()==saved_bv.size());
968  PRECONDITION(postponed.bv.size()>=1);
969  PRECONDITION(size_bv.size() == postponed.bv.size());
970 
971  literalt l1=bv_utils.equal(bv, saved_bv);
972  literalt l2=bv_utils.equal(postponed.bv, size_bv);
973 
974  prop.l_set_to_true(prop.limplies(l1, l2));
975  }
976  }
977  else
978  UNREACHABLE;
979 }
980 
982 {
983  // post-processing arrays may yield further objects, do this first
985 
986  for(postponed_listt::const_iterator
987  it=postponed_list.begin();
988  it!=postponed_list.end();
989  it++)
990  do_postponed(*it);
991 
992  // Clear the list to avoid re-doing in case of incremental usage.
993  postponed_list.clear();
994 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
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
static std::string bits_to_string(const propt &prop, const bvt &bv)
static bool is_pointer_subtraction(const exprt &expr)
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Operator to return the address of an object.
Definition: pointer_expr.h:361
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const namespacet & ns
Definition: arrays.h:56
message_handlert & message_handler
Definition: arrays.h:58
bool get_array_constraints
Definition: arrays.h:113
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
std::size_t get_width() const
Definition: std_types.h:864
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition: boolbv_map.cpp:41
virtual std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:24
Definition: boolbv.h:44
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: boolbv.cpp:98
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:40
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
virtual bvt convert_byte_update(const byte_update_exprt &expr)
void finish_eager_conversion() override
Definition: boolbv.h:77
bv_utilst bv_utils
Definition: boolbv.h:114
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:45
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:334
boolbv_mapt map
Definition: boolbv.h:120
Map bytes according to the configured endianness.
Definition: bv_pointers.cpp:26
void build_little_endian(const typet &type) override
Definition: bv_pointers.cpp:45
void build_big_endian(const typet &type) override
Definition: bv_pointers.cpp:59
const boolbv_widtht & boolbv_width
Definition: bv_pointers.cpp:39
bv_endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
Definition: bv_pointers.cpp:28
std::size_t get_object_width(const pointer_typet &type) const
Definition: bv_pointers.cpp:94
std::size_t get_address_width(const pointer_typet &type) const
std::size_t get_offset_width(const pointer_typet &type) const
std::size_t operator()(const typet &type) const override
Definition: bv_pointers.cpp:74
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
Definition: bv_pointers.h:146
bv_pointers_widtht bv_pointers_width
Definition: bv_pointers.h:53
void do_postponed(const postponedt &postponed)
literalt convert_rest(const exprt &expr) override
pointer_logict pointer_logic
Definition: bv_pointers.h:38
NODISCARD bvt encode(std::size_t object, const pointer_typet &type) const
virtual NODISCARD bvt add_addr(const exprt &expr)
virtual bvt convert_pointer_type(const exprt &expr)
postponed_listt postponed_list
Definition: bv_pointers.h:109
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
Definition: bv_pointers.cpp:68
NODISCARD bvt offset_arithmetic(const pointer_typet &type, const bvt &bv, const mp_integer &x)
void finish_eager_conversion() override
exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const override
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &expr)
std::size_t boolbv_width(const typet &type) const override
Definition: bv_pointers.h:29
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
bvt object_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to...
Definition: bv_pointers.h:118
bvt offset_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals representing the offset into an object that the p...
Definition: bv_pointers.h:133
static literalt sign_bit(const bvt &op)
Definition: bv_utils.h:133
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:61
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:182
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:92
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:11
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1103
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:740
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:177
representationt
Definition: bv_utils.h:28
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:62
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:84
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:105
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1279
struct configt::bv_encodingt bv_encoding
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Maps a big-endian offset to a little-endian offset.
virtual void build_big_endian(const typet &type)
void build(const typet &type, bool little_endian)
std::vector< size_t > map
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
const irep_idt & id() const
Definition: irep.h:396
bool is_false() const
Definition: literal.h:161
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & compound() const
Definition: std_expr.h:2708
irep_idt get_component_name() const
Definition: std_expr.h:2681
Binary minus.
Definition: std_expr.h:973
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The plus expression Associativity is not specified.
Definition: std_expr.h:914
std::size_t get_null_object() const
Definition: pointer_logic.h:58
std::size_t get_invalid_object() const
Definition: pointer_logic.h:64
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
bool is_dynamic_object(const exprt &expr) const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
TO_BE_DOCUMENTED.
Definition: prop.h:23
void l_set_to_true(literalt a)
Definition: prop.h:50
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual tvt l_get(literalt a) const =0
const irep_idt & get_identifier() const
Definition: std_expr.h:109
tv_enumt get_value() const
Definition: threeval.h:40
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The unary minus expression.
Definition: std_expr.h:390
configt config
Definition: config.cpp:25
#define forall_operands(it, expr)
Definition: expr.h:18
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:117
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition: pointer_expr.h:546
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:462
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition: pointer_expr.h:628
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Pointer Logic.
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:887
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t object_bits
Definition: config.h:321