CBMC
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 _base_type, std::size_t width)
27  : bitvector_typet(ID_pointer, width)
28  {
29  add_subtype() = std::move(_base_type);
30  }
31 
35  const typet &base_type() const
36  {
37  return subtype();
38  }
39 
44  {
45  return subtype();
46  }
47 
48  // Use .base_type() instead -- this method will be removed
49  const typet &subtype() const
50  {
51  // The existence of get_sub() front is enforced by check(...)
52  return static_cast<const typet &>(get_sub().front());
53  }
54 
55  // Use .base_type() instead -- this method will be removed
57  {
58  // The existence of get_sub() front is enforced by check(...)
59  return static_cast<typet &>(get_sub().front());
60  }
61 
63  {
64  return signedbv_typet(get_width());
65  }
66 
67  static void check(
68  const typet &type,
70  {
71  bitvector_typet::check(type, vm);
73  }
74 };
75 
79 template <>
80 inline bool can_cast_type<pointer_typet>(const typet &type)
81 {
82  return type.id() == ID_pointer;
83 }
84 
93 inline const pointer_typet &to_pointer_type(const typet &type)
94 {
97  return static_cast<const pointer_typet &>(type);
98 }
99 
102 {
104  pointer_typet::check(type);
105  return static_cast<pointer_typet &>(type);
106 }
107 
110 inline bool is_void_pointer(const typet &type)
111 {
112  return type.id() == ID_pointer &&
113  to_pointer_type(type).base_type().id() == ID_empty;
114 }
115 
121 {
122 public:
123  reference_typet(typet _subtype, std::size_t _width)
124  : pointer_typet(std::move(_subtype), _width)
125  {
126  set(ID_C_reference, true);
127  }
128 
129  static void check(
130  const typet &type,
132  {
133  PRECONDITION(type.id() == ID_pointer);
134  DATA_CHECK(
135  vm, type.get_sub().size() == 1, "reference must have one type parameter");
137  static_cast<const reference_typet &>(type);
138  DATA_CHECK(
139  vm, !reference_type.get(ID_width).empty(), "reference must have width");
140  DATA_CHECK(
141  vm, reference_type.get_width() > 0, "reference must have non-zero width");
142  }
143 };
144 
148 template <>
149 inline bool can_cast_type<reference_typet>(const typet &type)
150 {
151  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
152 }
153 
162 inline const reference_typet &to_reference_type(const typet &type)
163 {
165  return static_cast<const reference_typet &>(type);
166 }
167 
170 {
172  return static_cast<reference_typet &>(type);
173 }
174 
175 bool is_reference(const typet &type);
176 
177 bool is_rvalue_reference(const typet &type);
178 
181 {
182 public:
184  : binary_exprt(
185  exprt(ID_unknown),
186  ID_object_descriptor,
187  exprt(ID_unknown),
188  typet())
189  {
190  }
191 
192  explicit object_descriptor_exprt(exprt _object)
193  : binary_exprt(
194  std::move(_object),
195  ID_object_descriptor,
196  exprt(ID_unknown),
197  typet())
198  {
199  }
200 
205  void build(const exprt &expr, const namespacet &ns);
206 
208  {
209  return op0();
210  }
211 
212  const exprt &object() const
213  {
214  return op0();
215  }
216 
217  static const exprt &root_object(const exprt &expr);
218  const exprt &root_object() const
219  {
220  return root_object(object());
221  }
222 
224  {
225  return op1();
226  }
227 
228  const exprt &offset() const
229  {
230  return op1();
231  }
232 };
233 
234 template <>
236 {
237  return base.id() == ID_object_descriptor;
238 }
239 
240 inline void validate_expr(const object_descriptor_exprt &value)
241 {
242  validate_operands(value, 2, "Object descriptor must have two operands");
243 }
244 
251 inline const object_descriptor_exprt &
253 {
254  PRECONDITION(expr.id() == ID_object_descriptor);
255  const object_descriptor_exprt &ret =
256  static_cast<const object_descriptor_exprt &>(expr);
257  validate_expr(ret);
258  return ret;
259 }
260 
263 {
264  PRECONDITION(expr.id() == ID_object_descriptor);
265  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
266  validate_expr(ret);
267  return ret;
268 }
269 
272 {
273 public:
275  : binary_exprt(
276  exprt(ID_unknown),
277  ID_dynamic_object,
278  exprt(ID_unknown),
279  std::move(type))
280  {
281  }
282 
283  void set_instance(unsigned int instance);
284 
285  unsigned int get_instance() const;
286 
288  {
289  return op1();
290  }
291 
292  const exprt &valid() const
293  {
294  return op1();
295  }
296 };
297 
298 template <>
300 {
301  return base.id() == ID_dynamic_object;
302 }
303 
304 inline void validate_expr(const dynamic_object_exprt &value)
305 {
306  validate_operands(value, 2, "Dynamic object must have two operands");
307 }
308 
316 {
317  PRECONDITION(expr.id() == ID_dynamic_object);
318  const dynamic_object_exprt &ret =
319  static_cast<const dynamic_object_exprt &>(expr);
320  validate_expr(ret);
321  return ret;
322 }
323 
326 {
327  PRECONDITION(expr.id() == ID_dynamic_object);
328  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
329  validate_expr(ret);
330  return ret;
331 }
332 
335 {
336 public:
338  : unary_predicate_exprt(ID_is_dynamic_object, op)
339  {
340  }
341 
343  {
344  return op();
345  }
346 
347  const exprt &address() const
348  {
349  return op();
350  }
351 };
352 
353 template <>
355 {
356  return base.id() == ID_is_dynamic_object;
357 }
358 
359 inline void validate_expr(const is_dynamic_object_exprt &value)
360 {
361  validate_operands(value, 1, "is_dynamic_object must have one operand");
362 }
363 
364 inline const is_dynamic_object_exprt &
366 {
367  PRECONDITION(expr.id() == ID_is_dynamic_object);
369  expr.operands().size() == 1, "is_dynamic_object must have one operand");
370  return static_cast<const is_dynamic_object_exprt &>(expr);
371 }
372 
376 {
377  PRECONDITION(expr.id() == ID_is_dynamic_object);
379  expr.operands().size() == 1, "is_dynamic_object must have one operand");
380  return static_cast<is_dynamic_object_exprt &>(expr);
381 }
382 
387 {
388 public:
390  : ternary_exprt(
391  ID_pointer_in_range,
392  std::move(a),
393  std::move(b),
394  std::move(c),
395  bool_typet())
396  {
397  PRECONDITION(op0().type().id() == ID_pointer);
398  PRECONDITION(op1().type().id() == ID_pointer);
399  PRECONDITION(op2().type().id() == ID_pointer);
400  }
401 
402  const exprt &lower_bound() const
403  {
404  return op0();
405  }
406 
407  const exprt &pointer() const
408  {
409  return op1();
410  }
411 
412  const exprt &upper_bound() const
413  {
414  return op2();
415  }
416 
417  // translate into equivalent conjunction
418  exprt lower() const;
419 };
420 
421 template <>
423 {
424  return base.id() == ID_pointer_in_range;
425 }
426 
427 inline void validate_expr(const pointer_in_range_exprt &value)
428 {
429  validate_operands(value, 3, "pointer_in_range must have three operands");
430 }
431 
433 {
434  PRECONDITION(expr.id() == ID_pointer_in_range);
436  expr.operands().size() == 3, "pointer_in_range must have three operands");
437  return static_cast<const pointer_in_range_exprt &>(expr);
438 }
439 
443 {
444  PRECONDITION(expr.id() == ID_pointer_in_range);
446  expr.operands().size() == 3, "pointer_in_range must have three operands");
447  return static_cast<pointer_in_range_exprt &>(expr);
448 }
449 
452 {
453 public:
454  explicit address_of_exprt(const exprt &op);
455 
457  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
458  {
459  }
460 
462  {
463  return op0();
464  }
465 
466  const exprt &object() const
467  {
468  return op0();
469  }
470 };
471 
472 template <>
473 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
474 {
475  return base.id() == ID_address_of;
476 }
477 
478 inline void validate_expr(const address_of_exprt &value)
479 {
480  validate_operands(value, 1, "Address of must have one operand");
481 }
482 
489 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
490 {
491  PRECONDITION(expr.id() == ID_address_of);
492  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
493  validate_expr(ret);
494  return ret;
495 }
496 
499 {
500  PRECONDITION(expr.id() == ID_address_of);
501  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
502  validate_expr(ret);
503  return ret;
504 }
505 
508 {
509 public:
510  explicit object_address_exprt(const symbol_exprt &);
511 
513 
515  {
516  return get(ID_identifier);
517  }
518 
519  const pointer_typet &type() const
520  {
521  return static_cast<const pointer_typet &>(exprt::type());
522  }
523 
525  {
526  return static_cast<pointer_typet &>(exprt::type());
527  }
528 
530  const typet &object_type() const
531  {
532  return type().base_type();
533  }
534 
535  symbol_exprt object_expr() const;
536 };
537 
538 template <>
540 {
541  return base.id() == ID_object_address;
542 }
543 
544 inline void validate_expr(const object_address_exprt &value)
545 {
546  validate_operands(value, 0, "object_address must have zero operands");
547 }
548 
556 {
557  PRECONDITION(expr.id() == ID_object_address);
558  const object_address_exprt &ret =
559  static_cast<const object_address_exprt &>(expr);
560  validate_expr(ret);
561  return ret;
562 }
563 
566 {
567  PRECONDITION(expr.id() == ID_object_address);
568  object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
569  validate_expr(ret);
570  return ret;
571 }
572 
576 {
577 public:
581  exprt base,
582  const irep_idt &component_name,
584 
586  {
587  return op0();
588  }
589 
590  const exprt &base() const
591  {
592  return op0();
593  }
594 
595  const pointer_typet &type() const
596  {
597  return static_cast<const pointer_typet &>(exprt::type());
598  }
599 
601  {
602  return static_cast<pointer_typet &>(exprt::type());
603  }
604 
606  const typet &field_type() const
607  {
608  return type().base_type();
609  }
610 
611  const typet &compound_type() const
612  {
613  return to_pointer_type(base().type()).base_type();
614  }
615 
616  const irep_idt &component_name() const
617  {
618  return get(ID_component_name);
619  }
620 };
621 
622 template <>
624 {
625  return expr.id() == ID_field_address;
626 }
627 
628 inline void validate_expr(const field_address_exprt &value)
629 {
630  validate_operands(value, 1, "field_address must have one operand");
631 }
632 
640 {
641  PRECONDITION(expr.id() == ID_field_address);
642  const field_address_exprt &ret =
643  static_cast<const field_address_exprt &>(expr);
644  validate_expr(ret);
645  return ret;
646 }
647 
650 {
651  PRECONDITION(expr.id() == ID_field_address);
652  field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
653  validate_expr(ret);
654  return ret;
655 }
656 
660 {
661 public:
666 
671 
672  const pointer_typet &type() const
673  {
674  return static_cast<const pointer_typet &>(exprt::type());
675  }
676 
678  {
679  return static_cast<pointer_typet &>(exprt::type());
680  }
681 
683  const typet &element_type() const
684  {
685  return type().base_type();
686  }
687 
689  {
690  return op0();
691  }
692 
693  const exprt &base() const
694  {
695  return op0();
696  }
697 
699  {
700  return op1();
701  }
702 
703  const exprt &index() const
704  {
705  return op1();
706  }
707 };
708 
709 template <>
711 {
712  return expr.id() == ID_element_address;
713 }
714 
715 inline void validate_expr(const element_address_exprt &value)
716 {
717  validate_operands(value, 2, "element_address must have two operands");
718 }
719 
727 {
728  PRECONDITION(expr.id() == ID_element_address);
729  const element_address_exprt &ret =
730  static_cast<const element_address_exprt &>(expr);
731  validate_expr(ret);
732  return ret;
733 }
734 
737 {
738  PRECONDITION(expr.id() == ID_element_address);
739  element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
740  validate_expr(ret);
741  return ret;
742 }
743 
746 {
747 public:
748  // The given operand must have pointer type.
749  explicit dereference_exprt(const exprt &op)
750  : unary_exprt(ID_dereference, op, to_pointer_type(op.type()).base_type())
751  {
752  }
753 
755  : unary_exprt(ID_dereference, std::move(op), std::move(type))
756  {
757  }
758 
760  {
761  return op0();
762  }
763 
764  const exprt &pointer() const
765  {
766  return op0();
767  }
768 
769  static void check(
770  const exprt &expr,
772  {
773  DATA_CHECK(
774  vm,
775  expr.operands().size() == 1,
776  "dereference expression must have one operand");
777  }
778 
779  static void validate(
780  const exprt &expr,
781  const namespacet &ns,
783 };
784 
785 template <>
786 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
787 {
788  return base.id() == ID_dereference;
789 }
790 
791 inline void validate_expr(const dereference_exprt &value)
792 {
793  validate_operands(value, 1, "Dereference must have one operand");
794 }
795 
802 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
803 {
804  PRECONDITION(expr.id() == ID_dereference);
805  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
806  validate_expr(ret);
807  return ret;
808 }
809 
812 {
813  PRECONDITION(expr.id() == ID_dereference);
814  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
815  validate_expr(ret);
816  return ret;
817 }
818 
821 {
822 public:
824  : constant_exprt(ID_NULL, std::move(type))
825  {
826  }
827 };
828 
832 {
833 public:
835  : binary_predicate_exprt(std::move(pointer), id, std::move(size))
836  {
837  }
838 
839  const exprt &pointer() const
840  {
841  return op0();
842  }
843 
844  const exprt &size() const
845  {
846  return op1();
847  }
848 };
849 
850 template <>
851 inline bool can_cast_expr<r_or_w_ok_exprt>(const exprt &base)
852 {
853  return base.id() == ID_r_ok || base.id() == ID_w_ok || base.id() == ID_rw_ok;
854 }
855 
856 inline void validate_expr(const r_or_w_ok_exprt &value)
857 {
858  validate_operands(value, 2, "r_or_w_ok must have two operands");
859 }
860 
861 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
862 {
863  PRECONDITION(
864  expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
865  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
866  validate_expr(ret);
867  return ret;
868 }
869 
872 {
873 public:
875  : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
876  {
877  }
878 };
879 
880 template <>
881 inline bool can_cast_expr<r_ok_exprt>(const exprt &base)
882 {
883  return base.id() == ID_r_ok;
884 }
885 
886 inline void validate_expr(const r_ok_exprt &value)
887 {
888  validate_operands(value, 2, "r_ok must have two operands");
889 }
890 
891 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
892 {
893  PRECONDITION(expr.id() == ID_r_ok);
894  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
895  validate_expr(ret);
896  return ret;
897 }
898 
901 {
902 public:
904  : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
905  {
906  }
907 };
908 
909 template <>
910 inline bool can_cast_expr<w_ok_exprt>(const exprt &base)
911 {
912  return base.id() == ID_w_ok;
913 }
914 
915 inline void validate_expr(const w_ok_exprt &value)
916 {
917  validate_operands(value, 2, "w_ok must have two operands");
918 }
919 
920 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
921 {
922  PRECONDITION(expr.id() == ID_w_ok);
923  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
924  validate_expr(ret);
925  return ret;
926 }
927 
937 {
938 public:
940  const irep_idt &_value,
941  const exprt &_pointer)
942  : unary_exprt(ID_annotated_pointer_constant, _pointer, _pointer.type())
943  {
944  set_value(_value);
945  }
946 
947  const irep_idt &get_value() const
948  {
949  return get(ID_value);
950  }
951 
952  void set_value(const irep_idt &value)
953  {
954  set(ID_value, value);
955  }
956 
958  {
959  return op0();
960  }
961 
962  const exprt &symbolic_pointer() const
963  {
964  return op0();
965  }
966 };
967 
968 template <>
970 {
971  return base.id() == ID_annotated_pointer_constant;
972 }
973 
975 {
977  value, 1, "Annotated pointer constant must have one operand");
978 }
979 
988 {
989  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
991  static_cast<const annotated_pointer_constant_exprt &>(expr);
992  validate_expr(ret);
993  return ret;
994 }
995 
999 {
1000  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
1002  static_cast<annotated_pointer_constant_exprt &>(expr);
1003  validate_expr(ret);
1004  return ret;
1005 }
1006 
1009 {
1010 public:
1012  : unary_exprt(ID_pointer_offset, std::move(pointer), std::move(type))
1013  {
1014  }
1015 
1017  {
1018  return op0();
1019  }
1020 
1021  const exprt &pointer() const
1022  {
1023  return op0();
1024  }
1025 };
1026 
1027 template <>
1029 {
1030  return base.id() == ID_pointer_offset;
1031 }
1032 
1033 inline void validate_expr(const pointer_offset_exprt &value)
1034 {
1035  validate_operands(value, 1, "pointer_offset must have one operand");
1037  value.pointer().type().id() == ID_pointer,
1038  "pointer_offset must have pointer-typed operand");
1039 }
1040 
1048 {
1049  PRECONDITION(expr.id() == ID_pointer_offset);
1050  const pointer_offset_exprt &ret =
1051  static_cast<const pointer_offset_exprt &>(expr);
1052  validate_expr(ret);
1053  return ret;
1054 }
1055 
1058 {
1059  PRECONDITION(expr.id() == ID_pointer_offset);
1060  pointer_offset_exprt &ret = static_cast<pointer_offset_exprt &>(expr);
1061  validate_expr(ret);
1062  return ret;
1063 }
1064 
1067 {
1068 public:
1070  : unary_exprt(ID_pointer_object, std::move(pointer), std::move(type))
1071  {
1072  }
1073 
1075  {
1076  return op0();
1077  }
1078 
1079  const exprt &pointer() const
1080  {
1081  return op0();
1082  }
1083 };
1084 
1085 template <>
1087 {
1088  return base.id() == ID_pointer_object;
1089 }
1090 
1091 inline void validate_expr(const pointer_object_exprt &value)
1092 {
1093  validate_operands(value, 1, "pointer_object must have one operand");
1095  value.pointer().type().id() == ID_pointer,
1096  "pointer_object must have pointer-typed operand");
1097 }
1098 
1106 {
1107  PRECONDITION(expr.id() == ID_pointer_object);
1108  const pointer_object_exprt &ret =
1109  static_cast<const pointer_object_exprt &>(expr);
1110  validate_expr(ret);
1111  return ret;
1112 }
1113 
1116 {
1117  PRECONDITION(expr.id() == ID_pointer_object);
1118  pointer_object_exprt &ret = static_cast<pointer_object_exprt &>(expr);
1119  validate_expr(ret);
1120  return ret;
1121 }
1122 
1126 {
1127 public:
1129  : unary_exprt(ID_object_size, std::move(pointer), std::move(type))
1130  {
1131  }
1132 
1134  {
1135  return op();
1136  }
1137 
1138  const exprt &pointer() const
1139  {
1140  return op();
1141  }
1142 };
1143 
1150 inline const object_size_exprt &to_object_size_expr(const exprt &expr)
1151 {
1152  PRECONDITION(expr.id() == ID_object_size);
1153  const object_size_exprt &ret = static_cast<const object_size_exprt &>(expr);
1154  validate_expr(ret);
1155  return ret;
1156 }
1157 
1160 {
1161  PRECONDITION(expr.id() == ID_object_size);
1162  object_size_exprt &ret = static_cast<object_size_exprt &>(expr);
1163  validate_expr(ret);
1164  return ret;
1165 }
1166 
1167 template <>
1168 inline bool can_cast_expr<object_size_exprt>(const exprt &base)
1169 {
1170  return base.id() == ID_object_size;
1171 }
1172 
1173 inline void validate_expr(const object_size_exprt &value)
1174 {
1175  validate_operands(value, 1, "Object size expression must have one operand.");
1178  "Object size expression must have pointer typed operand.");
1179 }
1180 
1185 {
1186 public:
1188  : unary_predicate_exprt(ID_is_cstring, std::move(address))
1189  {
1190  PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1191  }
1192 
1194  {
1195  return op0();
1196  }
1197 
1198  const exprt &address() const
1199  {
1200  return op0();
1201  }
1202 };
1203 
1204 template <>
1205 inline bool can_cast_expr<is_cstring_exprt>(const exprt &base)
1206 {
1207  return base.id() == ID_is_cstring;
1208 }
1209 
1210 inline void validate_expr(const is_cstring_exprt &value)
1211 {
1212  validate_operands(value, 1, "is_cstring must have one operand");
1213 }
1214 
1221 inline const is_cstring_exprt &to_is_cstring_expr(const exprt &expr)
1222 {
1223  PRECONDITION(expr.id() == ID_is_cstring);
1224  const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
1225  validate_expr(ret);
1226  return ret;
1227 }
1228 
1231 {
1232  PRECONDITION(expr.id() == ID_is_cstring);
1233  is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
1234  validate_expr(ret);
1235  return ret;
1236 }
1237 
1243 {
1244 public:
1246  : unary_exprt(ID_cstrlen, std::move(address), std::move(type))
1247  {
1248  PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1249  }
1250 
1252  {
1253  return op0();
1254  }
1255 
1256  const exprt &address() const
1257  {
1258  return op0();
1259  }
1260 };
1261 
1262 template <>
1263 inline bool can_cast_expr<cstrlen_exprt>(const exprt &base)
1264 {
1265  return base.id() == ID_cstrlen;
1266 }
1267 
1268 inline void validate_expr(const cstrlen_exprt &value)
1269 {
1270  validate_operands(value, 1, "cstrlen must have one operand");
1271 }
1272 
1279 inline const cstrlen_exprt &to_cstrlen_expr(const exprt &expr)
1280 {
1281  PRECONDITION(expr.id() == ID_cstrlen);
1282  const cstrlen_exprt &ret = static_cast<const cstrlen_exprt &>(expr);
1283  validate_expr(ret);
1284  return ret;
1285 }
1286 
1289 {
1290  PRECONDITION(expr.id() == ID_cstrlen);
1291  cstrlen_exprt &ret = static_cast<cstrlen_exprt &>(expr);
1292  validate_expr(ret);
1293  return ret;
1294 }
1295 
1299 {
1300 public:
1302  : unary_predicate_exprt(ID_live_object, std::move(pointer))
1303  {
1304  PRECONDITION(as_const(*this).pointer().type().id() == ID_pointer);
1305  }
1306 
1308  {
1309  return op0();
1310  }
1311 
1312  const exprt &pointer() const
1313  {
1314  return op0();
1315  }
1316 };
1317 
1318 template <>
1319 inline bool can_cast_expr<live_object_exprt>(const exprt &base)
1320 {
1321  return base.id() == ID_live_object;
1322 }
1323 
1324 inline void validate_expr(const live_object_exprt &value)
1325 {
1326  validate_operands(value, 1, "live_object must have one operand");
1327 }
1328 
1335 inline const live_object_exprt &to_live_object_expr(const exprt &expr)
1336 {
1337  PRECONDITION(expr.id() == ID_live_object);
1338  const live_object_exprt &ret = static_cast<const live_object_exprt &>(expr);
1339  validate_expr(ret);
1340  return ret;
1341 }
1342 
1345 {
1346  PRECONDITION(expr.id() == ID_live_object);
1347  live_object_exprt &ret = static_cast<live_object_exprt &>(expr);
1348  validate_expr(ret);
1349  return ret;
1350 }
1351 
1355 {
1356 public:
1358  : unary_predicate_exprt(ID_writeable_object, std::move(pointer))
1359  {
1360  PRECONDITION(as_const(*this).pointer().type().id() == ID_pointer);
1361  }
1362 
1364  {
1365  return op0();
1366  }
1367 
1368  const exprt &pointer() const
1369  {
1370  return op0();
1371  }
1372 };
1373 
1374 template <>
1376 {
1377  return base.id() == ID_writeable_object;
1378 }
1379 
1380 inline void validate_expr(const writeable_object_exprt &value)
1381 {
1382  validate_operands(value, 1, "writeable_object must have one operand");
1383 }
1384 
1392 {
1393  PRECONDITION(expr.id() == ID_writeable_object);
1394  const writeable_object_exprt &ret =
1395  static_cast<const writeable_object_exprt &>(expr);
1396  validate_expr(ret);
1397  return ret;
1398 }
1399 
1402 {
1403  PRECONDITION(expr.id() == ID_writeable_object);
1404  writeable_object_exprt &ret = static_cast<writeable_object_exprt &>(expr);
1405  validate_expr(ret);
1406  return ret;
1407 }
1408 
1411 {
1412 public:
1413  explicit separate_exprt(exprt::operandst __operands)
1414  : multi_ary_exprt(ID_separate, std::move(__operands), bool_typet())
1415  {
1416  }
1417 
1419  : multi_ary_exprt(
1420  std::move(__op0),
1421  ID_separate,
1422  std::move(__op1),
1423  bool_typet())
1424  {
1425  }
1426 };
1427 
1428 template <>
1429 inline bool can_cast_expr<separate_exprt>(const exprt &base)
1430 {
1431  return base.id() == ID_separate;
1432 }
1433 
1434 inline void validate_expr(const separate_exprt &value)
1435 {
1436 }
1437 
1444 inline const separate_exprt &to_separate_expr(const exprt &expr)
1445 {
1446  PRECONDITION(expr.id() == ID_separate);
1447  const separate_exprt &ret = static_cast<const separate_exprt &>(expr);
1448  validate_expr(ret);
1449  return ret;
1450 }
1451 
1454 {
1455  PRECONDITION(expr.id() == ID_separate);
1456  separate_exprt &ret = static_cast<separate_exprt &>(expr);
1457  validate_expr(ret);
1458  return ret;
1459 }
1460 
1461 #endif // CPROVER_UTIL_POINTER_EXPR_H
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
Pre-defined bitvector types.
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:245
Operator to return the address of an object.
Definition: pointer_expr.h:452
address_of_exprt(const exprt &op)
const exprt & object() const
Definition: pointer_expr.h:466
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:456
exprt & object()
Definition: pointer_expr.h:461
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
Definition: pointer_expr.h:937
void set_value(const irep_idt &value)
Definition: pointer_expr.h:952
const irep_idt & get_value() const
Definition: pointer_expr.h:947
const exprt & symbolic_pointer() const
Definition: pointer_expr.h:962
annotated_pointer_constant_exprt(const irep_idt &_value, const exprt &_pointer)
Definition: pointer_expr.h:939
A base class for binary expressions.
Definition: std_expr.h:583
exprt & op1()
Definition: expr.h:128
exprt & op0()
Definition: expr.h:125
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:676
Base class of fixed-width bit-vector types.
Definition: std_types.h:865
std::size_t get_width() const
Definition: std_types.h:876
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:886
The Boolean type.
Definition: std_types.h:36
A constant literal expression.
Definition: std_expr.h:2942
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
exprt & address()
const exprt & address() const
cstrlen_exprt(exprt address, typet type)
Operator to dereference a pointer.
Definition: pointer_expr.h:746
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:769
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:749
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:764
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:754
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
bool empty() const
Definition: dstring.h:90
Representation of heap-allocated objects.
Definition: pointer_expr.h:272
unsigned int get_instance() const
const exprt & valid() const
Definition: pointer_expr.h:292
void set_instance(unsigned int instance)
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:274
Operator to return the address of an array element relative to a base address.
Definition: pointer_expr.h:660
const exprt & index() const
Definition: pointer_expr.h:703
const exprt & base() const
Definition: pointer_expr.h:693
const pointer_typet & type() const
Definition: pointer_expr.h:672
element_address_exprt(const 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:683
pointer_typet & type()
Definition: pointer_expr.h:677
exprt & op0()
Definition: expr.h:125
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
Operator to return the address of a field relative to a base address.
Definition: pointer_expr.h:576
pointer_typet & type()
Definition: pointer_expr.h:600
const typet & compound_type() const
Definition: pointer_expr.h:611
const typet & field_type() const
returns the type of the field whose address is represented
Definition: pointer_expr.h:606
const exprt & base() const
Definition: pointer_expr.h:590
const pointer_typet & type() const
Definition: pointer_expr.h:595
const irep_idt & component_name() const
Definition: pointer_expr.h:616
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:456
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
A predicate that indicates that a zero-terminated string starts at the given address.
const exprt & address() const
is_cstring_exprt(exprt address)
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:335
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:337
const exprt & address() const
Definition: pointer_expr.h:347
A predicate that indicates that the object pointed to is live.
const exprt & pointer() const
live_object_exprt(exprt pointer)
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:857
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:821
null_pointer_exprt(pointer_typet type)
Definition: pointer_expr.h:823
An expression without operands.
Definition: std_expr.h:22
Operator to return the address of an object.
Definition: pointer_expr.h:508
symbol_exprt object_expr() const
const typet & object_type() const
returns the type of the object whose address is represented
Definition: pointer_expr.h:530
pointer_typet & type()
Definition: pointer_expr.h:524
const pointer_typet & type() const
Definition: pointer_expr.h:519
irep_idt object_identifier() const
Definition: pointer_expr.h:514
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:181
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:192
const exprt & object() const
Definition: pointer_expr.h:212
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:218
const exprt & offset() const
Definition: pointer_expr.h:228
Expression for finding the size (in bytes) of the object a pointer points to.
const exprt & pointer() const
object_size_exprt(exprt pointer, typet type)
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
Definition: pointer_expr.h:387
const exprt & lower_bound() const
Definition: pointer_expr.h:402
pointer_in_range_exprt(exprt a, exprt b, exprt c)
Definition: pointer_expr.h:389
const exprt & pointer() const
Definition: pointer_expr.h:407
const exprt & upper_bound() const
Definition: pointer_expr.h:412
A numerical identifier for the object a pointer points to.
pointer_object_exprt(exprt pointer, typet type)
const exprt & pointer() const
The offset (in bytes) of a pointer relative to the object.
const exprt & pointer() const
pointer_offset_exprt(exprt pointer, typet type)
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:67
signedbv_typet difference_type() const
Definition: pointer_expr.h:62
const typet & subtype() const
Definition: pointer_expr.h:49
typet & base_type()
The type of the data what we point to.
Definition: pointer_expr.h:43
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
pointer_typet(typet _base_type, std::size_t width)
Definition: pointer_expr.h:26
typet & subtype()
Definition: pointer_expr.h:56
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:872
r_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:874
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:832
const exprt & size() const
Definition: pointer_expr.h:844
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
Definition: pointer_expr.h:834
const exprt & pointer() const
Definition: pointer_expr.h:839
The reference type.
Definition: pointer_expr.h:121
reference_typet(typet _subtype, std::size_t _width)
Definition: pointer_expr.h:123
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:129
A predicate that indicates that the objects pointed to are distinct.
separate_exprt(exprt::operandst __operands)
separate_exprt(exprt __op0, exprt __op1)
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition: std_expr.h:113
An expression with three operands.
Definition: std_expr.h:49
exprt & op1()
Definition: expr.h:128
exprt & op2()
Definition: expr.h:131
exprt & op0()
Definition: expr.h:125
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:166
The type of an expression, extends irept.
Definition: type.h:29
typet & add_subtype()
Definition: type.h:53
Generic base class for unary expressions.
Definition: std_expr.h:314
const exprt & op() const
Definition: std_expr.h:326
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:528
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:901
w_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:903
A predicate that indicates that the object pointed to is writeable.
const exprt & pointer() const
writeable_object_exprt(exprt pointer)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
bool can_cast_expr< separate_exprt >(const exprt &base)
void validate_expr(const object_descriptor_exprt &value)
Definition: pointer_expr.h:240
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: pointer_expr.h:149
const separate_exprt & to_separate_expr(const exprt &expr)
Cast an exprt to a separate_exprt.
bool can_cast_expr< field_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:623
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:110
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:861
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:80
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:920
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
Definition: pointer_expr.h:987
const is_cstring_exprt & to_is_cstring_expr(const exprt &expr)
Cast an exprt to a is_cstring_exprt.
bool can_cast_expr< live_object_exprt >(const exprt &base)
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:143
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:299
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition: pointer_expr.h:639
bool can_cast_expr< pointer_in_range_exprt >(const exprt &base)
Definition: pointer_expr.h:422
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:786
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:802
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:150
const live_object_exprt & to_live_object_expr(const exprt &expr)
Cast an exprt to a live_object_exprt.
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:354
const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)
Cast an exprt to a cstrlen_exprt.
bool can_cast_expr< cstrlen_exprt >(const exprt &base)
bool can_cast_expr< object_address_exprt >(const exprt &base)
Definition: pointer_expr.h:539
const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)
Cast an exprt to a writeable_object_exprt.
bool can_cast_expr< object_size_exprt >(const exprt &base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
bool can_cast_expr< is_cstring_exprt >(const exprt &base)
bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)
Definition: pointer_expr.h:969
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:473
bool can_cast_expr< pointer_offset_exprt >(const exprt &base)
bool can_cast_expr< w_ok_exprt >(const exprt &base)
Definition: pointer_expr.h:910
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:162
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:252
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:365
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
bool can_cast_expr< element_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:710
bool can_cast_expr< r_ok_exprt >(const exprt &base)
Definition: pointer_expr.h:881
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
Definition: pointer_expr.h:432
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:555
bool can_cast_expr< r_or_w_ok_exprt >(const exprt &base)
Definition: pointer_expr.h:851
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:235
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:315
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:489
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
Definition: pointer_expr.h:891
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition: pointer_expr.h:726
bool can_cast_expr< writeable_object_exprt >(const exprt &base)
bool can_cast_expr< pointer_object_exprt >(const exprt &base)
#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