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/expr_util.h>
17#include <util/namespace.h>
18#include <util/pointer_expr.h>
21#include <util/simplify_expr.h>
22
28{
29public:
31 const typet &type,
32 bool little_endian,
33 const namespacet &_ns,
34 const boolbv_widtht &_boolbv_width)
35 : endianness_mapt(_ns), boolbv_width(_boolbv_width)
36 {
37 build(type, little_endian);
38 }
39
40protected:
42
43 void build_little_endian(const typet &type) override;
44 void build_big_endian(const typet &type) override;
45};
46
48{
49 const auto &width_opt = boolbv_width.get_width_opt(src);
50 if(!width_opt.has_value())
51 return;
52
53 const std::size_t new_size = map.size() + *width_opt;
54 map.reserve(new_size);
55
56 for(std::size_t i = map.size(); i < new_size; ++i)
57 map.push_back(i);
58}
59
61{
62 if(src.id() == ID_pointer)
64 else
66}
67
69bv_pointerst::endianness_map(const typet &type, bool little_endian) const
70{
71 return bv_endianness_mapt{type, little_endian, ns, bv_width};
72}
73
75{
76 // not actually type-dependent for now
78}
79
80std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const
81{
82 const std::size_t pointer_width = type.get_width();
83 const std::size_t object_width = get_object_width(type);
84 PRECONDITION(pointer_width >= object_width);
85 return pointer_width - object_width;
86}
87
88std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const
89{
90 return type.get_width();
91}
92
94 const
95{
96 const std::size_t offset_width = get_offset_width(type);
97 const std::size_t object_width = get_object_width(type);
98 PRECONDITION(bv.size() >= offset_width + object_width);
99
100 return bvt(
101 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
102}
103
105 const
106{
107 const std::size_t offset_width = get_offset_width(type);
108 PRECONDITION(bv.size() >= offset_width);
109
110 return bvt(bv.begin(), bv.begin() + offset_width);
111}
112
113bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
114{
115 bvt result;
116 result.reserve(offset.size() + object.size());
117 result.insert(result.end(), offset.begin(), offset.end());
118 result.insert(result.end(), object.begin(), object.end());
119
120 return result;
121}
122
124{
125 PRECONDITION(expr.is_boolean());
126
127 const exprt::operandst &operands=expr.operands();
128
129 if(expr.id() == ID_is_invalid_pointer)
130 {
131 if(operands.size()==1 &&
132 operands[0].type().id()==ID_pointer)
133 {
134 const bvt &bv=convert_bv(operands[0]);
135
136 if(!bv.empty())
137 {
138 const pointer_typet &type = to_pointer_type(operands[0].type());
139 bvt object_bv = object_literals(bv, type);
140
141 bvt invalid_bv = object_literals(
143
144 const std::size_t object_bits = get_object_width(type);
145
146 bvt equal_invalid_bv;
147 equal_invalid_bv.reserve(object_bits);
148
149 for(std::size_t i=0; i<object_bits; i++)
150 {
151 equal_invalid_bv.push_back(prop.lequal(object_bv[i], invalid_bv[i]));
152 }
153
154 return prop.land(equal_invalid_bv);
155 }
156 }
157 }
158 else if(expr.id() == ID_is_dynamic_object)
159 {
160 if(operands.size()==1 &&
161 operands[0].type().id()==ID_pointer)
162 {
163 // we postpone
165
166 postponed_list.emplace_back(bvt{1, l}, convert_bv(operands[0]), expr);
167
168 return l;
169 }
170 }
171 else if(expr.id()==ID_lt || expr.id()==ID_le ||
172 expr.id()==ID_gt || expr.id()==ID_ge)
173 {
174 if(operands.size()==2 &&
175 operands[0].type().id()==ID_pointer &&
176 operands[1].type().id()==ID_pointer)
177 {
178 const bvt &bv0=convert_bv(operands[0]);
179 const bvt &bv1=convert_bv(operands[1]);
180
181 const pointer_typet &type0 = to_pointer_type(operands[0].type());
182 bvt offset_bv0 = offset_literals(bv0, type0);
183
184 const pointer_typet &type1 = to_pointer_type(operands[1].type());
185 bvt offset_bv1 = offset_literals(bv1, type1);
186
187 // Comparison over pointers to distinct objects is undefined behavior in
188 // C; we choose to always produce "false" in such a case. Alternatively,
189 // we could do a comparison over the integer representation of a pointer
190
191 // do the same-object-test via an expression as this may permit re-using
192 // already cached encodings of the equality test
193 const exprt same_object = ::same_object(operands[0], operands[1]);
194 const literalt same_object_lit = convert(same_object);
195 if(same_object_lit.is_false())
196 return same_object_lit;
197
198 // The comparison is UNSIGNED, to match the type of pointer_offsett
199 return prop.land(
200 same_object_lit,
202 offset_bv0,
203 expr.id(),
204 offset_bv1,
206 }
207 }
208 else if(
209 auto prophecy_r_or_w_ok =
211 {
212 return convert(simplify_expr(prophecy_r_or_w_ok->lower(ns), ns));
213 }
214 else if(
215 auto prophecy_pointer_in_range =
217 {
218 return convert(simplify_expr(prophecy_pointer_in_range->lower(ns), ns));
219 }
220
221 return SUB::convert_rest(expr);
222}
223
225 const namespacet &_ns,
226 propt &_prop,
227 message_handlert &message_handler,
228 bool get_array_constraints)
229 : boolbvt(_ns, _prop, message_handler, get_array_constraints),
230 pointer_logic(_ns)
231{
232}
233
235{
236 if(expr.id()==ID_symbol)
237 {
238 return add_addr(expr);
239 }
240 else if(expr.id()==ID_label)
241 {
242 return add_addr(expr);
243 }
244 else if(expr.id() == ID_null_object)
245 {
246 pointer_typet pt = pointer_type(expr.type());
248 }
249 else if(expr.id()==ID_index)
250 {
251 const index_exprt &index_expr=to_index_expr(expr);
252 const exprt &array=index_expr.array();
253 const exprt &index=index_expr.index();
254 const auto &array_type = to_array_type(array.type());
255
256 pointer_typet type = pointer_type(expr.type());
257 const std::size_t bits = boolbv_width(type);
258
259 bvt bv;
260
261 // recursive call
262 if(array_type.id()==ID_pointer)
263 {
264 // this should be gone
265 bv=convert_pointer_type(array);
266 CHECK_RETURN(bv.size()==bits);
267 }
268 else if(array_type.id()==ID_array ||
269 array_type.id()==ID_string_constant)
270 {
271 auto bv_opt = convert_address_of_rec(array);
272 if(!bv_opt.has_value())
273 return {};
274 bv = std::move(*bv_opt);
275 CHECK_RETURN(bv.size()==bits);
276 }
277 else
279
280 // get size
281 auto size = size_of_expr(array_type.element_type(), ns);
282 CHECK_RETURN(size.has_value());
283
284 bv = offset_arithmetic(type, bv, *size, index);
285 CHECK_RETURN(bv.size()==bits);
286
287 return std::move(bv);
288 }
289 else if(expr.id()==ID_byte_extract_little_endian ||
290 expr.id()==ID_byte_extract_big_endian)
291 {
292 const auto &byte_extract_expr=to_byte_extract_expr(expr);
293
294 // recursive call
295 auto bv_opt = convert_address_of_rec(byte_extract_expr.op());
296 if(!bv_opt.has_value())
297 return {};
298
299 pointer_typet type = pointer_type(expr.type());
300 const std::size_t bits = boolbv_width(type);
301 CHECK_RETURN(bv_opt->size() == bits);
302
303 bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
304 CHECK_RETURN(bv.size()==bits);
305 return std::move(bv);
306 }
307 else if(expr.id()==ID_member)
308 {
309 const member_exprt &member_expr=to_member_expr(expr);
310 const exprt &struct_op = member_expr.compound();
311 const typet &struct_op_type=ns.follow(struct_op.type());
312
313 // recursive call
314 auto bv_opt = convert_address_of_rec(struct_op);
315 if(!bv_opt.has_value())
316 return {};
317
318 bvt bv = std::move(*bv_opt);
319 if(struct_op_type.id()==ID_struct)
320 {
321 auto offset = member_offset(
322 to_struct_type(struct_op_type), member_expr.get_component_name(), ns);
323 CHECK_RETURN(offset.has_value());
324
325 // add offset
326 pointer_typet type = pointer_type(expr.type());
327 bv = offset_arithmetic(type, bv, *offset);
328 }
329 else
330 {
331 INVARIANT(
332 struct_op_type.id() == ID_union,
333 "member expression should operate on struct or union");
334 // nothing to do, all members have offset 0
335 }
336
337 return std::move(bv);
338 }
339 else if(
340 expr.is_constant() || expr.id() == ID_string_constant ||
341 expr.id() == ID_array)
342 { // constant
343 return add_addr(expr);
344 }
345 else if(expr.id()==ID_if)
346 {
347 const if_exprt &ifex=to_if_expr(expr);
348
349 literalt cond=convert(ifex.cond());
350
351 bvt bv1, bv2;
352
353 auto bv1_opt = convert_address_of_rec(ifex.true_case());
354 if(!bv1_opt.has_value())
355 return {};
356
357 auto bv2_opt = convert_address_of_rec(ifex.false_case());
358 if(!bv2_opt.has_value())
359 return {};
360
361 return bv_utils.select(cond, *bv1_opt, *bv2_opt);
362 }
363
364 return {};
365}
366
368{
369 const pointer_typet &type = to_pointer_type(expr.type());
370
371 const std::size_t bits = boolbv_width(expr.type());
372
373 if(expr.id()==ID_symbol)
374 {
375 const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
376
377 return map.get_literals(identifier, type, bits);
378 }
379 else if(expr.id()==ID_nondet_symbol)
380 {
381 return prop.new_variables(bits);
382 }
383 else if(expr.id()==ID_typecast)
384 {
385 const typecast_exprt &typecast_expr = to_typecast_expr(expr);
386
387 const exprt &op = typecast_expr.op();
388 const typet &op_type = op.type();
389
390 if(op_type.id()==ID_pointer)
391 return convert_bv(op);
392 else if(
393 can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_bool ||
394 op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
395 {
396 // Cast from a bitvector type to pointer.
397 // We just do a zero extension.
398
399 const bvt &op_bv=convert_bv(op);
400
401 return bv_utils.zero_extension(op_bv, bits);
402 }
403 }
404 else if(expr.id()==ID_if)
405 {
406 return SUB::convert_if(to_if_expr(expr));
407 }
408 else if(expr.id()==ID_index)
409 {
410 return SUB::convert_index(to_index_expr(expr));
411 }
412 else if(expr.id()==ID_member)
413 {
415 }
416 else if(expr.id()==ID_address_of)
417 {
418 const address_of_exprt &address_of_expr = to_address_of_expr(expr);
419
420 auto bv_opt = convert_address_of_rec(address_of_expr.op());
421 if(!bv_opt.has_value())
422 return conversion_failed(address_of_expr);
423
424 CHECK_RETURN(bv_opt->size() == bits);
425 return *bv_opt;
426 }
427 else if(expr.id() == ID_object_address)
428 {
429 const auto &object_address_expr = to_object_address_expr(expr);
430 return add_addr(object_address_expr.object_expr());
431 }
432 else if(expr.is_constant())
433 {
434 const constant_exprt &c = to_constant_expr(expr);
435
436 if(is_null_pointer(c))
437 return encode(pointer_logic.get_null_object(), type);
438 else
439 {
440 mp_integer i = bvrep2integer(c.get_value(), bits, false);
441 return bv_utils.build_constant(i, bits);
442 }
443 }
444 else if(expr.id()==ID_plus)
445 {
446 // this has to be pointer plus integer
447
448 const plus_exprt &plus_expr = to_plus_expr(expr);
449
450 bvt bv;
451
452 mp_integer size=0;
453 std::size_t count=0;
454
455 for(const auto &op : plus_expr.operands())
456 {
457 if(op.type().id() == ID_pointer)
458 {
459 count++;
460 bv = convert_bv(op);
461 CHECK_RETURN(bv.size()==bits);
462
463 typet pointer_base_type = to_pointer_type(op.type()).base_type();
465 pointer_base_type.id() != ID_empty,
466 "no pointer arithmetic over void pointers");
467 auto size_opt = pointer_offset_size(pointer_base_type, ns);
468 CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
469 size = *size_opt;
470 }
471 }
472
473 INVARIANT(
474 count == 1,
475 "there should be exactly one pointer-type operand in a pointer-type sum");
476
477 const std::size_t offset_bits = get_offset_width(type);
478 bvt sum = bv_utils.build_constant(0, offset_bits);
479
480 for(const auto &operand : plus_expr.operands())
481 {
482 if(operand.type().id() == ID_pointer)
483 continue;
484
485 if(
486 operand.type().id() != ID_unsignedbv &&
487 operand.type().id() != ID_signedbv)
488 {
489 return conversion_failed(plus_expr);
490 }
491
492 bv_utilst::representationt rep = operand.type().id() == ID_signedbv
495
496 bvt op = convert_bv(operand);
497 CHECK_RETURN(!op.empty());
498
499 op = bv_utils.extension(op, offset_bits, rep);
500
501 sum=bv_utils.add(sum, op);
502 }
503
504 return offset_arithmetic(type, bv, size, sum);
505 }
506 else if(expr.id()==ID_minus)
507 {
508 // this is pointer-integer
509
510 const minus_exprt &minus_expr = to_minus_expr(expr);
511
512 INVARIANT(
513 minus_expr.lhs().type().id() == ID_pointer,
514 "first operand should be of pointer type");
515
516 if(
517 minus_expr.rhs().type().id() != ID_unsignedbv &&
518 minus_expr.rhs().type().id() != ID_signedbv)
519 {
520 return conversion_failed(minus_expr);
521 }
522
523 const unary_minus_exprt neg_op1(minus_expr.rhs());
524
525 const bvt &bv = convert_bv(minus_expr.lhs());
526
527 typet pointer_base_type =
528 to_pointer_type(minus_expr.lhs().type()).base_type();
530 pointer_base_type.id() != ID_empty,
531 "no pointer arithmetic over void pointers");
532 auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
533 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
534 return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
535 }
536 else if(expr.id()==ID_byte_extract_little_endian ||
537 expr.id()==ID_byte_extract_big_endian)
538 {
540 }
541 else if(
542 expr.id() == ID_byte_update_little_endian ||
543 expr.id() == ID_byte_update_big_endian)
544 {
546 }
547 else if(expr.id() == ID_field_address)
548 {
549 const auto &field_address_expr = to_field_address_expr(expr);
550 const typet &compound_type = ns.follow(field_address_expr.compound_type());
551
552 // recursive call
553 auto bv = convert_bitvector(field_address_expr.base());
554
555 if(compound_type.id() == ID_struct)
556 {
557 auto offset = member_offset(
558 to_struct_type(compound_type), field_address_expr.component_name(), ns);
559 CHECK_RETURN(offset.has_value());
560
561 // add offset
562 bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
563 }
564 else if(compound_type.id() == ID_union)
565 {
566 // nothing to do, all fields have offset 0
567 }
568 else
569 {
570 INVARIANT(false, "field address expressions operate on struct or union");
571 }
572
573 return bv;
574 }
575 else if(expr.id() == ID_element_address)
576 {
577 const auto &element_address_expr = to_element_address_expr(expr);
578
579 // recursive call
580 auto bv = convert_bitvector(element_address_expr.base());
581
582 // get element size
583 auto size = pointer_offset_size(element_address_expr.element_type(), ns);
584 CHECK_RETURN(size.has_value() && *size >= 0);
585
586 // add offset
588 element_address_expr.type(), bv, *size, element_address_expr.index());
589
590 return bv;
591 }
592
593 return conversion_failed(expr);
594}
595
596static bool is_pointer_subtraction(const exprt &expr)
597{
598 if(expr.id() != ID_minus)
599 return false;
600
601 const auto &minus_expr = to_minus_expr(expr);
602
603 return minus_expr.lhs().type().id() == ID_pointer &&
604 minus_expr.rhs().type().id() == ID_pointer;
605}
606
608{
609 if(expr.type().id()==ID_pointer)
610 return convert_pointer_type(expr);
611
612 if(is_pointer_subtraction(expr))
613 {
614 std::size_t width=boolbv_width(expr.type());
615
616 // pointer minus pointer is subtraction over the offset divided by element
617 // size, iff the pointers point to the same object
618 const auto &minus_expr = to_minus_expr(expr);
619
620 // do the same-object-test via an expression as this may permit re-using
621 // already cached encodings of the equality test
622 const exprt same_object = ::same_object(minus_expr.lhs(), minus_expr.rhs());
623 const literalt same_object_lit = convert(same_object);
624
625 bvt bv = prop.new_variables(width);
626
627 if(!same_object_lit.is_false())
628 {
629 const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type());
630 const bvt &lhs = convert_bv(minus_expr.lhs());
631 const bvt lhs_offset =
632 bv_utils.zero_extension(offset_literals(lhs, lhs_pt), width);
633
634 const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type());
635 const bvt &rhs = convert_bv(minus_expr.rhs());
636 const bvt rhs_offset =
637 bv_utils.zero_extension(offset_literals(rhs, rhs_pt), width);
638
639 bvt difference = bv_utils.sub(lhs_offset, rhs_offset);
640
642 lhs_pt.base_type().id() != ID_empty,
643 "no pointer arithmetic over void pointers");
644 auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
645 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
646
647 if(*element_size_opt != 1)
648 {
649 bvt element_size_bv = bv_utils.build_constant(*element_size_opt, width);
650 difference = bv_utils.divider(
651 difference, element_size_bv, bv_utilst::representationt::SIGNED);
652 }
653
654 // test for null object (integer constants)
655 const exprt null_object = ::null_object(minus_expr.lhs());
656 literalt in_bounds = convert(null_object);
657
658 if(!in_bounds.is_true())
659 {
660 // compute the object size (again, possibly using cached results)
661 const exprt object_size = ::object_size(minus_expr.lhs());
662 const bvt object_size_bv =
664
665 const literalt lhs_in_bounds = prop.land(
666 !bv_utils.sign_bit(lhs_offset),
668 lhs_offset,
669 ID_le,
670 object_size_bv,
672
673 const literalt rhs_in_bounds = prop.land(
674 !bv_utils.sign_bit(rhs_offset),
676 rhs_offset,
677 ID_le,
678 object_size_bv,
680
681 in_bounds =
682 prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
683 }
684
686 prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
687 }
688
689 return bv;
690 }
691 else if(
692 expr.id() == ID_pointer_offset &&
693 to_pointer_offset_expr(expr).pointer().type().id() == ID_pointer)
694 {
695 std::size_t width=boolbv_width(expr.type());
696
697 const exprt &pointer = to_pointer_offset_expr(expr).pointer();
698 const bvt &pointer_bv = convert_bv(pointer);
699
700 bvt offset_bv =
701 offset_literals(pointer_bv, to_pointer_type(pointer.type()));
702
703 return bv_utils.zero_extension(offset_bv, width);
704 }
705 else if(
707 {
708 // we postpone until we know the objects
709 std::size_t width = boolbv_width(object_size->type());
710
711 postponed_list.emplace_back(
712 prop.new_variables(width),
713 convert_bv(object_size->pointer()),
714 *object_size);
715
716 return postponed_list.back().bv;
717 }
718 else if(
719 expr.id() == ID_pointer_object &&
720 to_pointer_object_expr(expr).pointer().type().id() == ID_pointer)
721 {
722 std::size_t width=boolbv_width(expr.type());
723
724 const exprt &pointer = to_pointer_object_expr(expr).pointer();
725 const bvt &pointer_bv = convert_bv(pointer);
726
727 bvt object_bv =
728 object_literals(pointer_bv, to_pointer_type(pointer.type()));
729
730 return bv_utils.zero_extension(object_bv, width);
731 }
732 else if(
733 expr.id() == ID_typecast &&
734 to_typecast_expr(expr).op().type().id() == ID_pointer)
735 {
736 // pointer to int
737 bvt op0 = convert_bv(to_typecast_expr(expr).op());
738
739 // squeeze it in!
740 std::size_t width=boolbv_width(expr.type());
741
742 return bv_utils.zero_extension(op0, width);
743 }
744
745 return SUB::convert_bitvector(expr);
746}
747
748static std::string bits_to_string(const propt &prop, const bvt &bv)
749{
750 std::string result;
751
752 for(const auto &literal : bv)
753 {
754 char ch=0;
755
756 // clang-format off
757 switch(prop.l_get(literal).get_value())
758 {
759 case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
760 case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
761 case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
762 }
763 // clang-format on
764
765 result = ch + result;
766 }
767
768 return result;
769}
770
772 const exprt &expr,
773 const bvt &bv,
774 std::size_t offset) const
775{
776 const typet &type = expr.type();
777
778 if(type.id() != ID_pointer)
779 return SUB::bv_get_rec(expr, bv, offset);
780
781 const pointer_typet &pt = to_pointer_type(type);
782 const std::size_t bits = boolbv_width(pt);
783 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
784
785 std::string value = bits_to_string(prop, value_bv);
786 std::string value_addr = bits_to_string(prop, object_literals(value_bv, pt));
787 std::string value_offset =
788 bits_to_string(prop, offset_literals(value_bv, pt));
789
790 // we treat these like bit-vector constants, but with
791 // some additional annotation
792
793 const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
794 return value[value.size() - 1 - i] == '1';
795 });
796
797 constant_exprt result(bvrep, type);
798
801 binary2integer(value_offset, false)};
802
804 bvrep, pointer_logic.pointer_expr(pointer, pt)};
805}
806
808 const
809{
810 const std::size_t offset_bits = get_offset_width(type);
811 const std::size_t object_bits = get_object_width(type);
812
813 bvt zero_offset(offset_bits, const_literal(false));
814 bvt object = bv_utils.build_constant(addr, object_bits);
815
816 return object_offset_encoding(object, zero_offset);
817}
818
820 const pointer_typet &type,
821 const bvt &bv,
822 const mp_integer &x)
823{
824 const std::size_t offset_bits = get_offset_width(type);
825
826 return offset_arithmetic(
827 type, bv, 1, bv_utils.build_constant(x, offset_bits));
828}
829
831 const pointer_typet &type,
832 const bvt &bv,
833 const mp_integer &factor,
834 const exprt &index)
835{
836 bvt bv_index=convert_bv(index);
837
839 index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
841
842 const std::size_t offset_bits = get_offset_width(type);
843 bv_index=bv_utils.extension(bv_index, offset_bits, rep);
844
845 return offset_arithmetic(type, bv, factor, bv_index);
846}
847
849 const pointer_typet &type,
850 const bvt &bv,
851 const exprt &factor,
852 const exprt &index)
853{
854 bvt bv_factor = convert_bv(factor);
855 bvt bv_index =
857
858 bv_utilst::representationt rep = factor.type().id() == ID_signedbv
861
862 bv_index = bv_utils.multiplier(bv_index, bv_factor, rep);
863
864 const std::size_t offset_bits = get_offset_width(type);
865 bv_index = bv_utils.extension(bv_index, offset_bits, rep);
866
867 return offset_arithmetic(type, bv, 1, bv_index);
868}
869
871 const pointer_typet &type,
872 const bvt &bv,
873 const mp_integer &factor,
874 const bvt &index)
875{
876 bvt bv_index;
877
878 if(factor==1)
879 bv_index=index;
880 else
881 {
882 bvt bv_factor=bv_utils.build_constant(factor, index.size());
883 bv_index = bv_utils.signed_multiplier(index, bv_factor);
884 }
885
886 const std::size_t offset_bits = get_offset_width(type);
887 bv_index = bv_utils.zero_extension(bv_index, offset_bits);
888
889 bvt offset_bv = offset_literals(bv, type);
890
891 bvt bv_tmp = bv_utils.add(offset_bv, bv_index);
892
893 return object_offset_encoding(object_literals(bv, type), bv_tmp);
894}
895
897{
898 const auto a = pointer_logic.add_object(expr);
899
900 const pointer_typet type = pointer_type(expr.type());
901 const std::size_t object_bits = get_object_width(type);
902 const std::size_t max_objects=std::size_t(1)<<object_bits;
903
904 if(a==max_objects)
906 "too many addressed objects: maximum number of objects is set to 2^n=" +
907 std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
908 "); " +
909 "use the `--object-bits n` option to increase the maximum number");
910
911 return encode(a, type);
912}
913
915 const postponedt &postponed)
916{
917 if(postponed.expr.id() == ID_is_dynamic_object)
918 {
919 const auto &type =
920 to_pointer_type(to_unary_expr(postponed.expr).op().type());
921 const auto &objects = pointer_logic.objects;
922 std::size_t number=0;
923
924 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
925 {
926 const exprt &expr=*it;
927
929
930 // only compare object part
931 pointer_typet pt = pointer_type(expr.type());
932 bvt bv = object_literals(encode(number, pt), type);
933
934 bvt saved_bv = object_literals(postponed.op, type);
935
936 POSTCONDITION(bv.size()==saved_bv.size());
937 PRECONDITION(postponed.bv.size()==1);
938
939 literalt l1=bv_utils.equal(bv, saved_bv);
940 literalt l2=postponed.bv.front();
941
942 if(!is_dynamic)
943 l2=!l2;
944
946 }
947 }
948 else if(
949 const auto postponed_object_size =
951 {
952 const auto &type = to_pointer_type(postponed_object_size->pointer().type());
953 const auto &objects = pointer_logic.objects;
954 std::size_t number=0;
955
956 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
957 {
958 const exprt &expr=*it;
959
960 if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
961 continue;
962
963 const auto size_expr = size_of_expr(expr.type(), ns);
964
965 if(!size_expr.has_value())
966 continue;
967
969 size_expr.value(), postponed_object_size->type());
970
971 // only compare object part
972 pointer_typet pt = pointer_type(expr.type());
973 bvt bv = object_literals(encode(number, pt), type);
974
975 bvt saved_bv = object_literals(postponed.op, type);
976
977 bvt size_bv = convert_bv(object_size);
978
979 POSTCONDITION(bv.size()==saved_bv.size());
980 PRECONDITION(postponed.bv.size()>=1);
981 PRECONDITION(size_bv.size() == postponed.bv.size());
982
983 literalt l1=bv_utils.equal(bv, saved_bv);
984 if(l1.is_true())
985 {
986 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
987 prop.set_equal(postponed.bv[i], size_bv[i]);
988 break;
989 }
990 else if(l1.is_false())
991 continue;
992#define COMPACT_OBJECT_SIZE_EQ
993#ifndef COMPACT_OBJECT_SIZE_EQ
994 literalt l2=bv_utils.equal(postponed.bv, size_bv);
995
997#else
998 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
999 {
1000 prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
1001 prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
1002 }
1003#endif
1004 }
1005 }
1006 else
1008}
1009
1011{
1012 // post-processing arrays may yield further objects, do this first
1014
1015 for(postponed_listt::const_iterator
1016 it=postponed_list.begin();
1017 it!=postponed_list.end();
1018 it++)
1019 do_postponed(*it);
1020
1021 // Clear the list to avoid re-doing in case of incremental usage.
1022 postponed_list.clear();
1023}
configt config
Definition config.cpp:25
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
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &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)
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:240
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...
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
const namespacet & ns
Definition arrays.h:56
exprt & lhs()
Definition std_expr.h:613
exprt & rhs()
Definition std_expr.h:623
std::size_t get_width() const
Definition std_types.h:876
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
virtual optionalt< std::size_t > get_width_opt(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:96
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
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)
boolbv_widtht bv_width
Definition boolbv.h:113
void finish_eager_conversion() override
Definition boolbv.h:77
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:38
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:82
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
literalt convert_rest(const exprt &expr) override
Definition boolbv.cpp:316
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 &) const
void do_postponed(const postponedt &postponed)
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &)
pointer_logict pointer_logic
Definition bv_pointers.h:33
NODISCARD bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
postponed_listt postponed_list
Definition bv_pointers.h:93
std::size_t get_address_width(const pointer_typet &) const
virtual NODISCARD bvt add_addr(const exprt &)
endianness_mapt endianness_map(const typet &, bool little_endian) const override
void finish_eager_conversion() override
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
NODISCARD bvt encode(const mp_integer &object, const pointer_typet &) const
std::size_t get_offset_width(const pointer_typet &) const
literalt convert_rest(const exprt &) override
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
bvt convert_bitvector(const exprt &) 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...
virtual bvt convert_pointer_type(const exprt &)
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:139
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:67
static bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:188
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:94
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:13
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)
representationt
Definition bv_utils.h:29
bvt sub(const bvt &op0, const bvt &op1)
Definition bv_utils.h:68
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:90
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:107
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:2942
const irep_idt & get_value() const
Definition std_expr.h:2950
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
const irep_idt & id() const
Definition irep.h:396
bool is_true() const
Definition literal.h:156
bool is_false() const
Definition literal.h:161
Extract member of struct or union.
Definition std_expr.h:2794
const exprt & compound() const
Definition std_expr.h:2843
irep_idt get_component_name() const
Definition std_expr.h:2816
Binary minus.
Definition std_expr.h:1006
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:947
const mp_integer & get_invalid_object() const
const mp_integer & get_null_object() const
numberingt< exprt, irep_hash > objects
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
mp_integer add_object(const exprt &expr)
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:25
void l_set_to_true(literalt a)
Definition prop.h:52
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1)
Definition prop.h:58
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition prop.cpp:12
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:30
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
virtual tvt l_get(literalt a) const =0
const irep_idt & get_identifier() const
Definition std_expr.h:142
tv_enumt get_value() const
Definition threeval.h:40
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
The unary minus expression.
Definition std_expr.h:423
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
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
static bool is_dynamic(const exprt &object)
This function returns true for heap allocated objects or false for stack allocated objects.
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 pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
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)
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:18
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:986
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1031
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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:844
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:899
std::size_t object_bits
Definition config.h:348