cprover
pointer_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for Pointers
4 
5 Author: 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 
18 class namespacet;
19 
24 {
25 public:
26  pointer_typet(typet _subtype, std::size_t width)
27  : bitvector_typet(ID_pointer, width)
28  {
29  subtype().swap(_subtype);
30  }
31 
33  {
34  return signedbv_typet(get_width());
35  }
36 
37  static void check(
38  const typet &type,
40  {
41  DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
42  }
43 };
44 
48 template <>
49 inline bool can_cast_type<pointer_typet>(const typet &type)
50 {
51  return type.id() == ID_pointer;
52 }
53 
62 inline const pointer_typet &to_pointer_type(const typet &type)
63 {
66  return static_cast<const pointer_typet &>(type);
67 }
68 
71 {
74  return static_cast<pointer_typet &>(type);
75 }
76 
79 inline bool is_void_pointer(const typet &type)
80 {
81  return type.id() == ID_pointer && type.subtype().id() == ID_empty;
82 }
83 
89 {
90 public:
91  reference_typet(typet _subtype, std::size_t _width)
92  : pointer_typet(std::move(_subtype), _width)
93  {
94  set(ID_C_reference, true);
95  }
96 
97  static void check(
98  const typet &type,
100  {
101  PRECONDITION(type.id() == ID_pointer);
103  static_cast<const reference_typet &>(type);
104  DATA_CHECK(
105  vm, !reference_type.get(ID_width).empty(), "reference must have width");
106  DATA_CHECK(
107  vm, reference_type.get_width() > 0, "reference must have non-zero width");
108  }
109 };
110 
114 template <>
115 inline bool can_cast_type<reference_typet>(const typet &type)
116 {
117  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
118 }
119 
128 inline const reference_typet &to_reference_type(const typet &type)
129 {
131  return static_cast<const reference_typet &>(type);
132 }
133 
136 {
138  return static_cast<reference_typet &>(type);
139 }
140 
141 bool is_reference(const typet &type);
142 
143 bool is_rvalue_reference(const typet &type);
144 
147 {
148 public:
150  : binary_exprt(
151  exprt(ID_unknown),
152  ID_object_descriptor,
153  exprt(ID_unknown),
154  typet())
155  {
156  }
157 
158  explicit object_descriptor_exprt(exprt _object)
159  : binary_exprt(
160  std::move(_object),
161  ID_object_descriptor,
162  exprt(ID_unknown),
163  typet())
164  {
165  }
166 
171  void build(const exprt &expr, const namespacet &ns);
172 
174  {
175  return op0();
176  }
177 
178  const exprt &object() const
179  {
180  return op0();
181  }
182 
183  static const exprt &root_object(const exprt &expr);
184  const exprt &root_object() const
185  {
186  return root_object(object());
187  }
188 
190  {
191  return op1();
192  }
193 
194  const exprt &offset() const
195  {
196  return op1();
197  }
198 };
199 
200 template <>
202 {
203  return base.id() == ID_object_descriptor;
204 }
205 
206 inline void validate_expr(const object_descriptor_exprt &value)
207 {
208  validate_operands(value, 2, "Object descriptor must have two operands");
209 }
210 
217 inline const object_descriptor_exprt &
219 {
220  PRECONDITION(expr.id() == ID_object_descriptor);
221  const object_descriptor_exprt &ret =
222  static_cast<const object_descriptor_exprt &>(expr);
223  validate_expr(ret);
224  return ret;
225 }
226 
229 {
230  PRECONDITION(expr.id() == ID_object_descriptor);
231  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
232  validate_expr(ret);
233  return ret;
234 }
235 
238 {
239 public:
241  : binary_exprt(
242  exprt(ID_unknown),
243  ID_dynamic_object,
244  exprt(ID_unknown),
245  std::move(type))
246  {
247  }
248 
249  void set_instance(unsigned int instance);
250 
251  unsigned int get_instance() const;
252 
254  {
255  return op1();
256  }
257 
258  const exprt &valid() const
259  {
260  return op1();
261  }
262 };
263 
264 template <>
266 {
267  return base.id() == ID_dynamic_object;
268 }
269 
270 inline void validate_expr(const dynamic_object_exprt &value)
271 {
272  validate_operands(value, 2, "Dynamic object must have two operands");
273 }
274 
282 {
283  PRECONDITION(expr.id() == ID_dynamic_object);
284  const dynamic_object_exprt &ret =
285  static_cast<const dynamic_object_exprt &>(expr);
286  validate_expr(ret);
287  return ret;
288 }
289 
292 {
293  PRECONDITION(expr.id() == ID_dynamic_object);
294  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
295  validate_expr(ret);
296  return ret;
297 }
298 
301 {
302 public:
304  : unary_predicate_exprt(ID_is_dynamic_object, op)
305  {
306  }
307 };
308 
309 template <>
311 {
312  return base.id() == ID_is_invalid_pointer;
313 }
314 
315 inline void validate_expr(const is_dynamic_object_exprt &value)
316 {
317  validate_operands(value, 1, "is_dynamic_object must have one operand");
318 }
319 
320 inline const is_dynamic_object_exprt &
322 {
323  PRECONDITION(expr.id() == ID_is_dynamic_object);
325  expr.operands().size() == 1, "is_dynamic_object must have one operand");
326  return static_cast<const is_dynamic_object_exprt &>(expr);
327 }
328 
332 {
333  PRECONDITION(expr.id() == ID_is_dynamic_object);
335  expr.operands().size() == 1, "is_dynamic_object must have one operand");
336  return static_cast<is_dynamic_object_exprt &>(expr);
337 }
338 
341 {
342 public:
343  explicit address_of_exprt(const exprt &op);
344 
346  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
347  {
348  }
349 
351  {
352  return op0();
353  }
354 
355  const exprt &object() const
356  {
357  return op0();
358  }
359 };
360 
361 template <>
362 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
363 {
364  return base.id() == ID_address_of;
365 }
366 
367 inline void validate_expr(const address_of_exprt &value)
368 {
369  validate_operands(value, 1, "Address of must have one operand");
370 }
371 
378 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
379 {
380  PRECONDITION(expr.id() == ID_address_of);
381  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
382  validate_expr(ret);
383  return ret;
384 }
385 
388 {
389  PRECONDITION(expr.id() == ID_address_of);
390  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
391  validate_expr(ret);
392  return ret;
393 }
394 
397 {
398 public:
399  explicit object_address_exprt(const symbol_exprt &);
400 
402  {
403  return get(ID_identifier);
404  }
405 
406  const pointer_typet &type() const
407  {
408  return static_cast<const pointer_typet &>(exprt::type());
409  }
410 
412  {
413  return static_cast<pointer_typet &>(exprt::type());
414  }
415 
417  const typet &object_type() const
418  {
419  return type().subtype();
420  }
421 
422  symbol_exprt object_expr() const;
423 };
424 
425 template <>
427 {
428  return base.id() == ID_object_address;
429 }
430 
431 inline void validate_expr(const object_address_exprt &value)
432 {
433  validate_operands(value, 1, "object_address must have one operand");
434 }
435 
443 {
444  PRECONDITION(expr.id() == ID_object_address);
445  const object_address_exprt &ret =
446  static_cast<const object_address_exprt &>(expr);
447  validate_expr(ret);
448  return ret;
449 }
450 
453 {
454  PRECONDITION(expr.id() == ID_object_address);
455  object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
456  validate_expr(ret);
457  return ret;
458 }
459 
463 {
464 public:
468  exprt base,
469  const irep_idt &component_name,
471 
473  {
474  return op0();
475  }
476 
477  const exprt &base() const
478  {
479  return op0();
480  }
481 
482  const pointer_typet &type() const
483  {
484  return static_cast<const pointer_typet &>(exprt::type());
485  }
486 
488  {
489  return static_cast<pointer_typet &>(exprt::type());
490  }
491 
493  const typet &field_type() const
494  {
495  return type().subtype();
496  }
497 
498  const typet &compound_type() const
499  {
500  return to_pointer_type(base().type()).subtype();
501  }
502 
503  const irep_idt &component_name() const
504  {
505  return get(ID_component_name);
506  }
507 };
508 
509 template <>
511 {
512  return expr.id() == ID_field_address;
513 }
514 
515 inline void validate_expr(const field_address_exprt &value)
516 {
517  validate_operands(value, 1, "field_address must have one operand");
518 }
519 
527 {
528  PRECONDITION(expr.id() == ID_field_address);
529  const field_address_exprt &ret =
530  static_cast<const field_address_exprt &>(expr);
531  validate_expr(ret);
532  return ret;
533 }
534 
537 {
538  PRECONDITION(expr.id() == ID_field_address);
539  field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
540  validate_expr(ret);
541  return ret;
542 }
543 
547 {
548 public:
553 
554  const pointer_typet &type() const
555  {
556  return static_cast<const pointer_typet &>(exprt::type());
557  }
558 
560  {
561  return static_cast<pointer_typet &>(exprt::type());
562  }
563 
565  const typet &element_type() const
566  {
567  return type().subtype();
568  }
569 
571  {
572  return op0();
573  }
574 
575  const exprt &base() const
576  {
577  return op0();
578  }
579 
581  {
582  return op1();
583  }
584 
585  const exprt &index() const
586  {
587  return op1();
588  }
589 };
590 
591 template <>
593 {
594  return expr.id() == ID_element_address;
595 }
596 
597 inline void validate_expr(const element_address_exprt &value)
598 {
599  validate_operands(value, 2, "element_address must have two operands");
600 }
601 
609 {
610  PRECONDITION(expr.id() == ID_element_address);
611  const element_address_exprt &ret =
612  static_cast<const element_address_exprt &>(expr);
613  validate_expr(ret);
614  return ret;
615 }
616 
619 {
620  PRECONDITION(expr.id() == ID_element_address);
621  element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
622  validate_expr(ret);
623  return ret;
624 }
625 
628 {
629 public:
630  explicit dereference_exprt(const exprt &op)
631  : unary_exprt(ID_dereference, op, op.type().subtype())
632  {
633  PRECONDITION(op.type().id() == ID_pointer);
634  }
635 
637  : unary_exprt(ID_dereference, std::move(op), std::move(type))
638  {
639  }
640 
642  {
643  return op0();
644  }
645 
646  const exprt &pointer() const
647  {
648  return op0();
649  }
650 
651  static void check(
652  const exprt &expr,
654  {
655  DATA_CHECK(
656  vm,
657  expr.operands().size() == 1,
658  "dereference expression must have one operand");
659  }
660 
661  static void validate(
662  const exprt &expr,
663  const namespacet &ns,
665 };
666 
667 template <>
668 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
669 {
670  return base.id() == ID_dereference;
671 }
672 
673 inline void validate_expr(const dereference_exprt &value)
674 {
675  validate_operands(value, 1, "Dereference must have one operand");
676 }
677 
684 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
685 {
686  PRECONDITION(expr.id() == ID_dereference);
687  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
688  validate_expr(ret);
689  return ret;
690 }
691 
694 {
695  PRECONDITION(expr.id() == ID_dereference);
696  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
697  validate_expr(ret);
698  return ret;
699 }
700 
703 {
704 public:
706  : constant_exprt(ID_NULL, std::move(type))
707  {
708  }
709 };
710 
714 {
715 public:
717  : binary_predicate_exprt(std::move(pointer), id, std::move(size))
718  {
719  }
720 
721  const exprt &pointer() const
722  {
723  return op0();
724  }
725 
726  const exprt &size() const
727  {
728  return op1();
729  }
730 };
731 
732 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
733 {
734  PRECONDITION(
735  expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
736  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
737  validate_expr(ret);
738  return ret;
739 }
740 
743 {
744 public:
746  : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
747  {
748  }
749 };
750 
751 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
752 {
753  PRECONDITION(expr.id() == ID_r_ok);
754  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
755  validate_expr(ret);
756  return ret;
757 }
758 
761 {
762 public:
764  : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
765  {
766  }
767 };
768 
769 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
770 {
771  PRECONDITION(expr.id() == ID_w_ok);
772  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
773  validate_expr(ret);
774  return ret;
775 }
776 
777 #endif // CPROVER_UTIL_POINTER_EXPR_H
Pre-defined bitvector types.
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
Operator to return the address of an object.
Definition: pointer_expr.h:341
address_of_exprt(const exprt &op)
const exprt & object() const
Definition: pointer_expr.h:355
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:345
exprt & object()
Definition: pointer_expr.h:350
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
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:832
std::size_t get_width() const
Definition: std_types.h:843
A constant literal expression.
Definition: std_expr.h:2753
Operator to dereference a pointer.
Definition: pointer_expr.h:628
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:651
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:630
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...
const exprt & pointer() const
Definition: pointer_expr.h:646
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:636
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.
Definition: pointer_expr.h:238
unsigned int get_instance() const
const exprt & valid() const
Definition: pointer_expr.h:258
void set_instance(unsigned int instance)
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:240
Operator to return the address of an array element relative to a base address.
Definition: pointer_expr.h:547
const exprt & index() const
Definition: pointer_expr.h:585
const exprt & base() const
Definition: pointer_expr.h:575
const pointer_typet & type() const
Definition: pointer_expr.h:554
element_address_exprt(exprt base, exprt index)
constructor for element addresses.
const typet & element_type() const
returns the type of the array element whose address is represented
Definition: pointer_expr.h:565
pointer_typet & type()
Definition: pointer_expr.h:559
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.
Definition: pointer_expr.h:463
pointer_typet & type()
Definition: pointer_expr.h:487
const typet & compound_type() const
Definition: pointer_expr.h:498
const typet & field_type() const
returns the type of the field whose address is represented
Definition: pointer_expr.h:493
const exprt & base() const
Definition: pointer_expr.h:477
const pointer_typet & type() const
Definition: pointer_expr.h:482
const irep_idt & component_name() const
Definition: pointer_expr.h:503
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:301
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:303
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.
Definition: pointer_expr.h:703
null_pointer_exprt(pointer_typet type)
Definition: pointer_expr.h:705
An expression without operands.
Definition: std_expr.h:22
Operator to return the address of an object.
Definition: pointer_expr.h:397
symbol_exprt object_expr() const
const typet & object_type() const
returns the type of the object whose address is represented
Definition: pointer_expr.h:417
pointer_typet & type()
Definition: pointer_expr.h:411
const pointer_typet & type() const
Definition: pointer_expr.h:406
irep_idt object_identifier() const
Definition: pointer_expr.h:401
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:147
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:158
const exprt & object() const
Definition: pointer_expr.h:178
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...
const exprt & root_object() const
Definition: pointer_expr.h:184
const exprt & offset() const
Definition: pointer_expr.h:194
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:37
signedbv_typet difference_type() const
Definition: pointer_expr.h:32
pointer_typet(typet _subtype, std::size_t width)
Definition: pointer_expr.h:26
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:743
r_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:745
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:714
const exprt & size() const
Definition: pointer_expr.h:726
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
Definition: pointer_expr.h:716
const exprt & pointer() const
Definition: pointer_expr.h:721
The reference type.
Definition: pointer_expr.h:89
reference_typet(typet _subtype, std::size_t _width)
Definition: pointer_expr.h:91
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:97
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
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.
Definition: pointer_expr.h:761
w_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:763
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
void validate_expr(const object_descriptor_exprt &value)
Definition: pointer_expr.h:206
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: pointer_expr.h:115
bool can_cast_expr< field_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:510
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:79
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:732
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:49
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:769
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:129
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:265
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition: pointer_expr.h:526
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:668
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:136
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:310
bool can_cast_expr< object_address_exprt >(const exprt &base)
Definition: pointer_expr.h:426
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:362
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:128
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:218
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:321
bool can_cast_expr< element_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:592
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:442
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:201
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:281
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
Definition: pointer_expr.h:751
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition: pointer_expr.h:608
#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