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/replace_expr.h>
22#include <util/simplify_expr.h>
23
26
32{
33public:
35 const typet &type,
36 bool little_endian,
37 const namespacet &_ns,
38 const boolbv_widtht &_boolbv_width)
39 : endianness_mapt(_ns), boolbv_width(_boolbv_width)
40 {
41 build(type, little_endian);
42 }
43
44protected:
46
47 void build_little_endian(const typet &type) override;
48 void build_big_endian(const typet &type) override;
49};
50
52{
53 const auto &width_opt = boolbv_width.get_width_opt(src);
54 if(!width_opt.has_value())
55 return;
56
57 const std::size_t new_size = map.size() + *width_opt;
58 map.reserve(new_size);
59
60 for(std::size_t i = map.size(); i < new_size; ++i)
61 map.push_back(i);
62}
63
65{
66 if(src.id() == ID_pointer)
68 else
70}
71
73bv_pointerst::endianness_map(const typet &type, bool little_endian) const
74{
75 return bv_endianness_mapt{type, little_endian, ns, bv_width};
76}
77
79{
80 // not actually type-dependent for now
82}
83
84std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const
85{
86 const std::size_t pointer_width = type.get_width();
87 const std::size_t object_width = get_object_width(type);
88 PRECONDITION(pointer_width >= object_width);
89 return pointer_width - object_width;
90}
91
92std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const
93{
94 return type.get_width();
95}
96
98 const
99{
100 const std::size_t offset_width = get_offset_width(type);
101 const std::size_t object_width = get_object_width(type);
102 PRECONDITION(bv.size() >= offset_width + object_width);
103
104 return bvt(
105 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
106}
107
109 const
110{
111 const std::size_t offset_width = get_offset_width(type);
112 PRECONDITION(bv.size() >= offset_width);
113
114 return bvt(bv.begin(), bv.begin() + offset_width);
115}
116
117bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
118{
119 bvt result;
120 result.reserve(offset.size() + object.size());
121 result.insert(result.end(), offset.begin(), offset.end());
122 result.insert(result.end(), object.begin(), object.end());
123
124 return result;
125}
126
128{
129 PRECONDITION(expr.is_boolean());
130
131 const exprt::operandst &operands=expr.operands();
132
133 if(expr.id() == ID_is_invalid_pointer)
134 {
135 if(operands.size()==1 &&
136 operands[0].type().id()==ID_pointer)
137 {
138 const bvt &bv=convert_bv(operands[0]);
139
140 if(!bv.empty())
141 {
142 const pointer_typet &type = to_pointer_type(operands[0].type());
143 bvt object_bv = object_literals(bv, type);
144
145 bvt invalid_bv = object_literals(
147
148 const std::size_t object_bits = get_object_width(type);
149
150 bvt equal_invalid_bv;
151 equal_invalid_bv.reserve(object_bits);
152
153 for(std::size_t i=0; i<object_bits; i++)
154 {
155 equal_invalid_bv.push_back(prop.lequal(object_bv[i], invalid_bv[i]));
156 }
157
158 return prop.land(equal_invalid_bv);
159 }
160 }
161 }
162 else if(expr.id() == ID_is_dynamic_object)
163 {
164 if(operands.size()==1 &&
165 operands[0].type().id()==ID_pointer)
166 {
167 // we postpone
169
170 postponed_list.emplace_back(bvt{1, l}, convert_bv(operands[0]), expr);
171
172 return l;
173 }
174 }
175 else if(expr.id()==ID_lt || expr.id()==ID_le ||
176 expr.id()==ID_gt || expr.id()==ID_ge)
177 {
178 if(operands.size()==2 &&
179 operands[0].type().id()==ID_pointer &&
180 operands[1].type().id()==ID_pointer)
181 {
182 const bvt &bv0=convert_bv(operands[0]);
183 const bvt &bv1=convert_bv(operands[1]);
184
185 const pointer_typet &type0 = to_pointer_type(operands[0].type());
186 bvt offset_bv0 = offset_literals(bv0, type0);
187
188 const pointer_typet &type1 = to_pointer_type(operands[1].type());
189 bvt offset_bv1 = offset_literals(bv1, type1);
190
191 // Comparison over pointers to distinct objects is undefined behavior in
192 // C; we choose to always produce "false" in such a case. Alternatively,
193 // we could do a comparison over the integer representation of a pointer
194
195 // do the same-object-test via an expression as this may permit re-using
196 // already cached encodings of the equality test
197 const exprt same_object = ::same_object(operands[0], operands[1]);
198 const literalt same_object_lit = convert(same_object);
199 if(same_object_lit.is_false())
200 return same_object_lit;
201
202 // The comparison is UNSIGNED, to match the type of pointer_offsett
203 return prop.land(
204 same_object_lit,
206 offset_bv0,
207 expr.id(),
208 offset_bv1,
210 }
211 }
212 else if(
213 auto prophecy_r_or_w_ok =
215 {
216 return convert(simplify_expr(prophecy_r_or_w_ok->lower(ns), ns));
217 }
218 else if(
219 auto prophecy_pointer_in_range =
221 {
222 return convert(simplify_expr(prophecy_pointer_in_range->lower(ns), ns));
223 }
224
225 return SUB::convert_rest(expr);
226}
227
229 const namespacet &_ns,
230 propt &_prop,
231 message_handlert &message_handler,
232 bool get_array_constraints)
233 : boolbvt(_ns, _prop, message_handler, get_array_constraints),
234 pointer_logic(_ns)
235{
236}
237
238std::optional<bvt> bv_pointerst::convert_address_of_rec(const exprt &expr)
239{
240 if(expr.id()==ID_symbol)
241 {
242 return add_addr(expr);
243 }
244 else if(expr.id()==ID_label)
245 {
246 return add_addr(expr);
247 }
248 else if(expr.id() == ID_null_object)
249 {
250 pointer_typet pt = pointer_type(expr.type());
252 }
253 else if(expr.id()==ID_index)
254 {
255 const index_exprt &index_expr=to_index_expr(expr);
256 const exprt &array=index_expr.array();
257 const exprt &index=index_expr.index();
258 const auto &array_type = to_array_type(array.type());
259
260 pointer_typet type = pointer_type(expr.type());
261 const std::size_t bits = boolbv_width(type);
262
263 bvt bv;
264
265 // recursive call
266 if(array_type.id()==ID_pointer)
267 {
268 // this should be gone
269 bv=convert_pointer_type(array);
270 CHECK_RETURN(bv.size()==bits);
271 }
272 else if(array_type.id()==ID_array ||
273 array_type.id()==ID_string_constant)
274 {
275 auto bv_opt = convert_address_of_rec(array);
276 if(!bv_opt.has_value())
277 return {};
278 bv = std::move(*bv_opt);
279 CHECK_RETURN(bv.size()==bits);
280 }
281 else
283
284 // get size
285 auto size = size_of_expr(array_type.element_type(), ns);
286 CHECK_RETURN(size.has_value());
287
288 bv = offset_arithmetic(type, bv, *size, index);
289 CHECK_RETURN(bv.size()==bits);
290
291 return std::move(bv);
292 }
293 else if(expr.id()==ID_byte_extract_little_endian ||
294 expr.id()==ID_byte_extract_big_endian)
295 {
296 const auto &byte_extract_expr=to_byte_extract_expr(expr);
297
298 // recursive call
299 auto bv_opt = convert_address_of_rec(byte_extract_expr.op());
300 if(!bv_opt.has_value())
301 return {};
302
303 pointer_typet type = pointer_type(expr.type());
304 const std::size_t bits = boolbv_width(type);
305 CHECK_RETURN(bv_opt->size() == bits);
306
307 bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
308 CHECK_RETURN(bv.size()==bits);
309 return std::move(bv);
310 }
311 else if(expr.id()==ID_member)
312 {
313 const member_exprt &member_expr=to_member_expr(expr);
314 const exprt &struct_op = member_expr.compound();
315
316 // recursive call
317 auto bv_opt = convert_address_of_rec(struct_op);
318 if(!bv_opt.has_value())
319 return {};
320
321 bvt bv = std::move(*bv_opt);
322 if(
323 struct_op.type().id() == ID_struct ||
324 struct_op.type().id() == ID_struct_tag)
325 {
326 const struct_typet &struct_op_type =
327 struct_op.type().id() == ID_struct_tag
328 ? ns.follow_tag(to_struct_tag_type(struct_op.type()))
329 : to_struct_type(struct_op.type());
330 auto offset =
331 member_offset(struct_op_type, member_expr.get_component_name(), ns);
332 CHECK_RETURN(offset.has_value());
333
334 // add offset
335 pointer_typet type = pointer_type(expr.type());
336 bv = offset_arithmetic(type, bv, *offset);
337 }
338 else
339 {
340 INVARIANT(
341 struct_op.type().id() == ID_union ||
342 struct_op.type().id() == ID_union_tag,
343 "member expression should operate on struct or union");
344 // nothing to do, all members have offset 0
345 }
346
347 return std::move(bv);
348 }
349 else if(
350 expr.is_constant() || expr.id() == ID_string_constant ||
351 expr.id() == ID_array)
352 { // constant
353 return add_addr(expr);
354 }
355 else if(expr.id()==ID_if)
356 {
357 const if_exprt &ifex=to_if_expr(expr);
358
359 literalt cond=convert(ifex.cond());
360
361 bvt bv1, bv2;
362
363 auto bv1_opt = convert_address_of_rec(ifex.true_case());
364 if(!bv1_opt.has_value())
365 return {};
366
367 auto bv2_opt = convert_address_of_rec(ifex.false_case());
368 if(!bv2_opt.has_value())
369 return {};
370
371 return bv_utils.select(cond, *bv1_opt, *bv2_opt);
372 }
373
374 return {};
375}
376
378{
379 const pointer_typet &type = to_pointer_type(expr.type());
380
381 const std::size_t bits = boolbv_width(expr.type());
382
383 if(expr.id()==ID_symbol)
384 {
385 const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
386
387 return map.get_literals(identifier, type, bits);
388 }
389 else if(expr.id()==ID_nondet_symbol)
390 {
391 return prop.new_variables(bits);
392 }
393 else if(expr.id()==ID_typecast)
394 {
395 const typecast_exprt &typecast_expr = to_typecast_expr(expr);
396
397 const exprt &op = typecast_expr.op();
398 const typet &op_type = op.type();
399
400 if(op_type.id()==ID_pointer)
401 return convert_bv(op);
402 else if(
403 can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_bool ||
404 op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
405 {
406 // Cast from a bitvector type to pointer.
407 // We just do a zero extension.
408
409 const bvt &op_bv=convert_bv(op);
410
411 return bv_utils.zero_extension(op_bv, bits);
412 }
413 }
414 else if(expr.id()==ID_if)
415 {
416 return SUB::convert_if(to_if_expr(expr));
417 }
418 else if(expr.id()==ID_index)
419 {
420 return SUB::convert_index(to_index_expr(expr));
421 }
422 else if(expr.id()==ID_member)
423 {
425 }
426 else if(expr.id()==ID_address_of)
427 {
428 const address_of_exprt &address_of_expr = to_address_of_expr(expr);
429
430 auto bv_opt = convert_address_of_rec(address_of_expr.op());
431 if(!bv_opt.has_value())
432 return conversion_failed(address_of_expr);
433
434 CHECK_RETURN(bv_opt->size() == bits);
435 return *bv_opt;
436 }
437 else if(expr.id() == ID_object_address)
438 {
439 const auto &object_address_expr = to_object_address_expr(expr);
440 return add_addr(object_address_expr.object_expr());
441 }
442 else if(expr.is_constant())
443 {
444 const constant_exprt &c = to_constant_expr(expr);
445
446 if(is_null_pointer(c))
447 return encode(pointer_logic.get_null_object(), type);
448 else
449 {
450 mp_integer i = bvrep2integer(c.get_value(), bits, false);
451 return bv_utils.build_constant(i, bits);
452 }
453 }
454 else if(expr.id()==ID_plus)
455 {
456 // this has to be pointer plus integer
457
458 const plus_exprt &plus_expr = to_plus_expr(expr);
459
460 bvt bv;
461
462 mp_integer size=0;
463 std::size_t count=0;
464
465 for(const auto &op : plus_expr.operands())
466 {
467 if(op.type().id() == ID_pointer)
468 {
469 count++;
470 bv = convert_bv(op);
471 CHECK_RETURN(bv.size()==bits);
472
473 typet pointer_base_type = to_pointer_type(op.type()).base_type();
475 pointer_base_type.id() != ID_empty,
476 "no pointer arithmetic over void pointers");
477 auto size_opt = pointer_offset_size(pointer_base_type, ns);
478 CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
479 size = *size_opt;
480 }
481 }
482
483 INVARIANT(
484 count == 1,
485 "there should be exactly one pointer-type operand in a pointer-type sum");
486
487 const std::size_t offset_bits = get_offset_width(type);
488 bvt sum = bv_utils.build_constant(0, offset_bits);
489
490 for(const auto &operand : plus_expr.operands())
491 {
492 if(operand.type().id() == ID_pointer)
493 continue;
494
495 if(
496 operand.type().id() != ID_unsignedbv &&
497 operand.type().id() != ID_signedbv)
498 {
499 return conversion_failed(plus_expr);
500 }
501
502 bv_utilst::representationt rep = operand.type().id() == ID_signedbv
505
506 bvt op = convert_bv(operand);
507 CHECK_RETURN(!op.empty());
508
509 op = bv_utils.extension(op, offset_bits, rep);
510
511 sum=bv_utils.add(sum, op);
512 }
513
514 return offset_arithmetic(type, bv, size, sum);
515 }
516 else if(expr.id()==ID_minus)
517 {
518 // this is pointer-integer
519
520 const minus_exprt &minus_expr = to_minus_expr(expr);
521
522 INVARIANT(
523 minus_expr.lhs().type().id() == ID_pointer,
524 "first operand should be of pointer type");
525
526 if(
527 minus_expr.rhs().type().id() != ID_unsignedbv &&
528 minus_expr.rhs().type().id() != ID_signedbv)
529 {
530 return conversion_failed(minus_expr);
531 }
532
533 const unary_minus_exprt neg_op1(minus_expr.rhs());
534
535 const bvt &bv = convert_bv(minus_expr.lhs());
536
537 typet pointer_base_type =
538 to_pointer_type(minus_expr.lhs().type()).base_type();
540 pointer_base_type.id() != ID_empty,
541 "no pointer arithmetic over void pointers");
542 auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
543 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
544 return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
545 }
546 else if(expr.id()==ID_byte_extract_little_endian ||
547 expr.id()==ID_byte_extract_big_endian)
548 {
550 }
551 else if(
552 expr.id() == ID_byte_update_little_endian ||
553 expr.id() == ID_byte_update_big_endian)
554 {
556 }
557 else if(expr.id() == ID_field_address)
558 {
559 const auto &field_address_expr = to_field_address_expr(expr);
560 const typet &compound_type = field_address_expr.compound_type();
561
562 // recursive call
563 auto bv = convert_bitvector(field_address_expr.base());
564
565 if(compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag)
566 {
567 const struct_typet &struct_type =
568 compound_type.id() == ID_struct_tag
569 ? ns.follow_tag(to_struct_tag_type(compound_type))
570 : to_struct_type(compound_type);
571 auto offset =
572 member_offset(struct_type, field_address_expr.component_name(), ns);
573 CHECK_RETURN(offset.has_value());
574
575 // add offset
576 bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
577 }
578 else if(
579 compound_type.id() == ID_union || compound_type.id() == ID_union_tag)
580 {
581 // nothing to do, all fields have offset 0
582 }
583 else
584 {
585 INVARIANT(false, "field address expressions operate on struct or union");
586 }
587
588 return bv;
589 }
590 else if(expr.id() == ID_element_address)
591 {
592 const auto &element_address_expr = to_element_address_expr(expr);
593
594 // recursive call
595 auto bv = convert_bitvector(element_address_expr.base());
596
597 // get element size
598 auto size = pointer_offset_size(element_address_expr.element_type(), ns);
599 CHECK_RETURN(size.has_value() && *size >= 0);
600
601 // add offset
603 element_address_expr.type(), bv, *size, element_address_expr.index());
604
605 return bv;
606 }
607
608 return conversion_failed(expr);
609}
610
611static bool is_pointer_subtraction(const exprt &expr)
612{
613 if(expr.id() != ID_minus)
614 return false;
615
616 const auto &minus_expr = to_minus_expr(expr);
617
618 return minus_expr.lhs().type().id() == ID_pointer &&
619 minus_expr.rhs().type().id() == ID_pointer;
620}
621
623{
624 if(expr.type().id()==ID_pointer)
625 return convert_pointer_type(expr);
626
627 if(is_pointer_subtraction(expr))
628 {
629 std::size_t width=boolbv_width(expr.type());
630
631 // pointer minus pointer is subtraction over the offset divided by element
632 // size, iff the pointers point to the same object
633 const auto &minus_expr = to_minus_expr(expr);
634
635 // do the same-object-test via an expression as this may permit re-using
636 // already cached encodings of the equality test
637 const exprt same_object = ::same_object(minus_expr.lhs(), minus_expr.rhs());
638 const literalt same_object_lit = convert(same_object);
639
640 bvt bv = prop.new_variables(width);
641
642 if(!same_object_lit.is_false())
643 {
644 const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type());
645 const bvt &lhs = convert_bv(minus_expr.lhs());
646 const bvt lhs_offset =
647 bv_utils.zero_extension(offset_literals(lhs, lhs_pt), width);
648
649 const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type());
650 const bvt &rhs = convert_bv(minus_expr.rhs());
651 const bvt rhs_offset =
652 bv_utils.zero_extension(offset_literals(rhs, rhs_pt), width);
653
654 bvt difference = bv_utils.sub(lhs_offset, rhs_offset);
655
657 lhs_pt.base_type().id() != ID_empty,
658 "no pointer arithmetic over void pointers");
659 auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
660 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
661
662 if(*element_size_opt != 1)
663 {
664 bvt element_size_bv = bv_utils.build_constant(*element_size_opt, width);
665 difference = bv_utils.divider(
666 difference, element_size_bv, bv_utilst::representationt::SIGNED);
667 }
668
669 // test for null object (integer constants)
670 const exprt null_object = ::null_object(minus_expr.lhs());
671 literalt in_bounds = convert(null_object);
672
673 if(!in_bounds.is_true())
674 {
675 // compute the object size (again, possibly using cached results)
676 const exprt object_size = ::object_size(minus_expr.lhs());
677 const bvt object_size_bv =
679
680 const literalt lhs_in_bounds = prop.land(
681 !bv_utils.sign_bit(lhs_offset),
683 lhs_offset,
684 ID_le,
685 object_size_bv,
687
688 const literalt rhs_in_bounds = prop.land(
689 !bv_utils.sign_bit(rhs_offset),
691 rhs_offset,
692 ID_le,
693 object_size_bv,
695
696 in_bounds =
697 prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
698 }
699
701 prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
702 }
703
704 return bv;
705 }
706 else if(
707 expr.id() == ID_pointer_offset &&
708 to_pointer_offset_expr(expr).pointer().type().id() == ID_pointer)
709 {
710 std::size_t width=boolbv_width(expr.type());
711
712 const exprt &pointer = to_pointer_offset_expr(expr).pointer();
713 const bvt &pointer_bv = convert_bv(pointer);
714
715 bvt offset_bv =
716 offset_literals(pointer_bv, to_pointer_type(pointer.type()));
717
718 return bv_utils.zero_extension(offset_bv, width);
719 }
720 else if(
722 {
723 // we postpone until we know the objects
724 std::size_t width = boolbv_width(object_size->type());
725
726 postponed_list.emplace_back(
727 prop.new_variables(width),
728 convert_bv(object_size->pointer()),
729 *object_size);
730
731 return postponed_list.back().bv;
732 }
733 else if(
734 expr.id() == ID_pointer_object &&
735 to_pointer_object_expr(expr).pointer().type().id() == ID_pointer)
736 {
737 std::size_t width=boolbv_width(expr.type());
738
739 const exprt &pointer = to_pointer_object_expr(expr).pointer();
740 const bvt &pointer_bv = convert_bv(pointer);
741
742 bvt object_bv =
743 object_literals(pointer_bv, to_pointer_type(pointer.type()));
744
745 return bv_utils.zero_extension(object_bv, width);
746 }
747 else if(
748 expr.id() == ID_typecast &&
749 to_typecast_expr(expr).op().type().id() == ID_pointer)
750 {
751 // pointer to int
752 bvt op0 = convert_bv(to_typecast_expr(expr).op());
753
754 // squeeze it in!
755 std::size_t width=boolbv_width(expr.type());
756
757 return bv_utils.zero_extension(op0, width);
758 }
759
760 return SUB::convert_bitvector(expr);
761}
762
763static std::string bits_to_string(const propt &prop, const bvt &bv)
764{
765 std::string result;
766
767 for(const auto &literal : bv)
768 {
769 char ch=0;
770
771 // clang-format off
772 switch(prop.l_get(literal).get_value())
773 {
774 case tvt::tv_enumt::TV_FALSE: ch = '0'; break;
775 case tvt::tv_enumt::TV_TRUE: ch = '1'; break;
776 case tvt::tv_enumt::TV_UNKNOWN: ch = '0'; break;
777 }
778 // clang-format on
779
780 result = ch + result;
781 }
782
783 return result;
784}
785
787 const exprt &expr,
788 const bvt &bv,
789 std::size_t offset) const
790{
791 const typet &type = expr.type();
792
793 if(type.id() != ID_pointer)
794 return SUB::bv_get_rec(expr, bv, offset);
795
796 const pointer_typet &pt = to_pointer_type(type);
797 const std::size_t bits = boolbv_width(pt);
798 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
799
800 std::string value = bits_to_string(prop, value_bv);
801 std::string value_addr = bits_to_string(prop, object_literals(value_bv, pt));
802 std::string value_offset =
803 bits_to_string(prop, offset_literals(value_bv, pt));
804
805 // we treat these like bit-vector constants, but with
806 // some additional annotation
807
808 const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
809 return value[value.size() - 1 - i] == '1';
810 });
811
812 constant_exprt result(bvrep, type);
813
816 binary2integer(value_offset, false)};
817
819 bvrep, pointer_logic.pointer_expr(pointer, pt)};
820}
821
823 const
824{
825 const std::size_t offset_bits = get_offset_width(type);
826 const std::size_t object_bits = get_object_width(type);
827
828 bvt zero_offset(offset_bits, const_literal(false));
829 bvt object = bv_utils.build_constant(addr, object_bits);
830
831 return object_offset_encoding(object, zero_offset);
832}
833
835 const pointer_typet &type,
836 const bvt &bv,
837 const mp_integer &x)
838{
839 const std::size_t offset_bits = get_offset_width(type);
840
841 return offset_arithmetic(
842 type, bv, 1, bv_utils.build_constant(x, offset_bits));
843}
844
846 const pointer_typet &type,
847 const bvt &bv,
848 const mp_integer &factor,
849 const exprt &index)
850{
851 bvt bv_index=convert_bv(index);
852
854 index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
856
857 const std::size_t offset_bits = get_offset_width(type);
858 bv_index=bv_utils.extension(bv_index, offset_bits, rep);
859
860 return offset_arithmetic(type, bv, factor, bv_index);
861}
862
864 const pointer_typet &type,
865 const bvt &bv,
866 const exprt &factor,
867 const exprt &index)
868{
869 bvt bv_factor = convert_bv(factor);
870 bvt bv_index =
872
873 bv_utilst::representationt rep = factor.type().id() == ID_signedbv
876
877 bv_index = bv_utils.multiplier(bv_index, bv_factor, rep);
878
879 const std::size_t offset_bits = get_offset_width(type);
880 bv_index = bv_utils.extension(bv_index, offset_bits, rep);
881
882 return offset_arithmetic(type, bv, 1, bv_index);
883}
884
886 const pointer_typet &type,
887 const bvt &bv,
888 const mp_integer &factor,
889 const bvt &index)
890{
891 bvt bv_index;
892
893 if(factor==1)
894 bv_index=index;
895 else
896 {
897 bvt bv_factor=bv_utils.build_constant(factor, index.size());
898 bv_index = bv_utils.signed_multiplier(index, bv_factor);
899 }
900
901 const std::size_t offset_bits = get_offset_width(type);
902 bv_index = bv_utils.zero_extension(bv_index, offset_bits);
903
904 bvt offset_bv = offset_literals(bv, type);
905
906 bvt bv_tmp = bv_utils.add(offset_bv, bv_index);
907
908 return object_offset_encoding(object_literals(bv, type), bv_tmp);
909}
910
912{
913 const auto a = pointer_logic.add_object(expr);
914
915 const pointer_typet type = pointer_type(expr.type());
916 const std::size_t object_bits = get_object_width(type);
917 const std::size_t max_objects=std::size_t(1)<<object_bits;
918
919 if(a==max_objects)
921 "too many addressed objects: maximum number of objects is set to 2^n=" +
922 std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
923 "); " +
924 "use the `--object-bits n` option to increase the maximum number");
925
926 return encode(a, type);
927}
928
930 std::vector<symbol_exprt> &placeholders) const
931{
932 PRECONDITION(placeholders.empty());
933
934 const auto &objects = pointer_logic.objects;
935 std::size_t number = 0;
936
937 exprt::operandst dynamic_objects_ops, not_dynamic_objects_ops;
938 dynamic_objects_ops.reserve(objects.size());
939 not_dynamic_objects_ops.reserve(objects.size());
940
941 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
942 {
943 const exprt &expr = *it;
944
945 // only compare object part
946 pointer_typet pt = pointer_type(expr.type());
947 bvt bv = object_literals(encode(number, pt), pt);
948
949 exprt::operandst conjuncts;
950 conjuncts.reserve(bv.size());
951 placeholders.reserve(bv.size());
952 for(std::size_t i = 0; i < bv.size(); ++i)
953 {
954 if(placeholders.size() <= i)
955 placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}});
956
957 POSTCONDITION(bv[i].is_constant());
958 if(bv[i].is_true())
959 conjuncts.emplace_back(placeholders[i]);
960 else
961 conjuncts.emplace_back(not_exprt{placeholders[i]});
962 }
963
965 dynamic_objects_ops.push_back(conjunction(conjuncts));
966 else
967 not_dynamic_objects_ops.push_back(conjunction(conjuncts));
968 }
969
970 exprt dynamic_objects = disjunction(dynamic_objects_ops);
971 exprt not_dynamic_objects = disjunction(not_dynamic_objects_ops);
972
973 bdd_exprt bdd_converter;
974 bddt dyn_bdd = bdd_converter.from_expr(dynamic_objects);
975 bddt not_dyn_bdd = bdd_converter.from_expr(not_dynamic_objects);
976
977 return {bdd_converter.as_expr(dyn_bdd), bdd_converter.as_expr(not_dyn_bdd)};
978}
979
980std::unordered_map<exprt, exprt, irep_hash>
982 std::vector<symbol_exprt> &placeholders) const
983{
984 PRECONDITION(placeholders.empty());
985
986 const auto &objects = pointer_logic.objects;
987 std::size_t number = 0;
988
989 std::unordered_map<exprt, exprt::operandst, irep_hash> per_size_object_ops;
990
991 for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
992 {
993 const exprt &expr = *it;
994
995 if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
996 continue;
997
998 const auto size_expr = size_of_expr(expr.type(), ns);
999 if(!size_expr.has_value())
1000 continue;
1001
1002 // only compare object part
1003 pointer_typet pt = pointer_type(expr.type());
1004 bvt bv = object_literals(encode(number, pt), pt);
1005
1006 exprt::operandst conjuncts;
1007 conjuncts.reserve(bv.size());
1008 placeholders.reserve(bv.size());
1009 for(std::size_t i = 0; i < bv.size(); ++i)
1010 {
1011 if(placeholders.size() <= i)
1012 placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}});
1013
1014 POSTCONDITION(bv[i].is_constant());
1015 if(bv[i].is_true())
1016 conjuncts.emplace_back(placeholders[i]);
1017 else
1018 conjuncts.emplace_back(not_exprt{placeholders[i]});
1019 }
1020
1021 per_size_object_ops[size_expr.value()].push_back(conjunction(conjuncts));
1022 }
1023
1024 std::unordered_map<exprt, exprt, irep_hash> result;
1025 for(const auto &size_entry : per_size_object_ops)
1026 {
1027 exprt all_objects_this_size = disjunction(size_entry.second);
1028 bdd_exprt bdd_converter;
1029 bddt bdd = bdd_converter.from_expr(all_objects_this_size);
1030
1031 result.emplace(size_entry.first, bdd_converter.as_expr(bdd));
1032 }
1033
1034 return result;
1035}
1036
1038{
1039 // post-processing arrays may yield further objects, do this first
1041
1042 // it would seem nicer to use `optionalt` here, but GCC >= 12 produces
1043 // spurious warnings about accessing uninitialized objects
1044 std::pair<exprt, exprt> is_dynamic_expr = {nil_exprt{}, nil_exprt{}};
1045 std::vector<symbol_exprt> is_dynamic_placeholders;
1046
1047 std::unordered_map<exprt, exprt, irep_hash> object_sizes;
1048 std::vector<symbol_exprt> object_size_placeholders;
1049
1050 for(const postponedt &postponed : postponed_list)
1051 {
1052 if(postponed.expr.id() == ID_is_dynamic_object)
1053 {
1054 if(is_dynamic_expr.first.is_nil())
1055 is_dynamic_expr =
1056 prepare_postponed_is_dynamic_object(is_dynamic_placeholders);
1057
1058 const auto &type =
1059 to_pointer_type(to_unary_expr(postponed.expr).op().type());
1060 bvt saved_bv = object_literals(postponed.op, type);
1061 POSTCONDITION(saved_bv.size() == is_dynamic_placeholders.size());
1062 replace_mapt replacements;
1063 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1064 {
1065 replacements.emplace(
1066 is_dynamic_placeholders[i], literal_exprt{saved_bv[i]});
1067 }
1068 exprt is_dyn = is_dynamic_expr.first;
1069 replace_expr(replacements, is_dyn);
1070 exprt is_not_dyn = is_dynamic_expr.second;
1071 replace_expr(replacements, is_not_dyn);
1072
1073 PRECONDITION(postponed.bv.size() == 1);
1075 prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
1077 prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
1078 }
1079 else if(
1080 const auto postponed_object_size =
1082 {
1083 if(object_sizes.empty())
1084 object_sizes = prepare_postponed_object_size(object_size_placeholders);
1085
1086 // we might not have any usable objects
1087 if(object_size_placeholders.empty())
1088 continue;
1089
1090 const auto &type =
1091 to_pointer_type(postponed_object_size->pointer().type());
1092 bvt saved_bv = object_literals(postponed.op, type);
1093 POSTCONDITION(saved_bv.size() == object_size_placeholders.size());
1094 replace_mapt replacements;
1095 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1096 {
1097 replacements.emplace(
1098 object_size_placeholders[i], literal_exprt{saved_bv[i]});
1099 }
1100
1101 for(const auto &object_size_entry : object_sizes)
1102 {
1104 object_size_entry.first, postponed_object_size->type());
1105 bvt size_bv = convert_bv(object_size);
1106 POSTCONDITION(size_bv.size() == postponed.bv.size());
1107
1108 exprt all_objects_this_size = object_size_entry.second;
1109 replace_expr(replacements, all_objects_this_size);
1110
1111 literalt l1 = convert_bv(all_objects_this_size)[0];
1112 if(l1.is_true())
1113 {
1114 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1115 prop.set_equal(postponed.bv[i], size_bv[i]);
1116 break;
1117 }
1118 else if(l1.is_false())
1119 continue;
1120#define COMPACT_OBJECT_SIZE_EQ
1121#ifndef COMPACT_OBJECT_SIZE_EQ
1122 literalt l2 = bv_utils.equal(postponed.bv, size_bv);
1123
1125#else
1126 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1127 {
1128 prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
1129 prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
1130 }
1131#endif
1132 }
1133 }
1134 else
1136 }
1137
1138 // Clear the list to avoid re-doing in case of incremental usage.
1139 postponed_list.clear();
1140}
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...
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.
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
exprt as_expr(const bddt &root) const
Definition bdd_expr.cpp:171
bddt from_expr(const exprt &expr)
Definition bdd_expr.cpp:87
Logical operations on BDDs.
Definition bdd_cudd.h:78
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
std::size_t get_width() const
Definition std_types.h:920
The Boolean type.
Definition std_types.h:36
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
virtual std::optional< 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 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:116
void finish_eager_conversion() override
Definition boolbv.h:80
bv_utilst bv_utils
Definition boolbv.h:117
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:102
literalt convert_rest(const exprt &expr) override
Definition boolbv.cpp:332
boolbv_mapt map
Definition boolbv.h:123
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 &)
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:138
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:2987
const irep_idt & get_value() const
Definition std_expr.h:2995
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:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
const irep_idt & id() const
Definition irep.h:388
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:2841
const exprt & compound() const
Definition std_expr.h:2890
irep_idt get_component_name() const
Definition std_expr.h:2863
Binary minus.
Definition std_expr.h:1061
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The NIL expression.
Definition std_expr.h:3073
Boolean negation.
Definition std_expr.h:2327
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 ...
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
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
tv_enumt get_value() const
Definition threeval.h:40
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
The unary minus expression.
Definition std_expr.h:484
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.
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)
exprt null_object(const exprt &pointer)
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:66
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:54
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1533
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
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:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
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:3037
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
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:943
std::size_t object_bits
Definition config.h:355