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