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