CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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#include <util/replace_expr.h>
21#include <util/simplify_expr.h>
22
25
31{
32public:
34 const typet &type,
35 bool little_endian,
36 const namespacet &_ns,
39 {
40 build(type, little_endian);
41 }
42
43protected:
45
46 void build_little_endian(const typet &type) override;
47 void build_big_endian(const typet &type) override;
48};
49
51{
52 const auto &width_opt = boolbv_width.get_width_opt(src);
53 if(!width_opt.has_value())
54 return;
55
56 const std::size_t new_size = map.size() + *width_opt;
57 map.reserve(new_size);
58
59 for(std::size_t i = map.size(); i < new_size; ++i)
60 map.push_back(i);
61}
62
64{
65 if(src.id() == ID_pointer)
67 else
69}
70
72bv_pointerst::endianness_map(const typet &type, bool little_endian) const
73{
74 return bv_endianness_mapt{type, little_endian, ns, bv_width};
75}
76
78{
79 // not actually type-dependent for now
80 return config.bv_encoding.object_bits;
81}
82
83std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const
84{
85 const std::size_t pointer_width = type.get_width();
86 const std::size_t object_width = get_object_width(type);
87 PRECONDITION(pointer_width >= object_width);
88 return pointer_width - object_width;
89}
90
91std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const
92{
93 return type.get_width();
94}
95
97 const
98{
99 const std::size_t offset_width = get_offset_width(type);
100 const std::size_t object_width = get_object_width(type);
101 PRECONDITION(bv.size() >= offset_width + object_width);
102
103 return bvt(
104 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
105}
106
108 const
109{
110 const std::size_t offset_width = get_offset_width(type);
111 PRECONDITION(bv.size() >= offset_width);
112
113 return bvt(bv.begin(), bv.begin() + offset_width);
114}
115
116bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
117{
118 bvt result;
119 result.reserve(offset.size() + object.size());
120 result.insert(result.end(), offset.begin(), offset.end());
121 result.insert(result.end(), object.begin(), object.end());
122
123 return result;
124}
125
127{
128 PRECONDITION(expr.is_boolean());
129
130 const exprt::operandst &operands=expr.operands();
131
132 if(expr.id() == ID_is_invalid_pointer)
133 {
134 if(operands.size()==1 &&
135 operands[0].type().id()==ID_pointer)
136 {
137 const bvt &bv=convert_bv(operands[0]);
138
139 if(!bv.empty())
140 {
141 const pointer_typet &type = to_pointer_type(operands[0].type());
142 bvt object_bv = object_literals(bv, type);
143
146
147 const std::size_t object_bits = get_object_width(type);
148
150 equal_invalid_bv.reserve(object_bits);
151
152 for(std::size_t i=0; i<object_bits; i++)
153 {
155 }
156
157 return prop.land(equal_invalid_bv);
158 }
159 }
160 }
161 else if(expr.id() == ID_is_dynamic_object)
162 {
163 if(operands.size()==1 &&
164 operands[0].type().id()==ID_pointer)
165 {
166 // we postpone
168
169 postponed_list.emplace_back(bvt{1, l}, convert_bv(operands[0]), expr);
170
171 return l;
172 }
173 }
174 else if(expr.id()==ID_lt || expr.id()==ID_le ||
175 expr.id()==ID_gt || expr.id()==ID_ge)
176 {
177 if(operands.size()==2 &&
178 operands[0].type().id()==ID_pointer &&
179 operands[1].type().id()==ID_pointer)
180 {
181 const bvt &bv0=convert_bv(operands[0]);
182 const bvt &bv1=convert_bv(operands[1]);
183
184 const pointer_typet &type0 = to_pointer_type(operands[0].type());
186
187 const pointer_typet &type1 = to_pointer_type(operands[1].type());
189
190 // Comparison over pointers to distinct objects is undefined behavior in
191 // C; we choose to always produce "false" in such a case. Alternatively,
192 // we could do a comparison over the integer representation of a pointer
193
194 // do the same-object-test via an expression as this may permit re-using
195 // already cached encodings of the equality test
196 const exprt same_object = ::same_object(operands[0], operands[1]);
198 if(same_object_lit.is_false())
199 return same_object_lit;
200
201 // The comparison is UNSIGNED, to match the type of pointer_offsett
202 return prop.land(
206 expr.id(),
209 }
210 }
211 else if(
212 auto prophecy_r_or_w_ok =
214 {
215 return convert(simplify_expr(prophecy_r_or_w_ok->lower(ns), ns));
216 }
217 else if(
220 {
222 }
223
224 return SUB::convert_rest(expr);
225}
226
228 const namespacet &_ns,
229 propt &_prop,
230 message_handlert &message_handler,
231 bool get_array_constraints)
232 : boolbvt(_ns, _prop, message_handler, get_array_constraints),
233 pointer_logic(_ns)
234{
235}
236
237std::optional<bvt> bv_pointerst::convert_address_of_rec(const exprt &expr)
238{
239 if(expr.id()==ID_symbol)
240 {
241 return add_addr(expr);
242 }
243 else if(expr.id()==ID_label)
244 {
245 return add_addr(expr);
246 }
247 else if(expr.id() == ID_null_object)
248 {
251 }
252 else if(expr.id()==ID_index)
253 {
255 const exprt &array=index_expr.array();
256 const exprt &index=index_expr.index();
257 const auto &array_type = to_array_type(array.type());
258
259 pointer_typet type = pointer_type(expr.type());
260 const std::size_t bits = boolbv_width(type);
261
262 bvt bv;
263
264 // recursive call
265 if(array_type.id()==ID_pointer)
266 {
267 // this should be gone
268 bv=convert_pointer_type(array);
269 CHECK_RETURN(bv.size()==bits);
270 }
271 else if(array_type.id()==ID_array ||
273 {
274 auto bv_opt = convert_address_of_rec(array);
275 if(!bv_opt.has_value())
276 return {};
277 bv = std::move(*bv_opt);
278 CHECK_RETURN(bv.size()==bits);
279 }
280 else
282
283 // get size
284 auto size = size_of_expr(array_type.element_type(), ns);
285 CHECK_RETURN(size.has_value());
286
287 bv = offset_arithmetic(type, bv, *size, index);
288 CHECK_RETURN(bv.size()==bits);
289
290 return std::move(bv);
291 }
292 else if(expr.id()==ID_byte_extract_little_endian ||
294 {
295 const auto &byte_extract_expr=to_byte_extract_expr(expr);
296
297 // recursive call
299 if(!bv_opt.has_value())
300 return {};
301
302 pointer_typet type = pointer_type(expr.type());
303 const std::size_t bits = boolbv_width(type);
304 CHECK_RETURN(bv_opt->size() == bits);
305
306 bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
307 CHECK_RETURN(bv.size()==bits);
308 return std::move(bv);
309 }
310 else if(expr.id()==ID_member)
311 {
313 const exprt &struct_op = member_expr.compound();
314
315 // recursive call
316 auto bv_opt = convert_address_of_rec(struct_op);
317 if(!bv_opt.has_value())
318 return {};
319
320 bvt bv = std::move(*bv_opt);
321 if(
322 struct_op.type().id() == ID_struct ||
323 struct_op.type().id() == ID_struct_tag)
324 {
326 struct_op.type().id() == ID_struct_tag
327 ? ns.follow_tag(to_struct_tag_type(struct_op.type()))
328 : to_struct_type(struct_op.type());
329 auto offset =
330 member_offset(struct_op_type, member_expr.get_component_name(), ns);
331 CHECK_RETURN(offset.has_value());
332
333 // add offset
334 pointer_typet type = pointer_type(expr.type());
335 bv = offset_arithmetic(type, bv, *offset);
336 }
337 else
338 {
339 INVARIANT(
340 struct_op.type().id() == ID_union ||
341 struct_op.type().id() == ID_union_tag,
342 "member expression should operate on struct or union");
343 // nothing to do, all members have offset 0
344 }
345
346 return std::move(bv);
347 }
348 else if(
349 expr.is_constant() || expr.id() == ID_string_constant ||
350 expr.id() == ID_array)
351 { // constant
352 return add_addr(expr);
353 }
354 else if(expr.id()==ID_if)
355 {
356 const if_exprt &ifex=to_if_expr(expr);
357
358 literalt cond=convert(ifex.cond());
359
360 bvt bv1, bv2;
361
362 auto bv1_opt = convert_address_of_rec(ifex.true_case());
363 if(!bv1_opt.has_value())
364 return {};
365
366 auto bv2_opt = convert_address_of_rec(ifex.false_case());
367 if(!bv2_opt.has_value())
368 return {};
369
370 return bv_utils.select(cond, *bv1_opt, *bv2_opt);
371 }
372
373 return {};
374}
375
377{
378 const pointer_typet &type = to_pointer_type(expr.type());
379
380 const std::size_t bits = boolbv_width(expr.type());
381
382 if(expr.id()==ID_symbol)
383 {
384 const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
385
386 return map.get_literals(identifier, type, bits);
387 }
388 else if(expr.id()==ID_nondet_symbol)
389 {
390 return prop.new_variables(bits);
391 }
392 else if(expr.id()==ID_typecast)
393 {
395
396 const exprt &op = typecast_expr.op();
397 const typet &op_type = op.type();
398
399 if(op_type.id()==ID_pointer)
400 return convert_bv(op);
401 else if(
403 op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
404 {
405 // Cast from a bitvector type to pointer.
406 // We just do a zero extension.
407
408 const bvt &op_bv=convert_bv(op);
409
410 return bv_utils.zero_extension(op_bv, bits);
411 }
412 }
413 else if(expr.id()==ID_if)
414 {
415 return SUB::convert_if(to_if_expr(expr));
416 }
417 else if(expr.id()==ID_index)
418 {
419 return SUB::convert_index(to_index_expr(expr));
420 }
421 else if(expr.id()==ID_member)
422 {
424 }
425 else if(expr.id()==ID_address_of)
426 {
428
430 if(!bv_opt.has_value())
432
433 CHECK_RETURN(bv_opt->size() == bits);
434 return *bv_opt;
435 }
436 else if(expr.id() == ID_object_address)
437 {
439 return add_addr(object_address_expr.object_expr());
440 }
441 else if(expr.is_constant())
442 {
443 const constant_exprt &c = to_constant_expr(expr);
444
445 if(c.is_null_pointer())
446 return encode(pointer_logic.get_null_object(), type);
447 else
448 {
449 mp_integer i = bvrep2integer(c.get_value(), bits, false);
450 return bv_utils.build_constant(i, bits);
451 }
452 }
453 else if(expr.id()==ID_plus)
454 {
455 // this has to be pointer plus integer
456
457 const plus_exprt &plus_expr = to_plus_expr(expr);
458
459 bvt bv;
460
461 mp_integer size=0;
462 std::size_t count=0;
463
464 for(const auto &op : plus_expr.operands())
465 {
466 if(op.type().id() == ID_pointer)
467 {
468 count++;
469 bv = convert_bv(op);
470 CHECK_RETURN(bv.size()==bits);
471
472 typet pointer_base_type = to_pointer_type(op.type()).base_type();
475 "no pointer arithmetic over void pointers");
477 CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
478 size = *size_opt;
479 }
480 }
481
482 INVARIANT(
483 count == 1,
484 "there should be exactly one pointer-type operand in a pointer-type sum");
485
486 const std::size_t offset_bits = get_offset_width(type);
488
489 for(const auto &operand : plus_expr.operands())
490 {
491 if(operand.type().id() == ID_pointer)
492 continue;
493
494 if(
495 operand.type().id() != ID_unsignedbv &&
496 operand.type().id() != ID_signedbv)
497 {
499 }
500
504
505 bvt op = convert_bv(operand);
506 CHECK_RETURN(!op.empty());
507
508 op = bv_utils.extension(op, offset_bits, rep);
509
510 sum=bv_utils.add(sum, op);
511 }
512
513 return offset_arithmetic(type, bv, size, sum);
514 }
515 else if(expr.id()==ID_minus)
516 {
517 // this is pointer-integer
518
519 const minus_exprt &minus_expr = to_minus_expr(expr);
520
521 INVARIANT(
522 minus_expr.lhs().type().id() == ID_pointer,
523 "first operand should be of pointer type");
524
525 if(
526 minus_expr.rhs().type().id() != ID_unsignedbv &&
527 minus_expr.rhs().type().id() != ID_signedbv)
528 {
530 }
531
533
534 const bvt &bv = convert_bv(minus_expr.lhs());
535
537 to_pointer_type(minus_expr.lhs().type()).base_type();
540 "no pointer arithmetic over void pointers");
543 return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
544 }
545 else if(expr.id()==ID_byte_extract_little_endian ||
547 {
549 }
550 else if(
553 {
555 }
556 else if(expr.id() == ID_field_address)
557 {
558 const auto &field_address_expr = to_field_address_expr(expr);
559 const typet &compound_type = field_address_expr.compound_type();
560
561 // recursive call
562 auto bv = convert_bitvector(field_address_expr.base());
563
564 if(compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag)
565 {
567 compound_type.id() == ID_struct_tag
568 ? ns.follow_tag(to_struct_tag_type(compound_type))
569 : to_struct_type(compound_type);
570 auto offset =
572 CHECK_RETURN(offset.has_value());
573
574 // add offset
575 bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
576 }
577 else if(
578 compound_type.id() == ID_union || compound_type.id() == ID_union_tag)
579 {
580 // nothing to do, all fields have offset 0
581 }
582 else
583 {
584 INVARIANT(false, "field address expressions operate on struct or union");
585 }
586
587 return bv;
588 }
589 else if(expr.id() == ID_element_address)
590 {
592
593 // recursive call
594 auto bv = convert_bitvector(element_address_expr.base());
595
596 // get element size
597 auto size = pointer_offset_size(element_address_expr.element_type(), ns);
598 CHECK_RETURN(size.has_value() && *size >= 0);
599
600 // add offset
602 element_address_expr.type(), bv, *size, element_address_expr.index());
603
604 return bv;
605 }
606
607 return conversion_failed(expr);
608}
609
610static bool is_pointer_subtraction(const exprt &expr)
611{
612 if(expr.id() != ID_minus)
613 return false;
614
615 const auto &minus_expr = to_minus_expr(expr);
616
617 return minus_expr.lhs().type().id() == ID_pointer &&
618 minus_expr.rhs().type().id() == ID_pointer;
619}
620
622{
623 if(expr.type().id()==ID_pointer)
624 return convert_pointer_type(expr);
625
626 if(is_pointer_subtraction(expr))
627 {
628 std::size_t width=boolbv_width(expr.type());
629
630 // pointer minus pointer is subtraction over the offset divided by element
631 // size, iff the pointers point to the same object
632 const auto &minus_expr = to_minus_expr(expr);
633
634 // do the same-object-test via an expression as this may permit re-using
635 // already cached encodings of the equality test
638
639 bvt bv = prop.new_variables(width);
640
641 if(!same_object_lit.is_false())
642 {
643 const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type());
644 const bvt &lhs = convert_bv(minus_expr.lhs());
645 const bvt lhs_offset =
647
648 const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type());
649 const bvt &rhs = convert_bv(minus_expr.rhs());
650 const bvt rhs_offset =
652
654
656 lhs_pt.base_type().id() != ID_empty,
657 "no pointer arithmetic over void pointers");
658 auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
660
661 if(*element_size_opt != 1)
662 {
666 }
667
670 }
671
672 return bv;
673 }
674 else if(
675 expr.id() == ID_pointer_offset &&
676 to_pointer_offset_expr(expr).pointer().type().id() == ID_pointer)
677 {
678 std::size_t width=boolbv_width(expr.type());
679
680 const exprt &pointer = to_pointer_offset_expr(expr).pointer();
681 const bvt &pointer_bv = convert_bv(pointer);
682
683 bvt offset_bv =
685
686 return bv_utils.zero_extension(offset_bv, width);
687 }
688 else if(
690 {
691 // we postpone until we know the objects
692 std::size_t width = boolbv_width(object_size->type());
693
694 postponed_list.emplace_back(
695 prop.new_variables(width),
696 convert_bv(object_size->pointer()),
697 *object_size);
698
699 return postponed_list.back().bv;
700 }
701 else if(
702 expr.id() == ID_pointer_object &&
703 to_pointer_object_expr(expr).pointer().type().id() == ID_pointer)
704 {
705 std::size_t width=boolbv_width(expr.type());
706
707 const exprt &pointer = to_pointer_object_expr(expr).pointer();
708 const bvt &pointer_bv = convert_bv(pointer);
709
710 bvt object_bv =
712
713 return bv_utils.zero_extension(object_bv, width);
714 }
715 else if(
716 expr.id() == ID_typecast &&
717 to_typecast_expr(expr).op().type().id() == ID_pointer)
718 {
719 // pointer to int
720 bvt op0 = convert_bv(to_typecast_expr(expr).op());
721
722 // squeeze it in!
723 std::size_t width=boolbv_width(expr.type());
724
725 return bv_utils.zero_extension(op0, width);
726 }
727
728 return SUB::convert_bitvector(expr);
729}
730
731static std::string bits_to_string(const propt &prop, const bvt &bv)
732{
733 std::string result;
734
735 for(const auto &literal : bv)
736 {
737 char ch=0;
738
739 // clang-format off
740 switch(prop.l_get(literal).get_value())
741 {
742 case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
743 case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
744 case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
745 }
746 // clang-format on
747
748 result = ch + result;
749 }
750
751 return result;
752}
753
755 const exprt &expr,
756 const bvt &bv,
757 std::size_t offset) const
758{
759 const typet &type = expr.type();
760
761 if(type.id() != ID_pointer)
762 return SUB::bv_get_rec(expr, bv, offset);
763
764 const pointer_typet &pt = to_pointer_type(type);
765 const std::size_t bits = boolbv_width(pt);
766 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
767
768 std::string value = bits_to_string(prop, value_bv);
770 std::string value_offset =
772
773 // we treat these like bit-vector constants, but with
774 // some additional annotation
775
776 const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
777 return value[value.size() - 1 - i] == '1';
778 });
779
780 constant_exprt result(bvrep, type);
781
785
788}
789
791 const
792{
793 const std::size_t offset_bits = get_offset_width(type);
794 const std::size_t object_bits = get_object_width(type);
795
797 bvt object = bv_utils.build_constant(addr, object_bits);
798
799 return object_offset_encoding(object, zero_offset);
800}
801
803 const pointer_typet &type,
804 const bvt &bv,
805 const mp_integer &x)
806{
807 const std::size_t offset_bits = get_offset_width(type);
808
809 return offset_arithmetic(
810 type, bv, 1, bv_utils.build_constant(x, offset_bits));
811}
812
814 const pointer_typet &type,
815 const bvt &bv,
816 const mp_integer &factor,
817 const exprt &index)
818{
819 bvt bv_index=convert_bv(index);
820
824
825 const std::size_t offset_bits = get_offset_width(type);
827
828 return offset_arithmetic(type, bv, factor, bv_index);
829}
830
832 const pointer_typet &type,
833 const bvt &bv,
834 const exprt &factor,
835 const exprt &index)
836{
838 bvt bv_index =
840
844
846
847 const std::size_t offset_bits = get_offset_width(type);
849
850 return offset_arithmetic(type, bv, 1, bv_index);
851}
852
854 const pointer_typet &type,
855 const bvt &bv,
856 const mp_integer &factor,
857 const bvt &index)
858{
860
861 if(factor==1)
862 bv_index=index;
863 else
864 {
867 }
868
869 const std::size_t offset_bits = get_offset_width(type);
871
872 bvt offset_bv = offset_literals(bv, type);
873
875
877}
878
880{
881 const auto a = pointer_logic.add_object(expr);
882
883 const pointer_typet type = pointer_type(expr.type());
884 const std::size_t object_bits = get_object_width(type);
885 const std::size_t max_objects=std::size_t(1)<<object_bits;
886
887 if(a==max_objects)
889 "too many addressed objects: maximum number of objects is set to 2^n=" +
890 std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
891 "); " +
892 "use the `--object-bits n` option to increase the maximum number");
893
894 return encode(a, type);
895}
896
898 std::vector<symbol_exprt> &placeholders) const
899{
900 PRECONDITION(placeholders.empty());
901
902 const auto &objects = pointer_logic.objects;
903 std::size_t number = 0;
904
906 dynamic_objects_ops.reserve(objects.size());
907 not_dynamic_objects_ops.reserve(objects.size());
908
909 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
910 {
911 const exprt &expr = *it;
912
913 // only compare object part
915 bvt bv = object_literals(encode(number, pt), pt);
916
918 conjuncts.reserve(bv.size());
919 placeholders.reserve(bv.size());
920 for(std::size_t i = 0; i < bv.size(); ++i)
921 {
922 if(placeholders.size() <= i)
923 placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}});
924
925 POSTCONDITION(bv[i].is_constant());
926 if(bv[i].is_true())
927 conjuncts.emplace_back(placeholders[i]);
928 else
929 conjuncts.emplace_back(not_exprt{placeholders[i]});
930 }
931
934 else
936 }
937
940
944
945 return {bdd_converter.as_expr(dyn_bdd), bdd_converter.as_expr(not_dyn_bdd)};
946}
947
948std::unordered_map<exprt, exprt, irep_hash>
950 std::vector<symbol_exprt> &placeholders) const
951{
952 PRECONDITION(placeholders.empty());
953
954 const auto &objects = pointer_logic.objects;
955 std::size_t number = 0;
956
957 std::unordered_map<exprt, exprt::operandst, irep_hash> per_size_object_ops;
958
959 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
960 {
961 const exprt &expr = *it;
962
963 if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
964 continue;
965
966 const auto size_expr = size_of_expr(expr.type(), ns);
967 if(!size_expr.has_value())
968 continue;
969
970 // only compare object part
972 bvt bv = object_literals(encode(number, pt), pt);
973
975 conjuncts.reserve(bv.size());
976 placeholders.reserve(bv.size());
977 for(std::size_t i = 0; i < bv.size(); ++i)
978 {
979 if(placeholders.size() <= i)
980 placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}});
981
982 POSTCONDITION(bv[i].is_constant());
983 if(bv[i].is_true())
984 conjuncts.emplace_back(placeholders[i]);
985 else
986 conjuncts.emplace_back(not_exprt{placeholders[i]});
987 }
988
990 }
991
992 std::unordered_map<exprt, exprt, irep_hash> result;
993 for(const auto &size_entry : per_size_object_ops)
994 {
998
999 result.emplace(size_entry.first, bdd_converter.as_expr(bdd));
1000 }
1001
1002 return result;
1003}
1004
1006{
1007 // post-processing arrays may yield further objects, do this first
1009
1010 // it would seem nicer to use `optionalt` here, but GCC >= 12 produces
1011 // spurious warnings about accessing uninitialized objects
1012 std::pair<exprt, exprt> is_dynamic_expr = {nil_exprt{}, nil_exprt{}};
1013 std::vector<symbol_exprt> is_dynamic_placeholders;
1014
1015 std::unordered_map<exprt, exprt, irep_hash> object_sizes;
1016 std::vector<symbol_exprt> object_size_placeholders;
1017
1018 for(const postponedt &postponed : postponed_list)
1019 {
1020 if(postponed.expr.id() == ID_is_dynamic_object)
1021 {
1022 if(is_dynamic_expr.first.is_nil())
1025
1026 const auto &type =
1027 to_pointer_type(to_unary_expr(postponed.expr).op().type());
1031 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1032 {
1033 replacements.emplace(
1035 }
1040
1041 PRECONDITION(postponed.bv.size() == 1);
1043 prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
1045 prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
1046 }
1047 else if(
1048 const auto postponed_object_size =
1050 {
1051 if(object_sizes.empty())
1053
1054 // we might not have any usable objects
1055 if(object_size_placeholders.empty())
1056 continue;
1057
1058 const auto &type =
1059 to_pointer_type(postponed_object_size->pointer().type());
1063 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1064 {
1065 replacements.emplace(
1067 }
1068
1069 for(const auto &object_size_entry : object_sizes)
1070 {
1074 POSTCONDITION(size_bv.size() == postponed.bv.size());
1075
1078
1080 if(l1.is_true())
1081 {
1082 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1083 prop.set_equal(postponed.bv[i], size_bv[i]);
1084 break;
1085 }
1086 else if(l1.is_false())
1087 continue;
1088#define COMPACT_OBJECT_SIZE_EQ
1089#ifndef COMPACT_OBJECT_SIZE_EQ
1091
1093#else
1094 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1095 {
1096 prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
1097 prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
1098 }
1099#endif
1100 }
1101 }
1102 else
1104 }
1105
1106 // Clear the list to avoid re-doing in case of incremental usage.
1108}
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
Conversion between exprt and miniBDD.
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:235
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
Definition bdd_expr.h:34
Logical operations on BDDs.
Definition bdd_cudd.h:78
std::size_t get_width() const
Definition std_types.h:925
The Boolean type.
Definition std_types.h:36
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
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:108
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:117
void finish_eager_conversion() override
Definition boolbv.h:81
bv_utilst bv_utils
Definition boolbv.h:118
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:94
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:103
literalt convert_rest(const exprt &expr) override
Definition boolbv.cpp:337
boolbv_mapt map
Definition boolbv.h:124
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
pointer_logict pointer_logic
Definition bv_pointers.h:31
std::unordered_map< exprt, exprt, irep_hash > prepare_postponed_object_size(std::vector< symbol_exprt > &placeholders) const
Create Boolean functions describing all objects of each known object size over placeholders as input ...
bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
postponed_listt postponed_list
Definition bv_pointers.h:86
std::size_t get_address_width(const pointer_typet &) const
virtual 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.
bvt encode(const mp_integer &object, const pointer_typet &) const
std::pair< exprt, exprt > prepare_postponed_is_dynamic_object(std::vector< symbol_exprt > &placeholders) const
Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholder...
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...
std::optional< bvt > convert_address_of_rec(const exprt &)
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 &)
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:66
static bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:187
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:95
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:14
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:28
bvt sub(const bvt &op0, const bvt &op1)
Definition bv_utils.h:67
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:89
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:108
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:3117
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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:224
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
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:2497
Array index operator.
Definition std_expr.h:1470
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2971
Binary minus.
Definition std_expr.h:1061
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
Boolean negation.
Definition std_expr.h:2454
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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 ...
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 tvt l_get(literalt a) const =0
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:131
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
The unary minus expression.
Definition std_expr.h:484
bool is_true(const literalt &l)
Definition literal.h:198
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
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.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Pointer Logic.
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#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
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:83
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:71
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888