cprover
Loading...
Searching...
No Matches
bv_pointers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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>
16#include <util/namespace.h>
17#include <util/pointer_expr.h>
20
26{
27public:
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
38protected:
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
68bv_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
74operator()(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(
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,
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),
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());
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
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 {
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
545static 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),
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),
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
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
753static 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
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
814bvt 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)
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
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
975 }
976 }
977 else
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 bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
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.
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)
virtual std::size_t operator()(const typet &type) const
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
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.
void build_little_endian(const typet &type) override
void build_big_endian(const typet &type) override
const boolbv_widtht & boolbv_width
bv_endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
std::size_t get_object_width(const pointer_typet &type) const
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
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.
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
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
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...
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...
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.
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)
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 & cond()
Definition std_expr.h:2243
exprt & false_case()
Definition std_expr.h:2263
exprt & true_case()
Definition std_expr.h:2253
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
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
std::size_t get_invalid_object() const
numberingt< exprt, irep_hash > objects
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 ...
const typet & base_type() const
The type of the data what we point to.
TO_BE_DOCUMENTED.
Definition prop.h:24
void l_set_to_true(literalt a)
Definition prop.h:51
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 element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, 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< exprt > size_of_expr(const typet &type, 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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:953
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:998
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 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::size_t object_bits
Definition config.h:321