cprover
Loading...
Searching...
No Matches
bv_pointers_wide.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_wide.h"
10
11#include <util/arith_tools.h>
12#include <util/byte_operators.h>
13#include <util/c_types.h>
15#include <util/expr_util.h>
16#include <util/namespace.h>
17#include <util/pointer_expr.h>
20
22{
23 return type.get_width();
24}
25
27{
28 const std::size_t pointer_width = 2 * type.get_width();
29 const std::size_t object_width = get_object_width(type);
30 PRECONDITION(pointer_width >= object_width);
31 return pointer_width - object_width;
32}
33
35 const
36{
37 const std::size_t offset_width = get_offset_width(type);
38 const std::size_t object_width = get_object_width(type);
40
41 return bvt(
42 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
43}
44
46 const
47{
48 const std::size_t offset_width = get_offset_width(type);
49 PRECONDITION(bv.size() >= offset_width);
50
51 return bvt(bv.begin(), bv.begin() + offset_width);
52}
53
55 const bvt &object,
56 const bvt &offset)
57{
58 bvt result;
59 result.reserve(offset.size() + object.size());
60 result.insert(result.end(), offset.begin(), offset.end());
61 result.insert(result.end(), object.begin(), object.end());
62
63 return result;
64}
65
67{
68 PRECONDITION(expr.type().id() == ID_bool);
69
70 const exprt::operandst &operands = expr.operands();
71
72 if(expr.id() == ID_is_invalid_pointer)
73 {
74 if(operands.size() == 1 && operands[0].type().id() == ID_pointer)
75 {
76 const bvt &bv = convert_bv(operands[0]);
77
78 if(!bv.empty())
79 {
80 const pointer_typet &type = to_pointer_type(operands[0].type());
81 bvt object_bv = object_literals(bv, type);
82
85
86 const std::size_t object_bits = get_object_width(type);
87
89 equal_invalid_bv.reserve(object_bits);
90
91 for(std::size_t i = 0; i < object_bits; i++)
92 {
94 }
95
97 }
98 }
99 }
100 else if(expr.id() == ID_is_dynamic_object)
101 {
102 if(operands.size() == 1 && operands[0].type().id() == ID_pointer)
103 {
104 // we postpone
106
107 postponed_list.emplace_back(bvt{1, l}, convert_bv(operands[0]), expr);
108
109 return l;
110 }
111 }
112 else if(
113 expr.id() == ID_lt || expr.id() == ID_le || expr.id() == ID_gt ||
114 expr.id() == ID_ge)
115 {
116 if(
117 operands.size() == 2 && operands[0].type().id() == ID_pointer &&
118 operands[1].type().id() == ID_pointer)
119 {
120 const bvt &bv0 = convert_bv(operands[0]);
121 const bvt &bv1 = convert_bv(operands[1]);
122
123 const pointer_typet &type0 = to_pointer_type(operands[0].type());
125
126 const pointer_typet &type1 = to_pointer_type(operands[1].type());
128
129 // Comparison over pointers to distinct objects is undefined behavior in
130 // C; we choose to always produce "false" in such a case. Alternatively,
131 // we could do a comparison over the integer representation of a pointer
132
133 // do the same-object-test via an expression as this may permit re-using
134 // already cached encodings of the equality test
135 const exprt same_object = ::same_object(operands[0], operands[1]);
137 if(same_object_lit.is_false())
138 return same_object_lit;
139
140 return prop.land(
144 expr.id(),
147 UNSIGNED)); // Note the UNSIGNED comparison
148 }
149 }
150
151 return SUB::convert_rest(expr);
152}
153
155 const namespacet &_ns,
156 propt &_prop,
157 message_handlert &message_handler,
158 bool get_array_constraints)
159 : boolbvt(_ns, _prop, message_handler, get_array_constraints),
160 pointer_logic(_ns)
161{
162}
163
165{
166 if(expr.id() == ID_symbol)
167 {
168 return add_addr(expr);
169 }
170 else if(expr.id() == ID_label)
171 {
172 return add_addr(expr);
173 }
174 else if(expr.id() == ID_null_object)
175 {
178 }
179 else if(expr.id() == ID_index)
180 {
181 const index_exprt &index_expr = to_index_expr(expr);
182 const exprt &array = index_expr.array();
183 const exprt &index = index_expr.index();
184 const auto &array_type = to_array_type(array.type());
185
186 pointer_typet type = pointer_type(expr.type());
187 const std::size_t bits = boolbv_width(type);
188
189 bvt bv;
190
191 // recursive call
192 if(array_type.id() == ID_pointer)
193 {
194 // this should be gone
195 bv = convert_pointer_type(array);
196 CHECK_RETURN(bv.size() == bits);
197 }
198 else if(
200 {
201 auto bv_opt = convert_address_of_rec(array);
202 if(!bv_opt.has_value())
203 return {};
204 bv = std::move(*bv_opt);
205 CHECK_RETURN(bv.size() == bits);
206 }
207 else
209
210 // get size
211 auto size = pointer_offset_size(array_type.element_type(), ns);
212 CHECK_RETURN(size.has_value() && *size >= 0);
213
214 bv = offset_arithmetic(type, bv, *size, index);
215 CHECK_RETURN(bv.size() == bits);
216
217 return std::move(bv);
218 }
219 else if(
222 {
223 const auto &byte_extract_expr = to_byte_extract_expr(expr);
224
225 // recursive call
227 if(!bv_opt.has_value())
228 return {};
229
230 pointer_typet type = pointer_type(expr.type());
231 const std::size_t bits = boolbv_width(type);
232 CHECK_RETURN(bv_opt->size() == bits);
233
234 bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
235 CHECK_RETURN(bv.size() == bits);
236 return std::move(bv);
237 }
238 else if(expr.id() == ID_member)
239 {
241 const exprt &struct_op = member_expr.compound();
242 const typet &struct_op_type = ns.follow(struct_op.type());
243
244 // recursive call
245 auto bv_opt = convert_address_of_rec(struct_op);
246 if(!bv_opt.has_value())
247 return {};
248
249 bvt bv = std::move(*bv_opt);
250 if(struct_op_type.id() == ID_struct)
251 {
252 auto offset = member_offset(
253 to_struct_type(struct_op_type), member_expr.get_component_name(), ns);
254 CHECK_RETURN(offset.has_value());
255
256 // add offset
257 pointer_typet type = pointer_type(expr.type());
258 bv = offset_arithmetic(type, bv, *offset);
259 }
260 else
261 {
262 INVARIANT(
263 struct_op_type.id() == ID_union,
264 "member expression should operate on struct or union");
265 // nothing to do, all members have offset 0
266 }
267
268 return std::move(bv);
269 }
270 else if(
271 expr.is_constant() || expr.id() == ID_string_constant ||
272 expr.id() == ID_array)
273 { // constant
274 return add_addr(expr);
275 }
276 else if(expr.id() == ID_if)
277 {
278 const if_exprt &ifex = to_if_expr(expr);
279
280 literalt cond = convert(ifex.cond());
281
282 bvt bv1, bv2;
283
284 auto bv1_opt = convert_address_of_rec(ifex.true_case());
285 if(!bv1_opt.has_value())
286 return {};
287
288 auto bv2_opt = convert_address_of_rec(ifex.false_case());
289 if(!bv2_opt.has_value())
290 return {};
291
292 return bv_utils.select(cond, *bv1_opt, *bv2_opt);
293 }
294
295 return {};
296}
297
299{
300 const pointer_typet &type = to_pointer_type(expr.type());
301
302 const std::size_t bits = boolbv_width(expr.type());
303
304 if(expr.id() == ID_symbol)
305 {
306 const irep_idt &identifier = to_symbol_expr(expr).get_identifier();
307
308 return map.get_literals(identifier, type, bits);
309 }
310 else if(expr.id() == ID_nondet_symbol)
311 {
312 return prop.new_variables(bits);
313 }
314 else if(expr.id() == ID_typecast)
315 {
317
318 const exprt &op = typecast_expr.op();
319 const typet &op_type = op.type();
320
321 if(op_type.id() == ID_pointer)
322 return convert_bv(op);
323 else if(
325 op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
326 {
327 // Cast from a bitvector type 'i' to pointer.
328 // 1) top bit not set: NULL + i, zero extended
329 // 2) top bit set: numbered pointer
330 const bvt &op_bv = convert_bv(op);
331 auto top_bit = op_bv.back();
332 const auto numbered_pointer_bv = prop.new_variables(bits);
333
334 for(std::size_t i = 1; i < numbered_pointers.size(); i++)
335 {
336 auto cond = bv_utils.equal(
337 op_bv,
339 bv_utilst::build_constant(i, op_bv.size() - 1),
340 {const_literal(true)}));
342 cond,
345 }
346
352 {const_literal(false)}));
353
355 }
356 }
357 else if(expr.id() == ID_if)
358 {
359 return SUB::convert_if(to_if_expr(expr));
360 }
361 else if(expr.id() == ID_index)
362 {
363 return SUB::convert_index(to_index_expr(expr));
364 }
365 else if(expr.id() == ID_member)
366 {
368 }
369 else if(expr.id() == ID_address_of)
370 {
372
374 if(!bv_opt.has_value())
376
377 CHECK_RETURN(bv_opt->size() == bits);
378 return *bv_opt;
379 }
380 else if(expr.id() == ID_object_address)
381 {
383 return add_addr(object_address_expr.object_expr());
384 }
385 else if(expr.is_constant())
386 {
387 const constant_exprt &c = to_constant_expr(expr);
388
389 if(is_null_pointer(c))
390 return encode(pointer_logic.get_null_object(), type);
391 else
392 {
393 mp_integer i = bvrep2integer(c.get_value(), bits, false);
394 return bv_utils.build_constant(i, bits);
395 }
396 }
397 else if(expr.id() == ID_plus)
398 {
399 // this has to be pointer plus integer
400
401 const plus_exprt &plus_expr = to_plus_expr(expr);
402
403 bvt bv;
404
405 mp_integer size = 0;
406 std::size_t count = 0;
407
408 for(const auto &op : plus_expr.operands())
409 {
410 if(op.type().id() == ID_pointer)
411 {
412 count++;
413 bv = convert_bv(op);
414 CHECK_RETURN(bv.size() == bits);
415
416 typet pointer_base_type = to_pointer_type(op.type()).base_type();
419 "no pointer arithmetic over void pointers");
421 CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
422 size = *size_opt;
423 }
424 }
425
426 INVARIANT(
427 count == 1,
428 "there should be exactly one pointer-type operand in a pointer-type sum");
429
430 const std::size_t offset_bits = get_offset_width(type);
432
433 for(const auto &op : plus_expr.operands())
434 {
435 if(op.type().id() == ID_pointer)
436 continue;
437
438 if(op.type().id() != ID_unsignedbv && op.type().id() != ID_signedbv)
439 {
441 }
442
443 bv_utilst::representationt rep = op.type().id() == ID_signedbv
446
447 bvt op_bv = convert_bv(op);
448 CHECK_RETURN(!op_bv.empty());
449
451
453 }
454
455 return offset_arithmetic(type, bv, size, sum);
456 }
457 else if(expr.id() == ID_minus)
458 {
459 // this is pointer-integer
460
461 const minus_exprt &minus_expr = to_minus_expr(expr);
462
463 INVARIANT(
464 minus_expr.lhs().type().id() == ID_pointer,
465 "first operand should be of pointer type");
466
467 if(
468 minus_expr.rhs().type().id() != ID_unsignedbv &&
469 minus_expr.rhs().type().id() != ID_signedbv)
470 {
472 }
473
475
476 const bvt &bv = convert_bv(minus_expr.lhs());
477
479 to_pointer_type(minus_expr.lhs().type()).base_type();
482 "no pointer arithmetic over void pointers");
485 return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
486 }
487 else if(
490 {
492 }
493 else if(
496 {
498 }
499 else if(expr.id() == ID_field_address)
500 {
501 const auto &field_address_expr = to_field_address_expr(expr);
502 const typet &compound_type = ns.follow(field_address_expr.compound_type());
503
504 // recursive call
505 auto bv = convert_bitvector(field_address_expr.base());
506
507 if(compound_type.id() == ID_struct)
508 {
509 auto offset = member_offset(
510 to_struct_type(compound_type), field_address_expr.component_name(), ns);
511 CHECK_RETURN(offset.has_value());
512
513 // add offset
514 bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
515 }
516 else if(compound_type.id() == ID_union)
517 {
518 // nothing to do, all fields have offset 0
519 }
520 else
521 {
522 INVARIANT(false, "field address expressions operate on struct or union");
523 }
524
525 return bv;
526 }
527 else if(expr.id() == ID_element_address)
528 {
530
531 // recursive call
532 auto bv = convert_bitvector(element_address_expr.base());
533
534 // get element size
535 auto size = pointer_offset_size(element_address_expr.element_type(), ns);
536 CHECK_RETURN(size.has_value() && *size >= 0);
537
538 // add offset
540 element_address_expr.type(), bv, *size, element_address_expr.index());
541
542 return bv;
543 }
544
545 return conversion_failed(expr);
546}
547
548static bool is_pointer_subtraction(const exprt &expr)
549{
550 if(expr.id() != ID_minus)
551 return false;
552
553 const auto &minus_expr = to_minus_expr(expr);
554
555 return minus_expr.lhs().type().id() == ID_pointer &&
556 minus_expr.rhs().type().id() == ID_pointer;
557}
558
560{
561 if(expr.type().id() == ID_pointer)
562 return convert_pointer_type(expr);
563
564 if(is_pointer_subtraction(expr))
565 {
566 std::size_t width = boolbv_width(expr.type());
567
568 if(width == 0)
569 return conversion_failed(expr);
570
571 // pointer minus pointer is subtraction over the offset divided by element
572 // size, iff the pointers point to the same object
573 const auto &minus_expr = to_minus_expr(expr);
574
575 // do the same-object-test via an expression as this may permit re-using
576 // already cached encodings of the equality test
579
580 // compute the object size (again, possibly using cached results)
582 const bvt object_size_bv =
584
585 bvt bv = prop.new_variables(width);
586
587 if(!same_object_lit.is_false())
588 {
589 const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type());
590 const bvt &lhs = convert_bv(minus_expr.lhs());
591 const bvt lhs_offset =
593
598 ID_le,
601
602 const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type());
603 const bvt &rhs = convert_bv(minus_expr.rhs());
604 const bvt rhs_offset =
606
611 ID_le,
614
616
618 lhs_pt.base_type().id() != ID_empty,
619 "no pointer arithmetic over void pointers");
620 auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
622
623 if(*element_size_opt != 1)
624 {
628 }
629
633 }
634
635 return bv;
636 }
637 else if(
638 expr.id() == ID_pointer_offset &&
639 to_pointer_offset_expr(expr).pointer().type().id() == ID_pointer)
640 {
641 std::size_t width = boolbv_width(expr.type());
642
643 if(width == 0)
644 return conversion_failed(expr);
645
646 const exprt &pointer = to_pointer_offset_expr(expr).pointer();
647 const bvt &pointer_bv = convert_bv(pointer);
648
649 bvt offset_bv =
651
652 // we do a sign extension to permit negative offsets
653 return bv_utils.sign_extension(offset_bv, width);
654 }
655 else if(
657 {
658 // we postpone until we know the objects
659 std::size_t width = boolbv_width(object_size->type());
660
661 postponed_list.emplace_back(
662 prop.new_variables(width),
663 convert_bv(object_size->pointer()),
664 *object_size);
665
666 return postponed_list.back().bv;
667 }
668 else if(
669 expr.id() == ID_pointer_object &&
670 to_pointer_object_expr(expr).pointer().type().id() == ID_pointer)
671 {
672 std::size_t width = boolbv_width(expr.type());
673
674 if(width == 0)
675 return conversion_failed(expr);
676
677 const exprt &pointer = to_pointer_object_expr(expr).pointer();
678 const bvt &pointer_bv = convert_bv(pointer);
679
680 bvt object_bv =
682
683 return bv_utils.zero_extension(object_bv, width);
684 }
685 else if(
686 expr.id() == ID_typecast &&
687 to_typecast_expr(expr).op().type().id() == ID_pointer)
688 {
689 // Pointer to int.
690 // We special-case NULL, which should always yield 0.
691 // Otherwise, we 'number' these, which are indicated by setting
692 // the top bit.
693 const auto &pointer_expr = to_typecast_expr(expr).op();
694 const bvt pointer_bv = convert_pointer_type(pointer_expr);
695 const auto is_null = bv_utils.is_zero(pointer_bv);
696 const auto target_width = boolbv_width(expr.type());
697
698 if(target_width == 0)
699 return conversion_failed(expr);
700
701 if(numbered_pointers.empty())
702 numbered_pointers.emplace_back(bvt{});
703
704 const auto number = numbered_pointers.size();
705
706 numbered_pointers.push_back(pointer_bv);
707
708 return bv_utils.select(
709 is_null,
713 {const_literal(true)}));
714 }
715
716 return SUB::convert_bitvector(expr);
717}
718
719static std::string bits_to_string(const propt &prop, const bvt &bv)
720{
721 std::string result;
722
723 for(const auto &literal : bv)
724 {
725 char ch = 0;
726
727 // clang-format off
728 switch(prop.l_get(literal).get_value())
729 {
730 case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
731 case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
732 case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
733 }
734 // clang-format on
735
736 result = ch + result;
737 }
738
739 return result;
740}
741
743 const exprt &expr,
744 const bvt &bv,
745 std::size_t offset) const
746{
747 const auto &type = expr.type();
748
749 if(type.id() != ID_pointer)
750 return SUB::bv_get_rec(expr, bv, offset);
751
752 const pointer_typet &pt = to_pointer_type(type);
753 const std::size_t bits = boolbv_width(pt);
754 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
755
756 std::string value = bits_to_string(prop, value_bv);
758 std::string value_offset =
760
761 // we treat these like bit-vector constants, but with
762 // some additional annotation
763
764 const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
765 return value[value.size() - 1 - i] == '1';
766 });
767
768 constant_exprt result(bvrep, type);
769
773
776}
777
779 const
780{
781 const std::size_t offset_bits = get_offset_width(type);
782 const std::size_t object_bits = get_object_width(type);
783
785 bvt object = bv_utils.build_constant(addr, object_bits);
786
787 return object_offset_encoding(object, zero_offset);
788}
789
791 const pointer_typet &type,
792 const bvt &bv,
793 const mp_integer &x)
794{
795 const std::size_t offset_bits = get_offset_width(type);
796
797 return offset_arithmetic(
798 type, bv, 1, bv_utils.build_constant(x, offset_bits));
799}
800
802 const pointer_typet &type,
803 const bvt &bv,
804 const mp_integer &factor,
805 const exprt &index)
806{
807 bvt bv_index = convert_bv(index);
808
812
813 const std::size_t offset_bits = get_offset_width(type);
815
816 return offset_arithmetic(type, bv, factor, bv_index);
817}
818
820 const pointer_typet &type,
821 const bvt &bv,
822 const mp_integer &factor,
823 const bvt &index)
824{
826
827 if(factor == 1)
828 bv_index = index;
829 else
830 {
831 bvt bv_factor = bv_utils.build_constant(factor, index.size());
833 }
834
835 const std::size_t offset_bits = get_offset_width(type);
837
838 bvt offset_bv = offset_literals(bv, type);
839
841
843}
844
846{
847 const auto a = pointer_logic.add_object(expr);
848
849 const pointer_typet type = pointer_type(expr.type());
850 const std::size_t object_bits = get_object_width(type);
851 const std::size_t max_objects = std::size_t(1) << object_bits;
852
853 if(a == max_objects)
855 "too many addressed objects: maximum number of objects is set to 2^n=" +
856 std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
857 "); " +
858 "use the `--object-bits n` option to increase the maximum number");
859
860 return encode(a, type);
861}
862
864{
865 if(postponed.expr.id() == ID_is_dynamic_object)
866 {
867 const auto &type =
868 to_pointer_type(to_unary_expr(postponed.expr).op().type());
869 const auto &objects = pointer_logic.objects;
870 std::size_t number = 0;
871
872 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
873 {
874 const exprt &expr = *it;
875
877
878 // only compare object part
880 bvt bv = object_literals(encode(number, pt), type);
881
883
884 POSTCONDITION(bv.size() == saved_bv.size());
885 PRECONDITION(postponed.bv.size() == 1);
886
888 literalt l2 = postponed.bv.front();
889
890 if(!is_dynamic)
891 l2 = !l2;
892
894 }
895 }
896 else if(
897 const auto postponed_object_size =
899 {
900 const auto &type = to_pointer_type(postponed_object_size->pointer().type());
901 const auto &objects = pointer_logic.objects;
902 std::size_t number = 0;
903
904 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
905 {
906 const exprt &expr = *it;
907
908 if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
909 continue;
910
911 const auto size_expr = size_of_expr(expr.type(), ns);
912
913 if(!size_expr.has_value())
914 continue;
915
917 size_expr.value(), postponed_object_size->type());
918
919 // only compare object part
921 bvt bv = object_literals(encode(number, pt), type);
922
924
926
927 POSTCONDITION(bv.size() == saved_bv.size());
928 PRECONDITION(postponed.bv.size() >= 1);
929 PRECONDITION(size_bv.size() == postponed.bv.size());
930
933
935 }
936 }
937 else
939}
940
942{
943 // post-processing arrays may yield further objects, do this first
945
946 for(postponed_listt::const_iterator it = postponed_list.begin();
947 it != postponed_list.end();
948 it++)
949 do_postponed(*it);
950
951 // Clear the list to avoid re-doing in case of incremental usage.
952 postponed_list.clear();
953}
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_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)
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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
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 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)
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
literalt convert_rest(const exprt &expr) override
Definition boolbv.cpp:316
boolbv_mapt map
Definition boolbv.h:120
bv_pointers_widet(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
virtual bvt convert_pointer_type(const exprt &)
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...
literalt convert_rest(const exprt &) override
bvt convert_bitvector(const exprt &) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
std::size_t get_object_width(const pointer_typet &) const
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &)
NODISCARD bvt encode(const mp_integer &object, const pointer_typet &) const
std::vector< bvt > numbered_pointers
Table that maps a 'pointer number' to its full-width bit-vector.
pointer_logict pointer_logic
postponed_listt postponed_list
NODISCARD bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
void do_postponed(const postponedt &postponed)
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
virtual NODISCARD bvt add_addr(const exprt &)
void finish_eager_conversion() override
std::size_t get_offset_width(const pointer_typet &) const
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...
std::size_t boolbv_width(const typet &type) const override
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 is_zero(const bvt &op)
Definition bv_utils.h:144
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)
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:78
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
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:107
static bvt zeros(std::size_t new_size)
Definition bv_utils.h:193
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
static bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:183
A constant literal expression.
Definition std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
Binary minus.
Definition std_expr.h:1006
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 ...
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
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
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
The unary minus expression.
Definition std_expr.h:423
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.
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)
Various predicates over pointers in programs.
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
static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
Expression which is true when the string is equal to the literal "null".