cprover
Loading...
Searching...
No Matches
pointer_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for Pointers
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_POINTER_EXPR_H
10#define CPROVER_UTIL_POINTER_EXPR_H
11
14
15#include "bitvector_types.h"
16#include "std_expr.h"
17
18class namespacet;
19
24{
25public:
26 pointer_typet(typet _base_type, std::size_t width)
27 : bitvector_typet(ID_pointer, width)
28 {
29 subtype().swap(_base_type);
30 }
31
35 const typet &base_type() const
36 {
37 return subtype();
38 }
39
44 {
45 return subtype();
46 }
47
49 {
50 return signedbv_typet(get_width());
51 }
52
53 static void check(
54 const typet &type,
56 {
58 DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
59 }
60};
61
65template <>
66inline bool can_cast_type<pointer_typet>(const typet &type)
67{
68 return type.id() == ID_pointer;
69}
70
79inline const pointer_typet &to_pointer_type(const typet &type)
80{
83 return static_cast<const pointer_typet &>(type);
84}
85
88{
91 return static_cast<pointer_typet &>(type);
92}
93
96inline bool is_void_pointer(const typet &type)
97{
98 return type.id() == ID_pointer &&
99 to_pointer_type(type).base_type().id() == ID_empty;
100}
101
107{
108public:
109 reference_typet(typet _subtype, std::size_t _width)
110 : pointer_typet(std::move(_subtype), _width)
111 {
112 set(ID_C_reference, true);
113 }
114
115 static void check(
116 const typet &type,
118 {
119 PRECONDITION(type.id() == ID_pointer);
121 vm, type.get_sub().size() == 1, "reference must have one type parameter");
123 static_cast<const reference_typet &>(type);
125 vm, !reference_type.get(ID_width).empty(), "reference must have width");
127 vm, reference_type.get_width() > 0, "reference must have non-zero width");
128 }
129};
130
134template <>
135inline bool can_cast_type<reference_typet>(const typet &type)
136{
137 return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
138}
139
148inline const reference_typet &to_reference_type(const typet &type)
149{
151 return static_cast<const reference_typet &>(type);
152}
153
156{
158 return static_cast<reference_typet &>(type);
159}
160
161bool is_reference(const typet &type);
162
163bool is_rvalue_reference(const typet &type);
164
167{
168public:
170 : binary_exprt(
171 exprt(ID_unknown),
172 ID_object_descriptor,
173 exprt(ID_unknown),
174 typet())
175 {
176 }
177
179 : binary_exprt(
180 std::move(_object),
181 ID_object_descriptor,
182 exprt(ID_unknown),
183 typet())
184 {
185 }
186
191 void build(const exprt &expr, const namespacet &ns);
192
194 {
195 return op0();
196 }
197
198 const exprt &object() const
199 {
200 return op0();
201 }
202
203 static const exprt &root_object(const exprt &expr);
204 const exprt &root_object() const
205 {
206 return root_object(object());
207 }
208
210 {
211 return op1();
212 }
213
214 const exprt &offset() const
215 {
216 return op1();
217 }
218};
219
220template <>
222{
223 return base.id() == ID_object_descriptor;
224}
225
226inline void validate_expr(const object_descriptor_exprt &value)
227{
228 validate_operands(value, 2, "Object descriptor must have two operands");
229}
230
237inline const object_descriptor_exprt &
239{
240 PRECONDITION(expr.id() == ID_object_descriptor);
241 const object_descriptor_exprt &ret =
242 static_cast<const object_descriptor_exprt &>(expr);
243 validate_expr(ret);
244 return ret;
245}
246
249{
250 PRECONDITION(expr.id() == ID_object_descriptor);
251 object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
252 validate_expr(ret);
253 return ret;
254}
255
258{
259public:
261 : binary_exprt(
262 exprt(ID_unknown),
263 ID_dynamic_object,
264 exprt(ID_unknown),
265 std::move(type))
266 {
267 }
268
269 void set_instance(unsigned int instance);
270
271 unsigned int get_instance() const;
272
274 {
275 return op1();
276 }
277
278 const exprt &valid() const
279 {
280 return op1();
281 }
282};
283
284template <>
286{
287 return base.id() == ID_dynamic_object;
288}
289
290inline void validate_expr(const dynamic_object_exprt &value)
291{
292 validate_operands(value, 2, "Dynamic object must have two operands");
293}
294
302{
303 PRECONDITION(expr.id() == ID_dynamic_object);
304 const dynamic_object_exprt &ret =
305 static_cast<const dynamic_object_exprt &>(expr);
306 validate_expr(ret);
307 return ret;
308}
309
312{
313 PRECONDITION(expr.id() == ID_dynamic_object);
314 dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
315 validate_expr(ret);
316 return ret;
317}
318
321{
322public:
324 : unary_predicate_exprt(ID_is_dynamic_object, op)
325 {
326 }
327};
328
329template <>
331{
332 return base.id() == ID_is_invalid_pointer;
333}
334
335inline void validate_expr(const is_dynamic_object_exprt &value)
336{
337 validate_operands(value, 1, "is_dynamic_object must have one operand");
338}
339
340inline const is_dynamic_object_exprt &
342{
343 PRECONDITION(expr.id() == ID_is_dynamic_object);
345 expr.operands().size() == 1, "is_dynamic_object must have one operand");
346 return static_cast<const is_dynamic_object_exprt &>(expr);
347}
348
352{
353 PRECONDITION(expr.id() == ID_is_dynamic_object);
355 expr.operands().size() == 1, "is_dynamic_object must have one operand");
356 return static_cast<is_dynamic_object_exprt &>(expr);
357}
358
361{
362public:
363 explicit address_of_exprt(const exprt &op);
364
366 : unary_exprt(ID_address_of, std::move(op), std::move(_type))
367 {
368 }
369
371 {
372 return op0();
373 }
374
375 const exprt &object() const
376 {
377 return op0();
378 }
379};
380
381template <>
383{
384 return base.id() == ID_address_of;
385}
386
387inline void validate_expr(const address_of_exprt &value)
388{
389 validate_operands(value, 1, "Address of must have one operand");
390}
391
398inline const address_of_exprt &to_address_of_expr(const exprt &expr)
399{
400 PRECONDITION(expr.id() == ID_address_of);
401 const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
402 validate_expr(ret);
403 return ret;
404}
405
408{
409 PRECONDITION(expr.id() == ID_address_of);
410 address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
411 validate_expr(ret);
412 return ret;
413}
414
417{
418public:
419 explicit object_address_exprt(const symbol_exprt &);
420
422 {
423 return get(ID_identifier);
424 }
425
426 const pointer_typet &type() const
427 {
428 return static_cast<const pointer_typet &>(exprt::type());
429 }
430
432 {
433 return static_cast<pointer_typet &>(exprt::type());
434 }
435
437 const typet &object_type() const
438 {
439 return type().base_type();
440 }
441
443};
444
445template <>
447{
448 return base.id() == ID_object_address;
449}
450
451inline void validate_expr(const object_address_exprt &value)
452{
453 validate_operands(value, 1, "object_address must have one operand");
454}
455
463{
464 PRECONDITION(expr.id() == ID_object_address);
465 const object_address_exprt &ret =
466 static_cast<const object_address_exprt &>(expr);
467 validate_expr(ret);
468 return ret;
469}
470
473{
474 PRECONDITION(expr.id() == ID_object_address);
475 object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
476 validate_expr(ret);
477 return ret;
478}
479
483{
484public:
488 exprt base,
491
493 {
494 return op0();
495 }
496
497 const exprt &base() const
498 {
499 return op0();
500 }
501
502 const pointer_typet &type() const
503 {
504 return static_cast<const pointer_typet &>(exprt::type());
505 }
506
508 {
509 return static_cast<pointer_typet &>(exprt::type());
510 }
511
513 const typet &field_type() const
514 {
515 return type().base_type();
516 }
517
518 const typet &compound_type() const
519 {
520 return to_pointer_type(base().type()).base_type();
521 }
522
524 {
525 return get(ID_component_name);
526 }
527};
528
529template <>
531{
532 return expr.id() == ID_field_address;
533}
534
535inline void validate_expr(const field_address_exprt &value)
536{
537 validate_operands(value, 1, "field_address must have one operand");
538}
539
547{
548 PRECONDITION(expr.id() == ID_field_address);
549 const field_address_exprt &ret =
550 static_cast<const field_address_exprt &>(expr);
551 validate_expr(ret);
552 return ret;
553}
554
557{
558 PRECONDITION(expr.id() == ID_field_address);
559 field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
560 validate_expr(ret);
561 return ret;
562}
563
567{
568public:
573
574 const pointer_typet &type() const
575 {
576 return static_cast<const pointer_typet &>(exprt::type());
577 }
578
580 {
581 return static_cast<pointer_typet &>(exprt::type());
582 }
583
585 const typet &element_type() const
586 {
587 return type().base_type();
588 }
589
591 {
592 return op0();
593 }
594
595 const exprt &base() const
596 {
597 return op0();
598 }
599
601 {
602 return op1();
603 }
604
605 const exprt &index() const
606 {
607 return op1();
608 }
609};
610
611template <>
613{
614 return expr.id() == ID_element_address;
615}
616
617inline void validate_expr(const element_address_exprt &value)
618{
619 validate_operands(value, 2, "element_address must have two operands");
620}
621
629{
630 PRECONDITION(expr.id() == ID_element_address);
631 const element_address_exprt &ret =
632 static_cast<const element_address_exprt &>(expr);
633 validate_expr(ret);
634 return ret;
635}
636
639{
640 PRECONDITION(expr.id() == ID_element_address);
641 element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
642 validate_expr(ret);
643 return ret;
644}
645
648{
649public:
650 // The given operand must have pointer type.
651 explicit dereference_exprt(const exprt &op)
652 : unary_exprt(ID_dereference, op, to_pointer_type(op.type()).base_type())
653 {
654 }
655
657 : unary_exprt(ID_dereference, std::move(op), std::move(type))
658 {
659 }
660
662 {
663 return op0();
664 }
665
666 const exprt &pointer() const
667 {
668 return op0();
669 }
670
671 static void check(
672 const exprt &expr,
674 {
676 vm,
677 expr.operands().size() == 1,
678 "dereference expression must have one operand");
679 }
680
681 static void validate(
682 const exprt &expr,
683 const namespacet &ns,
685};
686
687template <>
689{
690 return base.id() == ID_dereference;
691}
692
693inline void validate_expr(const dereference_exprt &value)
694{
695 validate_operands(value, 1, "Dereference must have one operand");
696}
697
705{
706 PRECONDITION(expr.id() == ID_dereference);
707 const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
708 validate_expr(ret);
709 return ret;
710}
711
714{
715 PRECONDITION(expr.id() == ID_dereference);
716 dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
717 validate_expr(ret);
718 return ret;
719}
720
723{
724public:
726 : constant_exprt(ID_NULL, std::move(type))
727 {
728 }
729};
730
734{
735public:
737 : binary_predicate_exprt(std::move(pointer), id, std::move(size))
738 {
739 }
740
741 const exprt &pointer() const
742 {
743 return op0();
744 }
745
746 const exprt &size() const
747 {
748 return op1();
749 }
750};
751
752inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
753{
755 expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
756 auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
757 validate_expr(ret);
758 return ret;
759}
760
763{
764public:
766 : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
767 {
768 }
769};
770
771inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
772{
773 PRECONDITION(expr.id() == ID_r_ok);
774 const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
775 validate_expr(ret);
776 return ret;
777}
778
781{
782public:
784 : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
785 {
786 }
787};
788
789inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
790{
791 PRECONDITION(expr.id() == ID_w_ok);
792 const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
793 validate_expr(ret);
794 return ret;
795}
796
797#endif // CPROVER_UTIL_POINTER_EXPR_H
void base_type(typet &type, const namespacet &ns)
Pre-defined bitvector types.
reference_typet reference_type(const typet &subtype)
Definition c_types.cpp:258
Operator to return the address of an object.
const exprt & object() const
address_of_exprt(exprt op, pointer_typet _type)
A base class for binary expressions.
Definition std_expr.h:550
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:643
Base class of fixed-width bit-vector types.
Definition std_types.h:853
std::size_t get_width() const
Definition std_types.h:864
A constant literal expression.
Definition std_expr.h:2807
Operator to dereference a pointer.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
dereference_exprt(const exprt &op)
const exprt & pointer() const
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
dereference_exprt(exprt op, typet type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Representation of heap-allocated objects.
unsigned int get_instance() const
void set_instance(unsigned int instance)
const exprt & valid() const
dynamic_object_exprt(typet type)
Operator to return the address of an array element relative to a base address.
const typet & element_type() const
returns the type of the array element whose address is represented
const exprt & index() const
pointer_typet & type()
const pointer_typet & type() const
const exprt & base() const
exprt & op0()
Definition expr.h:99
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
Operator to return the address of a field relative to a base address.
const typet & field_type() const
returns the type of the field whose address is represented
const exprt & base() const
const irep_idt & component_name() const
pointer_typet & type()
const typet & compound_type() const
const pointer_typet & type() const
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
subt & get_sub()
Definition irep.h:456
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
Evaluates to true if the operand is a pointer to a dynamic object.
is_dynamic_object_exprt(const exprt &op)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The null pointer constant.
null_pointer_exprt(pointer_typet type)
An expression without operands.
Definition std_expr.h:22
Operator to return the address of an object.
const pointer_typet & type() const
pointer_typet & type()
symbol_exprt object_expr() const
irep_idt object_identifier() const
const typet & object_type() const
returns the type of the object whose address is represented
Split an expression into a base object and a (byte) offset.
const exprt & root_object() const
object_descriptor_exprt(exprt _object)
const exprt & offset() const
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
const exprt & object() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
signedbv_typet difference_type() const
const typet & base_type() const
The type of the data what we point to.
typet & base_type()
The type of the data what we point to.
pointer_typet(typet _base_type, std::size_t width)
A predicate that indicates that an address range is ok to read.
r_ok_exprt(exprt pointer, exprt size)
A base class for a predicate that indicates that an address range is ok to read or write or both.
const exprt & size() const
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
const exprt & pointer() const
The reference type.
reference_typet(typet _subtype, std::size_t _width)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition std_expr.h:80
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:168
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
Generic base class for unary expressions.
Definition std_expr.h:281
const exprt & op() const
Definition std_expr.h:293
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:495
A predicate that indicates that an address range is ok to write.
w_ok_exprt(exprt pointer, exprt size)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
STL namespace.
void validate_expr(const object_descriptor_exprt &value)
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
bool can_cast_expr< field_address_exprt >(const exprt &expr)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
bool can_cast_expr< dereference_exprt >(const exprt &base)
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
bool can_cast_expr< object_address_exprt >(const exprt &base)
bool can_cast_expr< address_of_exprt >(const exprt &base)
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 w_ok_exprt & to_w_ok_expr(const exprt &expr)
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
bool can_cast_expr< element_address_exprt >(const exprt &expr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet